Intuitionistic Logic

First published Wed Sep 1, 1999; substantive revision Fri Jan 2, 2015

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 uncountable structures (e.g. monotone bar induction on the tree of potentially infinite sequences of natural numbers); 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 and arithmetic were developed by Heyting [1930], Gentzen [1935] and Kleene [1952]. Gödel [1933] proved the equiconsistency of intuitionistic and classical theories. Kripke [1965] provided a semantics with respect to which intuitionistic logic is correct and complete.

1. Rejection of Tertium Non Datur

Intuitionistic logic can be succinctly described as classical logic without the Aristotelian law of excluded middle (LEM): (A ∨ ¬A) or the classical law of double negation elimination (¬ ¬A → A), but with the law of contradiction (A → B) → ((A → ¬B) → ¬A) and ex falso quodlibet: (¬A → (A → B)). Brouwer [1908] observed that LEM was abstracted from finite situations, then extended without justification to statements about infinite collections. For example, let x, y range over the natural numbers 0, 1, 2, … and B(x) abbreviate the property expressed by the following claim in which the variable x is free: there is a y greater than x such that both y and y+2 are prime numbers, i.e.,

∃y(y>x & Prime(y) & Prime(y+2))

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.

The rejection of LEM has far-reaching consequences. On the one hand,

  • Intuitionistically, Reductio ad absurdum only proves negative statements, since ¬ ¬A → A does not hold in general. (If it did, LEM would follow by modus ponens from the intuitionistically provable ¬ ¬ (A ∨ ¬A).)
  • Not every propositional formula has an intuitionistically equivalent disjunctive or conjunctive normal form.
  • Not every predicate formula has an intuitionistically equivalent prenex form.
  • While ∀x ¬ ¬ (A(x) ∨ ¬A(x)) is a theorem of intuitionistic predicate logic, ¬ ¬ ∀x(A(x) ∨ ¬A(x)) is not.
  • Pure intuitionistic logic is axiomatically incomplete. Infinitely many intermediate axiomatic extensions of intuitionistic propositional and predicate logic are contained in classical logic.

On the other hand,

  • Every intuitionistic proof of a closed statement of the form A ∨ B can be effectively transformed into an intuitionistic proof of A or an intuitionistic proof of B, and similarly for closed existential statements.
  • Classical logic is finitistically interpretable in the negative fragment of intuitionistic logic.
  • Arithmetical formulas have relatively simple intuitionistic normal forms.
  • Intuitionistic arithmetic can consistently be extended by axioms (such as Church's Thesis) which contradict classical arithmetic, enabling the formal study of recursive mathematics.
  • Brouwer's controversial intuitionistic analysis, which conflicts with LEM, can be formalized and shown consistent relative to a classically and intuitionistically correct subtheory.

2. Intuitionistic First-Order Predicate Logic

Formalized intuitionistic logic is naturally motivated by the informal Brouwer-Heyting-Kolmogorov explanation of intuitionistic truth, outlined in Section 3.1 of the entry on intuitionism in the philosophy of mathematics and discussed extensively in the entry on the development of intuitionistic logic. The constructive independence of the logical operations &, ∨, →, ¬, ∀, ∃ contrasts with the classical situation, where e.g., (A ∨ B) is equivalent to ¬ (¬A & ¬B), and ∃xA(x) is equivalent to ¬ ∀x ¬A(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 H, from Kleene [1952], for intuitionistic first-order predicate logic IQC. 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 (, ). The prime formulas of L are expressions such as P, Q(a), R(a, b, a) where P, Q(.), R(…) are 0-ary, 1-ary and 3-ary predicate letters respectively; that is, the result of filling each blank in a predicate letter by an individual variable symbol is a prime formula. The (well-formed) formulas of L are defined inductively as follows.

  • Each prime formula is a formula.
  • If A and B are formulas, so are (A & B), (A ∨ B), (A → B) and ¬A.
  • If A is a formula and x is a variable, then ∀xA and ∃xA are formulas.

In general, 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. An occurrence of a variable x in a formula A is bound if it is within the scope of a quantifier ∀x or ∃x, otherwise free. Intuitionistically as classically, “(A ↔ B)” abbreviates “(A → B) & (B → A),” and parentheses are omitted when this causes no confusion.

There are three rules of inference:

  • Modus Ponens: From A and (A → B), conclude B.
  • ∀-Introduction: From (C → A(x)), where x is a variable which does not occur free in C, conclude (C → ∀xA(x)).
  • ∃-Elimination: From (A(x) → C), where x is a variable which does not occur free in C, conclude (∃xA(x) → C).

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 → (B → A).
  • (A → B) → ((A → (B → C)) → (A → C)).
  • A → (B → A & B).
  • A & B → A.
  • A & B → B.
  • A → A ∨ B.
  • B → A ∨ B.
  • (A → C) → ((B → C) → (A ∨ B → C)).
  • (A → B) → ((A → ¬B) → ¬A).
  • ¬A → (A → B).
  • ∀xA(x) → A(t).
  • A(t) → ∃xA(x).

A proof is any finite 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 IPC 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 expressing ex falso sequitur quodlibet:

¬A → (A → B).

is replaced by the classical law of double negation elimination:

¬ ¬A → A.

(or,equivalently, if the intuitionistic law of negation introduction

(A → B) → ((A → ¬B) → ¬A)

is replaced by LEM), a formal system for classical propositional logic CPC or classical predicate logic CQC results. Since the law of contradiction is a classical theorem, intuitionistic logic is contained in classical logic. In a sense, classical logic is also contained in intuitionistic logic; see Section 4.1 below.

It is important to note that while LEM and the law of double negation are equivalent as schemas, the implication (¬ ¬A → A) → (A ∨ ¬A) is not a theorem schema of IPC. For theories T based on intuitionistic logic, if E is an arbitrary formula of L(T) then by definition

  • E is decidable in T if and only if T proves (E ∨ ¬E).
  • E is stable in T if and only if T proves (¬ ¬E → E).
  • E is testable in T if and only if T proves (¬E ∨ ¬ ¬E).

Decidability implies stability, but not conversely. The conjunction of stability and testability is equivalent to decidability. By Brouwer's first published logical theorem ¬ ¬ ¬A → ¬A, every formula of the form ¬A is stable; but in IPC and IQC prime formulas and their negations are undecidable, as shown in Section 5.1 below.

The Hilbert-style system H is useful for metamathematical investigations of intuitionistic logic, but 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 results from the deductive system D, presented in Section 3 of the entry on classical logic in this Encyclopedia, by omitting the symbol and rules for identity, and 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.

While identity can of course be added to intuitionistic logic, for applications (e.g., to arithmetic) the equality symbol is generally treated as a distinguished predicate constant satisfying nonlogical axioms (e.g., the primitive recursive definitions of addition and multiplication) in addition to reflexivity, symmetry and transitivity. Identity is decidable, intuitionistically as well as classically, but intuitionistic extensional equality is not always decidable; see the discussion of Brouwer's continuity axioms in Section 3 of the entry on intuitionism in the philosophy of mathematics. The keys to proving that H is equivalent to I are modus ponens and its converse, the

Deduction Theorem: If B is derivable from A and possibly other formulas F, with all variables free in A held constant in the derivation (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 derivation before the inference in question), then (A → B) is derivable from F.

This fundamental result, roughly expressing the rule (→I) of I, can be proved for H by induction on the definition of a derivation. The other rules of I hold for H essentially by modus ponens, which corresponds to (→E) in I. To illustrate the usefulness of the Deduction Theorem, consider the (apparently trivial) theorem schema (A → A) of IPC. A correct proof in H takes five lines:

1. A → (A → A)
2. (A → (A → A)) → ((A → ((A → A) → A)) → (A → A))
3. (A → ((A → A) → A)) → (A → A)
4. A → ((A → A) → A)
5. A → A

where 1, 2 and 4 are axioms and 3, 5 come from earlier lines by modus ponens. However, A is derivable from A (as assumption) in one obvious step, so the Deduction Theorem allows us to conclude that a proof of (A → A) exists. (In fact, the formal proof of (A → A) just presented is part of the constructive proof of the Deduction Theorem!)

It is important to note that, in the definition of a derivation from assumptions in H, the assumption formulas are treated as if all their free variables were universally quantified, so that ∀x A(x) is derivable from the hypothesis A(x). However, the variable x will be varied (not held constant) in that derivation, by use of the rule of ∀-introduction; and so the Deduction Theorem cannot be used to conclude (falsely) that A(x) → ∀x A(x) (and hence, by ∃-elimination, ∃x A(x) → ∀x A(x)) are provable in H. As an example of a correct use of the Deduction Theorem for predicate logic, consider the implication ∃x A(x) → ¬∀x¬A(x). To show this is provable in IQC, we first derive ¬∀x¬A(x) from A(x) with all free variables held constant:

1. ∀x¬A(x) → ¬A(x)
2. A(x) → (∀x¬A(x) → A(x))
3. A(x) (assumption)
4. ∀x¬A(x) → A(x)
5. (∀x¬A(x) → A(x)) → ((∀x¬A(x) → ¬A(x)) → ¬∀x¬A(x))
6. (∀x¬A(x) → ¬A(x)) → ¬∀x¬A(x)
7. ¬∀x¬A(x)

Here 1, 2 and 5 are axioms; 4 comes from 2 and 3 by modus ponens; and 6 and 7 come from earlier lines by modus ponens; so no variables have been varied. The Deduction Theorem tells us there is a proof P in IQC of (A(x) → ¬∀x¬A(x)), and one application of ∃-elimination converts P into a proof of ∃x A(x) → ¬∀x¬A(x). The converse is not provable in IQC, as shown in Section 5.1 below.

3. Intuitionistic Number Theory (Heyting Arithmetic)

Intuitionistic (Heyting) arithmetic HA and classical (Peano) arithmetic PA share the same first-order language and the same non-logical axioms; only the logic is different. In addition to the logical connectives, quantifiers and parentheses and the individual variables a, b, c, … (with metavariables x, y, z as usual), the language L(HA) of arithmetic has a binary predicate symbol =, individual constant 0, unary function constant S, and finitely or countably infinitely many additional constants for primitive recursive functions including addition and multiplication; the precise choice is a matter of taste and convenience. Terms are built from variables and 0 using the function constants; in particular, each natural number n is expressed in the language by the numeral n obtained by applying S n times to 0 (e.g., S(S(0)) is the numeral for 2). Prime formulas are of the form (s = t) where s, t are terms, and compound formulas are obtained from these as usual.

The logical axioms and rules of HA are those of first-order intuitionistic predicate logic IQC. The nonlogical axioms include the reflexive, symmetric and transitive properties of =, primitive recursive defining equations for each function constant, the axioms characterizing 0 as the least natural number and S as a one-to-one function:

  • ∀x¬(S(x) = 0),
  • ∀x∀y(S(x) = S(y) → x = y),

the extensional equality axiom for S:

  • ∀x∀y (x = y → S(x) = S(y)),

and the (universal closure of the) schema of mathematical induction, for arbitrary formulas A(x):

  • A(0) & ∀x(A(x) → A(S(x))) → ∀x A(x).

Extensional equality axioms for all the other function constants are derivable by mathematical induction from the equality axiom for S and the primitive recursive function axioms.

The natural order relation x < y can be defined in HA by ∃z(S(z) + x = y), or by a quantifier-free formula if the symbol and defining axioms for cutoff subtraction are present in the formalism. HA proves the comparative law

∀x ∀y (x < y ∨ x = y ∨ y < x)

and an intuitionistic form of the least number principle, for arbitrary formulas A(x):

∀x[∀y (y < x → A(y) ∨ ¬A(y)) → ∃y (y < x & A(y) & ∀z(z < y → ¬A(z))) ∨ ∀y(y < x → ¬A(y))].

The hypothesis is needed because not all arithmetical formulas are decidable in HA. However, ∀x∀y(x = y ∨ ¬(x = y)) can be proved directly by mathematical induction, and so

  • Prime formulas (and hence all quantifier-free formulas) are decidable and stable in HA.

If A(x) is decidable in HA, then by induction on x so are ∀y (y < x → A(y)) and ∃y (y < x & A(y)). Hence

  • Formulas in which all quantifiers are bounded are decidable and stable in HA.

The collection Δ0 of arithmetical formulas in which all quantifiers are bounded is the lowest level of a classical arithmetical hierarchy based on the pattern of alternations of quantifiers in a prenex formula. In HA not every formula has a prenex form, but Burr [2004] discovered a simple intuitionistic arithmetical hierarchy corresponding level by level to the classical. For the purposes of the next two definitions only, ∀x denotes a block of finitely many universal number quantifiers, and similarly ∃x denotes a block of finitely many existential number quantifiers. With these conventions, Burr's classes Φn and Ψn are defined by

  • Φ0 = Ψ0 = Δ0,
  • Φ1 is the class of all formulas of the form ∀x A(x) where A(x) is in Ψ0. For n ≥ 2, Φn is the class of all formulas of the form ∀x [A(x) →∃y B(x,y)] where A(x) is in Φn-1 and B(x,y) is in Φn-2,
  • Ψ1 is the class of all formulas of the form ∃x A(x) where A(x) is in Φ0. For n ≥ 2, Ψn is the class of all formulas of the form A → B where A is in Φn and B is in Φn-1.

The corresponding classical prenex classes are defined more simply:

  • Π0 = Σ0 = Δ0,
  • Πn+1 is the class of all formulas of the form ∀x A(x) where A(x) is in Σn,
  • Σn+1 is the class of all formulas of the form ∃x A(x) where A(x) is in Πn.

Peano arithmetic PA comes from Heyting arithmetic HA by adding LEM or (¬ ¬A → A) to the list of logical axioms, i.e., by using classical instead of intuitionistic logic. The following results hold even in the fragments of HA and PA with the induction schema restricted to Δ0 formulas.

Burr's Theorem:
  • Every arithmetical formula is provably equivalent in HA to a formula in one of the classes Φn.
  • Every formula in Φn is provably equivalent in PA to a formula in Πn, and conversely.
  • Every formula in Ψn is provably equivalent in PA to a formula in Σn, and conversely.

HA and PA are proof-theoretically equivalent, as will be shown in Section 4. Each is capable of (numeralwise) expressing its own proof predicate. By Gödel's famous Incompleteness Theorem, if HA is consistent then neither HA nor PA can prove its own consistency.

4. Basic Proof Theory

4.1 Translating classical into intuitionistic logic

A fundamental fact about intuitionistic logic is that it has the same consistency strength as classical logic. For propositional logic this was first proved by Glivenko [1929].

Glivenko's Theorem: An arbitrary propositional formula A is classically provable, if and only if ¬¬A is intuitionistically provable.

Glivenko's Theorem does not extend to predicate logic, although an arbitrary predicate formula A is classically provable if and only if ¬¬A is provable in intuitionistic predicate logic plus the “double negation shift” schema

(DNS) ∀x¬¬B(x) → ¬¬∀x B(x).

The more sophisticated negative translation of classical into intuitionistic theories, due independently to Gödel and Gentzen, associates with each formula A of the language L another formula g(A) (with no ∨ or ∃), such that

(I) Classical predicate logic proves A ↔ g(A).
(II) Intuitionistic predicate logic proves g(A) ↔ ¬ ¬ g(A).
(III) If classical predicate logic proves A, then intuitionistic predicate logic proves g(A).

The proofs are straightforward from the following inductive definition of g(A) (using Gentzen's direct translation of implication, rather than Gödel's in terms of ¬ and &):

  • g(P) is ¬ ¬ P, if P is prime.
  • g(A & B) is (g(A) & g(B)).
  • g(A ∨ B) is ¬ (¬g(A) & ¬g(B)).
  • g(A → B) is (g(A) → g(B)).
  • g(¬A) is ¬ g(A).
  • g(∀xA(x)) is ∀x g(A(x)).
  • g(∃xA(x)) is ¬∀x¬g(A(x)).

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. Hence

(IV) Classical and intuitionistic predicate logic are equiconsistent.

The negative translation of classical into intuitionistic number theory is even simpler, since prime formulas of intuitionistic arithmetic are stable. Thus g(s=t) can be taken to be (s=t), and the other clauses are unchanged. The negative translation of any instance of mathematical induction is another instance of mathematical induction, and the other nonlogical axioms of arithmetic are their own negative translations, so

(I), (II), (III) and (IV) hold also for number theory.

Gödel [1933e] interpreted these results as showing that intuitionistic logic and arithmetic are richer than classical logic and arithmetic, because the intuitionistic theory distinguishes formulas which are classically equivalent, and has the same consistency strength as the classical theory.

Direct attempts to extend the negative interpretation to analysis fail because the negative translation of the countable axiom of choice is not a theorem of intuitionistic analysis. However, it is consistent with intuitionistic analysis, including Brouwer's controversial continuity principle, by the functional version of Kleene's recursive realizability (Section 5.2 below).

4.2 Admissible rules of intuitionistic logic and arithmetic

Gödel [1932] observed that intuitionistic propositional logic has the disjunction property:

(DP) 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:

(ED) If ∃xA(x) is a closed theorem, then for some closed term t, A(t) is a theorem.

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. For example, Harrop [1960] observed that the rule

If (¬A → (B ∨ C)) is a theorem, so is (¬A → B) ∨ (¬A → C)

is admissible for intuitionistic propositional logic IPC because if A, B and C are any formulas such that (¬A → (B ∨ C)) is provable in IPC, then also (¬A → B) ∨ (¬A → C) is provable in IPC. Harrop's rule is not derivable in IPC because (¬A → (B ∨ C)) → (¬A → B) ∨ (¬A → C) is not intuitionistically provable. Another important example of an admissible nonderivable rule of IPC is Mints' rule:

If ((A → B) → A ∨ C) is a theorem, so is ((A → B) → A) ∨ ((A → B) → C).

The two-valued truth table interpretation of classical propositional logic CPC gives rise to a simple proof that every admissible rule of CPC is derivable: otherwise, some assignment to A, B, etc. would make the hypothesis true and the conclusion false, and by substituting e.g. (P → P) for the letters assigned “true” and (P & ¬ P) for those assigned “false” one would have a provable hypothesis and unprovable conclusion. The fact that the intuitionistic situation is more interesting leads to many natural questions, some of which have recently been answered.

By generalizing Mints' Rule, Visser and de Jongh identified a recursively enumerable sequence of successively stronger admissible rules (“Visser's rules”) which, they conjectured, formed a basis for the admissible rules of IPC in the sense that every admissible rule is derivable from the disjunction property and one of the rules of the sequence. Building on work of Ghilardi [1999], Iemhoff [2001] succeeded in proving their conjecture. Rybakov [1997] proved that the collection of all admissible rules of IPC is decidable but has no finite basis. Visser [2002] showed that his rules are also the admissible propositional rules of HA, and of HA extended by Markov's Principle MP (defined in Section 5.2 below). More recently, Jerabek [2008] found a different basis for the admissible rules of IPC with the property that no rule in the basis derives another.

Much less is known about the admissible rules of intuitionistic predicate logic. Pure IQC, without individual or predicate constants, has the following remarkable admissible rule for A(x) with no variables free but x:

If ∃x A(x) is a theorem, so is ∀x A(x).

Not every admissible predicate rule of IQC is admissible for all formal systems based on IQC; for example, HA evidently violates the rule just stated. Visser proved in [1999] that the property of being an admissible predicate rule of HA is Π2 complete, and in [2002] that HA &plus; MP has the same predicate admissible rules as HA. Plisko [1992] proved that the predicate logic of HA + MP (the set of sentences in the language of IQC all of whose uniform substitution instances in the language of arithmetic are provable in HA + MP) is Π2 complete; Visser [2006] extended this result to some constructively interesting consistent extensions of HA which are not contained in PA.

While they have not been completely classified, the admissible rules of intuitionistic predicate logic are known to include Markov's Rule for decidable predicates:

If ∀x(A(x) ∨ ¬A(x)) & ¬∀x¬A(x) is a theorem, so is ∃x A(x)

and the following Independence-of-Premise Rule (where y is assumed not to occur free in A(x)):

If ∀x(A(x) ∨ ¬A(x)) & (∀x A(x) → ∃y B(y)) is a theorem, so is ∃y (∀x A(x) → B(y)).

Both rules are also admissible for HA. The corresponding implications (MP and IP respectively), which are not provable intuitionistically, are verified by Gödel's “Dialectica” interpretation of HA (cf. Section 6.3 below). So is the implication (CT) corresponding to one of the most interesting admissible rules of Heyting arithmetic, let us call it the Church-Kleene Rule:

If ∀x ∃y A(x, y) is a closed theorem of HA then there is a number n such that, provably in HA, the partial recursive function with Gödel number n is total and maps each x to a y satisfying A(x, y) (and moreover A(x,y) is provable, where x is the numeral for the natural number x and y is the numeral for y).

Combining Markov's Rule with the negative translation gives the result that classical and intuitionistic arithmetic prove the same formulas of the form ∀x ∃y A(x, y) where A(x, y) is quantifier-free. In general, if A(x, y) is provably decidable in HA and if ∀x ∃y A(x, y) is a closed theorem of classical arithmetic PA, the conclusion of the Church-Kleene Rule holds even in intuitionistic arithmetic. For if HA proves ∀x ∀y (A(x,y) ∨ ¬A(x,y)) then by the Church-Kleene Rule the characteristic function of A(x,y) has a Gödel number m, provably in HA; so HA proves ∀x ∃y A(x,y) ↔ ∀x ∃y ∃z B(m,x,y,z) where B is quantifier-free, and the adjacent existential quantifiers can be contracted in HA. It follows that HA and PA have the same provably recursive functions.

Here is a proof that the rule “If ∀x (A ∨ B(x)) is a theorem, so is A ∨ ∀x B(x)” (where x is not free in A) is not admissible for HA, if HA is consistent. Gödel numbering provides a quantifier-free formula G(x) which (numeralwise) expresses the predicate “x is the code of a proof in HA of (0 = 1).” By intuitionistic logic with the decidability of quantifier-free arithmetical formulas, HA proves ∀x(∃yG(y) ∨ ¬G(x)). However, if HA proved ∃yG(y) ∨ ∀x¬G(x) then by the disjunction property, HA must prove either ∃yG(y) or ∀x¬G(x). The first case is impossible, by the existence property with the consistency assumption and the fact that HA proves all true quantifier-free sentences. But the second case is also impossible, by Gödel's second incompleteness theorem, since ∀x¬G(x) expresses the consistency of HA.

5. Basic Semantics

5.1 Kripke semantics for intuitionistic logic

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, the Kleene and Aczel slashes, and models based on sheafs and topoi. 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 for L 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), 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 0-ary predicate letter (each proposition letter) P, either assign f(P, k) = true or leave f(P, k) undefined, consistent with the requirement that if k ≤ k′ and f(P, k) = true then f(P, k′) = true also. Say that

k forces P if and only if f(P, k) = true.

To each node k and each (n+1)-ary predicate letter Q(…), assign a (possibly empty) set T(Q, k) of (n+1)-tuples of elements of D(k) in such a way that if k ≤ k′ then T(Q, k) ⊆ T(Q, k′). Say that

k forces Q(d0,…,dn) if and only if (do,…,dn) ∈ T(Q, k).

Now define forcing for compound sentences of L(k) inductively as follows:

  • k forces (A & B) if k forces A and k forces B.
  • k forces (A ∨ B) if k forces A or k forces B.
  • k forces (A → B) if, for every k′ ≥ k, if k′ forces A then k′ forces B.
  • k forces ¬A if for no k′ ≥ k does k′ force A.
  • k forces ∀xA(x) if for every k′ ≥ k and every d ∈ D(k′), k′ forces A(d).
  • k forces ∃xA(x) if for some d ∈ D(k), k forces A(d).

Any such forcing relation is consistent and monotone:

  • for no sentence A and no k does k force both A and ¬A.
  • if k ≤ k′ and k forces A then k′ forces A.

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 (¬∀x¬P(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}. And to show the converse is intuitionistically provable (without actually exhibiting a proof), one only needs the consistency and monotonicity properties of arbitrary Kripke models, with the definition of forcing.

Kripke models for languages with equality may interpret = at each node by an arbitrary equivalence relation, subject to monotonicity. For applications to intuitionistic arithmetic, normal models (those in which equality is interpreted by identity at each node) suffice because equality of natural numbers is decidable.

Propositional Kripke semantics is particulary simple, since an arbitrary propositional formula is intuitionistically provable if and only if it is forced by the root of every Kripke model whose frame (the set K of nodes together with their partial ordering) is a finite tree with a least element (the root). For example, the Kripke model with K = {k, k′, k ′′}, k < k′ and k < k′′, and with P true only at k′, shows that both P ∨ ¬P and ¬P ∨ ¬¬P are unprovable in IPC.

Each terminal node or leaf of a Kripke model is a classical model, because a leaf forces every formula or its negation. Only those proposition letters which occur in a formula E, and only those nodes k′ such that k≤k′, are relevant to deciding whether or not k forces E. Such considerations allow us to associate effectively with each formula E of L(IPC) a finite class of finite Kripke structures which will include a countermodel to E if one exists. Since the class of all theorems of IPC is recursively enumerable, we conclude that

IPC is effectively decidable. There is a recursive procedure which determines, for each propositional formula E, whether or not E is a theorem of IPC, concluding with either a proof of E or a Kripke countermodel.

The decidability of IPC was first obtained by Gentzen in 1933 as an immediate corollary of his Hauptsatz. The undecidability of IQC follows from the undecidability of CQC by the negative interpretation.

Familiar non-intuitionistic logical schemata correspond to structural properties of Kripke models, for example

  • DNS holds in every Kripke model with finite frame.
  • (A → B) ∨ (B → A) holds in every Kripke model with linearly ordered frame. Conversely, every propositional formula which is not derivable in IPC + (A → B) ∨ (B → A) has a Kripke countermodel with linearly ordered frame.
  • If x is not free in A then (∀x(A∨B(x)) → (A ∨ ∀x B(x))) holds in every Kripke model K with constant domain (so that D(k) = D(k′) for all k, k′ in K). The same is true for MP.

Kripke models are a powerful tool for establishing properties of intuitionistic formal systems; cf. Troelstra and van Dalen [1988], Smorynski [1973], de Jongh and Smorynski [1976], Ghilardi [1999] and Iemhoff [2001], [2005]. Following Gödel, Kreisel [1962] argued that Kripke-completeness of intuitionistic logic entailed Markov's Principle. By modifying the definition of a Kripke model to allow “exploding nodes” which force every sentence, Veldman [1976] found an intuitionistic completeness proof avoiding (the informal use of) MP.

5.2 Realizability semantics for Heyting arithmetic

One way to implement the B-H-K explanation of intuitionistic truth for arithmetic is to associate with each sentence E of HA some collection of numerical codes for algorithms which could establish the constructive truth of E. Following Kleene [1945], a number e realizes a sentence E of the language of arithmetic by induction on the logical form of E:

  • e realizes (r = t), if (r = t) is true.
  • e realizes (A & B), if e codes a pair (f,g) such that f realizes A and g realizes B.
  • e realizes A∨B, if e codes a pair (f,g) such that if f = 0 then g realizes A, and if f > 0 then g realizes B.
  • e realizes A→B, if, whenever f realizes A, then the eth partial recursive function is defined at f and its value realizes B.
  • e realizes ¬A, if no f realizes A.
  • e realizes ∀x A(x), if, for every n, the eth partial recursive function is defined at n and its value realizes A(n).
  • e realizes ∃x A(x), if e codes a pair (n,g) and g realizes A(n).

An arbitrary formula is realizable if some number realizes its universal closure. Observe that not both A and ¬A are realizable, for any formula A. The fundamental result is

Nelson's Theorem [1947]. If A is derivable in HA from realizable formulas F, then A is realizable.

Some nonintuitionistic principles can be shown to be realizable. For example, Markov's Principle (for decidable formulas) can be expressed by the schema

(MP) ∀x(A(x) ∨ ¬A(x)) & ¬∀x¬A(x) → ∃x A(x).

Although unprovable in HA, MP is realizable by an argument which uses Markov's Principle informally. But realizability is a fundamentally nonclassical interpretation. In HA it is possible to express an axiom of recursive choice CT (for “Church's Thesis”), which contradicts LEM but is (constructively) realizable. Hence by Nelson's Theorem, HA + MP + CT is consistent.

Kleene used a variant of number-realizability to prove HA satisfies the Church-Kleene Rule; the same argument works for HA with MP and/or CT. In Kleene and Vesley [1965] and Kleene [1969], functions replace numbers as realizing objects, establishing the consistency of formalized intuitionistic analysis and its closure under a second-order version of the Church-Kleene Rule.

De Jongh [1970] combined realizability with Kripke modeling to show that intuitionistic predicate logic is arithmetically complete for HA. If, to each n-place predicate letter P(…), a formula f(P) of L(HA) with n free variables is assigned, and if the formula f(A) of L(HA) comes from the formula A of L by replacing each prime formula P(x1,…, xn) by f(P)(x1,…, xn), then f(A) is called an arithmetical substitution instance of A. A uniform assignment of simple existential formulas to predicate letters suffices to prove

De Jongh's Theorem. If a sentence A of the language L is not provable in IQC, then some arithmetical substitution instance of A is not provable in HA.

For example, if P(x, y) expresses “x codes a proof in HA of the formula with code y,” then ∀y (∃x P(x, y) ∨ ¬∃x P(x, y)) is unrealizable, hence unprovable in HA, and so is its double negation. (The proof of de Jongh's Theorem for IPC does not need realizability; cf. Smorynski [1973]. As an example, Rosser's form of Gödel's Incompleteness Theorem provides a sentence C of L(HA) such that PA proves neither C nor ¬C, so by the disjunction property HA cannot prove (C ∨ ¬C).)

Without claiming that number-realizability coincides with intuitionistic arithmetical truth, Nelson observed that for each formula A of L(HA) the predicate “y realizes A” can be expressed in HA by another formula (abbreviated “y re A”), and the schema A ↔ ∃y (y re A) is consistent with HA. Troelstra [1973] showed that HA + (A ↔ ∃y (y re A)) is equivalent to HA + ECT, where ECT is a strengthened form of CT. In HA + MP + ECT, which Troelstra considers to be a formalization of Russian recursive mathematics (cf. section 3.2 of the entry on constructive mathematics), every formula of the form (y re A) has an equivalent “classical” prenex form A′(y) consisting of a quantifier-free subformula preceded by alternating “classical” quantifiers of the forms ¬¬∃x and ∀z¬¬, and so ∃y A′(y) is a kind of prenex form of A.

6. Additional Topics and Further Reading

6.1 Subintuitionistic and superintuitionistic logics

At present there are several other entries in this encyclopedia treating intuitionistic logic in various contexts, but a general treatment of intermediate logics appears to be lacking so a brief one is included here. A subintuitionistic propositional logic can be obtained from IPC by restricting the language, or weakening the logic, or both. An extreme example of the first is RN, intuitionistic logic with a single propositional variable P, which is named after its discoverers Rieger and Nishimura [1960]. RN is characterized by the Rieger-Nishimura lattice of infinitely many nonequivalent formulas Fn such that every formula whose only propositional variable is P is equivalent by intuitionistic logic to some Fn. Nishimura's version is

  • F∞ = P → P.
  • F0 = P & ¬ P.
  • F1 = P.
  • F2 = ¬ P.
  • F2n+3 = F2n+1 ∨ F2n+2.
  • F2n+4 = F2n+3 → F2n+1.

In RN neither F2n + 1 nor F2n + 2 implies the other; but F2n implies F2n+1, and F2n+1 implies each of F2n+3 and F2n+4.

Fragments of IPC missing one or more logical connective restrict the language and incidentally the logic, since the intuitionistic connectives &, ∨, →, ¬ are logically independent over IPC. Rose [1953] proved that the implicationless fragment (without →) is complete with respect to realizability, in the sense that if every arithmetical substitution instance of a propositional formula E without → is (number)-realizable then E is a theorem of IPC. This result contrasts with

Rose's Theorem [1953]. IPC is incomplete with respect to realizability. Let F be the propositional formula

((¬ ¬ D → D) → (¬ ¬ D ∨ ¬ D)) → (¬ ¬ D ∨ ¬ D)

where D is (¬ P ∨ ¬ Q) and P, Q are prime. Every arithmetical substitution instance of F is realizable (using classical logic), but F is not provable in IPC.

It follows that IPC is arithmetically incomplete for HA + ECT (cf. Section 5.2).

An intermediate propositional logic is any consistent collection of propositional formulas containing all the axioms of IPC and closed under modus ponens and substitution of arbitrary formulas for proposition letters. Each intermediate propositional logic is contained in CPC. Some particular intermediate propositional logics, characterized by adding one or more classically correct but intuitionistically unprovable axiom schemas to IPC, have been studied extensively.

One of the simplest intermediate propositional logics is the Gödel-Dummett logic LC, obtained by adding to IPC the schema (A → B) ∨ (B → A) which is valid on all and only those Kripke frames in which the partial order of the nodes is linear. Gödel [1932] used an infinite sequence of successively stronger intermediate logics to show that IPC has no finite truth-table interpretation. For each positive integer n, let Gn be LC plus the schema (A1 → A2) ∨ ... ∨ (A1 & ... & An → An+1). Then Gn is valid on all and only those linearly ordered Kripke frames with no more than n nodes.

The Kreisel-Putnam logic KP, obtained by adding to IPC the schema (¬ A → B ∨ C) → ((¬ A → B) ∨ (¬ A → C)), has the disjunction property but does not satisfy all the Visser rules. The intermediate logic obtained by adding the schema ((¬ ¬ D → D) → (D ∨ ¬ D)) → (¬ ¬ D ∨ ¬ D), corresponding to Rose's counterexample, to IPC also has the disjunction property. Iemhoff [2005] proved that IPC is the only intermediate propositional logic with the disjunction property which is closed under all the Visser rules. Iemhoff and Metcalfe [2009] developed a formal calculus for generalized admissibility for IPC and some intermediate logics.

An intermediate propositional logic L is said to have the finite frame property if there is a class of finite frames on which the Kripke-valid formulas are exactly the theorems of L. Many intermediate logics, including LC (the class of finite linear frames) and KP, have this property. De Jongh, Verbrugge and Visser [2009] proved that every intermediate logic L with the finite frame property is the propositional logic of HA(L), that is, the class of all formulas in the language of IPC all of whose arithmetical substitution instances are provable in the logical extension of HA by L.

Some intermediate predicate logics, extending IQC and closed under substitution, are IQC &plus; DNS (Section 4.1), IQC &plus; MP (cf. Section 5.2), IQC &plus; MP &plus; IP (cf. Section 6.2), and the intuitionistic logic of constant domains CD obtained by adding to IQC the schema ∀x(A∨B(x)) → (A ∨ ∀x B(x)) for all formulas A, B(x) with x not occurring free in A. Mints, Olkhovikov and Urquhart [2012, Other Internet Resources] showed that CD does not have the interpolation property, refuting earlier published proofs by other authors.

6.2 Advanced topics

Brouwer's influence on Gödel was significant, although Gödel never became an intuitionist. Gödel's [1933f] translation of intuitionistic propositional logic into the modal logic S4 is described in Section 2.5 of the entry on Gödel and in Troelstra's introductory note to the translation of [1933f] in Volume I of Gödel's Collected Works. See also Mints [2012]. Kripke models for modal logic predated those for intuitionistic logic.

An alternative to realizability semantics for intuitionistic arithmetic is Gödel's [1958] “Dialectica” interpretation, which associates with each formula B of L(HA) a quantifier-free formula BD in the language of intuitionistic arithmetic of all finite types. The “Dialectica” interpretation of B, call it BD, is ∃Y∀x BD(Y, x). If B is a closed theorem of HA, then BD(F, x) is provable for some term F in Gödel's theory T of “primitive recursive” functionals of higher type. The translation from B to BD requires the axiom of choice (at all finite types), MP and IP, so is not strictly constructive; however, the number-theoretic functions expressible by terms F of T are precisely the provably recursive functions of HA (and of PA). The interpretation was extended to analysis by Spector [1962]; cf. Howard [1973]. Clear expositions, and additional references, are to be found in Troelstra's introduction to the English translation in Gödel [1990] of the original Dialectica article, and in Avigad and Feferman [1998].

While HA is a proper part of classical arithmetic, the intuitionistic attitude toward mathematical objects results in a theory of real numbers (cf. sections 3.4–3.7 of the entry on intuitionism in the philosophy of mathematics) diverging from the classical. Kleene's function-realizability interpretation, developed to prove the consistency of his formalization FIM of the intuitionistic theory of sequences (“intuitionistic analysis”), changes the interpretation of arithmetical formulas; for example, ¬ ¬∀x (A(x) ∨ ¬A(x)) is function-realizable for every arithmetical formula A(x). In the language of analysis, Markov's Principle and the negative translation of the countable axiom of choice are among the many non-intuitionistic principles which are function-realizable (by classical arguments) and hence consistent with FIM; cf. Kleene [1965], Vesley [1972] and Moschovakis [2003].

Concrete and abstract realizability semantics for a wide variety of formal systems have been developed and studied by logicians and computer scientists; cf. Troelstra [1998] and van Oosten [2002] and [2008]. Variations of the basic notions are especially useful for establishing relative consistency and relative independence of the nonlogical axioms in theories based on intuitionistic logic; some examples are Moschovakis [1971], Lifschitz [1979], and the realizability notions for constructive and intuitionistic set theories developed by Rathjen [2006, 2012] and Chen [2012]. Early abstract realizability notions include the slashes of Kleene [1962, 1963] and Aczel [1968], and Läuchli [1970]. Kohlenbach, Avigad and others have developed realizability interpretations for parts of classical mathematics.

Artemov's justification logic is an alternative interpretation of the B-H-K explanation of the intuitionistic connectives and quantifiers, with (idealized) proofs playing the part of realizing objects. See also Artemov and Iemhoff [2007].

Another line of research in intuitionistic logic concerns Brouwer's very controversial “creating subject counterexamples” to principles of classical analysis (such as Markov's Principle) which could not be refuted on the basis of the theory FIM of Kleene and Vesley [1965]. By weakening Kleene's form of Brouwer's principle of continuous choice, and adding an axiom he called Kripke's Schema (KP), Myhill managed to formalize the creating subject arguments. KP is inconsistent with FIM, but Vesley [1970] found an alternative principle (Vesley's Schema (VS)) which can consistently be added to FIM and implies all the counterexamples for which Brouwer required a creating subject. Krol and Scowcroft gave topological consistency proofs for intuitionistic analysis with Kripke's Schema and weak continuity.

6.3 Recommended reading

The entry on L. E. J. Brouwer discusses Brouwer's philosophy and mathematics, with a chronology of his life and a selected list of publications including translations and secondary sources. The best way to learn more is to read some of the original papers. English translations of Brouwer's doctoral dissertation and other papers which originally appeared in Dutch, along with a number of articles in German, can be found in L. E. J. Brouwer: Collected Works [1975], edited by Heyting. Benacerraf and Putnam's essential source book contains Brouwer [1912] (in English translation), Brouwer [1949] and Dummett [1975]. Mancosu's [1998] provides English translations of many fundamental articles by Brouwer, Heyting, Glivenko and Kolmogorov, with illuminating introductory material by W. van Stigt whose [1990] is another valuable resource.

The third edition [1971] of Heyting's classic [1956] is an attractive introduction to intuitionistic philosophy, logic and mathematical practice. As part of the formidable project of editing and publishing Brouwer's Nachlass, van Dalen [1981] provides a comprehensive view of Brouwer's own intuitionistic philosophy. The English translation, in van Heijenoort [1969], of Brouwer's [1927] (with a fine introduction by Parsons) is still an indispensable reference for Brouwer's theory of the continuum. Veldman [1990] and [2005] are authentic modern examples of traditional intuitionistic mathematical practice. Troelstra [1991] places intuitionistic logic in its historical context as the common foundation of constructive mathematics in the twentieth century. Bezhanishvili and de Jongh [2005, Other Internet Resources] includes very recent developments in intuitionistic logic.

Kleene and Vesley's [1965] gives a careful axiomatic treatment of intuitionistic analysis, a proof of its consistency relative to a classically correct subtheory, and an extended application to Brouwer's theory of real number generators. 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 gives the Church-Kleene Rule for intuitionistic analysis.

Troelstra's [1973], Beeson's [1985] and Troelstra and van Dalen's [1988] stand out as the most comprehensive studies of intuitionistic and semi-intutionistic formal theories, using both constructive and classical methods, with useful bibliographies. Troelstra's [1998] presents formulas-as-types and (Kleene and Aczel) slash interpretations for propositional and predicate logic, as well as abstract and concrete realizabilities for a multitude of applications. Martin-Löf's constructive theory of types [1984] (cf. Section 3.4 of the entry on constructive mathematics) provides another general framework within which intuitionistic reasoning continues to develop.

Bibliography

  • Aczel, P., 1968, “Saturated intuitionistic theories,” in H.A. Schmidt, K. Schütte, and H.-J. Thiele (eds.), Contributions to Mathematical Logic, Amsterdam: North-Holland: 1–11.
  • Artemov, S. and Iemhoff, R., 2007, “The basic intuitionistic logic of proofs,” Journal of Symbol Logic, 72: 439–451.
  • Avigad, J. and Feferman, S., 1998, “Gödel's functional (”Dialectica“) interpretation,” Chapter V of Buss (ed.) 1998: 337–405.
  • Bar-Hillel, Y. (ed.), 1965, Logic, Methodology and Philosophy of Science, Amsterdam: North Holland.
  • Beeson, M. J., 1985, Foundations of Constructive Mathematics, Berlin: Springer.
  • Benecerraf, P. and Hilary Putnam (eds.), 1983, Philosophy of Mathematics: Selected Readings, 2nd Edition, Cambridge: Cambridge University Press.
  • Brouwer, L. E. J., 1907, “On the Foundations of Mathematics,” Thesis, Amsterdam; English translation in Heyting (ed.) 1975: 11–101.
  • Brouwer, L. E. J., 1908, “The Unreliability of the Logical Principles,” English translation in Heyting (ed.) 1975: 107–111.
  • Brouwer, L. E. J., 1912, “Intuitionism and Formalism,” English translation by A. Dresden, Bulletin of the American Mathematical Society, 20 (1913): 81–96, reprinted in Benacerraf and Putnam (eds.) 1983: 77–89; also reprinted in Heyting (ed.) 1975: 123–138.
  • Brouwer, L. E. J., 1923, 1954, “On the significance of the principle of excluded middle in mathematics, especially in function theory,” “Addenda and corrigenda,” and “Further addenda and corrigenda,” English translation in van Heijenoort (ed.) 1967: 334–345.
  • Brouwer, L. E. J., 1927, “Intuitionistic reflections on formalism,” originally published in 1927, English translation in van Heijenoort (ed.) 1967: 490–492.
  • Brouwer, L. E. J., 1948, “Consciousness, philosophy and mathematics,” originally published (1948), reprinted in Benacerraf and Putnam (eds.) 1983: 90–96.
  • Burr, W., 2004, “The intuitionistic arithmetical hierarchy,” in J. van Eijck, V. van Oostrom and A. Visser (eds.), Logic Colloquium '99 (Lecture Notes in Logic 17), Wellesley, MA: ASL and A. K. Peters, 51–59.
  • Buss, S. (ed.), 1998, Handbook of Proof Theory, Amsterdam and New York: Elsevier.
  • Chen, R-M. and Rathjen, M., 2012, “Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory,” Archive for Mathematical Logic, 51: 789–818.
  • Crossley, J., and M. A. E. Dummett (eds.), 1965, Formal Systems and Recursive Functions, Amsterdam: North-Holland Publishing.
  • van Dalen, D. (ed.), 1981, Brouwer's Cambridge Lectures on Intuitionism, Cambridge: Cambridge University Press.
  • Dummett, M., 1975, “The philosophical basis of intuitionistic logic,” originally published (1975), reprinted in Benacerraf and Putnam (eds.) 1983: 97–129.
  • Friedman, H., 1975, “The disjunction property implies the numerical existence property,” Proceedings of the National Academy of Science, 72: 2877–2878.
  • Gentzen, G., 1934–5, “Untersuchungen Über das logische Schliessen,” Mathematsche Zeitschrift, 39: 176–210, 405–431.
  • Ghilardi, S., 1999, “Unification in intuitionistic logic,” Journal of Symbolic Logic, 64: 859–880.
  • Gödel, K., 1932, “Zum intuitionistischen Aussagenkalkül,” Anzeiger der Akademie der Wissenschaftischen in Wien 69: 65–66. Reproduced and translated with an introductory note by A. S. Troelstra in Gödel 1986: 222–225.
  • Gödel, K., 1933e, “Zur intuitionistischen Arithmetik und Zahlentheorie,” Ergebnisse eines mathematischen Kolloquiums, 4: 34–38.
  • Gödel, K., 1933f, “Eine Interpretation des intuitionistischen Aussagenkalküls,” reproduced and translated with an introductory note by A. S. Troelstra in Gödel 1986: 296–304.
  • Gödel, K., 1958, “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes,” Dialectica, 12: 280–287. Reproduced with an English translation in Gödel 1990: 241–251.
  • Gödel, K., 1986, Collected Works, Vol. I, S. Feferman et al. (eds.), Oxford: Oxford University Press.
  • Gödel, K., 1990, Collected Works, Vol. II, S. Feferman et al. (eds.), Oxford: Oxford University Press.
  • Glivenko, V., 1929, “Sur qulques points de la logique de M. Brouwer,” Academie Royale de Belgique, Bulletins de la classe des sciences, 5 (15): 183–188.
  • Harrop R., 1960, “Concerning formulas of the types A → B ∨ C, A → (Ex)B(x) in intuitionistic formal systems,” Journal of Symbolic Logic, 25: 27–32.
  • van Heijenoort, J. (ed.), 1967, From Frege to Gödel: A Source Book In Mathematical Logic 1879–1931, Cambridge, MA: Harvard University Press.
  • Heyting, A., 1930, “Die formalen Regeln der intuitionistischen Logik,” in three parts, Sitzungsberichte der preussischen Akademie der Wissenschaften: 42–71, 158–169. English translation of Part I in Mancosu 1998: 311–327.
  • Heyting, A., 1956, Intuitionism: An Introduction, Amsterdam: North-Holland Publishing, 3rd revised edition, 1971.
  • Heyting, A. (ed.), 1975, L. E. J. Brouwer: Collected Works (Volume 1: Philosophy and Foundations of Mathematics), Amsterdam and New York: Elsevier.
  • Howard, W. A., 1973, “Hereditarily majorizable functionals of finite type,” in Troelstra (ed.) 1973: 454–461.
  • Iemhoff, R., 2001, “On the admissible rules of intuitionistic propositional logic,” Journal of Symbolic Logic, 66: 281–294.
  • Iemhoff, R., 2005, “Intermediate logics and Visser's rules,” Notre Dame Journal of Formal Logic, 46: 65–81.
  • Iemhoff, R. and Metcalfe, G., 2009, “Proof theory for admissible rules,” Annals of Pure and Applied Logic, 159: 171–186.
  • Jerabek, E., 2008, “Independent bases of admissible rules,” Logic Journal of the IGPL, 16: 249–267.
  • de Jongh, D. H. J., 1970, “The maximality of the intuitionistic propositional calculus with respect to Heyting's Arithmetic,” Journal of Symbolic Logic, 6: 606.
  • de Jongh, D. H. J., and Smorynski, C., 1976, “Kripke models and the intuitionistic theory of species,” Annals of Mathematical Logic, 9: 157–186.
  • de Jongh, D., Verbrugge, R. and Visser, A., 2011, “Intermediate logics and the de Jongh property,” Archive for Mathematical Logic, 50: 197–213.
  • Kino, A., Myhill, J. and Vesley, R. E. (eds.), 1970, Intuitionism and Proof Theory: Proceedings of the summer conference at Buffalo, NY, 1968, Amsterdam: North-Holland.
  • Kleene, S. C., 1945, “On the interpretation of intuitionistic number theory,” Journal of Symbolic Logic, 10: 109–124.
  • Kleene, S. C., 1952, Introduction to Metamathematics, Princeton: Van Nostrand.
  • Kleene, S. C., 1962, “Disjunction and existence under implication in elementary intuitionistic formalisms,” Journal of Symbolic Logic, 27: 11–18.
  • Kleene, S. C., 1963, “An addendum,” Journal of Symbolic Logic, 28: 154–156.
  • Kleene, S. C., 1965, “Classical extensions of intuitionistic mathematics,” in Bar-Hillel (ed.) 1965: 31-44.
  • Kleene, S. C., 1969, Formalized Recursive Functionals and Formalized Realizability, Memoirs of the American Mathematical Society 89.
  • Kleene, S. C. and Vesley, R. E., 1965, The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions, Amsterdam: North-Holland.
  • Kreisel, G., 1962, “On weak completeness of intuitionistic predicate logic,” Journal of Symbolic Logic, 27: 139–158.
  • Kripke, S. A., 1965, “Semantical analysis of intuitionistic logic,” in J. Crossley and M. A. E. Dummett (eds.) 1965: 92–130.
  • Läuchli, H., 1970, “An abstract notion of realizability for which intuitionistic predicate calculus is complete,” in A. Kino et. al. (eds.) 1965: 227–234.
  • Lifschitz, V., 1979, “CT0 is stronger than CT0!,” Proceedings of the American Mathematical Society, 73: 101–106.
  • Mancosu, P., 1998, From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920s, New York and Oxford: Oxford University Press.
  • Martin-Löf, P., 1984, Intuitionistic Type Theory, Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980, Napoli: Bibliopolis.
  • Mints, G., 2012, “The Gödel–Tarski translations of intuitionistic propositional formulas,” in Correct Reasoning (Lecture Notes in Computer Science 7265), E. Erdem et al. (eds.), Dordrecht: Springer-Verlag: 487-491.
  • Moschovakis, J. R., 1971, “Can there be no nonrecursive functions?,” Journal of Symbolic Logic, 36: 309–315.
  • Moschovakis, J. R., 2003, “Classical and constructive hierarchies in extended intuitionistic analysis,” Journal of Symbolic Logic, 68: 1015–1043.
  • Moschovakis, J. R., 2009, “The logic of Brouwer and Heyting,” in Logic from Russell to Church (Handbook of the History of Logic, Volume 5), J. Woods and D. Gabbay (eds.), Amsterdam: Elsevier: 77–125.
  • Nishimura, I., 1960, “On formulas of one variable in intuitionistic propositional calculus,” Journal of Symbolic Logic, 25: 327–331.
  • van Oosten, J., 1991, “A semantical proof of de Jongh's theorem,” Archives for Mathematical Logic, 31: 105–114.
  • van Oosten, J., 2002, “Realizability: a historical essay,” Mathematical Structures in Computer Science, 12: 239–263.
  • van Oosten, J., 2008, Realizability: An Introduction to its Categorical Side, Amsterdam: Elsevier.
  • Plisko, V. E., 1992, “On arithmetic complexity of certain constructive logics,” Mathematical Notes, (1993): 701–709. Translated from Matematicheskie Zametki, 52 (1992): 94–104.
  • Rathjen, M., 2006, “Realizability for constructive Zermelo-Fraenkel set theory,” in Logic Colloquium 2003 (Lecture Notes in Logic 24), J. Väänänen et. al. (eds.), A. K. Peters 2006: 282–314.
  • Rathjen, M., 2012, “From the weak to the strong existence property,” Annals of Pure and Appled Logic, 163: 1400–1418.
  • Rose, G. F., 1953, “Propositional calculus and realizability,” Transactions of the American Mathematical Society, 75: 1–19.
  • Rybakov, V., 1997, Admissibility of Logical Inference Rules, Amsterdam: Elsevier.
  • Smorynski, C. A., 1973, “Applications of Kripke models,” in Troelstra (ed.) 1973: 324–391.
  • Spector, C., 1962, “Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics,” Recursive Function Theory: Proceedings of Symposia in Pure Mathematics, Volume 5, J. C. E. Dekker (ed.), Providence, RI: American Mathematical Society, 1–27.
  • van Stigt, W. P., 1990, Brouwer's Intuitionism, Amsterdam: North-Holland.
  • Troelstra, A. S. (ed.), 1973, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis (Lecture Notes in Mathematics 344), Berlin: Springer-Verlag. Corrections and additions available from the editor.
  • Troelstra, A. S., 1991, “History of constructivism in the twentieth century,” ITLI Prepublication Series ML–1991–05, Amsterdam. Final version in Set Theory, Arithmetic and Foundations of Mathematics (Lecture Notes in Logic 36), J. Kenney and R. Kossak (eds.), Association for Symbolic Logic, Ithaca, NY, 2011: 150–179.
  • Troelstra, A. S., 1998, “Realizability,” Chapter VI of Buss (ed.), 1998: 407–473.
  • Troelstra, A. S., Introductory note to 1958 and 1972, in Gödel, 1990: 217–241.
  • Troelstra, A. S. and van Dalen, D., 1988, Constructivism in Mathematics: An Introduction, 2 volumes, Amsterdam: North-Holland Publishing.
  • Veldman, W., 1976, “An intuitionistic completeness theorem for intuitionistic predicate logic,” Journal of Symbolic Logic, 41: 159–166.
  • Veldman, W., 1990, “A survey of intuitionistic descriptive set theory,” in P. P. Petkov (ed.), Mathematical Logic, Proceedings of the Heyting Conference, New York and London: Plenum Press, 155–174.
  • Veldman, W., 2005, “Two simple sets that are not positively Borel,” Annals of Pure and Applied Logic, 135: 151–209.
  • Vesley, R. E., 1972, “Choice sequences and Markov's principle,” Compositio Mathematica, 24: 33–53.
  • Vesley, R. E., 1970, “A palatable alternative to Kripke's Schema,” in A. Kino et al. (eds.) 1970: 197ff.
  • Visser, A., 1999, “Rules and arithmetics,” Notre Dame Journal of Formal Logic, 40: 116–140.
  • Visser, A., 2002, “Substitutions of Σ01 sentences: explorations between intuitionistic propositional logic and intuitionistic arithmetic,” Annals of Pure and Applied Logic, 114: 227–271.
  • Visser, A., 2006, “Predicate logics of constructive arithmetical theories,” Journal of Symbolic Logic, 72: 1311–1326.

Other Internet Resources

Acknowledgments

Over the years, many readers have offered corrections and improvements. This revision owes special thanks to Edward Horton for observing that replacing ex falso quodlibet by the LEM in the axioms for IPC does not yield all of CPC, and for providing the correct substitutions. I am also indebted to Chen Huan, Willemien and Tim Kirschner for corrections, to Nikos Vaporis for his MPLA master's thesis on the admissible rules of intermediate logics, to Rosalie Iemhoff for recent developments in intuitionistic proof theory, and no doubt to others whose names I have forgotten.

Copyright © 2015 by
Joan Moschovakis <joan@math.ucla.edu>

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.
[an error occurred while processing the directive]