This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Stanford Encyclopedia of Philosophy

A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

Intuitionistic Logic

Intuitionistic logic encompasses the principles of logical reasoning which were used by L. E. J. Brouwer in developing his intuitionistic mathematics, beginning in [1907]. Because these principles also underly Russian recursive analysis and the constructive analysis of E. Bishop and his followers, intuitionistic logic may be considered the logical basis of constructive mathematics.

Philosophically, intuitionism differs from logicism by treating logic as a part of mathematics rather than as the foundation of mathematics; from finitism by allowing (constructive) reasoning about infinite collections; and from platonism by viewing mathematical objects as mental constructs with no independent ideal existence. Hilbert's formalist program, to justify classical mathematics by reducing it to a formal system whose consistency should be established by finitistic (hence constructive) means, was the most powerful contemporary rival to Brouwer's developing intuitionism. In his 1912 essay Intuitionism and Formalism Brouwer correctly predicted that any attempt to prove the consistency of complete induction on the natural numbers would lead to a vicious circle.

Brouwer rejected formalism per se but admitted the potential usefulness of formulating general logical principles expressing intuitionistically correct constructions, such as modus ponens. Formal systems for intuitionistic propositional and predicate logic were developed by Heyting [1930], Gentzen [1935] and Kleene [1952]. The Gödel-Gentzen negative translation interpreted classical predicate logic in its intuitionistic subsystem. In [1965] Kripke provided a semantics with respect to which intuitionistic predicate logic is complete.

Rejection of Tertium Non Datur

Intuitionistic logic can be succinctly described as classical logic without the Aristotelian law of excluded middle LEM (A A), but with the law of contradiction (A (A B)). Brouwer [1908] observed that LEM was abstracted from finite situations, then extended without justification to statements about infinite collections. For example, if x, y range over the natural numbers 0, 1, 2, ... and B(x) abbreviates the property (there is a y > x such that both y and y+2 are prime numbers), then we have no general method for deciding whether B(x) is true or false for arbitrary x, so x(B(x) B(x)) cannot be asserted in the present state of our knowledge. And if A abbreviates the statement xB(x), then (A A) cannot be asserted because neither A nor (A) has yet been proved.

One may object that these examples depend on the fact that the Twin Primes Conjecture has not yet been settled. A number of Brouwer's original "counterexamples" depended on problems (such as Fermat's Last Theorem) which have since been solved. But to Brouwer the general LEM was equivalent to the a priori assumption that every mathematical problem has a solution -- an assumption he rejected, anticipating Gödel's incompleteness theorem by a quarter of a century.

Intuitionistic First-Order Predicate Logic

The Brouwer-Heyting-Kolmogorov explication of intuitionistic truth, outlined in Section 1 ("The Basis of Constructive Mathematics") of the article on Constructive Mathematics in this Encyclopedia, results in the constructive independence of the logical operations &, , , , . This contrasts with the classical situation, where e.g., (A B) is equivalent to (A & B), and xA(x) is equivalent to xA(x). Intuitionistically, a sentence of the form (A B) asserts that either a proof of A, or a proof of B, has been constructed; while (A & B) asserts that an algorithm has been constructed which would effectively convert any pair of constructions proving A and B respectively, into a proof of a known contradiction.

Following is a Hilbert-style formalism, from Kleene [1952], for intuitionistic first-order predicate logic. The language L has predicate letters P, Q(.),... of all arities, individual variables, and symbols for the logical operations. We use A, B, C as metavariables for well-formed formulas. There are three rules of inference:

The axioms are all formulas of the following forms, where in the last two schemas the subformula A(t) is the result of substituting an occurrence of the term t for every free occurrence of x in A(x), and no variable free in t becomes bound in A(t) as a result of the substitution. A proof is any sequence of formulas, each of which is an axiom or an immediate consequence, by a rule of inference, of preceding formulas of the sequence. Any proof is said to prove its last formula, which is called a theorem or provable formula of first-order intuitionistic predicate logic.

If, in the given list of axiom schemas, the law of contradiction:

  • A (A B).
  • is replaced by the law of double negation:
  • A A.
  • (or, equivalently, by LEM), a formal system for classical first-order predicate logic results. Since the law of contradiction is a classical theorem, intuitionistic logic is contained in classical logic.

    A Little Proof Theory

    The Gödel-Gentzen negative translation associates with each formula A of the language L a formula g(A) with no or , which is equivalent to A in classical predicate logic. We define g(A) by induction on the logical form of A, as follows: For each formula A, g(A) is provable intuitionistically if and only if A is provable classically. In particular, if (B & B) were classically provable for some formula B, then (g(B) & g(B)) (which is g(B & B)) would in turn be provable intuitionistically. Gödel [1933] interpreted these results as showing that intuitionistic logic is richer than classical logic, because Gödel extended the negative translation to number theory, but attempts to apply it to intuitionistic analysis failed because the negative translation of the countable axiom of choice has no intuitionistic justification.

    Gödel [1932] observed that intuitionistic propositional logic has the disjunction property: If (A B) is a theorem, then A is a theorem or B is a theorem. Gentzen [1935] established the disjunction property for closed formulas of intuitionistic predicate logic. From this follows e.g., that (P P) is not a theorem if P is prime. Kleene [1945, 1952] proved that intuitionistic first-order number theory also has the related (cf., Friedman [1975]) existence property: If xA(x) is a closed theorem, then for some closed term t, A(t) is a theorem. Kleene and Friedman also proved existence properties for second-order intuitionistic systems.

    Some Semantics

    Intuitionistic systems have inspired a variety of interpretations, including Beth's tableaus, Rasiowa and Sikorski's topological models, and Kleene's recursive realizabilities. Kripke's [1965] possible-world semantics, with respect to which intuitionistic predicate logic is complete and consistent, most resembles classical model theory.

    A Kripke structure K consists of a partially ordered set K of nodes and a domain function D assigning to each node k in K an inhabited set D(k) of constructive objects, such that if k k, then D(k) D(k). In addition K has a forcing relation determined as follows.

    For each node k let L(k) be the language extending L by new constants for all the elements of D(k). To each node k and each prime predicate P(x) assign a (possibly empty) subset T(P,k) of D(k) in such a way that if k k then T(P,k) T(P,k), and similarly for predicates of more variables. Say that k forces P(d) if and only if d T(P,k). Now define forcing for compound sentences of L(k) by

    Any such forcing relation is consistent and monotone: Kripke's Soundness and Completeness Theorems establish that a sentence of L is provable in intuitionistic predicate logic if and only if it is forced by every node of every Kripke structure. Thus to show that (xP(x) xP(x)) is intuitionistically unprovable, it is enough to consider a Kripke structure with K = {k, k}, k < k, D(k) = D(k) = {0}, T(P,k) empty but T(P,k) = {0}.

    Additional Topics

    While intuitionistic arithmetic is a proper part of classical arithmetic, the intuitionistic attitude toward mathematical objects results in a theory of real numbers diverging from the classical. For readers wishing to pursue this subject farther, the third edition [1971] of Heyting's classic [1956] is an authentic and accessible introduction to intuitionistic philosophy, logic and mathematical practice. Kleene and Vesley's [1965] provides a careful axiomatic treatment of, and a constructive consistency proof for, intuitionistic analysis. Troelstra and van Dalen's comprehensive [1988] brings the story nearly up to date.


    Other Internet Resources

    [Please contact the author with suggestions.]

    Related Entries

    Brouwer, Luitzen Egbertus Jan | finitism | formalism | logicism | mathematics: constructive | Platonism: in metaphysics

    Copyright © 1999 by
    Joan R. Moschovakis

    A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

    Table of Contents

    First published: September 1, 1999
    Content last modified: September 1, 1999