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

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
  • Most Recent Proofs (this mirror) (latest)
  • Bibliographic Cross-Reference
  • Definition List
  • ASCII Equivalents for Text-Only Browsers
  • Metamath database iset.mm (ASCII file)
  • External links
  • Github repository [accessed 06-Jan-2018]

  • Overview of intuitionistic logic

    (Placeholder for future use)


    Overview of this work

    (By Gérard Lang, 7-May-2018)

    Mario Carneiro's work (Metamath database) "iset.mm" provides in Metamath a development of "set.mm" 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, iset.mm adds (or substitutes) intuitionistic axioms for a number of the classical logical axioms of set.mm.

    Among these new axioms, the 6 first (ax-ia1, ax-ia2, ax-ia3, ax-io, ax-in1 and ax-in2), when added to ax-1, ax-2 and ax-mp, allow for the development of intuitionistic propositional logic. We omit the classical axiom ((¬ 𝜑 → ¬ 𝜓) → (𝜓𝜑)) (which is ax-3 in set.mm). Each of our new axioms 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 equivalence 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-ie1 and ax-ie2) together with the set.mm axioms ax-4, ax-5, ax-7 and ax-gen do not mention equality or distinct variables.

    The ax-i9 axiom is just a slight variation of the classical ax-9. The classical axiom ax-12 is strengthened into first ax-i12 and then ax-bnd (two results which would be fairly readily equivalent to ax-12 classically but which do not follow from ax-12, at least not in an obvious way, in intuitionistic logic). The substitution of ax-i9, ax-i12, and ax-bnd for ax-9 and ax-12 and the inclusion of 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 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 derived 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

    As with the classical axioms we have propositional logic and predicate logic.

    The axioms of intuitionistic propositional logic consist of some of the axioms from classical propositional logic, plus additional axioms for the operation of the 'and', 'or' and 'not' connectives.

    Axioms of intuitionistic propositional calculus
    Axiom Simp ax-1 (φ → (ψφ))
    Axiom Frege ax-2 ((φ → (ψχ)) → ((φψ) → (φχ)))
    Rule of Modus Ponens ax-mp φ   &   φψ   =>   ψ
    Left 'and' eliminationax-ia1 ((φ ψ) → φ)
    Right 'and' eliminationax-ia2 ((φ ψ) → ψ)
    'And' introductionax-ia3 (φ → (ψ → (φ ψ)))
    Definition of 'or'ax-io (((φ χ) → ψ) ↔ ((φψ) (χψ)))
    'Not' introductionax-in1 ((φ → ¬ φ) → ¬ φ)
    'Not' eliminationax-in2 φ → (φψ))

    Unlike in classical propositional logic, 'and' and 'or' are not readily defined in terms of implication and 'not'. In particular, φψ is not equivalent to ¬ φψ, nor is φψ equivalent to ¬ φψ, nor is φψ equivalent to ¬ (φ → ¬ ψ).

    The ax-in1 axiom is a form of proof by contradiction which does hold intuitionistically. That is, if φ implies a contradiction (such as its own negation), then one can conclude ¬ φ. By contrast, assuming ¬ φ and then deriving a contradiction only serves to prove ¬ ¬ φ, which in intuitionistic logic is not the same as φ.

    The biconditional can be defined as the conjunction of two implications, as in dfbi2 and df-bi.

    Predicate logic adds set variables (individual variables) and the ability to quantify them with ∀ (for-all) and ∃ (there-exists). Unlike in classical logic, ∃ cannot be defined in terms of ∀. As in classical logic, we also add = for equality (which is key to how we handle substitution in metamath) and ∈ (which for current purposes can just be thought of as an arbitrary predicate, but which will later come to mean set membership).

    Our axioms are based on the classical set.mm predicate logic axioms, but adapted for intuitionistic logic, chiefly by adding additional axioms for ∃ and also changing some aspects of how we handle negations.

    Axioms of intuitionistic predicate logic
    Axiom of Specialization ax-4 (xφφ)
    Axiom of Quantified Implication ax-5 (x(φψ) → (xφxψ))
    The converse of ax-5o ax-i5r ((xφxψ) → x(xφψ))
    Axiom of Quantifier Commutation ax-7 (xyφyxφ)
    Rule of Generalization ax-gen φ   =>    xφ
    x is bound in xφ ax-ial (xφxxφ)
    x is bound in xφ ax-ie1 (xφxxφ)
    Define existential quantification ax-ie2 (x(ψxψ) → (x(φψ) ↔ (xφψ)))
    Axiom of Equality ax-8 (x = y → (x = zy = z))
    Axiom of Existence ax-i9 x x = y
    Axiom of Quantifier Substitution ax-10 (x x = yy y = x)
    Axiom of Variable Substitution ax-11 (x = y → (yφx(x = yφ)))
    Axiom of Quantifier Introduction ax-i12 (z z = x (z z = y z(x = yz x = y)))
    Axiom of Bundling ax-bnd (z z = x (z z = y xz(x = yz x = y)))
    Left Membership Equality ax-13 (x = y → (x zy z))
    Right Membership Equality ax-14 (x = y → (z xz y))
    Distinctness ax-17 (φxφ), where x does not occur in φ

    Set theory uses the formalism of propositional and predicate calculus to assert properties of arbitrary mathematical objects called "sets." A set can be contained in another set, and this relationship is indicated by the e. symbol. Starting with the simplest mathematical object, called the empty set, set theory builds up more and more complex structures whose existence follows from the axioms, eventually resulting in extremely complicated sets that we identify with the real numbers and other familiar mathematical objects. These axioms were developed in response to Russell's Paradox, a discovery that revolutionized the foundations of mathematics and logic.

    In the IZF axioms that follow, all set variables are assumed to be distinct. If you click on their links you will see the explicit distinct variable conditions.

    Intuitionistic Zermelo-Fraenkel Set Theory (IZF)
    Axiom of Extensionality ax-ext (z(z xz y) → x = y)
    Axiom of Collection ax-coll (x 𝑎 yφ𝑏x 𝑎 y 𝑏 φ)
    Axiom of Separation ax-sep yx(x y ↔ (x z φ))
    Axiom of Power Sets ax-pow yz(w(w zw x) → z y)
    Axiom of Pairing ax-pr zw((w = x w = y) → w z)
    Axiom of Union ax-un yz(w(z w w x) → z y)
    Axiom of Infinity To be added
    Axiom of ∈-Induction To be added


    A Theorem Sampler   

    From a psychological point of view, learning constructive mathematics is agonizing, for it requires one to first unlearn certain deeply ingrained intuitions and habits acquired during classical mathematical training.
    —Andrej Bauer

    Listed here are some examples of starting points for your journey through the maze. You should study some simple proofs from propositional calculus until you get the hang of it. Then try some predicate calculus and finally set theory. The Theorem List shows the complete set of theorems in the database. You may also find the Bibliographic Cross-Reference useful.

    Propositional calculus
  • Law of identity
  • Praeclarum theorema
  • Contraposition introduction
  • Double negation introduction
  • Triple negation
  • Definition of exclusive or
  • Negation and the false constant
  • Predicate calculus
  • Existential and universal quantifier swap
  • Existentially quantified implication
  • x = x
  • Definition of proper substitution
  • Double existential uniqueness
  • Set theory
  • Commutative law for union
  • A basic relationship between class and wff variables
  • Two ways of saying "is a set"
  • Russell's paradox
  • ...watch this space as we build out more of set theory

  • Bibliography   
    1. [Bauer] Bauer, Andrej, "Five stages of accepting constructive mathematics," Bulletin (New Series) of the American Mathematical Society, 54:481-498 (2017), DOI: 10.1090/bull/1556 .
    2. [BellMachover] Bell, J. L., and M. Machover, A Course in Mathematical Logic, North-Holland, Amsterdam (1977) [QA9.B3953].
    3. [ChoquetDD] Choquet-Bruhat, Yvonne and Cecile DeWitt-Morette, with Margaret Dillard-Bleick, Analysis, Manifolds and Physics, Elsevier Science B.V., Amsterdam (1982) [QC20.7.A5C48 1981].
    4. [Crosilla] Crosilla, Laura, "Set Theory: Constructive and Intuitionistic ZF", The Stanford Encyclopedia of Philosophy (Summer 2015 Edition), Edward N. Zalta (ed.), https://plato.stanford.edu/archives/sum2015/entries/set-theory-constructive/.
    5. [Moschovakis] Moschovakis, Joan, "Intuitionistic Logic", The Stanford Encyclopedia of Philosophy (Spring 2015 Edition), Edward N. Zalta (ed.), https://plato.stanford.edu/archives/spr2015/entries/logic-intuitionistic/.
    6. [Eisenberg] Eisenberg, Murray, Axiomatic Theory of Sets and Classes, Holt, Rinehart and Winston, Inc., New York (1971) [QA248.E36].
    7. [Enderton] Enderton, Herbert B., Elements of Set Theory, Academic Press, Inc., San Diego, California (1977) [QA248.E5].
    8. [Hamilton] Hamilton, A. G., Logic for Mathematicians, Cambridge University Press, Cambridge, revised edition (1988) [QA9.H298 1988].
    9. [Heyting] Heyting, A., Intuitionism: An introduction, North-Holland publishing company, Amsterdam, second edition (1966).
    10. [Hitchcock] Hitchcock, David, The peculiarities of Stoic propositional logic, McMaster University; available at http://www.humanities.mcmaster.ca/~hitchckd/peculiarities.pdf (retrieved 3 Jul 2016).
    11. [HoTT] The {Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, https://homotopytypetheory.org/book, first edition.
    12. [Jech] Jech, Thomas, Set Theory, Academic Press, San Diego (1978) [QA248.J42].
    13. [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].
    14. [Kunen] Kunen, Kenneth, Set Theory: An Introduction to Independence Proofs, Elsevier Science B.V., Amsterdam (1980) [QA248.K75].
    15. [KuratowskiMostowski] Kuratowski, K. and A. Mostowski, Set Theory: with an Introduction to Descriptive Set Theory, 2nd ed., North-Holland, Amsterdam (1976) [QA248.K7683 1976].
    16. [Levy] Levy, Azriel, Basic Set Theory, Dover Publications, Mineola, N.Y. (2002) [QA248.L398 2002].
    17. [Lopez-Astorga] Lopez-Astorga, Miguel, "The First Rule of Stoic Logic and its Relationship with the Indemonstrables", Revista de Filosofía Tópicos (2016); available at http://www.scielo.org.mx/pdf/trf/n50/n50a1.pdf (retrieved 3 Jul 2016).
    18. [Margaris] Margaris, Angelo, First Order Mathematical Logic, Blaisdell Publishing Company, Waltham, Massachusetts (1967) [QA9.M327].
    19. [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.
    20. [Mendelson] Mendelson, Elliott, Introduction to Mathematical Logic, 2nd ed., D. Van Nostrand (1979) [QA9.M537].
    21. [Monk1] Monk, J. Donald, Introduction to Set Theory, McGraw-Hill, Inc. (1969) [QA248.M745].
    22. [Monk2] Monk, J. Donald, "Substitutionless Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:103-121 (1965) [QA.A673].
    23. [Quine] Quine, Willard van Orman, Set Theory and Its Logic, Harvard University Press, Cambridge, Massachusetts, revised edition (1969) [QA248.Q7 1969].
    24. [Sanford] Sanford, David H., If P, then Q: Conditionals and the Foundations of Reasoning, 2nd ed., Routledge Taylor & Francis Group (2003); ISBN 0-415-28369-8; available at https://books.google.com/books?id=h_AUynB6PA8C&pg=PA39#v=onepage&q&f=false (retrieved 3 Jul 2016).
    25. [Stoll] Stoll, Robert R., Set Theory and Logic, Dover Publications, Inc. (1979) [QA248.S7985 1979].
    26. [Suppes] Suppes, Patrick, Axiomatic Set Theory, Dover Publications, Inc. (1972) [QA248.S959].
    27. [TakeutiZaring] Takeuti, Gaisi, and Wilson M. Zaring, Introduction to Axiomatic Set Theory, Springer-Verlag, New York, second edition (1982) [QA248.T136 1982].
    28. [Tarski] Tarski, Alfred, "A Simplified Formalization of Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:61-79 (1965) [QA.A673].
    29. [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 15-Aug-2015.
    Your comments are welcome: Norman Megill nm at alum dot mit dot edu
    Copyright terms: Public domain
    W3C HTML validation [external]