# Intuitionistic Logic

*First published Wed Sep 1, 1999; substantive revision Tue Feb 6, 2007*

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

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

Brouwer rejected formalism *per se* but admitted the
potential usefulness of formulating general logical principles
expressing intuitionistically correct constructions, such as *modus
ponens*. Formal systems for intuitionistic propositional and
predicate logic and arithmetic were developed by Heyting [1930],
Gentzen [1935] and Kleene [1952]. Gödel [1933] proved the
equiconsistency of intuitionistic and classical theories. Kripke [1965]
provided a semantics with respect to which intuitionistic logic is
correct and complete.

- 1. Rejection of
*Tertium Non Datur* - 2. Intuitionistic First-Order Predicate Logic
- 3. Intuitionistic Number Theory (Heyting Arithmetic)
- 4. Basic Proof Theory
- 5. Basic Semantics
- 6. Advanced Topics and Recommended Reading
- Bibliography
- 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 (LEM): (*A*
¬*A*), but with the law of
contradiction (¬*A* → (*A* → *B*)).
Brouwer [1908] observed that LEM was abstracted from finite situations,
then extended without justification to statements about infinite
collections. For example, if *x*, *y* range over the
natural numbers 0, 1, 2, … and *B*(*x*)
abbreviates the property (there is a *y* > *x* such
that both *y* and *y*+2 are prime numbers), then we have
no general method for deciding whether *B*(*x*) is true
or false for arbitrary *x*, so
∀*x*(*B*(*x*)
¬*B*(*x*)) cannot be asserted in the
present state of our knowledge. And if *A* abbreviates the
statement ∀*x**B*(*x*), then (*A*
¬*A*) cannot be asserted
because neither *A* nor (¬*A*) has yet been
proved.

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

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

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

On the other hand,

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

## 2. Intuitionistic First-Order Predicate Logic

Formalized intuitionistic logic is naturally motivated by the
informal Brouwer-Heyting-Kolmogorov explication of intuitionistic
truth, outlined in Section 2 of the article on Constructive Mathematics
in this Encyclopedia. The constructive independence of the logical
operations &,
,
→, ¬,
∀, ∃ contrasts with the classical situation, where e.g.,
(*A*
*B*) is equivalent to
¬(¬*A* & ¬*B*), and
∃*x**A*(*x*) is equivalent to
¬∀*x*¬*A*(*x*). From the B-H-K
viewpoint, a sentence of the form (*A*
*B*) asserts that either a proof of *A*, or a
proof of *B*, has been constructed; while ¬(¬*A*
& ¬*B*) asserts that an algorithm has been constructed
which would effectively convert any pair of constructions proving
¬*A* and ¬*B* respectively, into a proof of a
known contradiction.

Following is a Hilbert-style formalism **H**, from
Kleene [1952], for intuitionistic first-order predicate logic
**IQC**. The language *L* has predicate letters
*P*, *Q*(.),… of all arities and individual
variables *a*, *b*, *c*,… (with or without
subscripts 1,2,…), as well as symbols &,
,
→, ¬, ∀, ∃ for the logical
connectives and quantifiers, and parentheses (, ). The *prime
formulas* of *L* are expressions such as *P*,
*Q*(*a*), *R*(*a*, *b*, *a*)
where *P*, *Q*(.), *R*(…) are 0-ary, 1-ary
and 3-ary predicate letters respectively; that is, the result of
filling each blank in a predicate letter by an individual variable
symbol is a prime formula. The *(well-formed) formulas* of
*L* are defined inductively as follows.

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

In general, we use *A*, *B*, *C* as
metavariables for well-formed formulas and
*x*, *y*, *z* as metavariables for individual
variables. Anticipating applications (for example to intuitionistic
arithmetic) we use *s*, *t* as metavariables for
*terms*; in the case of pure predicate logic, terms are simply
individual variables. An occurrence of a variable *x* in a
formula *A* is *bound* if it is within the scope of a
quantifier ∀*x* or ∃*x*, otherwise
*free*. Intuitionistically as classically, "(*A* ↔
*B*)" abbreviates "(*A* → *B*) &
(*B* → *A*)," and parentheses are omitted when this
causes no confusion.

There are three rules of inference:

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

The axioms are all formulas of the following forms, where in the
last two schemas the subformula *A*(*t*) is the result of
substituting an occurrence of the term *t* for every free
occurrence of *x* in *A*(*x*), and no variable
free in *t* becomes bound in *A*(*t*) as a result
of the substitution.

*A*→ (*B*→*A*).- (
*A*→*B*) → ((*A*→ (*B*→*C*)) → (*A*→*C*)). *A*→ (*B*→*A*&*B*).*A*&*B*→*A*.*A*&*B*→*B*.*A*→*A**B*.*B*→*A**B*.- (
*A*→*C*) → ((*B*→*C*) → (*A**B*→*C*)). - (
*A*→*B*) → ((*A*→ ¬*B*) → ¬*A*). - ¬
*A*→ (*A*→*B*). - ∀
*x**A*(*x*) →*A*(*t*). *A*(*t*) → ∃*x**A*(*x*).

A *proof* is any finite sequence of formulas, each of which
is an axiom or an immediate consequence, by a rule of inference, of
(one or two) preceding formulas of the sequence. Any proof is said to
*prove* its last formula, which is called a *theorem* or
*provable formula* of first-order intuitionistic predicate
logic. A *derivation of* a formula *E* *from* a
collection *F* of *assumptions* is any sequence of
formulas, each of which belongs to *F* or is an axiom or an
immediate consequence, by a rule of inference, of preceding formulas of
the sequence, such that *E* is the last formula of the sequence.
If such a derivation exists, we say *E* is *derivable
from* *F*.

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

If, in the given list of axiom schemas for intuitionistic propositional or first-order predicate logic, the law of contradiction:

¬A→ (A→B).

is replaced by the law of double negation:

¬¬A→A.

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

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

(INE)IfFentailsAandFentails ¬A, thenFentailsB.

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

Deduction Theorem: IfBis derivable fromAand possibly other formulasF, with all variables free inAheld constant in the derivation (that is, without using the second or third rule of inference on any variablexoccurring free inA, unless the assumptionAdoes not occur in the derivation before the inference in question), then (A→B) is derivable fromF.

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

1.A→ (A→A)

2. (A→ (A→A)) → ((A→ ((A→A) →A)) → (A→A))

3. (A→ ((A→A) →A)) → (A→A)

4.A→ ((A→A) →A)

5.A→A

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

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

1. ∀Here 1, 2 and 5 are axioms; 4 comes from 2 and 3 byx¬A(x) → ¬A(x)

2.A(x) → (∀x¬A(x) →A(x))

3.A(x) (assumption)

4. ∀x¬A(x) →A(x)

5. (∀x¬A(x) →A(x)) → ((∀x¬A(x) → ¬A(x)) → ¬∀x¬A(x))

6. (∀x¬A(x) → ¬A(x)) → ¬∀x¬A(x)

7. ¬∀x¬A(x))

*modus ponens*; and 6 and 7 come from earlier lines by

*modus ponens*; so no variables have been varied. The Deduction Theorem tells us there is a proof

*P*in

**IQC**of (

*A*(

*x*) → ¬∀x¬

*A*(

*x*)), and one application of ∃-

*introduction*converts

*P*into a proof of ∃

*x*

*A*(

*x*) → ¬∀

*x*¬

*A*(

*x*). The converse is not provable in

**IQC**, as shown in Section 5.1 below.

## 3. Intuitionistic Number Theory (Heyting Arithmetic)

Intuitionistic (Heyting) arithmetic**HA**and classical (Peano) arithmetic

**PA**share the same first-order language and the same non-logical axioms; only the logic is different. In addition to the logical connectives, quantifiers and parentheses and the individual variables

*a*,

*b*,

*c*, … (with metavariables

*x*,

*y*,

*z*as usual), the language

*L*(

**HA**) of arithmetic has a binary predicate symbol =, individual constant 0, unary function constant

*S*, and finitely or countably infinitely many additional constants for primitive recursive functions including addition and multiplication; the precise choice is a matter of taste and convenience.

*Terms*are built from variables and 0 using the function constants; in particular, each natural number

*n*is expressed in the language by the

*numeral*

**n**obtained by applying

*S*

*n*times to 0 (e.g.,

*S*(

*S*(0)) is the numeral for 2).

*Prime formulas*are of the form (

*s*=

*t*) where

*s*,

*t*are terms, and

*compound formulas*are obtained from these as usual.

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

- ∀
*x*¬(*S*(*x*) = 0), - ∀
*x*∀*y*(*S*(*x*) =*S*(*y*) →*x*=*y*),

the extensional equality axiom for S:

- ∀
*x*∀*y*(*x*=*y*→*S*(*x*) =*S*(*y*)),

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

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

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

For theories **T** based on intuitionistic logic, if
*E* is an arbitrary formula of *L*(**T**)
then by definition

- E is
*decidable in***T**if and only if**T**proves (*E*¬*E*). *E*is*stable in***T**if and only if**T**proves (¬¬*E*→*E*).

Decidability implies stability, but not conversely; in
**IPC**, the negation of any prime formula is stable but
not decidable. However, using mathematical induction in
**HA**, one can prove
∀*x*∀*y*(*x* = *y*
¬(*x* = *y*)), and so

- Prime formulas (and hence
quantifier-freeformulas) are decidable and stable inHA.

Peano arithmetic **PA** comes from Heyting arithmetic
**HA** by adding LEM or (¬¬*A* →
*A*) to the list of logical axioms, i.e., by using classical
instead of intuitionistic logic. The two theories are
proof-theoretically equivalent, as will be shown in the next section.
Each is capable of (numeralwise) expressing its own proof predicate. By
Gödel's famous Incompleteness Theorem, if **HA** is
consistent then neither **HA** nor **PA** can
prove its own consistency.

## 4. Basic Proof Theory

### 4.1 Translating classical into intuitionistic logic

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

Glivenko's Theorem: An arbitrary propositional formulaAis classically provable, if and only if ¬¬Ais intuitionistically provable.

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

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

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

(I)Classical predicate logic provesA↔(gA).

(II)Intuitionistic predicate logic provesg(A) ↔ ¬¬g(A).

(III)If classical predicate logic provesA, then intuitionistic predicate logic provesg(A).

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

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

For each formlula *A*, *g*(*A*) is provable
intuitionistically if and only if *A* is provable classically.
In particular, if (*B* & ¬*B*) were classically
provable for some formula *B*, then (*g*(*B*)
& ¬*g*(*B*)) (which is *g*(*B*
& ¬*B*)) would in turn be provable intuitionistically.
Hence

(IV)Classical and intuitionistic predicate logic are equiconsistent.

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

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

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

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

### 4.2 Admissible rules of intuitionistic logic

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

(DP)If (AB) is a theorem, thenAis a theorem orBis a theorem.

Gentzen [1935] established the disjunction property for closed formulas
of intuitionistic predicate logic. From this it follows that if
intuitionistic logic is consistent, then (*P*
¬*P*) is not a theorem if *P* is prime.
Kleene [1945, 1952] proved that intuitionistic first-order number
theory also has the related (cf. Friedman [1975]) *existence
property*:

(ED)If ∃xA(x) is a closed theorem, then for some closed termt,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

(¬A→ (BC)) / (¬A→B) (¬A→C)

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

((A→B) →AC) / ((A→B) →A) ((A→B) →C).

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

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

An *intermediate propositional logic* is any consistent
collection of propositional formulas containing all the axioms of
**IPC** and closed under *modus ponens* and
substitution of arbitrary formulas for proposition letters. Each
intermediate propositional logic is contained in **CPC**.
Gödel [1933] used an infinite sequence of successively stronger
intermediate logics to show that **IPC** has no finite
truth-table interpretation. Iemhoff [2005] proved that
**IPC** is the only intermediate logic with the
disjunction property which is closed under all the Visser rules.

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

∀x(A(x) ¬A(x)) & ¬∀x¬A(x) / ∃xA(x)

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

∀x(A(x) ¬A(x)) & (∀xA(x) → ∃yB(y)) / ∃y(∀xA(x) →B(y)).

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

If ∀x∃yA(x,y) is a closed theorem ofHAthen there is a numbernsuch that, provably inHA, the partial recursive function with Gödel numbernis total and maps eachxto aysatisfyingA(x,y) (and moreoverA(x,y) is provable, wherexis the numeral for the natural numberxandyis the numeral fory).

Combining Markov's Rule with the negative translation gives the result
that classical and intuitionistic arithmetic prove the same formulas of
the form ∀*x* ∃*y*
*A*(*x*, *y*) where
*A*(*x*, *y*) is quantifier-free. In general, if
*A*(*x*, *y*) is provably decidable in
**HA** and if ∀*x* ∃*y*
*A*(*x*, *y*) is a closed theorem of
*classical* arithmetic, the conclusion of the Church-Kleene Rule
holds even in *intuitionistic* arithmetic.

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

## 5. Basic Semantics

### 5.1 Kripke semantics for intuitionistic logic

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

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

For each node *k* let *L*(*k*) be the language
extending *L* by new constants for all the elements of
*D*(*k*). To each node *k* and each *0*-ary
predicate letter (each proposition letter) *P*, either assign
*f*(*P*, *k*) = *true* or leave
*f*(*P*, *k*) undefined, consistent with the
requirement that if *k* ≤ *k*′ and
*f*(*P*, *k*) = *true* then
*f*(*P*, *k*′) = *true* also. Say
that

k forcesPif and only iff(P,k) =true.

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

k forcesQ(d) if and only if (_{0},…,d_{n}d) ∈_{o},…,d_{n}T(Q,k).

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

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

Any such forcing relation is *consistent* and *monotone*:

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

**Kripke's Soundness and Completeness Theorems** establish
that a sentence of *L* is provable in intuitionistic predicate
logic if and only if it is forced by every node of every Kripke
structure. Thus to show that
(¬∀*x*¬*P*(*x*) →
∃*x**P*(*x*)) is intuitionistically
unprovable, it is enough to consider a Kripke structure with *K*
= {*k*, *k*′}, *k* < *k*′,
*D*(*k*) = *D*(*k*′) = {0},
*T*(*P*, *k*) empty but
*T*(*P*, *k*′) = {0}. And to show the
converse is intuitionistically provable (without actually exhibiting a
proof), one only needs the consistency and monotonicity properties of
arbitrary Kripke models, with the definition of *forcing*.

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

Propositional Kripke semantics is particulary simple, since an
arbitrary propositional formula is intuitionistically provable if and
only if it is forced by the root of every Kripke model whose
*frame* (the set *K* of nodes together with their
partial ordering) is a finite tree with a least element (the
*root*). Each terminal node or *leaf* of a Kripke model
is a classical model, because a leaf forces every formula or its
negation. Only those proposition letters which occur in a formula
*E*, and only those nodes *k*′ such that
*k*≤*k*′, are relevant to deciding whether or
not *k* forces *E*. Such considerations allow us to
associate effectively with each formula *E* of
*L*(**IPC**) a finite class of finite Kripke
structures which will include a countermodel to *E* if one
exists. Since the class of all theorems of **IPC** is
recursively enumerable, we conclude that

IPCis effectively decidable. There is a recursive procedure which determines, for each propositional formulaE, whether or notEis a theorem ofIPC, concluding with either a proof ofEor a Kripke countermodel.

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

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

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

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

### 5.2 Realizability semantics for Heyting arithmetic

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

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

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

Nelson's Theorem[1947]. IfAis derivable inHAfrom realizable formulasF, thenAis realizable.

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

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

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

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

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

De Jongh's Theorem.If a sentenceAof the languageLis not provable inIQC, then some arithmetical substitution instance ofAis not provable inHA.

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

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

While **HA** is a proper part of classical arithmetic,
the intuitionistic attitude toward mathematical objects results in a
theory of real numbers (INT in the article on
Constructive Mathematics)
diverging from the classical. Kleene's function-realizability,
developed to prove the consistency of INT, changes the interpretation
of arithmetical formulas. For example, ¬¬∀*x*
(*A*(*x*)
¬*A*(*x*)) is function-realizable for every
arithmetical formula *A*(*x*). In the language of
analysis, Markov's Principle and the negative translation of the
countable axiom of choice are among the many non-intuitionistic
principles which are function-realizable (by classical arguments) and
hence consistent with INT; cf. Kleene [1965], Vesley [1972] and
Moschovakis [2003]. Abstract and concrete 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
[2000]. Variations of the basic notions are useful for establishing
relative independence of the nonlogical axioms in theories based on
intuitionistic logic.

## 6. Advanced Topics and Recommended Reading

The article on
L. E. J. Brouwer
in this
Encyclopedia 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.

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.

An alternative to realizability semantics for intuitionistic
arithmetic is Gödel's [1958] "Dialectica" interpretation, which
associates with each formula *B* of
*L*(**HA**) a quantifier-free formula
*B*_{D} in the language of intuitionistic
arithmetic of all finite types. The *"Dialectica"
interpretation* of *B*, call it
*B*^{D}, is ∃*Y*∀*x*
*B*_{D}(*Y*, *x*). If *B*
is a closed theorem of **HA**, then
*B*_{D}(*F*, *x*) is provable for
some term *F* in Gödel's theory **T** of
"primitive recursive" functionals of higher type. The translation from
*B* to *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 **T** are precisely the provably
recursive functions of **HA** (and of
**PA**). The interpretation was extended to analysis by
Spector [1962]; cf. Howard [1973]. Clear expositions, and additional
references, are to be found in Troelstra's introduction to the English
translation in Gödel [1990] of the original *Dialectica*
article, and in Avigad and Feferman [1998].

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

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

## Bibliography

- Avigad, J. and Feferman, S., 1998, "Gödel's functional ("Dialectica") interpretation," Chapter V of S. Buss, ed., 1998: 337-405.
- Bar-Hillel, Y., ed., 1965,
*Logic, Methodology and Philosophy of Science*, North Holland Publishing, Amsterdam. - Beeson, M. J., 1985,
*Foundations of Constructive Mathematics*, Springer, Berlin. - Benecerraf, P. and Hilary Putnam, eds., 1983,
*Philosophy of Mathematics: Selected Readings*, 2nd Edition, Cambridge University Press, Cambridge. - Brouwer, L. E. J., 1907, "On the Foundations of Mathematics," Thesis, Amsterdam; English translation in A. Heyting, ed., 1975: 11-101.
- Brouwer, L. E. J., 1908, "The Unreliability of the Logical Principles," English translation in Heyting, ed., 1975: 107-111.
- Brouwer, L. E. J., 1912, "Intuitionism and Formalism," English
translation by A. Dresden in
*Bull. Amer. Math. Soc.***20**(1913): 81-96, reprinted in Benacerraf and Putnam, eds., 1983: 77-89; also reprinted in Heyting, ed., 1975: 123-138. - Brouwer, L. E. J., 1923, 1954, "On the significance of the principle of excluded middle in mathematics, especially in function theory," "Addenda and corrigenda," and "Further addenda and corrigenda," English translation in van Heijenoort, ed., 1967: 334-345.
- Brouwer, L. E. J., 1927, "Intuitionistic reflections on formalism," originally published in 1927, English translation in van Heijenoort, ed., 1967: 490-492.
- Brouwer, L. E. J., 1948, "Consciousness, philosophy and mathematics," originally published (1948), reprinted in Benacerraf and Putnam, eds., 1983: 90-96.
- Buss, S., Ed., 1998,
*Handbook of Proof Theory*, Elsevier, Amsterdam and New York. - Crossley, J., and M. A. E. Dummett, eds., 1965,
*Formal Systems and Recursive Functions*. North-Holland Publishing, Amsterdam. - van Dalen, D., ed., 1981,
*Brouwer's Cambridge Lectures on Intuitionism*, Cambridge University Press, Cambridge. - Dummett, M., 1975, "The philosophical basis of intuitionistic logic," originally published (1975), reprinted in Benacerraf and Putnam, eds., 1983: 97-129.
- Friedman, H., 1975, "The disjunction property implies the numerical
existence property,"
*Proc. Nat. Acad. Sci.***72**: 2877-2878. - Gentzen, G., 1934-5, "Untersuchungen Über das logische
Schliessen,"
*Math. Zeitschrift***39**: 176-210, 405-431. - Ghilardi, S., 1999, "Unification in intuitionistic logic,"
*Jour. Symb. Logic***64**: 859-880. - Gödel, K., 1932, "Zum intuitionistischen Aussagenkalkül,"
*Anzeiger der Akademie der Wissenschaftischen in Wien***69**: 65-66. - Gödel, K., 1933, "Zur intuitionistischen Arithmetik und
Zahlentheorie,"
*Ergebnisse eines mathematischen Kolloquiums***4**: 34-38. - Gödel, K., 1958, "Über eine bisher noch nicht
benützte Erweiterung des finiten Standpunktes,"
*Dialectica***12**: 280-287. Reproduced with an English translation in Gödel, 1990: 241-251. - Gödel, K., 1990,
*Collected Works*, Vol. II, eds. S. Feferman et. al., Oxford University Press, Oxford. - Glivenko, V., 1929, "Sur qulques points de la logique de M.
Brouwer,"
*Academie Royale de Belgique, Bulletins de la classe des sciences*, ser. 5, vol. 15: 183-188. - Harrop R., 1960, "Concerning formulas of the types
*A*→*B**C*,*A*→ (*E**x*)*B*(*x*) in intuitionistic formal systems,"*Jour. Symb. Logic***25**: 27-32. - van Heijenoort, J., ed., 1967,
*From Frege to Gödel: A Source Book In Mathematical Logic 1879-1931*, Harvard University Press, Cambridge, MA. - Heyting, A., 1930, "Die formalen Regeln der intuitionistischen
Logik," in three parts,
*Sitzungsber. preuss. Akad. Wiss.*: 42-71, 158-169. English translation of Part I in Mancosu 1998: 311-327. - Heyting, A., 1956,
*Intuitionism: An Introduction*, North-Holland Publishing, Amsterdam. Third Revised Edition (1971). - Heyting, A., ed., 1975,
*L. E. J. Brouwer: Collected Works***1**:*Philosophy and Foundations of Mathematics*, Elsevier, Amsterdam and New York. - Howard, W. A., 1973, "Hereditarily majorizable functionals of finite type," in Troelstra, ed., 1973: 454-461.
- Iemhoff, R., 2001, "On the admissible rules of intuitionistic
propositional logic,"
*Jour. Symb. Logic***66**: 281-294. - Iemhoff, R., 2005, "Intermediate logics and Visser's rules,"
*Notre Dame Jour. Form. Logic***46**: 65-81. - de Jongh, D. H. J., 1970, "The maximality of the intuitionistic
propositional calculus with respect to Heyting's Arithmetic,"
*Jour. Symb. Logic***36**: 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. - Kleene, S. C., 1945, "On the interpretation of intuitionistic
number theory,"
*Jour. Symb. Logic***10**: 109-124. - Kleene, S. C., 1965, "Classical extensions of intuitionistic mathematics," in Y. Bar-Hillel, ed., 1965: 31-44.
- Kleene, S. C., 1952,
*Introduction to Metamathematics*, Van Nostrand, Princeton. - Kleene, S. C., 1969,
*Formalized Recursive Functionals and Formalized Realizability*, Memoirs of the American Mathematical Society 89. - Kleene, S. C. and Vesley, R. E., 1965,
*The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions*, North-Holland, Amsterdam. - Kreisel, G., 1962, "On weak completeness of intuitionistic
predicate logic,"
*Jour. Symb. Logic***27**: 139-158. - Kripke, S. A., "Semantical analysis of intuitionistic logic," in J. Crossley and M. A. E. Dummett, eds., 1965: 92-130.
- Mancosu, P., 1998,
*From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920s*, Oxford University Press, New York and Oxford. - Martin-Löf, P., 1984,
*Intuitionistic Type Theory*, Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980, Bibliopolis, Napoli. - Moschovakis, J. R., 2003, "Classical and constructive hierarchies
in extended intuitionistic analysis,"
*Jour. Symb. Logic***68**: 1015-1043. - van Oosten, J., 1991, "A semantical proof of de Jongh's theorem,"
*Arch. Math. Logic***31**: 105-114. - van Oosten, J., 2002, "Realizability: a historical essay,"
*Math. Struct. Comp. Sci.***13**: 239-263. - Rybakov, V., 1997,
*Admissibility of Logical Inference Rules*, Elsevier, Amsterdam. - 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 an analysis by an extension of principles
formulated in current intuitionistic mathematics,"
*Recursive Function Theory: Proceedings of Symposia in Pure Mathematics*, Vol. 5, J. C. E. Dekker, ed.,: 1-27. - van Stigt, W. P., 1990,
*Brouwer's Intuitionism*, North-Holland, Amsterdam. - Troelstra, A. S., ed., 1973,
*Metamathematical Investigation of Intuitionistic Arithmetic and Analysis*, Lecture Notes in Mathematics 344, Springer-Verlag, Berlin. Corrections and additions available from the editor. - Troelstra, A. S., 1991, "History of constructivism in the twentieth century," ITLI Prepublication Series ML-91-05, Amsterdam. Available from Troelstra's internet homepage.
- Troelstra, A. S., "Realizability," Chapter VI of S. R. Buss, ed., 1998: 407-473.
- Troelstra, A. S., Introductory note to 1958 and 1972, in Gödel, 1990: 217-241.
- Troelstra, A. S. and van Dalen, D., 1988,
*Constructivism in Mathematics: An Introduction*, in two volumes, North-Holland Publishing, Amsterdam. - Veldman, W., 1976, "An intuitionistic completeness theorem for
intuitionistic predicate logic,"
*Jour. Symb. Logic***41**: 159-166. - Veldman, W., 1990, "A survey of intuitionistic descriptive set
theory," in P. P. Petkov, ed.,
*Mathematical Logic, Proceedings of the Heyting Conference*, Plenum Press, New York and London: 155-174. - Veldman, W., 2005, "Two simple sets that are not positively Borel,"
*Annals of Pure and Applied Logic***135**: 151-209. - Vesley, R. E., 1972, "Choice sequences and Markov's principle,"
*Compositio Mathematica*24: 33-53. - Visser, A., 1999, "Rules and arithmetics,"
*Notre Dame Jour. Form. Logic***40**: 116-140. - Visser, A., 2002, "Substitutions of Sigma
^{0}_{1}sentences: explorations between intuitionistic propositional logic and intuitionistic arithmetic,"*Annals of Pure and Applied Logic*114: 227-271.

## Other Internet Resources

- Excerpts from Brouwer's Cambridge lectures.
- Open problems in provability logic, maintained by Lev Beklemishev.
- Realizability bibliography, maintained by Lars Birkedal.
- van Oosten, 2000, and other preprints related to realizability, maintained by Jaap van Oosten.