Metamath Home Higher-Order Logic Explorer Home Page First >
Last >
Mirrors  >  Home  >  HOL Home  >  Th. List

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

      This page was last updated on 12-Jul-2015.
    Your comments are welcome: Norman Megill nm at alum dot mit dot edu
    Copyright terms: Public domain
    W3C HTML validation [external]