Home - HOL Explorer

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].

Contents of this page Overview of type theory The axioms Some theorems Bibliography

Related pages Table of Contents and Theorem List Bibliographic Cross-Reference Definition List ASCII Equivalents for Text-Only Browsers Metamath database hol.mm (ASCII file) External links Github repository [accessed 12-Jul-2015]

Overview of type theory

(Placeholder for future use)

The axioms

(Placeholder for future use)

Some theorems

Proof of the ZF Axiom of Extensionality

Proof of the ZF Axiom of Replacement

Proof of the ZF Axiom of Power Sets

Proof of the ZF Axiom of Union

Bibliography   

1. [BellMachover] Bell, J. L., and M. Machover, A Course in Mathematical Logic, North-Holland, Amsterdam (1977) [QA9.B3953].
2. [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).
3. [Hamilton] Hamilton, A. G., Logic for Mathematicians, Cambridge University Press, Cambridge, revised edition (1988) [QA9.H298 1988].
4. [Margaris] Margaris, Angelo, First Order Mathematical Logic, Blaisdell Publishing Company, Waltham, Massachusetts (1967) [QA9.M327].
5. [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.
6. [Monk2] Monk, J. Donald, "Substitutionless Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:103-121 (1965) [QA.A673].
7. [TakeutiZaring] Takeuti, Gaisi, and Wilson M. Zaring, Introduction to Axiomatic Set Theory, Springer-Verlag, New York, second edition (1982) [QA248.T136 1982].
8. [Tarski] Tarski, Alfred, "A Simplified Formalization of Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:61-79 (1965) [QA.A673].