Intuitionistic logic encompasses the general principles of logicalreasoning which have been abstracted by logicians from intuitionisticmathematics, as developed byL. E. J. Brouwer beginning in his [1907] and [1908]. Because these principles alsohold for Russian recursive mathematics and the constructive analysisof E. Bishop and his followers, intuitionistic logic may be consideredthe logical basis ofconstructive mathematics. Although intuitionistic analysis conflicts with classical analysis,intuitionistic Heyting arithmetic is a subsystem of classical Peanoarithmetic. It follows that intuitionistic propositional logic is aproper subsystem of classical propositional logic, and pureintuitionistic predicate logic is a proper subsystem of pure classicalpredicate logic.

Philosophically,intuitionism differs fromlogicism by treating logic as a part of mathematics rather than as thefoundation of mathematics; from finitism by allowing constructive reasoning about potentially uncountablestructures (e.g., monotone bar induction on the tree of potentiallyinfinite sequences of natural numbers); and fromPlatonism by viewing mathematical objects as mental constructs with noindependent ideal existence. Hilbert’sformalist program, to justify classical mathematics by reducing it to a formal systemwhose consistency should be established by finitistic (henceconstructive) means, was the most powerful contemporary rival toBrouwer’s developing intuitionism. In his 1912 essayIntuitionism and Formalism Brouwer correctly predicted thatany attempt to prove the consistency of complete induction on thenatural numbers would lead to a vicious circle.

Brouwer rejectedformalismper se but admitted the potential usefulness of formulatinggeneral logical principles expressing intuitionistically correctconstructions, such asmodus ponens. Formal systems forintuitionistic propositional and predicate logic and arithmetic werefully developed by Heyting [1930], Gentzen [1935] and Kleene [1952].Gödel [1933] proved the equiconsistency of intuitionistic andclassical theories. Beth [1956] and Kripke [1965] provided semanticswith respect to which intuitionistic logic is correct and complete,although the completeness proofs for intuitionistic predicate logicrequire some classical reasoning.

• 1. Rejection ofTertium Non Datur
• 2. Intuitionistic First-Order Predicate Logic
  • 2.1 The formal systems \(\mathbf{H–IPC}\) and \(\mathbf{H–IQC}\)
  • 2.2 Alternative formalisms, and the deduction theorem
• 3. Intuitionistic Number Theory (Heyting Arithmetic) \(\mathbf{HA}\)
• 4. Basic Proof Theory
  • 4.1 Translating classical into intuitionistic logic
  • 4.2 Admissible rules of intuitionistic logic and arithmetic
• 5. Basic Semantics
  • 5.1 Kripke and Beth semantics for intuitionistic logic
  • 5.2 Realizability semantics for Heyting arithmetic
• 6. Additional Topics and Further Reading
  • 6.1 Subintuitionistic and Intermediate Logics
  • 6.2 Basic Intuitionistic Modal Logic
  • 6.3 Advanced topics
  • 6.4 Recommended reading
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. Rejection ofTertium Non Datur

Intuitionistic logic can be succinctly described as classical logicwithout the Aristotelian law of excluded middle:

or the classical law of double negation elimination:

but with the law of contradiction:

andex falso sequitur quodlibet:

Brouwer [1908] observed that LEM was abstracted from finitesituations, then extended without justification to statements aboutinfinite collections. For example, let \(x, y\) range over the naturalnumbers \(0, 1, 2, \ldots\) and let \(B(y)\) abbreviate\((\primepred(y) \oldand \primepred(y+2)),\) where \(\primepred(y)\)expresses “\(y\) is a prime number.” Then \(\forall y(B(y) \vee \neg B(y))\) holds intuitionistically as well asclassically, because in order to determine whether or not a naturalnumber is prime we need only check whether or not it has a divisorstrictly between itself and 1.

But if \(A(x)\) abbreviates \(\exists y(y\gt x \oldand B(y)),\) thenin order to assert \(\forall x (A(x) \vee \neg A(x))\)intuitionistically we would need aneffective (cf.the Church-Turing thesis) method to determine whether or not there is a pair of twin primeslarger than an arbitrary natural number \(x,\) and so far no suchmethod is known. An obvioussemi-effective method is to listthe prime number pairs using a refinement of Eratosthenes’ sieve(generating the natural numbers one by one and striking out everynumber \(y\) which fails to satisfy \(B(y)\)), and if there is a pairof twin primes larger than \(x\) this method will eventually find thefirst one. However, \(\forall x A(x)\) expresses the Twin PrimesConjecture, which has not yet been proved or disproved, so in thepresent state of our knowledge we can assert neither \(\forall x (A(x)\vee \neg A(x))\) nor \(\forall x A(x) \vee \neg \forall x A(x).\)

One may object that these examples depend on the fact that the TwinPrimes Conjecture has not yet been settled. A number ofBrouwer’s original “counterexamples” depended onproblems (such as Fermat’s Last Theorem) which have since beensolved. But to Brouwer the general LEM was equivalent to theapriori assumption thatevery mathematical problem has asolution—an assumption he rejected, anticipatingGö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 provesnegative statements, since \(\neg \neg A \rightarrow A\) doesnot hold in general. (If it did, LEM would follow bymodusponens from the intuitionistically provable \(\neg \neg(A \vee\neg A).\))
• Intuitionistic propositional logic does not have a finitetruth-table interpretation. There are infinitely many distinctaxiomatic systems between intuitionistic and classical logic.
• Not every propositional formula has an intuitionisticallyequivalent disjunctive or conjunctive normal form, built from primeformulas and their negations using only \(\vee\) and \(\oldand.\)
• Not every predicate formula has an intuitionistically equivalentprenex normal form, with all the quantifiers at the front.
• While \(\forall x \neg \neg(A(x) \vee \neg A(x))\) is a theorem ofintuitionistic predicate logic, \(\neg \neg \forall x(A(x) \vee \negA(x))\) is not; so \(\neg \forall x(A(x) \vee \neg A(x))\) isconsistent with intuitionistic predicate logic.

On the other hand:

• Every intuitionistic proof of a closed statement of the form \(A\vee B\) can be effectively transformed into an intuitionistic proofof \(A\) or an intuitionistic proof of \(B,\) and similarly for closedexistential statements.
• Intuitionistic propositional logic is effectively decidable, inthe sense that a finite constructive process applies uniformly toevery propositional formula, either producing an intuitionistic proofof the formula or demonstrating that no such proof can exist.
• The negative fragment of intuitionistic logic (without \(\vee\) or\(\exists\)) contains a faithful translation of classical logic, andsimilarly for intuitionistic and classical arithmetic.
• Intuitionistic arithmetic can consistently be extended by axiomswhich contradict classical arithmetic, enabling the formal study of recursive mathematics.
• Brouwer’s controversial intuitionistic analysis, which conflicts with LEM, can be formalized and shown consistentrelative to a classicallyand intuitionistically correctsubtheory.

2. Intuitionistic First-Order Predicate Logic

Formalized intuitionistic logic is naturally motivated by the informalBrouwer-Heyting-Kolmogorov explanation of intuitionistic truth,outlined in the entries onintuitionism in the philosophy of mathematics andthe development of intuitionistic logic. The constructive independence of the logical operations \(\oldand,\vee , \rightarrow , \neg , \forall , \exists\) contrasts with theclassical situation, where e.g., \(A \vee B\) is equivalent to\(\neg(\neg A \oldand \neg B),\) and \(\exists xA(x)\) is equivalentto \(\neg \forall x \neg A(x).\) From the B-H-K viewpoint, a sentenceof the form \(A \vee B\) asserts that either a proof of \(A,\) or aproof of \(B,\) has been constructed; while \(\neg(\neg A \oldand \negB)\) asserts that an algorithm has been constructed which wouldeffectively convert any pair of constructions proving \(\neg A\) and\(\neg B\) respectively, into a proof of a known contradiction.

2.1 The formal systems \(\mathbf{H–IPC}\) and \(\mathbf{H–IQC}\)

Following is a Hilbert-style formalism \(\mathbf{H–IQC}\) fromKleene [1952] (cf. Troelstra and van Dalen [1988]) for intuitionisticfirst-order predicate logic. The language \(L\) of\(\mathbf{H–IQC}\) has predicate letters \(P, Q(.), \ldots\) ofall arities and individual variables \(x, y, z, \ldots\) (with orwithout subscripts \(1, 2, \ldots\)), as well as symbols \(\oldand,\vee , \rightarrow , \neg , \forall , \exists\) for the logicalconnectives and quantifiers, and parentheses (, ). Theatomic(orprime)formulas of \(L\) are expressions such as\(P, Q(x), R(x, y, x)\) 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 anindividual variable symbol is a prime formula. The(well-formed)formulas of \(L\) are defined inductively as follows:

• Each atomic formula is aformula.
• If \(A\) and \(B\) areformulas, so are \((A \oldand B),(A \vee B), (A \rightarrow B)\) and \(\neg A.\)
• If \(A\) is aformula and \(x\) is a variable, then\(\forall xA\) and \(\exists xA\) areformulas.

In general, we use \(A, B, C\) as metavariables for well-formedformulas and \(x, y, z\) as metavariables for individual variables.Anticipating applications (for example to intuitionistic arithmetic)we use \(s, t\) as metavariables forterms; in the case ofpure predicate logic, terms are simply individual variables. Anoccurrence of a variable \(x\) in a formula \(A\) isbound ifit is within the scope of a quantifier \(\forall x\) or \(\exists x,\)otherwisefree. Intuitionistically as classically, \((A\leftrightarrow B)\) abbreviates \(((A \rightarrow B) \oldand (B\rightarrow A)),\) and parentheses will be omitted when this causes noconfusion.

There are three rules of inference:

Modus Ponens
From \(A\) and \(A \rightarrow B,\) conclude \(B.\)

\(\forall\)-Introduction
From \(C \rightarrow A(x),\) where \(x\) is a variable which does notoccur free in \(C,\) conclude \(C \rightarrow \forall x A(x).\)

\(\exists\)-Elimination
From \(A(x) \rightarrow C,\) where \(x\) is a variable which does notoccur free in \(C,\) conclude \(\exists x A(x) \rightarrow C.\)

The axioms are all formulas of the following forms, where in the lasttwo schemas the subformula \(A(t)\) is the result of substituting anoccurrence 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 aresult of the substitution.

Aproof is any finite sequence of formulas, each of which isan axiom or an immediate consequence, by a rule of inference, of (oneor two) preceding formulas of the sequence. Any proof is said toprove its last formula, which is called atheorem orprovable formula of first-order intuitionistic predicatelogic. Aderivation of a formula \(E\)from acollection \(F\) ofassumptions is any sequence of formulas,each of which belongs to \(F\) or is an axiom or an immediateconsequence, by a rule of inference, of preceding formulas of thesequence, such that \(E\) is the last formula of the sequence. If sucha derivation exists, we say \(E\) isderivable from \(F.\)

Intuitionistic propositional logic \(\mathbf{H–IPC}\) is thesubsystem of \(\mathbf{H–IQC}\) which results when the languageis restricted to formulas built from proposition letters \(P, Q,R,\ldots\) using the propositional connectives \(\oldand, \vee ,\rightarrow\) and \(\neg,\) and only the propositional postulates areused. Thus the last two rules of inference and the last two axiomschemas are absent from the propositional subsystem.

If, in the given list of axiom schemas for intuitionisticpropositional or first-order predicate logic, the law expressingex falso sequitur quodlibet:

is replaced by the classical law of double negation eliminationDNE:

(or, equivalently, if the intuitionistic law of negationintroduction:

is replaced by LEM), a formal system \(\mathbf{H–CPC}\) forclassical propositional logic or \(\mathbf{H–CQC}\) forclassical predicate logic results. Sinceex falso and the lawof contradiction are classical theorems, intuitionistic logic iscontained in classical logic. In a sense, classical logic is alsocontained in intuitionistic logic; see Section 4.1 below.

It is important to note that while LEM and DNE are equivalent asschemas over \(\mathbf{H–IPC},\) theimplication

is not a theorem schema of \(\mathbf{H–IPC}.\) For theories\(\mathbf{T}\) based on intuitionistic logic, if \(E\) is an arbitraryformula of \(L(\mathbf{T})\) then by definition:

\(E\) isdecidable in \(\mathbf{T}\) if and only if\(\mathbf{T}\) proves \(E \vee \neg E.\)

\(E\) isstable in \(\mathbf{T}\) if and only if\(\mathbf{T}\) proves \(\neg \neg E \rightarrow E.\)

\(E\) istestable in \(\mathbf{T}\) if and only if\(\mathbf{T}\) proves \(\neg E \vee \neg \neg E.\)

Decidability implies stability, but not conversely. The conjunction ofstability and testability is equivalent to decidability. Brouwerhimself proved that “absurdity of absurdity of absurdity isequivalent to absurdity” (Brouwer [1923C]), so every formula ofthe form \(\neg A\) is stable; but in \(\mathbf{H–IPC}\) and\(\mathbf{H–IQC}\) prime formulas and their negations areundecidable, as shown in Section 5.1 below.

2.2 Alternative formalisms, and the deduction theorem

The Hilbert-style system \(\mathbf{H–IQC}\) is useful formetamathematical investigations of intuitionistic logic, but itsforced linearization of deductions and its preference for axioms overrules make it an awkward instrument for establishing derivability. Anatural deduction system \(\mathbf{N–IQC}\) for intuitionisticpredicate logic results from the deductive system \(\mathbf{D},\)presented in Section 3 of the entry onclassical logic in this Encyclopedia, by omitting the symbol and rules for identity,and replacing the classical rule (DNE) of double negation eliminationby the intuitionistic negation elimination rule expressingexfalso:

(INE)

If \(F\) entails \(A\) and \(F\) entails \(\neg A,\) then \(F\)entails \(B.\)

The keys to proving that \(\mathbf{H–IQC}\) is equivalent to\(\mathbf{N–IQC}\) aremodus 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 (thatis, without using the second or third rule of inference on anyvariable \(x\) occurring free in \(A,\) unless the assumption \(A\)does not occur in the derivation before the inference in question),then \(A \rightarrow B\) is derivable from \(F.\)

This fundamental result, roughly expressing the rule \((\rightarrowI)\) of \(\mathbf{I},\) can be proved for \(\mathbf{H–IQC}\) byinduction on the definition of a derivation. The other rules of\(\mathbf{I}\) hold for \(\mathbf{H–IQC}\) essentially bymodus ponens, which corresponds to \((\rightarrow E)\) in\(\mathbf{N–IQC};\) and all the axioms of\(\mathbf{H–IQC}\) are provable in \(\mathbf{N–IQC}.\)

To illustrate the usefulness of the Deduction Theorem, consider the(apparently trivial) theorem schema \((A \rightarrow A).\) A correctproof in \(\mathbf{H–IPC}\) takes five lines:

1. \(A \rightarrow (A \rightarrow A)\)
2. \((A \rightarrow (A \rightarrow A)) \rightarrow ((A \rightarrow((A \rightarrow A) \rightarrow A)) \rightarrow (A \rightarrowA))\)
3. \((A \rightarrow ((A \rightarrow A) \rightarrow A)) \rightarrow(A\rightarrow A)\)
4. \(A \rightarrow((A \rightarrow A) \rightarrow A)\)
5. \(A \rightarrow A\)

where 1, 2 and 4 are axioms and 3, 5 come from earlier lines bymodus ponens. However, \(A\) is derivable from \(A\) (asassumption) in one obvious step, so the Deduction Theorem allows us toconclude that a proof of \(A \rightarrow A\) exists. (In fact, theformal proof of \(A \rightarrow A\) just presented is part of theconstructive proof of the Deduction Theorem!)

It is important to note that, in the definition of a derivation fromassumptions in \(\mathbf{H–IQC},\) the assumption formulas aretreated as if all their free variables were universally quantified, sothat \(\forall x A(x)\) is derivable from the hypothesis \(A(x).\)However, the variable \(x\) will bevaried (not heldconstant) in that derivation, by use of the rule of\(\forall\)-introduction; and so the Deduction Theorem cannot be usedto conclude (falsely) that \(A(x) \rightarrow \forall x A(x)\) (andhence, by \(\exists\)-elimination, \(\exists x A(x) \rightarrow\forall x A(x))\) are provable in \(\mathbf{H–IQC}.\) As anexample of a correct use of the Deduction Theorem for predicate logic,consider the implication \(\exists x A(x) \rightarrow \neg \forallx\neg A(x).\) To show this is provable in \(\mathbf{H–IQC},\) wefirst derive \(\neg \forall x\neg A(x)\) from \(A(x)\) with all freevariables held constant:

1. \(\forall x\neg A(x) \rightarrow \neg A(x)\)
2. \(A(x) \rightarrow (\forall x\neg A(x) \rightarrow A(x))\)
3. \(A(x)\) (assumption)
4. \(\forall x\neg A(x) \rightarrow A(x)\)
5. \((\forall x\neg A(x) \rightarrow A(x)) \rightarrow ((\forallx\neg A(x) \rightarrow \neg A(x)) \rightarrow \neg \forall x\negA(x))\)
6. \((\forall x\neg A(x) \rightarrow \neg A(x)) \rightarrow \neg\forall x\neg A(x)\)
7. \(\neg \forall x\neg A(x)\)

Here 1, 2 and 5 are axioms; 4 comes from 2 and 3 bymodusponens; and 6 and 7 come from earlier lines bymodusponens; so no variables have been varied. The Deduction Theoremtells us there is a proof \(P\) in \(\mathbf{H–IQC}\) of \(A(x)\rightarrow \neg \forall\)x\(\neg A(x),\) and one application of\(\exists\)-elimination converts \(P\) into a proof of\(\exists x A(x) \rightarrow \neg \forall x\neg A(x).\) The converseis not provable in \(\mathbf{H–IQC},\) as shown in Section 5.1below.

Other important alternatives to \(\mathbf{H–IQC}\) and\(\mathbf{N–IQC}\) are the various sequent calculi forintuitionistic propositional and predicate logic. The first suchcalculus was defined by Gentzen [1934–5], cf. Kleene [1952].Sequent systems, which prove exactly the same formulas as\(\mathbf{H–IQC}\) and \(\mathbf{N–IQC},\) keep trackexplicitly of all assumptions and conclusions at each step of a proof,replacingmodus ponens (which eliminates an intermediateformula) by acut rule (which can be shown to be anadmissible rule (cf. Section 4.2) for the subsystem remaining when itis omitted).

When the details of the formalism are not important, from now on wefollow Troelstra and van Dalen [1988] in letting“\(\mathbf{IQC}\)” or “\(\mathbf{IPC}\)” referto any formal system for intuitionistic predicate or propositionallogic respectively, and similarly “\(\mathbf{CQC}\)” and“\(\mathbf{CPC}\)” for classical predicate andpropositional logic.

Both \(\mathbf{IPC}\) and \(\mathbf{IQC}\) satisfyinterpolationtheorems, e.g.: If \(A\) and \(B\) are propositional formulashaving at least one proposition letter in common, and if \(A\rightarrow B\) is provable in \(\mathbf{IPC},\) then there is aformula \(C,\) containing only proposition letters which occur in both\(A\) and \(B,\) such that both \(A \rightarrow C\) and \(C\rightarrow B\) are provable. These topics are treated in Kleene[1952] and Troelstra and Schwichtenberg [2000].

While identity can of course be added to intuitionistic logic, forapplications (e.g., to arithmetic) the equality symbol is generallytreated as a distinguished predicate constant satisfying the axiomsfor an equivalence relation (reflexivity, symmetry and transitivity)and additional nonlogical axioms (e.g., the primitive recursivedefinitions of addition and multiplication). Identity is decidable,intuitionistically as well as classically, but intuitionisticextensional equality is not always decidable; see the discussion ofBrouwer’s continuity axioms in Section 3 of the entry onintuitionism in the philosophy of mathematics.

3. Intuitionistic Number Theory (Heyting Arithmetic) \(\mathbf{HA}\)

Intuitionistic (Heyting) arithmetic \(\mathbf{HA}\) and classical(Peano) arithmetic \(\mathbf{PA}\) share the same first-order languageand the same non-logical axioms; only the logic is different. Inaddition to the logical connectives, quantifiers and parentheses andthe individual variables \(x, y, z,\ldots\) (also used asmetavariables), the language \(L(\mathbf{HA})\) of arithmetic has abinary predicate symbol \(=,\) individual constant \(0,\) unaryfunction constant \(S,\) and finitely or countably infinitely manyadditional constants for primitive recursive functions includingaddition and multiplication; the precise choice is a matter of tasteand convenience.Terms are built from variables and \(0\)using the function constants; in particular, each natural number \(n\)is expressed in the language by thenumeral \(\mathbf{n}\)obtained by applying \(S\) \(n\) times to \(0\) (e.g., \(S(S(0))\) isthe numeral for \(2\)).Prime formulas are of the form \((s =t)\) where \(s, t\) are terms, andcompound formulas areobtained from these as usual.

The logical axioms and rules of \(\mathbf{HA}\) are those offirst-order intuitionistic predicate logic \(\mathbf{IQC}.\) Thenonlogical axioms include the reflexive, symmetric and transitiveproperties of \(=\): \[\forall x (x = x),\] \[\forall x \forall y (x = y \rightarrow y = x),\] \[\forall x \forall y \forall z ((x = y \oldand y = z) \rightarrow x = z);\] the axiomcharacterizing \(0\) as the least natural number:

the axiom characterizing \(S\) as a one-to-one function:

the extensional equality axiom for \(S\):

the primitive recursive defining equations for each function constant,in particular for addition: \[\forall x (x + 0 = x),\] \[\forall x \forall y (x + S(y) = S(x + y));\] andmultiplication: \[\forall x (x \cdot 0 = 0),\] \[\forall x \forall y (x \cdot S(y) = (x \cdot y) + x);\] and the (universal closureof the) schema of mathematical induction, for arbitrary formulas\(A(x)\):

Extensional equality axioms for all function constants are derivableby mathematical induction from the equality axiom for \(S\) and theprimitive recursive function axioms.

The natural order relation \(x \lt y\) can be defined in\(\mathbf{HA}\) by \(\exists z(S(z) + x = y),\) or by thequantifier-free formula \(S(x) \dotminus y = 0\) if the symbol andprimitive recursive defining equations for predecessor : \[Pd(0) = 0,\]\[\forall x (Pd(S(x)) = x)\] and cutoff subtraction : \[\forall x (x \dotminus 0 = x),\]\[\forall x \forall y (x \dotminus S(y) = Pd(x \dotminus y))\] arepresent in the formalism. \(\mathbf{HA}\) proves the comparativelaw

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

The hypothesis is needed because not all arithmetical formulas aredecidable in \(\mathbf{HA}.\) However, \(\forall x\forall y(x = y \vee\neg(x = y))\) can be proved directly by mathematical induction, andso:

• Prime formulas (and hence allquantifier-free formulas)are decidable and stable in \(\mathbf{HA}.\)

If \(A(x)\) is decidable in \(\mathbf{HA},\) then by induction on\(x\) so are \(\forall y (y \lt x \rightarrow A(y))\) and \(\exists y(y \lt x \oldand A(y)).\) Hence:

• Formulas in which all quantifiers arebounded aredecidable and stable in \(\mathbf{HA}.\)

The collection \(\Delta_0\) of arithmetical formulas in which allquantifiers are bounded is the lowest level of a classicalarithmetical hierarchy based on the pattern of alternations ofquantifiers in a prenex formula. In \(\mathbf{HA}\) not every formulahas a prenex form, but Burr [2004] discovered a simple intuitionisticarithmetical hierarchy corresponding level by level to the classical.For the purposes of the next two definitions only, \(\forall x\)denotes a block of finitely many universal number quantifiers, andsimilarly \(\exists x\) denotes a block of finitely many existentialnumber quantifiers. With these conventions, Burr’s classes\(\Phi_n\) and \(\Psi_n\) are defined by:

• \(\Phi_0 = \Psi_0 = \Delta_0,\)
• \(\Phi_1\) is the class of all formulas of the form \(\forall xA(x)\) where \(A(x)\) is in \(\Psi_0.\) For \(n \ge 2,\) \(\Phi_n\) isthe class of all formulas of the form \(\forall x [A(x) \rightarrow\exists y B(x,y)]\) where \(A(x)\) is in \(\Phi_{n-1}\) and \(B(x,y)\)is in \(\Phi_{n-2},\)
• \(\Psi_1\) is the class of all formulas of the form \(\exists xA(x)\) where \(A(x)\) is in \(\Phi_0.\) For \(n \ge 2,\) \(\Psi_n\) isthe class of all formulas of the form \(A \rightarrow B\) where \(A\)is in \(\Phi_n\) and \(B\) is in \(\Phi_{n-1}.\)

The corresponding classical prenex classes are defined more simply:

• \(\Pi_0 = \Sigma_0 = \Delta_0,\)
• \(\Pi_{n +1}\) is the class of all formulas of the form \(\forallx A(x)\) where \(A(x)\) is in \(\Sigma_n,\)
• \(\Sigma_{n +1}\) is the class of all formulas of the form\(\exists x A(x)\) where \(A(x)\) is in \(\Pi_n.\)

Peano arithmetic \(\mathbf{PA}\) comes from Heyting arithmetic\(\mathbf{HA}\) by adding LEM or \(\neg \neg A \rightarrow A\) to thelist of logical axioms, i.e., by using classical instead ofintuitionistic logic. The following results hold even in the fragmentsof \(\mathbf{HA}\) and \(\mathbf{PA}\) with the induction schemarestricted to \(\Delta_0\) formulas.

Burr’s Theorem:

• Every arithmetical formula is provably equivalent in\(\mathbf{HA}\) to a formula in one of the classes \(\Phi_n.\)
• Every formula in \(\Phi_n\) is provably equivalent in\(\mathbf{PA}\) to a formula in \(\Pi_n,\) and conversely.
• Every formula in \(\Psi_n\) is provably equivalent in\(\mathbf{PA}\) to a formula in \(\Sigma_n,\) and conversely.

\(\mathbf{HA}\) and \(\mathbf{PA}\) are proof-theoreticallyequivalent, as will be shown in Section 4. Each is capable of(numeralwise) expressing its own proof predicate. ByGödel’s famous Incompleteness Theorem, if \(\mathbf{HA}\)is consistent then neither \(\mathbf{HA}\) nor \(\mathbf{PA}\) canprove 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 sameconsistency strength as classical logic. For propositional logic thiswas first proved by Glivenko [1929]:

Glivenko’s Theorem
An arbitrary propositional formula \(A\) is classically provable, ifand only if \(\neg \neg A\) is intuitionistically provable.

Glivenko’s Theorem does not extend to predicate logic, althoughan arbitrary predicate formula \(A\) is classically provable if andonly if \(\neg \neg A\) is provable in intuitionistic predicate logicplus the “double negation shift” schema.

The more sophisticatednegative translation ofclassical into intuitionistic theories, due independently toGödel and Gentzen, associates with each formula \(A\) of thelanguage \(L\) another formula \(g(A)\) (with no \(\vee\) or\(\exists),\) such that:

1. Classical predicate logic proves \(A \leftrightarrow g(A).\)
2. Intuitionistic predicate logic proves \(g(A) \leftrightarrow \neg\neg g(A).\)
3. If classical predicate logic proves \(A,\) then intuitionisticpredicate logic proves \(g(A).\)

The proofs are straightforward from the following inductive definitionof \(g(A)\) (using Gentzen’s direct translation of implication,rather than Gödel’s in terms of \(\neg\) and\(\oldand\)):

For each formula \(A,\) \(g(A)\) is provable intuitionistically if andonly if \(A\) is provable classically. In particular, if \(B \oldand\neg B\) were classically provable for some formula \(B,\) then \(g(B)\oldand \neg g(B)\) (which is \(g(B \oldand \neg B))\) would in turnbe provable intuitionistically. Hence:

4. Classical and intuitionistic predicate logic are equiconsistent.

The negative translation of classical into intuitionistic numbertheory is even simpler, since prime formulas of intuitionisticarithmetic are stable. Thus \(g(s=t)\) can be taken to be \(s=t,\) andthe other clauses are unchanged. The negative translation of eachinstance of the schema of mathematical induction is an instance of thesame schema, and the other nonlogical axioms of arithmetic are theirown negative translations, so:

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

Gödel [1933e] interpreted these results as showing thatintuitionistic logic and arithmetic arericher than classicallogic and arithmetic, because the intuitionistic theory distinguishesformulas which are classically equivalent, and has the sameconsistency strength as the classical theory. In particular, Gödel’sincompleteness theorems apply to \(\mathbf{HA}\) as well as to\(\mathbf{PA}.\)

Direct attempts to extend the negative interpretation to analysis failbecause the negative translation of the countable axiom of choice isnot a theorem of intuitionistic analysis. However, it is consistentwith intuitionistic analysis, including Brouwer’s controversialcontinuity principle, by the functional version of Kleene’srecursive realizability (cf. Section 6.3 below). It follows thatintuitionistic mathematics, which can only be expressed by using allthe standard logical connectives and quantifiers, is consistent with afaithful translation of classical mathematics avoiding \(\vee\) and\(\exists.\)

This is important because Brouwer’s intuitionistic analysis isinconsistent with LEM. However, if \(A\) is anynegativeformula (without \(\vee\) or \(\exists\)) then \(\neg \neg A\rightarrow A\) is provable using intuitionistic logic. Areconciliation of intuitionistic and classical analysis along theselines, inspired by Troelstra [1977] and Kripke[2019], is suggested inMoschovakis [2017].

4.2 Admissible rules of intuitionistic logic and arithmetic

Gödel [1932] observed that intuitionistic propositional logic hasthedisjunction property:

(DP)

If \(A \vee B\) is a theorem, then \(A\) is a theorem or \(B\) isa theorem.

Gentzen [1935] established the disjunction property for closedformulas of intuitionistic predicate logic. From this it follows thatif intuitionistic logic is consistent, then \(P \vee \neg P\) is not atheorem if \(P\) is an atomic formula. Kleene [1945, 1952] proved thatintuitionistic first-order number theory also has the related (cf.Friedman [1975])existence property:

(EP)

If \(\exists x A(x)\) is a closed theorem, then for some closedterm \(t,\) \(A(t)\) is a theorem.

The disjunction and existence properties are special cases of ageneral phenomenon peculiar to nonclassical theories. Theadmissible rules of a theory are the rules under which thetheory is closed. For example, Harrop [1960] observed that therule:

• If \(\neg A \rightarrow (B \vee C)\) is a theorem, so is \((\neg A\rightarrow B) \vee(\neg A \rightarrow C)\)

is admissible for intuitionistic propositional logic \(\mathbf{IPC}\)because if \(A,\) \(B\) and \(C\) are any formulas such that \(\neg A\rightarrow(B \vee C)\) is provable in \(\mathbf{IPC},\) then \((\negA \rightarrow B) \vee (\neg A \rightarrow C)\) is provable in\(\mathbf{IPC}.\) Harrop’s rule is notderivable in\(\mathbf{IPC}\) because the formula

is not intuitionistically provable. Another important example of anadmissible nonderivable rule of \(\mathbf{IPC}\) is Mints’srule:

• If \((A \rightarrow B) \rightarrow (A \vee C)\) is a theorem, sois \(((A \rightarrow B) \rightarrow A) \vee ((A \rightarrow B)\rightarrow C).\)

The two-valued truth table interpretation of classical propositionallogic \(\mathbf{CPC}\) gives rise to a simple proof that everyadmissible rule of \(\mathbf{CPC}\) is derivable: otherwise, someassignment to \(A,\) \(B,\) etc. would make the hypothesis true andthe conclusion false, and by substituting e.g. \(P \rightarrow P\) forthe letters assigned “true” and \(P \oldand \neg P\) forthose assigned “false” one would have a provablehypothesis and unprovable conclusion. The fact that the intuitionisticsituation is more interesting leads to many natural questions, some ofwhich have recently been answered.

By generalizing Mints’s Rule, Visser and de Jongh identified arecursively enumerable sequence of successively stronger admissiblerules (“Visser’s rules”) which, they conjectured,formed abasis for the admissible rules of \(\mathbf{IPC}\)in the sense that every admissible rule is derivable from thedisjunction property and one of the rules of the sequence. Building onwork of Ghilardi [1999], Iemhoff [2001] succeeded in proving theirconjecture. Rybakov [1997] proved that the collection of alladmissible rules of \(\mathbf{IPC}\) is decidable but has no finitebasis. Visser [2002] showed that his rules are also the admissiblepropositional rules of \(\mathbf{HA},\) and of \(\mathbf{HA}\)extended by Markov’s Principle MP (defined in Section 5.2below). More recently, Jerabek [2008] found an independent basis forthe admissible rules of \(\mathbf{IPC},\) with the property that norule in the basis derives another.

Much less is known about the admissible rules of intuitionisticpredicate logic. Pure \(\mathbf{IQC},\) without individual orpredicate constants, has the following remarkable admissible rule for\(A(x)\) with no variables free but \(x\):

• If \(\exists x A(x)\) is a theorem, so is \(\forall x A(x).\)

Not every admissible predicate rule of \(\mathbf{IQC}\) is admissiblefor all formal systems based on \(\mathbf{IQC};\) for example,\(\mathbf{HA}\) evidently violates the rule just stated. Visser provedin [1999] that the property of being an admissible predicate rule of\(\mathbf{HA}\) is \(\Pi_2\) complete, and in [2002] that\(\mathbf{HA}\) \(+\) MP has the same predicate admissible rules as\(\mathbf{HA}.\) Plisko [1992] proved that thepredicatelogic of \(\mathbf{HA}\) \(+\) MP (the set of sentences in thelanguage of \(\mathbf{IQC}\) all of whose uniform substitutioninstances in the language of arithmetic are provable in\(\mathbf{HA}\) \(+\) MP) is \(\Pi_2\) complete; Visser [2006]extended this result to some constructively interesting consistentextensions of \(\mathbf{HA}\) which are not contained in\(\mathbf{PA}.\)

While they have not been completely classified, the admissible rulesof intuitionistic predicate logic are known to includeMarkov’s Rule for decidable predicates:

• If \(\forall x(A(x) \vee \neg A(x)) \oldand \neg \forall x\negA(x)\) is a theorem, so is \(\exists x A(x).\)

And the followingIndependence-of-Premise Rule (where\(y\) is assumed not to occur free in \(A(x))\):

• If \(\forall x(A(x) \vee \neg A(x)) \oldand (\forall x A(x)\rightarrow \exists y B(y))\) is a theorem, so is \(\exists y (\forallx A(x) \rightarrow B(y)).\)

Both rules are also admissible for \(\mathbf{HA}.\) The correspondingimplications (MP and IP respectively), which are not provableintuitionistically, are verified by Gödel’s“Dialectica” interpretation of \(\mathbf{HA}\) (cf.Section 6.3 below). So is the implication (CT) corresponding to one ofthe most interesting admissible rules of Heyting arithmetic, let uscall it theChurch-Kleene Rule:

• If \(\forall x \exists y A(x, y)\) is a closed theorem of\(\mathbf{HA}\) then there is a number \(n\) such that, provably in\(\mathbf{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(\mathbf{x},\mathbf{y})\) is provable, where\(\mathbf{x}\) is the numeral for the natural number \(x\) and\(\mathbf{y}\) is the numeral for \(y).\)

Combining Markov’s Rule with the negative translation gives theresult that classical and intuitionistic arithmetic prove the sameformulas of the form \(\forall x \exists y A(x, y)\) where \(A(x, y)\)is quantifier-free. In general, if \(A(x, y)\) is provably decidablein \(\mathbf{HA}\) and if \(\forall x \exists y A(x, y)\) is a closedtheorem ofclassical arithmetic \(\mathbf{PA},\) theconclusion of the Church-Kleene Rule holds even inintuitionistic arithmetic. For if \(\mathbf{HA}\) proves\(\forall x \forall y (A(x,y) \vee \neg A(x,y))\) then by theChurch-Kleene Rule the characteristic function of \(A(x,y)\) has aGödel number \(m,\) provably in \(\mathbf{HA};\) so\(\mathbf{HA}\) proves \(\forall x \exists y A(x,y) \leftrightarrow\forall x \exists y \exists z B(\mathbf{m},x,y,z)\) where \(B\) isquantifier-free, and the adjacent existential quantifiers can becontracted in \(\mathbf{HA}.\) It follows that \(\mathbf{HA}\) and\(\mathbf{PA}\) have the same provably recursive functions.

Here is a proof that the rule “If \(\forall x (A \vee B(x))\) isa theorem, so is \(A \vee \forall x B(x)\)” (where \(x\) is notfree in \(A)\) isnot admissible for \(\mathbf{HA},\) if\(\mathbf{HA}\) is consistent. Gödel numbering provides aquantifier-free formula \(G(x)\) which (numeralwise) expresses thepredicate “\(x\) is the code of a proof in \(\mathbf{HA}\) of\((0 = 1).\)” By intuitionistic logic with the decidability ofquantifier-free arithmetical formulas, \(\mathbf{HA}\) proves\(\forall x(\exists y G(y) \vee \neg G(x)).\) However, if\(\mathbf{HA}\) proved \(\exists yG(y) \vee \forall x\neg G(x)\) thenby the disjunction property, \(\mathbf{HA}\) must prove either\(\exists yG(y)\) or \(\forall x\neg G(x).\) The first case isimpossible, by the existence property with the consistency assumptionand the fact that \(\mathbf{HA}\) proves all true quantifier-freesentences. But the second case is also impossible, byGödel’s second incompleteness theorem, since \(\forallx\neg G(x)\) expresses the consistency of \(\mathbf{HA}.\)

5. Basic Semantics

The most direct way to show that a formula (or schema) \(F\) isprovable in a formal system \(\mathbf{S}\) is to construct aproof of \(F\) in \(\mathbf{S}.\) But if a formula (or somesubstitution instance of a schema) happensnot to be provablein \(\mathbf{S},\) how can that fact be known? Our failure to find aproof may suggest unprovability, but is not in general decisive unlessthe proof search is a canonical one in Gentzen’s system forintuitionistic propositional logic. Usually what is needed is aninterpretation with respect to which \(\mathbf{S}\) issound, in the sense that every provable formula isvalid under the interpretation. Then to show \(F\)unprovable in \(\mathbf{S}\) it suffices to show that \(F\)isinvalid under the interpretation, typically byconstructing acountermodel to \(F.\)

If a system \(\mathbf{S}\) iscomplete for an interpretation,in the sense that every formula which is valid under theinterpretation is provable in \(\mathbf{S},\) then an indirect way toshow that a formula (or schema) is provable in \(\mathbf{S}\) is toestablish its validity under the interpretation. Completeness does notalways accompany soundness; for instance, Heyting arithmetic is soundbut incomplete for the realizability interpretation described inSection 5.2 below.

Intuitionistic systems have inspired a variety of interpretations,including Beth’s tableaux, Rasiowa and Sikorski’stopological models, Heyting algebras, formulas-as-types,Kleene’s recursive realizabilities, the Kleene and Aczelslashes, and models based on sheafs and topoi. Of all theseinterpretations Kripke’s [1965] possible-world semantics, withrespect to which intuitionistic predicate logic is sound and complete,most resembles classical model theory. Recursive realizabilityinterpretations, on the other hand, attempt to effectively implementthe B-H-K explanation of intuitionistic truth.

5.1 Kripke and Beth semantics for intuitionistic logic

AKripke structure \(\mathbf{K}\) for \(L\) consists of apartially ordered set \(K\) ofnodes and adomainfunction D assigning to each node \(k\) in \(K\) an inhabited set\(D(k),\) such that if \(k \le k',\) then \(D(k) \subseteq D(k').\) Inaddition \(\mathbf{K}\) has aforcing relation determined asfollows.

For each node \(k\) let \(L(k)\) be the language extending \(L\) bynew constants for all the elements of \(D(k).\) To each node \(k\) andeach \(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 \le k'\) and\(f(P, k) =\)true then \(f(P, k') =\)true also.Say that:

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

To each node \(k\) and each \((n+1)\)-ary predicate letter\(Q(\ldots),\) assign a (possibly empty) set \(T(Q, k)\) of\((n+1)\)-tuples of elements of \(D(k)\) in such a way that if \(k \lek'\) then \(T(Q, k) \subseteq T(Q, k').\) Say that:

\(k\) \(\Vdash\) \(Q(d_0 ,\ldots, d_n)\) if and only if \((d_0 ,\ldots,d_n) \in T(Q, k).\)

Now define \(k\) \(\Vdash\) \(E\) (which may be read“ \(k\)forces \(E\) ”) forcompound sentences \(E\) of \(L(k)\) inductively as follows:

Any such forcing relation isconsistent:

For no sentence \(A\) and no \(k\) is it the case that both \(k\)\(\Vdash\) \(A\) and \(k\) \(\Vdash\) \(\neg A.\)

andmonotone:

If \(k \le k'\) and \(k\) \(\Vdash\) \(A\) then \(k'\) \(\Vdash\)\(A.\)

Kripke’s Soundness and Completeness Theoremsestablish that a sentence of \(L\) is provable in intuitionisticpredicate logic if and only if it is forced by every node of everyKripke structure. Thus to show that \(\neg \forall x \neg P(x)\rightarrow \exists x P(x)\) is intuitionistically unprovable, it isenough to consider a Kripke structure with \(K = \{k, k'\},\) \(k \ltk',\) \(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 consistencyand monotonicity properties of arbitrary Kripke models, with thedefinition of \(\Vdash.\)

Kripke models for languages with equality may interpret \(=\) at eachnode 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 particularly simple, since anarbitrary propositional formula is intuitionistically provable if andonly if it is forced by the root of every Kripke model whoseframe (the set \(K\) of nodes together with their partialordering) is a finite tree with a least element (theroot).For example, the Kripke model with \(K = \{k, k', k''\}, k \lt k'\)and \(k \lt k'',\) and with \(P\) true only at \(k',\) shows that both\(P \vee \neg P\) and \(\neg P \vee \neg \neg P\) are unprovable in\(\mathbf{IPC}.\)

Each terminal node orleaf of a Kripke model is a classicalmodel, because a leaf forces every formula or its negation. Only thoseproposition letters which occur in a formula \(E,\) and only thosenodes \(k'\) such that \(k\le k',\) are relevant to deciding whetheror not \(k\) forces \(E.\) Such considerations allow us to associateeffectively with each formula \(E\) of \(L(\mathbf{IPC})\) a finiteclass of finite Kripke structures which will include a countermodel to\(E\) if one exists. Since the class of all theorems of\(\mathbf{IPC}\) is recursively enumerable, we conclude that:

\(\mathbf{IPC}\) is effectively decidable. There is a recursiveprocedure which determines, for each propositional formula \(E,\)whether or not \(E\) is a theorem of \(\mathbf{IPC},\) concluding witheither a proof of \(E\) or a (finite) Kripke countermodel.

The decidability of \(\mathbf{IPC}\) was first obtained by Gentzen in1935. The undecidability of \(\mathbf{IQC}\) follows from theundecidability of \(\mathbf{CQC}\) by the negative interpretation.

Familiar non-intuitionistic logical schemata correspond to structuralproperties of Kripke models, for example:

• DNS holds in every Kripke model with finite frame.
• \((A \rightarrow B) \vee (B \rightarrow A)\) holds in every Kripkemodel with linearly ordered frame. Conversely, every propositionalformula which is not derivable in \(\mathbf{IPC} + (A \rightarrow B)\vee (B \rightarrow A)\) has a Kripke countermodel with linearlyordered frame (cf. Section 6.1 below).
• If \(x\) is not free in \(A\) then \(\forall x (A \vee B(x))\rightarrow (A \vee \forall x B(x))\) holds in every Kripke model\(\mathbf{K}\) with constant domain (so that \(D(k) = D(k')\) for all\(k, k'\) in \(K).\) The same is true for MP.

Beth’s semantic tableaux, inspired byBrouwer’s notion ofspread, predated Kripke’ssemantics;Troelstra and van Ulsen give an authoritative account of the history. For a modern version ofBeth semantics which facilitates comparison with Kripke semantics, aBeth structure is a Kripke structure in which the partiallyordered set \(K\) is a rooted tree with \(k_0\) as the root, and theforcing conditions in aBeth model are the same as those in aKripke model with two exceptions. The forcing conditions for \((A \veeB)\) and \(\exists x A(x)\) in a Beth model are as follows, where abranch of \(K\) is a maximal linearly ordered subset \(k_0\le k_1 \le k_2 \le ...\) of \(K.\)

To use a temporal analogy, a Beth model allows a decision between twoalternatives, or the production of a witness to an existentialstatement, to be postponed until more information and possibly moreindividuals are available. A Kripke model demands an immediatedecision between two alternatives, or the immediate choice of awitness to an existential statement from the current domain ofindividuals.

Kripke models and Beth models are powerful tools for establishingproperties of intuitionistic formal systems; cf. Troelstra and vanDalen [1988], Smorynski [1973], de Jongh and Smorynski [1976],Ghilardi [1999] and Iemhoff [2001], [2005]. However, there is nopurely intuitionistic proof that every sentence which is valid in allKripke and Beth models is provable in \(\mathbf{IQC}.\) Following anobservation by Gödel, Kreisel [1958] verified that thecompleteness of intuitionistic predicate logic for Beth semantics isequivalent to Markov’s Principle MP, which Brouwer rejected.

Moreover, Dyson and Kreisel [1961] showed that if \(\mathbf{IQC}\) isweakly complete for Beth semantics (that is, if no unprovablesentence holds in every Beth model) then the following consequence ofMP holds : \[ \tag{GDK} \forall \alpha_{B(\alpha)} \neg \neg \exists x R(\alpha,x) \rightarrow \neg \neg \forall \alpha_{B(\alpha)} \exists xR(\alpha, x),\] where \(x\) ranges over all natural numbers,\(\alpha\) ranges over all infinite sequences of natural numbers,\(B(\alpha)\) abbreviates \(\forall x (\alpha(x) \leq 1),\) and \(R\)expresses a primitive recursive relation of \(\alpha\) and \(x.\)Conversely, GDK entails the weak completeness of \(\mathbf{IQC}.\)This interesting principle, considered as a schema with \(R\) requiredto be quantifier-free, would justify the negative interpretation of aform of Brouwer’s Fan Theorem. It is weaker than MP butunprovable in current systems of intuitionistic analysis. Kreisel[1962] suggested that GDK may eventually be provable on the basis ofas yet undiscovered properties of intuitionistic mathematics.

By modifying the definition of a Kripke model to allow“exploding nodes” which force every sentence, Veldman[1976] and de Swart [1976] independently found completeness proofsusing only intuitionistic logic. However, Veldman questioned whetherKripke models with exploding nodes were intuitionistically meaningfulmathematical objects.

5.2 Realizability semantics for Heyting arithmetic

One way to implement the B-H-K explanation of intuitionistic truth forarithmetic is to associate with each sentence \(E\) of \(\mathbf{HA}\)some collection of numerical codes for algorithms which couldestablish the constructive truth of \(E.\) Following Kleene [1945], anumber \(e\)realizes a sentence \(E\) of the language ofarithmetic by induction on the logical form of \(E\):

An arbitrary formula is realizable if some number realizes itsuniversal closure. Observe that not both \(A\) and \(\neg A\) arerealizable, for any formula \(A.\) The fundamental result is:

Nelson’s Theorem [1947]
If \(A\) is derivable in \(\mathbf{HA}\) from realizable formulas\(F,\) then \(A\) is realizable.

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

(MP)

\(\forall x (A(x) \vee \neg A(x)) \oldand \neg \forall x \neg A(x)\rightarrow \exists x A(x).\)

Although unprovable in \(\mathbf{HA},\) MP is realizable by anargument which uses Markov’s Principle informally. Butrealizability is a fundamentally nonclassical interpretation. In\(\mathbf{HA}\) it is possible to express an axiom of recursive choiceCT (for “Church’s Thesis”), which contradicts LEMbut is (constructively) realizable. Hence by Nelson’s Theorem,\(\mathbf{HA}\) \(+\) MP \(+\) CT is consistent.

Kleene used a variant of number-realizability to prove \(\mathbf{HA}\)satisfies the Church-Kleene Rule; the same argument works for\(\mathbf{HA}\) with MP or CT, and for \(\mathbf{HA}\) \(+\) MP \(+\)CT. In Kleene and Vesley [1965] and Kleene [1969], functions replacenumbers as realizing objects, establishing the consistency offormalized intuitionistic analysis and its closure under asecond-order version of the Church-Kleene Rule.

Nelson’s Theorem establishes the unprovability in\(\mathbf{IQC}\) of some theorems of classical predicate logic. If, toeach \(n\)-place predicate letter \(P(\ldots ),\) a formula \(f(P)\)of \(L(\mathbf{HA})\) with \(n\) free variables is assigned, and ifthe formula \(f(A)\) of \(L(\mathbf{HA})\) comes from the formula\(A\) of \(L\) by replacing each prime formula \(P(x_1, \ldots, x_n)\)by \(f(P)(x_1 ,\ldots ,x_n),\) then \(f(A)\) is called anarithmetical substitution instance of \(A.\) As an example,if a formula of \(L(\mathbf{HA})\) expressing “\(y\) is the codeof a sentence and \(x\) codes a proof in \(\mathbf{HA}\) of thesentence with code \(y\)” is assigned to \(P(x,y),\) then(assuming \(\mathbf{HA}\) is consistent) the resulting arithmeticalsubstitution instance of \(\forall y (\exists x P(x, y) \vee \neg\exists x P(x, y))\) is unrealizable and hence unprovable in\(\mathbf{HA},\) and so is its double negation. It follows that \(\neg\neg \forall y (\exists x P(x, y) \vee \neg \exists x P(x, y))\) isnot provable in \(\mathbf{IQC}.\)

De Jongh [1970] combined realizability with Kripke modeling to showthat intuitionistic propositional logic \(\mathbf{IPC}\) and afragment of \(\mathbf{IQC}\) arearithmetically complete for\(\mathbf{HA}.\) A uniform assignment of simple existential formulasto predicate letters suffices to prove:

De Jongh’s Theorem (for IPC) [1970]
If a propositional formula \(A\) of the language \(L\) is not provablein \(\mathbf{IPC},\) then some arithmetical substitution instance of\(A\) is not provable in \(\mathbf{HA}.\)

The proof of this version of de Jongh’s Theorem does not needrealizability; cf. Smorynski [1973]. As an example, Rosser’sform of Gödel’s Incompleteness Theorem provides a sentence\(C\) of \(L(\mathbf{HA})\) such that \(\mathbf{PA}\) proves neither\(C\) nor \(\neg C,\) so by the disjunction property \(\mathbf{HA}\)cannot prove \((C \vee \neg C).\) But de Jongh’s semanticalproof also established that every intuitionistically unprovablepredicate formula of a restricted kind has an arithmeticalsubstitution instance which is unprovable in \(\mathbf{HA}.\) Using asyntactic method, Daniel Leivant [1979] extended de Jongh’sTheorem to all intuitionistically unprovable predicate formulas,proving that \(\mathbf{IQC}\) is arithmetically complete for\(\bf{HA}.\) See van Oosten [1991] for a historical exposition and asimpler proof of the full theorem, using abstract realizability withBeth models instead of Kripke models.

Without claiming that number-realizability coincides withintuitionistic arithmetical truth, Nelson observed that for eachformula \(A\) of \(L(\mathbf{HA})\) the predicate “\(y\)realizes \(A\)” can be expressed in \(\mathbf{HA}\) by anotherformula (abbreviated “\(y \realizesrel A\)”), and theschema \(A \leftrightarrow \exists y (y \realizesrel A)\) isconsistent with \(\mathbf{HA}.\) Troelstra [1973] showed that \((A\leftrightarrow \exists y (y \realizesrel A))\) isequivalentover \(\mathbf{HA}\) to “extended Church’s Thesis”ECT, a stronger version of CT enabling recursive choice underassumptions which are “almost negative” (containing no\(\vee,\) and with \(\exists x\) only applied to prime formulas).While \(\mathbf{HA}\) is sound but not complete for Kleene’snumber-realizability, the next theorem shows that \(\mathbf{HA}\) +ECT is both sound and complete for this interpretation.

Troelstra’s Characterization Theorem (fornumber-realizability over \(\mathbf{HA}\)) [1973]
If \(A\) is a closed formula of the language \(L(\mathbf{HA}),\) then:

1. \(\mathbf{HA}\) + ECT \(\vdash\) \((A \leftrightarrow \exists y (y\realizesrel A)).\)
2. \(\mathbf{HA}\) + ECT \(\vdash\) \(A\) if and only if\(\mathbf{HA}\) \(\vdash\) \(\exists y (y \realizesrel A).\)

In \(\mathbf{HA}\) \(+\) MP \(+\) ECT, which Troelstra considers to bea formalization of Russian recursive mathematics (cf. section 3.2 ofthe entry onconstructive mathematics), every formula of the form \((y \realizesrel A)\) has an equivalent“classical” prenex form \(A'(y)\) consisting of aquantifier-free subformula preceded by alternating“classical” quantifiers of the forms \(\neg \neg \exists x\) and \(\forall z \neg \neg ,\) and so \(\exists y A'(y)\) is a kindof prenex form of \(A.\)

6. Additional Topics and Further Reading

6.1 Subintuitionistic and Intermediate Logics

At present there are several other entries in this encyclopediatreating intuitionistic logic in various contexts, but a generaltreatment of weaker and stronger propositional and predicate logicsappears to be lacking. Many such logics have been identified andstudied. Here are a few examples.

Asubintuitionistic propositional logic can be obtained from\(\mathbf{IPC}\) by restricting the language, or weakening the logic,or both. An extreme example of the first is \(\mathbf{RN},\)intuitionistic logic with a single propositional variable \(P,\) whichis named after its discoverers Rieger and Nishimura [1960].\(\mathbf{RN}\) is characterized by theRieger-Nishimuralattice of infinitely many nonequivalent formulas \(F_n\) suchthat every formula whose only propositional variable is \(P\) isequivalent by intuitionistic logic to some \(F_n.\) Nishimura’sversion is

In \(\mathbf{RN}\) neither \(F_{2 n + 1}\) nor \(F_{2 n + 2}\) impliesthe other; but \(F_{2 n}\) implies \(F_{2 n + 1},\) and \(F_{2 n +1}\) implies each of \(F_{2 n + 3}\) and \(F_{2 n + 4}.\)

Fragments of \(\mathbf{IPC}\) missing one or more logical connectivesrestrict the language and incidentally the logic, since theintuitionistic connectives \(\oldand,\) \(\vee,\) \(\rightarrow,\)\(\neg\) are logically independent over \(\mathbf{IPC}.\) Rose [1953]proved that theimplicationless fragment (without\(\rightarrow\)) is complete with respect to realizability, in thesense that if every arithmetical substitution instance of apropositional formula \(E\) without \(\rightarrow\) is(number)-realizable then \(E\) is a theorem of \(\mathbf{IPC}.\) Thisresult contrasts with:

Rose’s Theorem [1953]
\(\mathbf{IPC}\) is incomplete with respect to realizability.

Let \(F\) be the propositional formula \[( ( \neg \neg D \rightarrow D) \rightarrow( \neg \neg D \vee \neg D ) )\rightarrow ( \neg \neg D \vee \neg D)\] where \(D\) is\((\neg P \vee \neg Q)\) and \(P,\) \(Q\) are prime. Everyarithmetical substitution instance of \(F\) is realizable (usingclassical logic), but \(F\) is not provable in \(\mathbf{IPC}.\)

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

Minimal logic \(\mathbf{ML}\) comes from intuitionistic logicby deletingex falso. Kolmogorov [1925] showed that thisfragment already contains a negative interpretation of classical logicretaining both quantifiers, cf. Leivant [1985]. Minimal logic doesprove the special case \(\neg A \rightarrow (A \rightarrow \neg B)\)ofex falso for negations. Colacito, de Jongh and Vardas[2017] study varioussubminimal logics, each weaker than\(\mathbf{ML}.\)

Tennant [2017] has proposed a radical intuitionisticCoreLogic \(\mathbf{CL}\) in which the Deduction Theorem issacrificed along withex falso. Unsatisfiable assumptionsentail only falsity; thus \(\neg A \vdash (A \rightarrow B)\) but\(\neg A, A \not\vdash B\) (unless \(B\) is \(\bot\)). All core proofsare in normal form; in a core deduction all assumptions arerelevant.

Griss contested Brouwer’s use of negation, objecting to both thelaw of contradiction andex falso. It is worth noting thatnegation is not really needed for intuitionistic mathematics since \(0= 1\) is a known contradiction so \(\neg A\) can be defined by \(A\rightarrow 0 = 1.\) Thenex falso can be stated as \(0 = 1\rightarrow A,\) and the law of contradiction is provable from theremaining axioms of \(\mathbf{H}.\)

Anintermediate propositional logic is any consistentcollection of propositional formulas containing all the axioms of\(\mathbf{IPC}\) and closed undermodus ponens andsubstitution of arbitrary formulas for proposition letters. Eachintermediate propositional logic is contained in \(\mathbf{CPC}.\)Some particular intermediate propositional logics, characterized byadding one or more classically correct but intuitionisticallyunprovable axiom schemas to \(\mathbf{IPC},\) have been studiedextensively.

One of the simplest intermediate propositional logics is theGödel-Dummett logic \(\mathbf{LC},\) obtained by adding to\(\mathbf{IPC}\) the schema \((A \rightarrow B) \vee (B \rightarrowA)\) which is valid on all and only those Kripke frames in which thepartial order of the nodes is linear. Gödel [1932] used aninfinite sequence of successively stronger intermediate logics to showthat \(\mathbf{IPC}\) has no finite truth-table interpretation. Foreach positive integer \(n,\) let \(\mathbf{G_n}\) be \(\mathbf{LC}\)plus the schema \((A_1 \rightarrow A_2) \vee \ldots \vee (A_1 \oldand\ldots \oldand A_n \rightarrow A_{n + 1}).\) Then \(\mathbf{G_n}\) isvalid on all and only those linearly ordered Kripke frames with nomore than \(n\) nodes.

The Jankov logic \(\mathbf{KC},\) which adds to \(\mathbf{IPC}\) theprinciple oftestability \(\neg A \vee \neg \neg A,\)obviously does not have the disjunction property. The Kreisel-Putnamlogic \(\mathbf{KP},\) obtained by adding to \(\mathbf{IPC}\) theschema \((\neg A \rightarrow (B \vee C)) \rightarrow((\neg A\rightarrow B) \vee (\neg A \rightarrow C)),\) has the disjunctionproperty but does not satisfy all the Visser rules. The intermediatelogic obtained by adding the schema

corresponding to Rose’s counterexample, to \(\mathbf{IPC}\) alsohas the disjunction property. Iemhoff [2005] proved that\(\mathbf{IPC}\) is the only intermediate propositional logic with thedisjunction property which is closed under all the Visser rules.Iemhoff and Metcalfe [2009] developed a formal calculus forgeneralized admissibility for \(\mathbf{IPC}\) and some intermediatelogics. Goudsmit [2015] is a thorough study of the admissible rules ofintermediate logics, with a comprehensive bibliography.

An intermediate propositional logic \(\mathbf{L}\) is said to have thefinite frame property if there is a class of finite frames onwhich the Kripke-valid formulas are exactly the theorems of\(\mathbf{L}.\) Many intermediate logics, including \(\mathbf{LC}\)and \(\mathbf{KP},\) have this property. Jankov [1968] used aninfinite sequence of finite rooted Kripke frames to prove that thereare continuum many intermediate logics. De Jongh, Verbrugge and Visser[2009] proved that every intermediate logic \(\mathbf{L}\) with thefinite frame property is thepropositional logic of\(\mathbf{HA(L)},\) that is, the class of all formulas in the languageof \(\mathbf{IPC}\) all of whose arithmetical substitution instancesare provable in the logical extension of \(\mathbf{HA}\) by\(\mathbf{L}.\)

An intermediate propositional logic \(\mathbf{L}\) isstructurallycomplete if every rule which is admissible for \(\mathbf{L}\) isderivable in \(\mathbf{L},\) andhereditarily structurallycomplete if every intermediate logic extending \(\mathbf{L}\) isalso structurally complete. Every intermediate logic \(\mathbf{L}\)has astructural completion \(\mathbf{\overline{L}},\)obtained by adjoining all its admissible rules. \(\mathbf{LC}\) and\(\mathbf{G_n}\) are hereditarily structurally complete. While\(\mathbf{IPC},\) \(\mathbf{RN}\) and \(\mathbf{KC}\) are notstructurally complete, their structural completions are hereditarilystructurally complete. For these results and more, see Citkin [2016,Other Internet Resources].

Someintermediate predicate logics, extending\(\mathbf{IQC}\) and closed under substitution, are \(\mathbf{IQC}\)\(+\) DNS (Section 4.1), \(\mathbf{IQC}\) \(+\) MP (cf. Section 5.2),\(\mathbf{IQC}\) \(+\) MP \(+\) IP (cf. Section 4.2), and theintuitionistic logic of constant domains \(\mathbf{CD}\)obtained by adding to \(\mathbf{IQC}\) the schema \(\forall x (A \veeB(x)) \rightarrow (A \vee \forall x B(x))\) for all formulas \(A,\)\(B(x)\) with \(x\) not occurring free in \(A.\) Mints, Olkhovikov andUrquhart [2013] showed that \(\mathbf{CD}\) does not have theinterpolation property, refuting earlier published proofs by otherauthors.

6.2 Basic Intuitionistic Modal Logic

This section offers only a glimpse of intuitionistic modal logic. Anyclassicalmodal logic has an intuitionistic companion defined by replacing the underlyingclassical propositional or predicate logic by the correspondingintuitionistic propositional or predicate logic. Simpson [1994] andPlotkin and Stirling [1986] provide a general framework forintuitionistic modal logics which is adaptable to a multitude ofuses.

The basic intuitionistic modal propositional logic \(\mathbf{iK}\) hasas axioms:

• all propositional axioms of intuitionistic logic in the modallanguage with logical connectives \(\wedge, \vee, \rightarrow,\leftrightarrow, \neg,\) logical constants \(\top\) and \(\bot,\) anda unary operator \(\Box\) (necessity), and
• all substitution instances of Kripke’s distributive schema\(\Box(A \rightarrow B) \rightarrow (\Box A \rightarrow \BoxB);\)

and as rules of inference all substitution instances of:

• modus ponens: from \(A\) and \((A \rightarrow B),\) infer \(B,\)and
• necessitation: from \(A\) infer \(\Box A.\)

\(\mathbf{iL}\) adds to \(\mathbf{iK}\) the Löb axiom schema\(\Box (\Box A \rightarrow A) \rightarrow \Box A.\)

\(\mathbf{iK4}\) adds to \(\mathbf{iL}\) the transitive axiom schema\(\Box A \rightarrow \Box \Box A.\)

The unary operator \(\lozenge\) (possibility), classically equivalentto \(\neg \Box \neg\), increases the expressiveness of theintuitionistic modal language. Simpson argues that the correctintuitionistic analogue of the classical modal logic \(\mathbf{K}\) isPlotkin and Stirling’s \(\mathbf{IK}\), which treats\(\lozenge\) as an additional primitive and adds to \(\mathbf{iK}\)the schemas:

• \(\Box (A \rightarrow B) \rightarrow (\lozenge A \rightarrow\lozenge B).\)
• \(\neg \lozenge \bot.\)
• \(\lozenge (A \vee B) \rightarrow (\lozenge A \vee \lozenge B).\)
• \((\lozenge A \rightarrow \Box B) \rightarrow \Box (A \rightarrowB).\)

6.3 Advanced topics

Brouwer’s influence on Gödel was significant, althoughGödel never became an intuitionist. Gödel’s [1933f]translation of intuitionistic propositional logic into themodal logic \(\mathbf{S4}\) is described in Section 2.5 of the entry onGödel and in Troelstra’s introductory note to the translation of[1933f] in Volume I of Gödel’s Collected Works. See alsoMints [2012]. Kripke models for modal logic predated those forintuitionistic logic.

Alternatives to Kripke and Beth semantics for intuitionisticpropositional and predicate logic include the topologicalinterpretation of Stone [1937], Tarski [1938] and Mostowski [1948](cf. Rasiowa and Sikorski [1963], Rasiowa [1974]), which was extendedto intuitionistic analysis by Scott [1968] and Krol [1978]. M. Hyland[1982] defined the effective toposEff and proved that itslogic is intuitionistic. For a very informative discussion ofsemantics for intuitionistic logic and mathematics by W. Ruitenberg,and an interesting new perspective by G. Bezhanishvili and W.Holliday, see Other Internet Resources (below).

One alternative to realizability semantics for intuitionisticarithmetic is Gödel’s [1958] “Dialectica”interpretation, which associates with each formula \(B\) of\(L(\mathbf{HA})\) a quantifier-free formula \(B_D\) in the languageof intuitionistic arithmetic of all finite types. The“Dialectica” interpretation of \(B,\) call it\(B^D,\) is \(\exists Y\forall x B_D (Y, x).\) If \(B\) is a closedtheorem of \(\mathbf{HA},\) then \(B_D (F, x)\) is provable for someterm \(F\) in Gödel’s theory \(\mathbf{T}\) of“primitive recursive” functionals of higher type. Thetranslation from \(B\) to \(B^D\) requires the axiom of choice (at allfinite types), MP and IP, so is not strictly constructive; however,the number-theoretic functions expressible by terms \(F\) of\(\mathbf{T}\) are precisely the provably recursive functions of\(\mathbf{HA}\) (and of \(\mathbf{PA}).\) The interpretation wasextended to analysis by Spector [1962]; cf. Howard [1973]. Clearexpositions, and additional references, are to be found inTroelstra’s introduction to the English translation inGödel [1990] of the originalDialectica article, inAvigad and Feferman [1998], and in Ferreira [2008].

While \(\mathbf{HA}\) is a proper part of classical arithmetic, theintuitionistic attitude toward mathematical objects results in atheory of real numbers (cf. sections 3.4–3.7 of the entry onintuitionism in the philosophy of mathematics) diverging from the classical. Kleene’s function-realizabilityinterpretation, developed to prove the consistency of hisformalization \(\mathbf{FIM}\) of the intuitionistic theory ofsequences (“intuitionistic analysis”), changes theinterpretation of arithmetical formulas; for example, \(\neg \neg\forall x (A(x) \vee \neg A(x))\) is function-realizable for everyarithmetical formula \(A(x).\) In the language of analysis,Markov’s Principle and the negative translation of the countableaxiom of choice are among the many non-intuitionistic principles whichare function-realizable (by classical arguments) and hence consistentwith \(\mathbf{FIM};\) cf. Kleene [1965], Vesley [1972] andMoschovakis [2003].

Concrete and abstract realizability semantics for a wide variety offormal systems have been developed and studied by logicians andcomputer scientists; cf. Troelstra [1998] and van Oosten [2002] and[2008]. Variations of the basic notions are especially useful forestablishing relative consistency and relative independence of thenonlogical axioms in theories based on intuitionistic logic; someexamples are Moschovakis [1971], Lifschitz [1979], and therealizability notions for constructive and intuitionistic set theoriesdeveloped by Rathjen [2006, 2012] and Chen [2012]. Early abstractrealizability notions include theslashes of Kleene [1962,1963] and Aczel [1968], and Läuchli [1970]. Kohlenbach, Avigadand others have developed realizability interpretations for parts ofclassical mathematics.

Artemov’sjustification logic is an alternative interpretation of the B-H-K explanation of theintuitionistic connectives and quantifiers, with (idealized) proofsplaying the part of realizing objects. See also Artemov and Iemhoff[2007].

Another line of research in intuitionistic logic concernsBrouwer’s controversial “creating subjectcounterexamples” to principles of classical analysis (such asMarkov’s Principle) which could not be refuted on the basis ofthe theory \(\mathbf{FIM}\) of Kleene and Vesley [1965]. By weakeningKleene’s strong form of Brouwer’s principle of continuouschoice, and adding an axiom he calledKripke’s Schema(KP), Myhill [1967] formalized Brouwer’s creating subjectarguments in the language of intuitionistic analysis. Krol [1978] andScowcroft gave topological consistency proofs for intuitionisticanalysis with Kripke’s Schema and weak continuity. Kripkehimself preferredWeak Kripke’s Schema (WKP), whichstill conflicts with strong continuous choice. Kripke [2019] andBrauer, Linnebo and Shapiro [2022] recently provided an attractivemodal interpretation of Brouwer’s theory of the creatingsubject.

Vesley [1970] found an alternative principle (Vesley’sSchema VS) which can consistently be added to \(\mathbf{FIM}\)and implies all the counterexamples for which Brouwer required acreating subject. Troelstra’sgeneralized continuouschoice (GC), which characterizes Kleene’s function-realizabilityjust as his ECT characterizes number-realizability, and Vesley’sVS express two incompatible possible extensions of intuitionisticanalysis, with different mathematical properties.

Constructive mathematicians, following Bishop, traditionally assumeintuitionistic logic and work with strong definitions of concepts. Forexample, they equate “there is at most one number \(n\) suchthat \(P(n)\)” with “if \(n\) and \(m\) are distinctnumbers then not \(P(n)\) or not \(P(m),\)” rather than the morenatural “if \(n\) and \(m\) are numbers such that \(P(n)\) and\(P(m)\) then \(n = m\)”. Shulman [2022] suggests that an“affine” logic of proof and refutation, with additionalconnectives and an antithesis translation into intuitionistic logic,would be more useful for constructive mathematics.

6.4 Recommended reading

The entry onL. E. J. Brouwer discusses Brouwer’s philosophy and mathematics, with achronology of his life and a selected list of publications includingtranslations and secondary sources. The best way to learn more is toread some of the original papers. English translations ofBrouwer’s doctoral dissertation and other papers whichoriginally appeared in Dutch, along with a number of articles inGerman, can be found inL. E. J. Brouwer: Collected Works[1975], edited by Heyting. Benacerraf and Putnam’s essentialsource book contains Brouwer [1912] (in English translation), Brouwer[1949] and Dummett [1975]. Mancosu’s [1998] provides Englishtranslations of many fundamental articles by Brouwer, Heyting,Glivenko and Kolmogorov, with illuminating introductory material by W.van Stigt whose [1990] is another valuable resource.

A delightful, accessible and authoritative introduction tointuitionistic mathematics and logic is Wim Veldman’s [2021].The third edition [1971] of Heyting’s classic [1956] is anattractive introduction to intuitionistic philosophy, logic andmathematical practice. As part of the formidable project of editingand publishing Brouwer’sNachlass, van Dalen [1981]provides a comprehensive view of Brouwer’s own intuitionisticphilosophy. The English translation, in van Heijenoort [1969], ofBrouwer’s [1927] (with a fine introduction by Parsons) is stillan indispensable reference for Brouwer’s theory of thecontinuum. Veldman [1990] and [2005] are authentic modern examples oftraditional intuitionistic mathematical practice. Troelstra [1991]places intuitionistic logic in its historical context as the commonfoundation of constructive mathematics in the twentieth century.Bezhanishvili and de Jongh [2005, Other Internet Resources] includesrecent developments in intuitionistic logic.

Kleene and Vesley’s [1965] gives a careful axiomatic treatmentof intuitionistic analysis, a proof of its consistency relative to aclassically correct subtheory, and an extended application toBrouwer’s theory of real number generators. Kleene’s[1969] formalizes the theory of partial recursive functionals,enabling precise formalizations of the function-realizabilityinterpretation used in [1965] and of a related q-realizabilityinterpretation which gives the Church-Kleene Rule for intuitionisticanalysis.

Troelstra’s [1973], Beeson’s [1985] and Troelstra and vanDalen’s [1988] (withcorrections) stand out as the most comprehensive studies of intuitionistic andsemi-intuitionistic formal theories, using both constructive andclassical methods, with useful bibliographies. Troelstra andSchwichtenberg [2000] presents the proof theory of classical,intuitionistic and minimal logic in parallel, focusing on sequentsystems. Troelstra’s [1998] presents formulas-as-types and(Kleene and Aczel) slash interpretations for propositional andpredicate logic, as well as abstract and concrete realizabilities fora multitude of applications. Martin-Löf’s constructivetheory of types [1984] (cf. Section 3.4 of the entry onconstructive mathematics) provides another general framework within which intuitionisticreasoning 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 intuitionisticlogic of proofs,”Journal of Symbol Logic, 72:439–451.
• Avigad, J. and Feferman, S., 1998, “Gödel’sfunctional (”Dialectica“) interpretation,” Chapter Vof Buss (ed.) 1998: 337–405.
• Bar-Hillel, Y. (ed.), 1965,Logic, Methodology and Philosophyof Science, Amsterdam: North Holland.
• Beeson, M. J., 1985,Foundations of ConstructiveMathematics, Berlin: Springer.
• Benacerraf, P. and Hilary Putnam (eds.), 1983,Philosophy ofMathematics: Selected Readings, 2nd Edition, Cambridge: CambridgeUniversity Press.
• Beth, E. W., 1956, “Semantic construction of intuitionisticlogic,”Koninklijke Nederlandse Akad. vonWettenscappen, 19(11): 357–388.
• Brauer, E., 2022, “The modal logic of potential infinity:convergent versus branching possibilities,”Erkenntnis87:2161–2179.
• Brauer, E., Linnebo O. and Shapiro, S., 2022, “Divergentpotentialism: a modal analysis with an application to choicesequences,”Philosophia Mathematica 30(2):143–172.
• Brouwer, L. E. J., 1907, “On the Foundations ofMathematics,” Thesis, Amsterdam; English translation in Heyting(ed.) 1975: 11–101.
• –––, 1908, “The Unreliability of theLogical Principles,” English translation in Heyting (ed.) 1975:107–111.
• –––, 1912, “Intuitionism andFormalism,” English translation by A. Dresden,Bulletin ofthe American Mathematical Society, 20 (1913): 81–96,reprinted in Benacerraf and Putnam (eds.) 1983: 77–89; alsoreprinted in Heyting (ed.) 1975: 123–138.
• –––, 1923 [1954], “On the significance ofthe principle of excluded middle in mathematics, especially infunction theory,” “Addenda and corrigenda,” and“Further addenda and corrigenda,” English translation invan Heijenoort (ed.) 1967: 334–345.
• –––, 1923C, “Intuitionistische Zerlegungmathematischer Grundbegriffe,”Jahresbericht der DeutschenMathematiker-Vereinigung, 33 (1925): 251–256; reprinted inHeyting (ed.) 1975, 275–280.
• –––, 1927, “Intuitionistic reflections onformalism,” originally published in 1927, English translation invan Heijenoort (ed.) 1967: 490–492.
• –––, 1948, “Consciousness, philosophy andmathematics,” originally published (1948), reprinted inBenacerraf and Putnam (eds.) 1983: 90–96.
• Burr, W., 2004, “The intuitionistic arithmeticalhierarchy,” in J. van Eijck, V. van Oostrom and A. Visser(eds.),Logic Colloquium ’99 (Lecture Notes in Logic17), Wellesley, MA: ASL and A. K. Peters, 51–59.
• Buss, S. (ed.), 1998,Handbook of Proof Theory, Amsterdamand New York: Elsevier.
• Chen, R-M. and Rathjen, M., 2012, “Lifschitz realizabilityfor intuitionistic Zermelo-Fraenkel set theory,”Archive forMathematical Logic, 51: 789–818.
• Colacito, A., de Jongh, D. and Vargas, A., 2017, “SubminimalNegation”,Soft Computing, 21: 165–164.
• Crossley, J., and M. A. E. Dummett (eds.), 1965,FormalSystems and Recursive Functions, Amsterdam: North-HollandPublishing.
• van Dalen, D. (ed.), 1981,Brouwer’s Cambridge Lectureson Intuitionism, Cambridge: Cambridge University Press.
• Dummett, M., 1975, “The philosophical basis ofintuitionistic logic,” originally published (1975), reprinted inBenacerraf and Putnam (eds.) 1983: 97–129.
• Dyson, V. and Kreisel, G., 1961,Analysis of Beth’ssemantic construction of intuitionistic logic, Technical ReportNo. 3, Stanford: Applied Mathematics and Statistics Laboratory,Stanford University.
• Ewald, W. B., 1986, “Intuitionistic tense and modallogic,”Journal of Symbolic Logic 51(1):166–179.
• Ferreira, F., 2008, “A most artistic package of a jumble ofideas,”Dialectica, 62: 205–222.
• Fitting, M., 1987, “Resolution for intuitionisticlogic”,Proceedings of the Second International Symposium onMethodologies for Intelligent Systems, December 1987:400–407.
• Friedman, H., 1975, “The disjunction property implies thenumerical existence property,”Proceedings of the NationalAcademy of Science, 72: 2877–2878.
• Gentzen, G., 1934–5, “Untersuchungen Über daslogische Schliessen,”Mathematische Zeitschrift, 39:176–210, 405–431.
• Ghilardi, S., 1999, “Unification in intuitionisticlogic,”Journal of Symbolic Logic, 64:859–880.
• Glivenko, V., 1929, “Sur quelques points de la logique de M.Brouwer,”Académie Royale de Belgique, Bulletins dela classe des sciences, 5 (15): 183–188.
• Gödel, K., 1932, “Zum intuitionistischenAussagenkalkül,”Anzeiger der Akademie derWissenschaften in Wien, 69: 65–66. Reproduced andtranslated with an introductory note by A. S. Troelstra in Gödel1986: 222–225.
• –––, 1933e, “Zur intuitionistischenArithmetik und Zahlentheorie,”Ergebnisse einesmathematischen Kolloquiums, 4: 34–38.
• –––, 1933f, “Eine Interpretation desintuitionistischen Aussagenkalküls,” reproduced andtranslated with an introductory note by A. S. Troelstra in Gödel1986: 296–304.
• –––, 1958, “Über eine bisher nochnicht benützte Erweiterung des finiten Standpunktes,”Dialectica, 12: 280–287. Reproduced with an Englishtranslation in Gödel 1990: 241–251.
• –––, 1986,Collected Works, Vol. I, S.Fefermanet al. (eds.), Oxford: Oxford University Press.
• –––, 1990,Collected Works, Vol. II, S.Fefermanet al. (eds.), Oxford: Oxford University Press.
• Goudsmit, J. P., 2015,Intuitionistic Rules: Admissible Rulesof Intermediate Logics, Ph.D. dissertation, University ofUtrecht.
• Harrop R., 1960, “Concerning formulas of the types \(A\rightarrow B \vee C, A \rightarrow (Ex)B(x)\) in intuitionisticformal systems,”Journal of Symbolic Logic, 25:27–32.
• van Heijenoort, J. (ed.), 1967,From Frege to Gödel: ASource Book In Mathematical Logic 1879–1931, Cambridge, MA:Harvard University Press.
• Heyting, A., 1930, “Die formalen Regeln derintuitionistischen Logik,” in three parts,Sitzungsberichteder preussischen Akademie der Wissenschaften: 42–71,158–169. English translation of Part I in Mancosu 1998:311–327.
• –––, 1956,Intuitionism: AnIntroduction, Amsterdam: North-Holland Publishing, 3rd revisededition, 1971.
• Heyting, A. (ed.), 1975,L. E. J. Brouwer: CollectedWorks (Volume 1:Philosophy and Foundations ofMathematics), Amsterdam and New York: Elsevier.
• Howard, W. A., 1973, “Hereditarily majorizable functionalsof finite type,” in Troelstra (ed.) 1973: 454–461.
• Hyland, J. M. E., 1982, “The effective topos,” inTroelstra and van Dalen (ed.) 1982: 165–216.
• Iemhoff, R., 2001, “On the admissible rules ofintuitionistic propositional logic,”Journal of SymbolicLogic, 66: 281–294.
• –––, 2005, “Intermediate logics andVisser’s rules,”Notre Dame Journal of FormalLogic, 46: 65–81.
• Iemhoff, R. and Metcalfe, G., 2009, “Proof theory foradmissible rules,”Annals of Pure and Applied Logic,159: 171–186.
• Jankov, V. A., 1968, “The construction of a sequence ofstrongly independent superintuitionistic propositionalcalculii,”Soviet Math. Doklady, 9: 801–807.
• Jerabek, E., 2008, “Independent bases of admissiblerules,”Logic Journal of the IGPL, 16:249–267.
• de Jongh, D. H. J., 1970, “The maximality of theintuitionistic propositional calculus with respect to Heyting’sArithmetic,”Journal of Symbolic Logic, 6: 606.
• de Jongh, D. H. J., and Smorynski, C., 1976, “Kripke modelsand the intuitionistic theory of species,”Annals ofMathematical 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 summerconference at Buffalo, NY, 1968, Amsterdam: North-Holland.
• Kleene, S. C., 1945, “On the interpretation ofintuitionistic number theory,”Journal of SymbolicLogic, 10: 109–124.
• –––, 1952,Introduction toMetamathematics, Princeton: Van Nostrand.
• –––, 1962, “Disjunction and existenceunder implication in elementary intuitionistic formalisms,”Journal of Symbolic Logic, 27: 11–18.
• –––, 1963, “An addendum,”Journal of Symbolic Logic, 28: 154–156.
• –––, 1965, “Classical extensions ofintuitionistic mathematics,” in Bar-Hillel (ed.) 1965:31–44.
• –––, 1969,Formalized Recursive Functionalsand Formalized Realizability, Memoirs of the AmericanMathematical Society 89.
• Kleene, S. C. and Vesley, R. E., 1965,The Foundations ofIntuitionistic Mathematics, Especially in Relation to RecursiveFunctions, Amsterdam: North-Holland.
• Kreisel, G., 1958, “Elementary completeness properties ofintuitionistic logic with a note on negations of prenexformulas,”Journal of Symbolic Logic, 23:317–330.
• –––, 1962, “On weak completeness ofintuitionistic predicate logic,”Journal of SymbolicLogic, 27: 139–158.
• Kripke, S. A., 1965, “Semantical analysis of intuitionisticlogic,” in J. Crossley and M. A. E. Dummett (eds.) 1965:92–130.
• –––, 2019, “Free choice sequences: Atemporal interpretation compatible with acceptance of classicalmathematics,”Indag.Math., 30: 492–499.
• Krol, M., 1978, “A topological model of intuitionisticanalysis with Kripke’s Schema,”Zeitschrift fürMath. Logik und Grundlagen der Math., 24: 427–436.
• Leivant, D., 1979, “Maximality of IntuitionisticLogic,” Mathematical Centre Tracts 73, Mathematisch Centrum,Amsterdam.
• –––, 1985, “Syntactic translations andprovably recursive functions,”Journal of SymbolicLogic, 50: 682–688.
• Läuchli, H., 1970, “An abstract notion of realizabilityfor which intuitionistic predicate calculus is complete,” in A.Kino et al. (eds.) 1965: 227–234.
• Lifschitz, V., 1979, “CT\(_0\) is stronger thanCT\(_0\)!,”Proceedings of the American MathematicalSociety, 73(1): 101–106.
• Mancosu, P., 1998,From Brouwer to Hilbert: The Debate on theFoundations 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, June1980, Napoli: Bibliopolis.
• Mints, G., 2012, “The Gödel–Tarski translationsof intuitionistic propositional formulas,” inCorrectReasoning (Lecture Notes in Computer Science 7265), E. Erdem etal. (eds.), Dordrecht: Springer-Verlag: 487–491.
• Mints, G., Olkhovikov, G. and Urquhart, A., 2013, “Failureof interpolation in the intuitionistic logic of constantdomains,”Journal of Symbolic Logic 78(3):937–950.
• Moschovakis, J. R., 1971, “Can there be no nonrecursivefunctions?,”Journal of Symbolic Logic, 36:309–315.
• –––, 2003, “Classical and constructivehierarchies in extended intuitionistic analysis,”Journal ofSymbolic Logic, 68: 1015–1043.
• –––, 2009, “The logic of Brouwer andHeyting,” inLogic from Russell to Church (Handbookof the History of Logic, Volume 5), J. Woods and D. Gabbay(eds.), Amsterdam: Elsevier: 77–125.
• –––, 2017, “Intuitionistic analysis at theend of time,”Bulletin of Symbolic Logic, 23:279–295.
• Myhill, J., 1967, “Notes toward an axiomatization ofintuitionistic analysis,”Logique et Analyse 9:280–297.
• Nelson, D., 1947, “Recursive functions and intuitionisticnumber theory,”Transactions of the American MathematicalSociety, 61: 307–368.
• Nishimura, I., 1960, “On formulas of one variable inintuitionistic propositional calculus,”Journal of SymbolicLogic, 25: 327–331.
• van Oosten, J., 1991, “A semantical proof of deJongh’s theorem,”Archives for MathematicalLogic, 31: 105–114.
• –––, 2002, “Realizability: a historicalessay,”Mathematical Structures in Computer Science,12: 239–263.
• –––, 2008,Realizability: An Introduction toits Categorical Side, Amsterdam: Elsevier.
• Plisko, V. E., 1992, “On arithmetic complexity of certainconstructive logics,”Mathematical Notes, (1993):701–709. Translated fromMatematicheskie Zametki, 52(1992): 94–104.
• Plotkin, G. and Stirling, C., 1986, “A framework forintuitionistic modal logic,” inTARK ’86: Proceedingsof the 1986 conference on theoretical aspects of reasoning aboutknowledge, J. Halpern (ed.), Morgan Kaufmann Publishers, LosAltos 1986: 399–406. Abstract inJournal of SymbolicLogic 53(2): 669.
• Rasiowa, H., 1974,Algebraic Approach to Non-ClassicalLogics, Amsterdam: North-Holland.
• Rasiowa, H. and Sikorski, R., 1963,The Mathematics ofMetamathematics, Warsaw: Panstwowe Wydawnictwo Naukowe.
• Rathjen, M., 2006, “Realizability for constructiveZermelo-Fraenkel set theory,” inLogic Colloquium 2003(Lecture Notes in Logic 24), J. Väänänen et al. (eds.),A. K. Peters 2006: 282–314.
• –––, 2012, “From the weak to the strongexistence property,”Annals of Pure and Applied Logic,163: 1400–1418.
• Rose, G. F., 1953, “Propositional calculus andrealizability,”Transactions of the American MathematicalSociety, 75: 1–19.
• Ruitenberg, W., 1991, “The unintended interpretations ofintuitionistic logic”, in: T. Drucker (ed.),Perspectives onthe History of Mathematical Logic, Birkhauser 1991:134–160.
• Rybakov, V., 1997,Admissibility of Logical InferenceRules, Amsterdam: Elsevier.
• Scott, D., 1968, “Extending the topological interpretationto intuitionistic analysis,”Compositio Mathematica,20: 194–210.
• Shulman, M., 2022, “Affine logic for constructivemathematics”,Bulletin of Symbolic Logic, 28:327–386.
• Simpson, A. K., 1994,The proof theory and semantics ofintuitionistic modal logic, Doctoral dissertation, University ofEdinburgh.
• Smorynski, C. A., 1973, “Applications of Kripkemodels,” in Troelstra (ed.) 1973: 324–391.
• Spector, C., 1962, “Provably recursive functionals ofanalysis: a consistency proof of analysis by an extension ofprinciples formulated in current intuitionistic mathematics,”Recursive Function Theory: Proceedings of Symposia in PureMathematics, 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.
• Stone, M. H., 1937, “Topological representation ofdistributive lattices and Brouwerian logics”,Casopis Pest.Mat. Fys., 67: 1–25.
• Swart, H. C. M. de, 1976, “Another intuitionisticcompleteness proof,”Journal of Symbolic Logic 41:644–662.
• Tarski, A., 1938, “Der Aussagenkalkül und dieTopologie”,Fundamenta Mathematicae, 31:103–134.
• Tennant, N., 2017,Core Logic, Oxford University Press,Oxford.
• Troelstra, A. S., 1977,Choice Sequences: A Chapter ofIntuitionistic Mathematics, Oxford Logic Guides, Clarendon Press,Oxford.
• –––, 1991, “History of constructivism inthe twentieth century,” ITLI Prepublication SeriesML–1991–05, Amsterdam. Final version inSet Theory,Arithmetic and Foundations of Mathematics (Lecture Notes in Logic36), J. Kenney and R. Kossak (eds.), Association for Symbolic Logic,Ithaca, NY, 2011: 150–179.
• –––, 1998, “Realizability,” ChapterVI of Buss (ed.), 1998: 407–473.
• –––, Introductory note to 1958 and 1972, inGödel, 1990: 217–241.
• Troelstra, A. S. (ed.), 1973,Metamathematical Investigationof Intuitionistic Arithmetic and Analysis (Lecture Notes inMathematics 344), Berlin: Springer-Verlag. Corrections and additionsavailable from the editor.
• Troelstra, A. S. and Schwichtenberg, H., 2000,Basic ProofTheory (Cambridge Tracts in Theoretical Computer Science: Volume43), 2nd edition, Cambridge: Cambridge University Press.
• Troelstra, A. S. and van Dalen, D., 1988,Constructivism inMathematics: An Introduction, 2 volumes, Amsterdam: North-HollandPublishing. [See also theCorrections, in Other InternetResources.]
• Troelstra, A. S. and van Dalen, D. (eds.), 1982,The L. E. J.Brouwer Centenary Symposium, Amsterdam: North-HollandPublishing.
• Veldman, W., 1976, “An intuitionistic completeness theoremfor intuitionistic predicate logic,”Journal of SymbolicLogic, 41: 159–166.
• –––, 1990, “A survey of intuitionisticdescriptive set theory,” in P. P. Petkov (ed.),MathematicalLogic, Proceedings of the Heyting Conference, New York andLondon: Plenum Press, 155–174.
• –––, 2005, “Two simple sets that are notpositively Borel,”Annals of Pure and Applied Logic,135: 151–209.
• –––, 2021, “Intuitionism: Aninspiration?,”Jahresbericht der DeutscherMathematiker-Vereinigung, 123: 221–284.
• Vesley, R. E., 1972, “Choice sequences and Markov’sprinciple,”Compositio Mathematica, 24:33–53.
• –––, 1970, “A palatable substitute forKripke’s Schema,” in A. Kino et al. (eds.) 1970:197ff.
• Visser, A., 1999, “Rules and arithmetics,”NotreDame Journal of Formal Logic, 40: 116–140.
• –––, 2002, “Substitutions of\(\Sigma^{0}_1\) sentences: explorations between intuitionisticpropositional logic and intuitionistic arithmetic,”Annalsof Pure and Applied Logic, 114: 227–271.
• –––, 2006, “Predicate logics ofconstructive arithmetical theories,”Journal of SymbolicLogic, 72: 1311–1326.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

• Bezhanishvili, G. and Holliday, W., 2018, “A semantic hierarchy for intuitionistic logic,” manuscript, UC Berkeley Faculty Publications.
• Bezhanishvili, N. and de Jongh, D. H. J., 2005,Intuitionistic Logic, Lecture notes presented at ESSLLI, Edinburgh.
• Brouwer,Excerpts from Brouwer’s Cambridge lectures.
• Citkin, A., 2016, “Hereditarily structurally complete superintuitionistic deductive systems,” manuscript at arXiv.org.
• de Paiva, Valeria, 2015,Intuitionistic modal logic: 15 years later.
• Troelstra, A. S., 2018,Corrections to some publications.
• Troelstra, A. S., and van Ulsen, P.,The discovery of E. W. Beth’s semantics for intuitionistic logic.
• Realizability Bibliography, maintained by Lars Birkedal.
• van Oosten 2000, and other preprints related to realizability, maintained by Jaap van Oosten.

Related Entries

Brouwer, Luitzen Egbertus Jan |Gödel, Kurt |logic, history of: intuitionistic logic |logic: classical |logic: modal |logic: provability |logicism and neologicism |mathematics, philosophy of |mathematics, philosophy of: formalism |mathematics, philosophy of: intuitionism |mathematics, philosophy of: Platonism |mathematics: constructive |proof theory: development of |set theory: constructive and intuitionistic ZF

Acknowledgments

I would like to thank Wim Veldman especially for his recentopen-access article “Intuitionism: An Inspiration?”, whichis a gift to curious students, mathematically inclined philosophersand philosophically inclined mathematicians. Veldman is a practicingintuitionistic mathematician whose mentor was M. de Jongh, one ofBrouwer’s students.Intuitionism: An Introduction waswritten more than half a century ago by another of Brouwer’sstudents, A. Heyting, for a similar audience. The similarity of titlesis appropriate.

Over the years, many readers and a few wise and conscientious refereeshave offered corrections and improvements to this entry. I am stillgrateful to Edward Horton (for pointing out that replacingexfalso by the LEM in the axioms for \(\mathbf{IPC}\) does notyield all of \(\mathbf{CPC},\) and for providing the correctsubstitutions) and to all the other readers who have corrected errorsin earlier editions. I thank Mark van Atten, Robert Thomas, VictorPambuccian, Michael Beeson, Mariusz Stopa and Antonino Drago forbringing new and old work to my attention since the last revision.Questions from students are always appreciated; this time, MilesShi’s question led to an improvement in Section 5. As always, Ithank Ed Zalta for his patience and attention to detail, and for thevery existence of this comprehensive open-access encyclopedia.