# Intuitionistic Logic

*First published Wed Sep 1, 1999; substantive revision Tue Sep 4, 2018*

Intuitionistic logic encompasses the general principles of logical reasoning which have been abstracted by logicians from intuitionistic mathematics, as developed by L. E. J. Brouwer beginning in his [1907] and [1908]. Because these principles also hold for Russian recursive mathematics and the constructive analysis of E. Bishop and his followers, intuitionistic logic may be considered the logical basis of constructive mathematics. Although intuitionistic analysis conflicts with classical analysis, intuitionistic Heyting arithmetic is a subsystem of classical Peano arithmetic. It follows that intuitionistic propositional logic is a proper subsystem of classical propositional logic, and pure intuitionistic predicate logic is a proper subsystem of pure classical predicate logic.

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
fully developed by Heyting [1930], Gentzen [1935] and Kleene [1952].
Gödel [1933] proved the equiconsistency of intuitionistic and
classical theories. Beth [1956] and Kripke [1965] provided semantics
with respect to which intuitionistic logic is correct and complete,
although the completeness proofs for intuitionistic predicate logic
require some classical reasoning.

- 1. Rejection of
*Tertium Non Datur* - 2. Intuitionistic First-Order Predicate Logic
- 3. Intuitionistic Number Theory (Heyting Arithmetic) \(\mathbf{HA}\)
- 4. Basic Proof Theory
- 5. Basic Semantics
- 6. Additional Topics and Further Reading
- Bibliography
- Academic Tools
- Other Internet Resources
- Related Entries

## 1. Rejection of *Tertium Non Datur*

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

\[ \tag{LEM} A \vee \neg A \]or the classical law of double negation elimination:

\[ \tag{DNE} \neg \neg A \rightarrow A \]but with the law of contradiction:

\[ (A \rightarrow B) \rightarrow ((A \rightarrow \neg B) \rightarrow \neg A) \]
and *ex falso sequitur quodlibet*:

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, \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 as classically, because in order to determine whether or not a natural number is prime we need only check whether or not it has a divisor strictly between itself and 1.

But if \(A(x)\) abbreviates \(\exists y(y\gt x \oldand B(y))\), then
in order to assert \(\forall x (A(x) \vee \neg A(x))\)
intuitionistically we would need an *effective* (cf.
the Church-Turing thesis)
method to determine whether or not there is a pair of twin primes
larger than an arbitrary natural number \(x\), and so far no such
method is known. An obvious *semi-effective* method is to list
the prime number pairs using a refinement of Eratosthenes’ sieve
(generating the natural numbers one by one and striking out every
number \(y\) which fails to satisfy \(B(y)\)), and if there is a pair
of twin primes larger than \(x\) this method will eventually find the
first one. However, \(\forall x A(x)\) expresses the Twin Primes
Conjecture, which has not yet been proved or disproved, so in the
present 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 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 \(\neg \neg A \rightarrow A\) does not hold in general. (If it did, LEM would follow by*modus ponens*from the intuitionistically provable \(\neg \neg(A \vee \neg A)\).) - Intuitionistic propositional logic does not have a finite truth-table interpretation. There are infinitely many distinct axiomatic systems between intuitionistic and classical logic.
- Not every propositional formula has an intuitionistically equivalent disjunctive or conjunctive normal form, built from prime formulas and their negations using only \(\vee\) and \(\oldand\).
- Not every predicate formula has an intuitionistically equivalent prenex normal form, with all the quantifiers at the front.
- While \(\forall x \neg \neg(A(x) \vee \neg A(x))\) is a theorem of intuitionistic predicate logic, \(\neg \neg \forall x(A(x) \vee \neg A(x))\) is not; so \(\neg \forall x(A(x) \vee \neg A(x))\) is consistent 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 proof of \(A\) or an intuitionistic proof of \(B\), and similarly for closed existential statements.
- Intuitionistic propositional logic is effectively decidable, in the sense that a finite constructive process applies uniformly to every propositional formula, either producing an intuitionistic proof of 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, and similarly for intuitionistic and classical arithmetic.
- Intuitionistic arithmetic can consistently be extended by axioms 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 the entries on intuitionism in the philosophy of mathematics and the development of intuitionistic logic. The constructive independence of the logical operations \(\oldand, \vee , \rightarrow , \neg , \forall , \exists\) contrasts with the classical situation, where e.g., \(A \vee B\) is equivalent to \(\neg(\neg A \oldand \neg B)\), and \(\exists xA(x)\) is equivalent to \(\neg \forall x \neg A(x)\). From the B-H-K viewpoint, a sentence of the form \(A \vee B\) asserts that either a proof of \(A\), or a proof of \(B\), has been constructed; while \(\neg(\neg A \oldand \neg B)\) asserts that an algorithm has been constructed which would effectively 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}\) from
Kleene [1952] (cf. Troelstra and van Dalen [1988]) for intuitionistic
first-order predicate logic. The language \(L\) of
\(\mathbf{H–IQC}\) has predicate letters \(P, Q(.), \ldots\) of
all arities and individual variables \(x, y, z, \ldots\) (with or
without subscripts \(1, 2, \ldots\)), as well as symbols \(\oldand,
\vee , \rightarrow , \neg , \forall , \exists\) for the logical
connectives and quantifiers, and parentheses (, ). The *atomic*
(or *prime*) *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 an
individual variable symbol is a prime formula. The *(well-formed)
formulas* of \(L\) are defined inductively as follows.

- Each atomic formula is a
*formula*. - If \(A\) and \(B\) are
*formulas*, so are \((A \oldand B), (A \vee B), (A \rightarrow B)\) and \(\neg A\). - If \(A\) is a
*formula*and \(x\) is a variable, then \(\forall xA\) and \(\exists 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 \(\forall x\) or \(\exists x\),
otherwise *free*. Intuitionistically as classically, \((A
\leftrightarrow B)\) abbreviates \(((A \rightarrow B) \oldand (B
\rightarrow A))\), and parentheses will be omitted when this causes no
confusion.

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 not
occur free in \(C\), conclude \(C \rightarrow \forall x A(x)\).

*\(\exists\)-Elimination*

From \(A(x) \rightarrow C\), where \(x\) is a variable which does not
occur free in \(C\), conclude \(\exists x A(x) \rightarrow 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.

\[\begin{array}{l} A \rightarrow(B \rightarrow A) \\ (A \rightarrow B) \rightarrow ((A \rightarrow (B \rightarrow C)) \rightarrow(A \rightarrow C)) \\ A \rightarrow(B \rightarrow (A \oldand B)) \\ (A \oldand B) \rightarrow A \\ (A \oldand B) \rightarrow B \\ A \rightarrow (A \vee B) \\ B \rightarrow (A \vee B) \\ (A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow((A \vee B) \rightarrow C)) \\ (A \rightarrow B) \rightarrow ((A \rightarrow \neg B) \rightarrow \neg A) \\ \neg A \rightarrow(A \rightarrow B) \\ \forall xA(x) \rightarrow A(t) \\ A(t) \rightarrow \exists xA(x) \end{array}\]
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 \(\mathbf{H–IPC}\) is the subsystem of \(\mathbf{H–IQC}\) which results when the language is 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 are used. Thus the last two rules of inference and the last two axiom schemas are absent from the propositional subsystem.

If, in the given list of axiom schemas for intuitionistic
propositional or first-order predicate logic, the law expressing
*ex falso sequitur quodlibet*:

is replaced by the classical law of double negation elimination DNE:

\[\neg \neg A \rightarrow A\](or, equivalently, if the intuitionistic law of negation introduction:

\[ (A \rightarrow B) \rightarrow ((A \rightarrow \neg B) \rightarrow \neg A) \]
is replaced by LEM), a formal system \(\mathbf{H–CPC}\) for
classical propositional logic or \(\mathbf{H–CQC}\) for
classical predicate logic results. Since *ex falso* and the law
of contradiction are classical theorems, 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 DNE are equivalent as
*schemas* over \(\mathbf{H–IPC}\), the
*implication*

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

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

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

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

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

### 2.2 Alternative formalisms, and the deduction theorem

The Hilbert-style system \(\mathbf{H–IQC}\) 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 \(\mathbf{N–IQC}\) for intuitionistic
predicate logic results from the deductive system \(\mathbf{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 expressing *ex
falso*:

- (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}\) 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 \rightarrow B\) is derivable from \(F\).

This fundamental result, roughly expressing the rule \((\rightarrow
I)\) of \(\mathbf{I}\), can be proved for \(\mathbf{H–IQC}\) by
induction on the definition of a derivation. The other rules of
\(\mathbf{I}\) hold for \(\mathbf{H–IQC}\) essentially by
*modus 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 correct proof 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 \rightarrow A))\)
- 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 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 \rightarrow A\) exists. (In fact, the
formal proof of \(A \rightarrow 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 \(\mathbf{H–IQC}\), the assumption formulas are
treated as if all their free variables were universally quantified, so
that \(\forall 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
\(\forall\)-introduction; and so the Deduction Theorem cannot be used
to conclude (falsely) that \(A(x) \rightarrow \forall x A(x)\) (and
hence, by \(\exists\)-elimination, \(\exists x A(x) \rightarrow
\forall x A(x))\) are provable in \(\mathbf{H–IQC}\). As an
example of a correct use of the Deduction Theorem for predicate logic,
consider the implication \(\exists x A(x) \rightarrow \neg \forall
x\neg A(x)\). To show this is provable in \(\mathbf{H–IQC}\), we
first derive \(\neg \forall x\neg A(x)\) from \(A(x)\) with all free
variables 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 ((\forall x\neg A(x) \rightarrow \neg A(x)) \rightarrow \neg \forall x\neg A(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 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 \(\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 converse
is not provable in \(\mathbf{H–IQC}\), as shown in Section 5.1
below.

Other important alternatives to \(\mathbf{H–IQC}\) and
\(\mathbf{N–IQC}\) are the various sequent calculi for
intuitionistic propositional and predicate logic. The first such
calculus 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 track
explicitly of all assumptions and conclusions at each step of a proof,
replacing *modus ponens* (which eliminates an intermediate
formula) by a *cut rule* (which can be shown to be an
admissible rule (cf. Section 4.2) for the subsystem remaining when it
is omitted).

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

Both \(\mathbf{IPC}\) and \(\mathbf{IQC}\) satisfy *interpolation
theorems*, e.g.: If \(A\) and \(B\) are propositional formulas
having at least one proposition letter in common, and if \(A
\rightarrow B\) is provable in \(\mathbf{IPC}\), then there is a
formula \(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, for applications (e.g., to arithmetic) the equality symbol is generally treated as a distinguished predicate constant satisfying the axioms for an equivalence relation (reflexivity, symmetry and transitivity) and additional nonlogical axioms (e.g., the primitive recursive definitions of addition and multiplication). 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.

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

Intuitionistic (Heyting) arithmetic \(\mathbf{HA}\) and classical
(Peano) arithmetic \(\mathbf{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 \(x, y, z,\ldots\) (also used as
metavariables), the language \(L(\mathbf{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* \(\mathbf{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 \(\mathbf{HA}\) are those of first-order intuitionistic predicate logic \(\mathbf{IQC}\). The nonlogical axioms include the reflexive, symmetric and transitive properties 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 axiom characterizing \(0\) as the least natural number:

\[ \forall x\neg(S(x) = 0),\]the axiom characterizing \(S\) as a one-to-one function:

\[ \forall x\forall y(S(x) = S(y) \rightarrow x = y),\]the extensional equality axiom for \(S\):

\[\forall x\forall y (x = y \rightarrow S(x) = S(y));\]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));\] and multiplication: \[ \forall x (x \cdot 0 = 0),\] \[ \forall x \forall y (x \cdot S(y) = (x \cdot y) + x);\] and the (universal closure of the) schema of mathematical induction, for arbitrary formulas \(A(x)\):

\[ ( A(0) \oldand \forall x (A(x) \rightarrow A(S(x))) ) \rightarrow \forall x A(x).\]Extensional equality axioms for all function constants are derivable by mathematical induction from the equality axiom for \(S\) and the primitive 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 the quantifier-free formula \(S(x) \dot{-} y = 0\) if the symbol and primitive recursive defining equations for predecessor : \[ Pd(0) = 0,\] \[ \forall x (Pd(S(x)) = x)\] and cutoff subtraction : \[ \forall x (x \dot{-} 0 = x),\] \[ \forall x \forall y (x \dot{-} S(y) = Pd(x \dot{-} y))\] are present in the formalism. \(\mathbf{HA}\) proves the comparative law

\[\forall x \forall y (x \lt y \vee x = y \vee y \lt x)\]and an intuitionistic form of the least number principle, for arbitrary formulas \(A(x)\):

\[ \forall x[\forall y (y \lt x \rightarrow (A(y) \vee \neg A(y))) \rightarrow \\ (\exists y ((y \lt x \oldand A(y)) \oldand \forall z(z \lt y \rightarrow \neg A(z))) \vee \\ \forall y(y \lt x \rightarrow \neg A(y)))]. \]The hypothesis is needed because not all arithmetical formulas are decidable in \(\mathbf{HA}\). However, \(\forall x\forall y(x = y \vee \neg(x = y))\) can be proved directly by mathematical induction, and so

Prime formulas (and hence all *quantifier-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 are *bounded* are decidable
and stable in \(\mathbf{HA}\).

The collection \(\Delta_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 \(\mathbf{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, \(\forall x\) denotes a block of finitely many universal number quantifiers, and similarly \(\exists x\) denotes a block of finitely many existential number 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 x A(x)\) where \(A(x)\) is in \(\Psi_0\). For \(n \ge 2\), \(\Phi_n\) is the 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 x A(x)\) where \(A(x)\) is in \(\Phi_0\). For \(n \ge 2\), \(\Psi_n\) is the 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 \(\forall x 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 the list of logical axioms, i.e., by using classical instead of intuitionistic logic. The following results hold even in the fragments of \(\mathbf{HA}\) and \(\mathbf{PA}\) with the induction schema restricted 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-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 \(\mathbf{HA}\) is consistent then neither \(\mathbf{HA}\) nor \(\mathbf{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 \(\neg \neg 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 \(\neg \neg A\) is provable in intuitionistic predicate logic plus the “double negation shift” schema.

\[ \tag{DNS} \forall x\neg \neg B(x) \rightarrow \neg \neg \forall 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 \(\vee\) or
\(\exists)\), such that

- (I) Classical predicate logic proves \(A \leftrightarrow g(A)\).
- (II) Intuitionistic predicate logic proves \(g(A) \leftrightarrow \neg \neg 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 \(\neg\) and \(\oldand\)):

\[\begin{align*} g(P) &\text{ is } \neg \neg P, \text{ if } P \text{ is prime}.\\ g(A \oldand B) &\text{ is } g(A) \oldand g(B). \\ g(A \vee B) &\text{ is } \neg(\neg g(A) \oldand \neg g(B)). \\ g(A \rightarrow B) &\text{ is } g(A) \rightarrow g(B). \\ g(\neg A) &\text{ is } \neg g(A). \\ g(\forall xA(x)) &\text{ is }\forall x g(A(x)). \\ g(\exists xA(x)) &\text{ is } \neg \forall x\neg g(A(x)). \end{align*}\]For each formula \(A\), \(g(A)\) is provable intuitionistically if and only 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 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. In particular, Gödel’s
incompleteness theorems apply to \(\mathbf{HA}\) as well as to
\(\mathbf{PA}\).

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 (cf. Section 6.2 below). It follows that intuitionistic mathematics, which can only be expressed by using all the standard logical connectives and quantifiers, is consistent with a faithful translation of classical mathematics avoiding \(\vee\) and \(\exists\).

This is important because Brouwer’s intuitionistic analysis is
inconsistent with LEM. However, if \(A\) is any *negative*
formula (without \(\vee\) or \(\exists\)) then \(\neg \neg A
\rightarrow A\) is provable using intuitionistic logic. A
reconciliation of intuitionistic and classical analysis along these
lines, inspired by Kripke’s notion of choice sequence, is
suggested in Moschovakis [2017].

### 4.2 Admissible rules of intuitionistic logic and arithmetic

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

- (DP) If \(A \vee 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 \vee \neg P\) is not a
theorem if \(P\) is an atomic formula. Kleene [1945, 1952] proved that
intuitionistic 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 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 \(\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 also
\((\neg A \rightarrow B) \vee(\neg A \rightarrow C)\) is provable in
\(\mathbf{IPC}\). Harrop’s rule is not *derivable* in
\(\mathbf{IPC}\) because \((\neg A \rightarrow(B \vee C)) \rightarrow
(\neg A \rightarrow B) \vee (\neg A \rightarrow C)\) is not
intuitionistically provable. Another important example of an
admissible nonderivable rule of \(\mathbf{IPC}\) is Mints’s
rule:

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

The two-valued truth table interpretation of classical propositional logic \(\mathbf{CPC}\) gives rise to a simple proof that every admissible rule of \(\mathbf{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 \rightarrow P\) for the letters assigned “true” and \(P \oldand \neg 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’s 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 \(\mathbf{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 \(\mathbf{IPC}\) is decidable but has no finite
basis. Visser [2002] showed that his rules are also the admissible
propositional rules of \(\mathbf{HA}\), and of \(\mathbf{HA}\)
extended by Markov’s Principle MP (defined in Section 5.2
below). More recently, Jerabek [2008] found an independent basis for
the admissible rules of \(\mathbf{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 \(\mathbf{IQC}\), without individual or predicate 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 admissible
for all formal systems based on \(\mathbf{IQC}\); for example,
\(\mathbf{HA}\) evidently violates the rule just stated. Visser proved
in [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 the *predicate
logic* of \(\mathbf{HA}\) \(+\) MP (the set of sentences in the
language of \(\mathbf{IQC}\) all of whose uniform substitution
instances in the language of arithmetic are provable in
\(\mathbf{HA}\) \(+\) MP) is \(\Pi_2\) complete; Visser [2006]
extended this result to some constructively interesting consistent
extensions of \(\mathbf{HA}\) which are not contained in
\(\mathbf{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 \(\forall x(A(x) \vee \neg A(x)) \oldand \neg \forall x\neg A(x)\) is a theorem, so is \(\exists x A(x)\).

and the following **Independence-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 (\forall x A(x) \rightarrow B(y))\).

Both rules are also admissible for \(\mathbf{HA}\). The corresponding
implications (MP and IP respectively), which are not provable
intuitionistically, are verified by Gödel’s
“Dialectica” interpretation of \(\mathbf{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 \(\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 the
result that classical and intuitionistic arithmetic prove the same
formulas 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 decidable
in \(\mathbf{HA}\) and if \(\forall x \exists y A(x, y)\) is a closed
theorem of *classical* arithmetic \(\mathbf{PA}\), the
conclusion of the Church-Kleene Rule holds even in
*intuitionistic* arithmetic. For if \(\mathbf{HA}\) proves
\(\forall x \forall y (A(x,y) \vee \neg A(x,y))\) then by the
Church-Kleene Rule the characteristic function of \(A(x,y)\) has a
Gö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\) is
quantifier-free, and the adjacent existential quantifiers can be
contracted 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))\) is
a theorem, so is \(A \vee \forall x B(x)\)” (where \(x\) is not
free in \(A)\) is *not* admissible for \(\mathbf{HA}\), if
\(\mathbf{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 \(\mathbf{HA}\) of
\((0 = 1)\).” By intuitionistic logic with the decidability of
quantifier-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)\) then
by the disjunction property, \(\mathbf{HA}\) must prove either
\(\exists yG(y)\) or \(\forall x\neg G(x)\). The first case is
impossible, by the existence property with the consistency assumption
and the fact that \(\mathbf{HA}\) proves all true quantifier-free
sentences. But the second case is also impossible, by
Gödel’s second incompleteness theorem, since \(\forall
x\neg G(x)\) expresses the consistency of \(\mathbf{HA}\).

## 5. Basic Semantics

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

### 5.1 Kripke semantics for intuitionistic logic

A *Kripke structure* \(\mathbf{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 \le k'\), then \(D(k) \subseteq D(k')\). In
addition \(\mathbf{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 \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 \le k'\) 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\) ”) for compound sentences \(E\) of
\(L(k)\) inductively as follows:

\(k\) \(\vDash\) \((A \oldand B)\) | if \(k\) \(\vDash\) \(A\) and \(k\) \(\vDash\) \(B\). |

\(k\) \(\vDash\) \((A \vee B)\) | if \(k\) \(\vDash\) \(A\) or \(k\) \(\vDash\) \(B\). |

\(k\) \(\vDash\) \((A \rightarrow B)\) | if, for every \(k' \ge k\), if \(k'\) \(\vDash\) \(A\) then \(k'\) \(\vDash\) \(B\). |

\(k\) \(\vDash\) \(\neg A\) | if for no \(k' \ge k\) does \(k'\) \(\vDash\) \(A\). |

\(k\) \(\vDash\) \(\forall x A(x)\) | if for every \(k' \ge k\) and every \(d \in D(k')\), \(k'\) \(\vDash\) \(A(d)\). |

\(k\) \(\vDash\) \(\exists x A(x)\) | if for some \(d \in D(k)\), \(k\) \(\vDash\) \(A(d)\). |

Any such forcing relation is *consistent*:

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

and *monotone*:

If \(k \le k'\) and \(k\) \(\vDash\) \(A\) then \(k'\) \(\vDash\) \(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 \(\neg \forall x \neg P(x)
\rightarrow \exists x P(x)\) is intuitionistically unprovable, it is
enough to consider a Kripke structure with \(K = \{k, k'\},\) \(k \lt
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 \(\vDash\).

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 particularly 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 \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 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\le k'\), are relevant to deciding whether
or not \(k\) forces \(E\). Such considerations allow us to associate
effectively with each formula \(E\) of \(L(\mathbf{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
\(\mathbf{IPC}\) is recursively enumerable, we conclude that

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

The decidability of \(\mathbf{IPC}\) was first obtained by Gentzen in 1935. The undecidability of \(\mathbf{IQC}\) follows from the undecidability of \(\mathbf{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 \rightarrow B) \vee (B \rightarrow A)\) holds in every Kripke model with linearly ordered frame. Conversely, every propositional formula which is not derivable in \(\mathbf{IPC} + (A \rightarrow B) \vee (B \rightarrow A)\) has a Kripke countermodel with linearly ordered 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.

Kripke models and Beth models (which differ from Kripke models in detail, but are intuitionistically equivalent) 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]. However, there is no purely intuitionistic proof that every sentence which is valid in all Kripke and Beth models is provable in \(\mathbf{IQC}\). Following an observation by Gödel, Kreisel [1958] verified that the completeness of intuitionistic predicate logic for Beth semantics is equivalent to Markov’s Principle MP, which Brouwer rejected.

Moreover, Dyson and Kreisel [1961] showed that if \(\mathbf{IQC}\) is
*weakly* complete for Beth semantics (that is, if no unprovable
sentence holds in every Beth model) then the following consequence of
MP holds :
\[ \tag{GDK} \forall \alpha_{B(\alpha)} \neg \neg \exists x R(\alpha,
x) \rightarrow \neg \neg \forall \alpha_{B(\alpha)} \exists x
R(\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, which would justify the negative
interpretation of a form of Brouwer’s Fan Theorem, is weaker
than MP but unprovable in current systems of intuitionistic analysis.
Kreisel [1962] suggested that GDK may eventually be provable on the
basis of as yet undiscovered properties of intuitionistic
mathematics.

By modifying the definition of a Kripke model to allow “exploding nodes” which force every sentence, Veldman [1976] found a completeness proof using only intuitionistic logic, but he questioned whether Kripke models with exploding nodes were intuitionistically meaningful mathematical objects.

### 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 \(\mathbf{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 \oldand B\) | if \(e\) codes a pair \((f,g)\) such that \(f\) realizes \(A\) and \(g\) realizes \(B\). |

\(e\) realizes \(A \vee B\) | if \(e\) codes a pair \((f,g)\) such that if \(f = 0\) then \(g\) realizes \(A\), and if \(f \gt 0\) then \(g\) realizes \(B\). |

\(e\) realizes \(A\rightarrow B\) | if, whenever \(f\) realizes \(A\), then the \(e\)th partial recursive function is defined at \(f\) and its value realizes \(B\). |

\(e\) realizes \(\neg A\) | if no \(f\) realizes \(A\). |

\(e\) realizes \(\forall x A(x)\) | if, for every \(n\), the \(e\)th partial recursive function is defined at \(n\) and its value realizes \(A(\mathbf{n})\). |

\(e\) realizes \(\exists x A(x)\) | if \(e\) codes a pair \((n,g)\) and \(g\) realizes \(A(\mathbf{n})\). |

An arbitrary formula is realizable if some number realizes its universal closure. Observe that not both \(A\) and \(\neg A\) are realizable, 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. For
example, *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 an argument which uses Markov’s Principle informally. But realizability is a fundamentally nonclassical interpretation. In \(\mathbf{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, \(\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 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.

Nelson’s Theorem establishes the unprovability in
\(\mathbf{IQC}\) of some theorems of classical predicate logic. If, to
each \(n\)-place predicate letter \(P(\ldots )\), a formula \(f(P)\)
of \(L(\mathbf{HA})\) with \(n\) free variables is assigned, and if
the 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
an *arithmetical substitution instance* of \(A\). As an
example, if a formula of \(L(\mathbf{HA})\) expressing “\(x\)
codes a proof in \(\mathbf{HA}\) of the formula with code \(y\)”
is assigned to \(P(x,y)\), the resulting arithmetical substitution
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))\) is not provable in
\(\mathbf{IQC}\).

De Jongh [1970] combined realizability with Kripke modeling to show that intuitionistic propositional logic \(\mathbf{IPC}\) and a fragment of \(\mathbf{IQC}\) are arithmetically complete for \(\mathbf{HA}\). A uniform assignment of simple existential formulas to predicate letters suffices to prove

**De Jongh’s Theorem (for IPC) [1970]**

If a propositional formula \(A\) of the language \(L\) is not provable in
\(\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 need realizability; cf. Smorynski [1973]. As an example, Rosser’s form 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 semantical proof also established that every intuitionistically unprovable predicate formula of a restricted kind has an arithmetical substitution instance which is unprovable in \(\mathbf{HA}\). Using a syntactic method, Daniel Leivant [1979] extended de Jongh’s Theorem 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 a simpler proof of the full theorem, using abstract realizability with Beth models instead of Kripke models.

Without claiming that number-realizability coincides with intuitionistic arithmetical truth, Nelson observed that for each formula \(A\) of \(L(\mathbf{HA})\) the predicate “\(y\) realizes \(A\)” can be expressed in \(\mathbf{HA}\) by another formula (abbreviated “\(y \realizesrel A\)”), and the schema \(A \leftrightarrow \exists y (y \realizesrel A)\) is consistent with \(\mathbf{HA}\). Troelstra [1973] showed that \(\mathbf{HA}\) \(+\) \((A \leftrightarrow \exists y (y \realizesrel A))\) is equivalent to \(\mathbf{HA}\) \(+\) ECT, where ECT is a strengthened form of CT. In \(\mathbf{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 \realizesrel A)\) has an equivalent “classical” prenex form \(A'(y)\) consisting of a quantifier-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 kind of 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 encyclopedia treating intuitionistic logic in various contexts, but a general treatment of weaker and stronger propositional and predicate logics appears to be lacking. Many such logics have been identified and studied. Here are a few examples.

A *subintuitionistic 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\), which
is named after its discoverers Rieger and Nishimura [1960].
\(\mathbf{RN}\) is characterized by the *Rieger-Nishimura
lattice* of infinitely many nonequivalent formulas \(F_n\) such
that every formula whose only propositional variable is \(P\) is
equivalent by intuitionistic logic to some \(F_n\). Nishimura’s
version is

In \(\mathbf{RN}\) neither \(F_{2 n + 1}\) nor \(F_{2 n + 2}\) implies the 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 connectives
restrict the language and incidentally the logic, since the
intuitionistic connectives \(\oldand\), \(\vee\), \(\rightarrow\),
\(\neg\) are logically independent over \(\mathbf{IPC}\). Rose [1953]
proved that the *implicationless fragment* (without
\(\rightarrow\)) is complete with respect to realizability, in the
sense that if every arithmetical substitution instance of a
propositional formula \(E\) without \(\rightarrow\) is
(number)-realizable then \(E\) is a theorem of \(\mathbf{IPC}\). This
result 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. Every arithmetical substitution instance of \(F\) is realizable (using classical 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 logic
by deleting *ex falso*. Kolmogorov [1925] showed that this
fragment already contains a negative interpretation of classical logic
retaining both quantifiers, cf. Leivant [1985]. Minimal logic does
prove the special case \(\neg A \rightarrow (A \rightarrow \neg B)\)
of *ex falso* for negations. Colacito, de Jongh and Vardas
[2017] study various *subminimal logics*, each weaker than
\(\mathbf{ML}\).

Griss contested Brouwer’s use of negation, objecting to both the
law of contradiction and *ex falso*. It is worth noting that
negation 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\). Then *ex falso* can be stated as \(0 = 1
\rightarrow A\), and the law of contradiction is provable from the
remaining axioms of \(\mathbf{H}\).

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

One of the simplest intermediate propositional logics is the Gödel-Dummett logic \(\mathbf{LC}\), obtained by adding to \(\mathbf{IPC}\) the schema \((A \rightarrow B) \vee (B \rightarrow 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 \(\mathbf{IPC}\) has no finite truth-table interpretation. For each 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}\) is valid on all and only those linearly ordered Kripke frames with no more than \(n\) nodes.

The Jankov logic \(\mathbf{KC}\), which adds to \(\mathbf{IPC}\) the
principle of *testability* \(\neg A \vee \neg \neg A\),
obviously does not have the disjunction property. The Kreisel-Putnam
logic \(\mathbf{KP}\), obtained by adding to \(\mathbf{IPC}\) the
schema \((\neg A \rightarrow B \vee C) \rightarrow((\neg A \rightarrow
B) \vee (\neg A \rightarrow C))\), has the disjunction property but
does not satisfy all the Visser rules. The intermediate logic obtained
by adding the schema \(((\neg \neg D \rightarrow D) \rightarrow(D \vee
\neg D)) \rightarrow (\neg \neg D \vee \neg D)\), corresponding to
Rose’s counterexample, to \(\mathbf{IPC}\) also has the
disjunction property. Iemhoff [2005] proved that \(\mathbf{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 \(\mathbf{IPC}\) and some intermediate logics.
Goudsmit [2015] is a thorough study of the admissible rules of
intermediate logics, with a comprehensive bibliography.

An intermediate propositional logic \(\mathbf{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
\(\mathbf{L}\). Many intermediate logics, including \(\mathbf{LC}\)
and \(\mathbf{KP}\), have this property. Jankov [1968] used an
infinite sequence of finite rooted Kripke frames to prove that there
are continuum many intermediate logics. De Jongh, Verbrugge and Visser
[2009] proved that every intermediate logic \(\mathbf{L}\) with the
finite frame property is the *propositional logic* of
\(\mathbf{HA(L)}\), that is, the class of all formulas in the language
of \(\mathbf{IPC}\) all of whose arithmetical substitution instances
are provable in the logical extension of \(\mathbf{HA}\) by
\(\mathbf{L}\).

An intermediate propositional logic \(\mathbf{L}\) is *structurally
complete* if every rule which is admissible for \(\mathbf{L}\) is
derivable in \(\mathbf{L}\), and *hereditarily structurally
complete* if every intermediate logic extending \(\mathbf{L}\) is
also structurally complete. Every intermediate logic \(\mathbf{L}\)
has a *structural 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 not
structurally complete, their structural completions are hereditarily
structurally complete. For these results and more, see Citkin [2016,
Other Internet Resources].

Some *intermediate 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 the
*intuitionistic logic of constant domains* \(\mathbf{CD}\)
obtained by adding to \(\mathbf{IQC}\) the schema \(\forall x (A \vee
B(x)) \rightarrow (A \vee \forall 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 \(\mathbf{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 \(\mathbf{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.

Alternatives to Kripke and Beth semantics for intuitionistic
propositional and predicate logic include the topological
interpretation of Stone [1937], Tarski [1938] and Mostowski [1948]
(cf. Rasiowa and Sikorski [1963], Rasiowa [1974]), which was extended
to intuitionistic analysis by Scott [1968] and Krol [1978]. M. Hyland
[1982] defined the effective topos *Eff* and proved that its
logic is intuitionistic. For a very informative discussion of
semantics 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 intuitionistic
arithmetic 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 language
of 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 closed
theorem of \(\mathbf{HA}\), then \(B_D (F, x)\) is provable for some
term \(F\) in Gödel’s theory \(\mathbf{T}\) of
“primitive recursive” functionals of higher type. The
translation from \(B\) to \(B^D\) 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
\(\mathbf{T}\) are precisely the provably recursive functions of
\(\mathbf{HA}\) (and of \(\mathbf{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, in
Avigad and Feferman [1998], and in Ferreira [2008].

While \(\mathbf{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 \(\mathbf{FIM}\) of the intuitionistic theory of sequences (“intuitionistic analysis”), changes the interpretation of arithmetical formulas; for example, \(\neg \neg \forall x (A(x) \vee \neg 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 \(\mathbf{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 \(\mathbf{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 \(\mathbf{FIM}\), but Vesley [1970] found an
alternative principle (*Vesley’s Schema* VS) which can
consistently be added to \(\mathbf{FIM}\) and implies all the
counterexamples for which Brouwer required a creating subject. Krol
[1978] 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
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] (with corrections) stand out as the most comprehensive studies of intuitionistic and semi-intuitionistic formal theories, using both constructive and classical methods, with useful bibliographies. Troelstra and Schwichtenberg [2000] presents the proof theory of classical, intuitionistic and minimal logic in parallel, focusing on sequent systems. 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. - Benacerraf, P. and Hilary Putnam (eds.), 1983,
*Philosophy of Mathematics: Selected Readings*, 2nd Edition, Cambridge: Cambridge University Press. - Beth, E. W., 1956, “Semantic construction of intuitionistic
logic,”
*Koninklijke Nederlandse Akad. von Wettenscappen*, 19(11): 357–388. - Brouwer, L. E. J., 1907, “On the Foundations of Mathematics,” Thesis, Amsterdam; English translation in Heyting (ed.) 1975: 11–101.
- –––, 1908, “The Unreliability of the Logical Principles,” English translation in Heyting (ed.) 1975: 107–111.
- –––, 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. - –––, 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.
- –––, 1923C, “Intuitionistische Zerlegung
mathematischer Grundbegriffe,”
*Jahresbericht der Deutschen Mathematiker-Vereinigung*, 33 (1925): 251-256; reprinted in Heyting (ed.) 1975, 275–280. - –––, 1927, “Intuitionistic reflections on formalism,” originally published in 1927, English translation in van Heijenoort (ed.) 1967: 490–492.
- –––, 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. - Colacito, A., de Jongh, D. and Vargas, A., 2017, “Subminimal
Negation”,
*Soft Computing*, 21: 165–164. - 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.
- Dyson, V. and Kreisel, G., 1961, ,
*Analysis of Beth’s semantic construction of intuitionistic logic*, Technical Report No. 3, Stanford: Applied Mathematics and Statistics Laboratory, Stanford University. - Ferreira, F., 2008, “A most artistic package of a jumble of
ideas,”
*Dialectica*, 62: 205–222. - 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,”
*Mathematische Zeitschrift*, 39: 176–210, 405–431. - Ghilardi, S., 1999, “Unification in intuitionistic
logic,”
*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 de la classe des sciences*, 5 (15): 183–188. - Gödel, K., 1932, “Zum intuitionistischen
Aussagenkalkül,”
*Anzeiger der Akademie der Wissenschaften in Wien*, 69: 65–66. Reproduced and translated with an introductory note by A. S. Troelstra in Gödel 1986: 222–225. - –––, 1933e, “Zur intuitionistischen
Arithmetik und Zahlentheorie,”
*Ergebnisse eines mathematischen Kolloquiums*, 4: 34–38. - –––, 1933f, “Eine Interpretation des intuitionistischen Aussagenkalküls,” reproduced and translated with an introductory note by A. S. Troelstra in Gödel 1986: 296–304.
- –––, 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. - –––, 1986,
*Collected Works*, Vol. I, S. Feferman*et al*. (eds.), Oxford: Oxford University Press. - –––, 1990,
*Collected Works*, Vol. II, S. Feferman*et al*. (eds.), Oxford: Oxford University Press. - Goudsmit, J. P., 2015,
*Intuitionistic Rules: Admissible Rules of Intermediate Logics*, Ph.D. dissertation, University of Utrecht. - Harrop R., 1960, “Concerning formulas of the types \(A
\rightarrow B \vee C, A \rightarrow (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. - –––, 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.
- Hyland, J. M. E., 1982, “The effective topos,” in Troelstra and van Dalen (ed.) 1982: 165–216.
- Iemhoff, R., 2001, “On the admissible rules of
intuitionistic propositional logic,”
*Journal of Symbolic Logic*, 66: 281–294. - –––, 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. - Jankov, V. A., 1968, “The construction of a sequence of
strongly independent superintuitionistic propositional
calculii,”
*Soviet Math. Doklady*, 9: 801–807. - 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. - –––, 1952,
*Introduction to Metamathematics*, Princeton: Van Nostrand. - –––, 1962, “Disjunction and existence
under 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 of intuitionistic mathematics,” in Bar-Hillel (ed.) 1965: 31–44.
- –––, 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., 1958, “Elementary completeness properties of
intuitionistic logic with a note on negations of prenex
formulas,”
*Journal of Symbolic Logic*, 23: 317–330. - –––, 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.
- Krol, M., 1978, “A topological model of intuitionistic
analysis with Kripke’s Schema,”
*Zeitschrift für Math. Logik und Grundlagen der Math.*, 24: 427–436. - Leivant, D., 1979, “Maximality of Intuitionistic Logic,” Mathematical Centre Tracts 73, Mathematisch Centrum, Amsterdam.
- –––, 1985, “Syntactic translations and provably
recursive functions,”
*Journal of Symbolic Logic*, 50: 682–688. - 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, “CT\(_0\) is stronger than
CT\(_0\)!,”
*Proceedings of the American Mathematical Society*, 73(1): 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. - –––, 2003, “Classical and constructive
hierarchies in extended intuitionistic analysis,”
*Journal of Symbolic Logic*, 68: 1015–1043. - –––, 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. - –––, 2017, “Intuitionistic analysis and
the end of time,”
*Bulletin of Symbolic Logic*, 23: 279–295. - Nelson, D., 1947, “Recursive functions and intuitionistic
number theory,”
*Transactions of the American Mathematical Society*, 61: 307–368. - 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. - –––, 2002, “Realizability: a historical
essay,”
*Mathematical Structures in Computer Science*, 12: 239–263. - –––, 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. - Rasiowa, H., 1974,
*Algebraic Appriach to Non-Classical Logics*, Amsterdam: North-Holland. - Rasiowa, H. and Sikorski, R., 1963,
*The Mathematics of Metamathematics*, Warsaw: Panstwowe Wydawnictwo Naukowe. - 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. - –––, 2012, “From the weak to the strong
existence property,”
*Annals of Pure and Applied 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. - Scott, D., 1968, “Extending the topological interpretation
to intuitionistic analysis,”
*Compositio Mathematica*, 20: 194-210. - 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. - Stone, M. H., 1937, “Topological representation of
distributive lattices and Brouwerian logics”,
*Casopis Pest. Mat. Fys.*, 67: 1–25. - Tarski, A., 1938, “Der Aussagenkalkül und die
Topologie”,
*Fundamenta Mathematicae*, 31: 103–104. - 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. - –––, 1998, “Realizability,” Chapter VI of Buss (ed.), 1998: 407–473.
- –––, Introductory note to 1958 and 1972, in Gödel, 1990: 217–241.
- 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. and Schwichtenberg, H., 2000,
*Basic Proof Theory*(Cambridge Tracts in Theoretical Computer Science: Volume 43), 2nd edition, Cambridge: Cambridge University Press. - Troelstra, A. S. and van Dalen, D., 1988,
*Constructivism in Mathematics: An Introduction*, 2 volumes, Amsterdam: North-Holland Publishing. [See also the*Corrections*, in Other Internet Resources.] - Troelstra, A. S. and van Dalen, D. (eds.), 1982,
*The L. E. J. Brouwer Centenary Symposium*, Amsterdam: North-Holland Publishing. - Veldman, W., 1976, “An intuitionistic completeness theorem
for intuitionistic predicate logic,”
*Journal of Symbolic Logic*, 41: 159–166. - –––, 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. - –––, 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. - –––, 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. - –––, 2002, “Substitutions of
\(\Sigma^{0}_1\) sentences: explorations between intuitionistic
propositional logic and intuitionistic arithmetic,”
*Annals of Pure and Applied Logic*, 114: 227–271. - –––, 2006, “Predicate logics of
constructive arithmetical theories,”
*Journal of Symbolic Logic*, 72: 1311–1326.

## Academic Tools

How to cite this entry. Preview the PDF version of this entry at the Friends of the SEP Society. Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO). Enhanced bibliography for this entry at PhilPapers, 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.
- Mints, G., Olkhovikov, G. and Urquhart, A., 2012, “Failure of interpolation in the intuitionistic logic of constant domains,” manuscript, arXiv.org.
- Troelstra, A. S. and J. R. Moschovakis, 2018,
Corrections
to A. S. Troelstra and D. van Dalen, 1988,
*Constructivism in Mathematics*. - Realizability Bibliography, maintained by Lars Birkedal.
- van Oosten 2000, and other preprints related to realizability, maintained by Jaap van Oosten.

### Acknowledgments

Over the years, many readers have offered corrections and
improvements. This revision owes special thanks to Ed Zalta, who
gently pointed out that the online format invites full exposition
rather than efficient compression of facts, and to the wise and
conscientious referee of an earlier draft. I am still grateful to
Edward Horton (for pointing out that replacing *ex falso* by
the LEM in the axioms for \(\mathbf{IPC}\) does not yield all of
\(\mathbf{CPC}\), and for providing the correct substitutions) and to
all the other readers who have corrected errors in earlier editions. I
thank Satoru Niki for bringing subminimal logics to my attention, Dick de Jongh for continuing to ask interesting questions about
intuitionistic logic, and Daniel Leivant for pointing out an error of attribution (now corrected).