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

This document uses HTML 4/Unicode to display special characters. Older browsers and/or operating systems may not display these characters correctly.
last substantive
content change


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 correct and 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 2 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). From the B-H-K viewpoint, 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 and individual variables a,b,c,... (with or without subscripts 1,2,...), as well as symbols &, , , , , for the logical connectives and quantifiers, and parentheses (, ). We use A, B, C as metavariables for well-formed formulas and x,y,z as metavariables for individual variables. Anticipating applications (for example to intuitionistic arithmetic) we use s,t as metavariables for terms; in the case of pure predicate logic, terms are simply individual variables.

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 (one or two) 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. A derivation of a formula E from a collection F of assumptions is any sequence of formulas, each of which belongs to F or is an axiom or an immediate consequence, by a rule of inference, of preceding formulas of the sequence, such that E is the last formula of the sequence. If such a derivation exists, we say E is derivable from F.

Intuitionistic propositional logic is the subtheory which results when the language is restricted to formulas built from proposition letters P, Q, R,... using the propositional connectives &, , and , and only the propositional postulates are used. Thus the last two rules of inference and the last two axiom schemas are absent from the propositional theory.

If, in the given list of axiom schemas for intuitionistic propositional or first-order predicate logic, 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 propositional or first-order predicate logic results. Since the law of contradiction is a classical theorem, intuitionistic logic is contained in classical logic.

    While the Hilbert-style system H is useful for metamathematical investigations of intuitionistic logic, its forced linearization of deductions and its preference for axioms over rules make it an awkward instrument for establishing derivability. A natural deduction system I for intuitionistic predicate logic (with identity) results from the deductive system D, presented in Section 3 of the entry on Classical Logic in this Encyclopedia, by replacing the classical rule (DNE) of double negation elimination by the intuitionistic negation elimination rule

  • (INE) If F entails A and F entails A, then F entails B.
  • The reader may also wish to consult Section 2 (on Language) of the same entry, which applies mutatis mutandum to the language L of H and I. The Deduction Theorem and its converse, stated in the next section, are the keys to the equivalence of H with (the identity-free part of) I,

    A Little Proof Theory

    Like their classical extensions, intuitionistic propositional and predicate logic satisfy the Deduction Theorem: If B is derivable from A with all variables free in A held constant in the deduction (that is, without using the second or third rule of inference on any variable x occurring free in A, unless the assumption A does not occur in the deduction before the inference in question), then (A B) is provable. The converse of this theorem holds simply by the first rule of inference.

    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 it follows that if intuitionistic logic is consistent, then (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, Friedman and Troelstra also proved existence properties for second-order intuitionistic systems.

    The disjunction and existence properties are special cases of a general phenomenon peculiar to nonclassical theories. The admissible rules of a theory are the rules under which the theory is closed. In classical propositional logic, if (A is provable) implies (B is provable), then (A B) is provable; thus every classically admissible rule is classically derivable. Intuitionistically the situation is more interesting. Harrop [1960] observed that intuitionistic propositional logic is closed under the rule (A (B C)) / (A B) (A C), while the corresponding implication is not provable intuitionistically. In [2001] Iemhoff succeeded in proving a conjecture of de Jongh and Visser, which provides a recursively enumerable basis for the admissible rules of intuitionistic propositional logic; Visser [2002] has shown that these are also the admissible propositional rules of intuitionistic arithmetic, and of intuitionistic arithmetic extended by Markov's Principle (see the article on Constructive Mathematics in this Encyclopedia).

    Kripke Semantics

    Intuitionistic systems have inspired a variety of interpretations, including Beth's tableaus, Rasiowa and Sikorski's topological models, formulas-as-types, Kleene's recursive realizabilities, and the Kleene and Aczel slashes. 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}.

    Advanced Topics and Resources

    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. Kleene's [1969] formalizes the theory of partial recursive functionals, enabling precise formalizations of the function-realizability interpretation used in [1965] and of a related q-realizability interpretation which establishes a recursive uniformization rule for intuitionistic analysis.

    Troelstra's [1973], Beeson's [1985] and Troelstra and van Dalen's [1988] are comprehensive studies of intuitionistic and semi-intutionistic theories, using both constructive and classical methods. Troelstra's [1998] presents formulas-as-types and (Kleene and Aczel) slash interpretations for propositional and predicate logic, as well as abstract and concrete realizability interpretations for a multitude of intuitionistic theories. Veldman's [1990] treats descriptive set theory from a strictly intuitionistic viewpoint. Martin-Löf's intuitionistic theory of types [1984] provides a general framework within which intuitionistic reasoning continues to develop.


    Other Internet Resources

    [Please contact the author with suggestions.]

    Related Entries

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

    Copyright © 1999, 2002
    Joan 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

    Stanford Encyclopedia of Philosophy