Metamath Home Intuitionistic Logic Explorer Home Page First >
Last >
Mirrors  >  Home  >  ILE Home  >  Th. List

Created by Mario Carneiro

Intuitionistic Logic Proof Explorer

Intuitionistic Logic (Wikipedia [accessed 19-Jul-2015], Stanford Encyclopedia of Philosophy [accessed 19-Jul-2015]) can be thought of as a constructive logic in which we must build and exhibit concrete examples of objects before we can accept their existence. Unproved statements in intuitionistic logic are not given an intermediate truth value, instead, they remain of unknown truth value until they are either proved or disproved. Intuitionist logic can also be thought of as a weakening of classical logic such that the law of excluded middle (LEM), (φ ¬ φ), doesn't always hold. Specifically, it holds if we have a proof for φ or we have a proof for ¬ φ, but it doesn't necessarily hold if we don't have a proof of either one. There is also no rule for double negation elimination. Brouwer observed in 1908 that LEM was abstracted from finite situations, then extended without justification to statements about infinite collections.

Contents of this page
  • Overview of intuitionistic logic
  • Overview of this work
  • 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 19-Jul-2015]

  • Overview of intuitionistic logic

    (Placeholder for future use)

    Overview of this work

    (By Gérard Lang, 19-Jul-2015)

    Mario Carneiro's work (Metamath database) "" provides in Metamath a development of "" whose eventual aim is to show how many of the theorems of set theory and mathematics that can be derived from classical first order logic can also be derived from a weaker system called "intuitionistic logic." To achieve this task, adds (or substitutes) 13 intuitionistic axioms whose second part of the name begins with the letter "i" to the classical logical axioms of

    Among these 13 new axioms, the 6 first (ax-ia1, ax-ia2, ax-ia3, ax-io, ax-in1 and ax-in2), when substituted to ax-3 and added with ax-1, ax-2 and ax-mp, allow for the development of intuitionistic propositional logic. Each of them is a theorem of classical propositional logic, but ax-3 cannot be derived from them. Similarly, other basic classical theorems, like the third middle excluded or the equvalence of a proposition with its double negation, cannot be derived in intuitionistic propositional calculus. Glivenko showed that a proposition φ is a theorem of classical propositional calculus if and only if ¬¬φ is a theorem of intuitionistic propositional calculus.

    The next 4 new axioms (ax-ial, ax-i5r, ax-ia1 and ax-ia2) being added to ax-4, ax-5, ax-6, ax-7 and ax-gen allow for the development of intuitionistic pure predicate calculus.

    The last 3 new axioms (ax-i9, ax-i11e and ax-i12) are variants of the classical axioms ax-9, ax-11 and ax-12. The substitution of ax-i9 and ax-i12 with ax-9 and ax-12 and the addition of ax-i11e with ax-8, ax-10, ax-11, ax-13, ax-14 and ax-17 allow for the development of the intuitionistic predicate calculus.

    Each of the 13 new axioms is a theorem of classical first order logic with equality. But some axioms of classical first order logic with equality, like ax-3, cannot be derivefd in the intuitionistic predicate calculus.

    One of the major interests of the intuitionistic predicate calculus is that its use can be considered as a realization of the program of the constructivist philosophical view of mathematics.

    The axioms

    (Placeholder for future use)

    Some theorems

    (Placeholder for future use)

    1. [BellMachover] Bell, J. L., and M. Machover, A Course in Mathematical Logic, North-Holland, Amsterdam (1977) [QA9.B3953].
    2. [Hamilton] Hamilton, A. G., Logic for Mathematicians, Cambridge University Press, Cambridge, revised edition (1988) [QA9.H298 1988].
    3. [KalishMontague] Kalish, D. and R. Montague, "On Tarski's formalization of predicate logic with identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:81-101 (1965) [QA.A673].
    4. [Kunen] Kunen, Kenneth, Set Theory: An Introduction to Independence Proofs, Elsevier Science B.V., Amsterdam (1980) [QA248.K75].
    5. [Margaris] Margaris, Angelo, First Order Mathematical Logic, Blaisdell Publishing Company, Waltham, Massachusetts (1967) [QA9.M327].
    6. [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.
    7. [Mendelson] Mendelson, Elliott, Introduction to Mathematical Logic, 2nd ed., D. Van Nostrand (1979) [QA9.M537].
    8. [Monk2] Monk, J. Donald, "Substitutionless Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:103-121 (1965) [QA.A673].
    9. [Quine] Quine, Willard van Orman, Set Theory and Its Logic, Harvard University Press, Cambridge, Massachusetts, revised edition (1969) [QA248.Q7 1969].
    10. [Stoll] Stoll, Robert R., Set Theory and Logic, Dover Publications, Inc. (1979) [QA248.S7985 1979].
    11. [TakeutiZaring] Takeuti, Gaisi, and Wilson M. Zaring, Introduction to Axiomatic Set Theory, Springer-Verlag, New York, second edition (1982) [QA248.T136 1982].
    12. [Tarski] Tarski, Alfred, "A Simplified Formalization of Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:61-79 (1965) [QA.A673].
    13. [WhiteheadRussell] Whitehead, Alfred North, and Bertrand Russell, Principia Mathematica to *56, Cambridge University Press, Cambridge, 1962 [QA9.W592 1962].

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