Created by Mario Carneiro
Higher-Order Logic Proof Explorer
Higher-Order Logic (Wikipedia
[accessed 12-Jul-2015], Stanford
Encyclopedia of Philosophy [accessed 12-Jul-2015]) is an alternative
approach to predicate logic that is distinguished from first-order logic
by additional quantifiers and a stronger semantics. It is also called
simple type theory. A nice introduction can be found in William
Farmer's "The
Seven Virtues of Simple Type Theory" [accessed 12-Jul-2015].
Overview of type theory
(Placeholder for future use)
The axioms
(Placeholder for future use)
Some theorems
Bibliography
- [BellMachover] Bell, J. L., and M.
Machover, A Course in Mathematical Logic, North-Holland,
Amsterdam (1977) [QA9.B3953].
- [Farmer] Farmer, William M.,
"The Seven Virtues of Simple Type Theory," Journal
of Applied Logic (2003); available
at
http://imps.mcmaster.ca/doc/seven-virtues.pdf (accessed 12 Jul 2015).
- [Hamilton] Hamilton, A. G., Logic for
Mathematicians, Cambridge University Press, Cambridge, revised
edition (1988) [QA9.H298 1988].
- [Margaris] Margaris, Angelo, First Order
Mathematical Logic, Blaisdell Publishing Company, Waltham,
Massachusetts (1967) [QA9.M327].
- [Megill] Megill, N.,
"A Finitely Axiomatized Formalization of Predicate Calculus with
Equality," Notre Dame Journal of Formal Logic, 36:435-453
(1995) [QA.N914]; available at http://projecteuclid.org/euclid.ndjfl/1040149359 (accessed
11 Nov 2014); the PDF
preprint has the same content (with corrections) but pages are
numbered 1-22, and the database references use the numbers printed on the
page itself, not the PDF page numbers.
- [Monk2] Monk, J. Donald, "Substitutionless
Predicate Logic with Identity," Archiv für Mathematische Logik
und Grundlagenforschung, 7:103-121 (1965) [QA.A673].
- [TakeutiZaring] Takeuti, Gaisi, and
Wilson M. Zaring, Introduction to Axiomatic Set Theory,
Springer-Verlag, New York, second edition (1982) [QA248.T136 1982].
- [Tarski] Tarski, Alfred, "A Simplified
Formalization of Predicate Logic with Identity," Archiv für
Mathematische Logik und Grundlagenforschung, 7:61-79 (1965)
[QA.A673].