# Constructive Mathematics

*First published Tue Nov 18, 1997; substantive revision Thu May 21, 2009*

Constructive mathematics is distinguished from its traditional counterpart, classical mathematics, by the strict interpretation of the phrase “there exists” as “we can construct”. In order to work constructively, we need to re-interpret not only the existential quantifier but all the logical connectives and quantifiers as instructions on how to construct a proof of the statement involving these logical expressions.

Although certain individuals — most notably Kronecker — had expressed disapproval of the “idealistic”, nonconstructive methods used by some of their nineteenth century contemporaries, it is in the polemical writings of L.E.J. Brouwer (1881–1966), beginning with his Amsterdam doctoral thesis (Brouwer 1907) and continuing over the next forty-seven years, that the foundations of a precise, systematic approach to constructive mathematics were laid. In Brouwer's philosophy, known as intuitionism, mathematics is a free creation of the human mind, and an object exists if and only if it can be (mentally) constructed.

- 1. Introduction
- 2. The Constructive Interpretation of Logic
- 3. Varieties of Constructive Mathematics
- 4. Constructive Reverse Mathematics
- 5. Concluding Remarks
- Bibliography
- Other Internet Resources
- Related Entries

## 1. Introduction

Before mathematicians assert something (other than an axiom) they are
supposed to have proved it true. What, then, do mathematicians mean
when they assert a disjunction *P* ∨ *Q*,
where *P* and *Q* are syntactically correct statements
in some (formal or informal) language that a mathematician can use? A
natural — although, as we shall see, not the unique —
interpretation of this disjunction is that not only does (at least)
one of the statements *P*, *Q* hold, but also we can
decide which one holds. Thus just as mathematicians will assert
that *P* only when they have decided that *P* by proving
it, they may assert *P* ∨ *Q* only when they
either can decide — that is, prove — that *P* or
decide (prove) that
*Q*.

With this interpretation, however, mathematicians run into a serious
problem in the special case where *Q* is the negation,
¬*P*, of *P*. To decide that ¬*P* is to
show that *P* implies a contradiction (such as 0=1). But it will
often be that mathematicians have neither decided that *P* nor
decided that ¬*P*. To see this, we need only reflect on the
following:

Goldbach Conjecture:

Every even integer > 2 can be written as a sum of two primes,

which remains neither proved nor disproved despite the best efforts
of many of the leading mathematicians since it was first raised in a
letter from Goldbach to Euler in 1742. We are forced to conclude that,
under the very natural decidability interpretation of *P*
∨ *Q*, only an optimist can retain a belief in the *law of
excluded middle*,

Law of Excluded Middle(LEM):

For every statementP, eitherPor ¬Pholds.

Traditional, or *classical*, mathematics gets round this by
widening the interpretation of disjunction: it interprets
*P* ∨ *Q* as
¬(¬*P*∧¬*Q*), or in other words,
“it is contradictory that both *P* and *Q* be
false”. In turn, this leads to the *idealistic*
interpretation of existence, in which
∃*x**P*(*x*) means
¬∀*x*¬*P*(*x*) (“it is
contradictory that *P*(*x*) be false for
every *x*”). It is on these interpretations of
disjunction and existence that mathematicians have built the grand,
and apparently impregnable, edifice of classical mathematics which
serves a foundation for the physical, the social, and (increasingly)
the biological sciences. However, the wider interpretations come at a
cost: for example, when we pass from our initial, natural
interpretation of
*P* ∨ *Q* to the unrestricted use of the
idealistic one, ¬(¬*P*∧¬*Q*), the
resulting mathematics cannot generally be interpreted within
computational models such as recursive function theory.

This point is illustrated by a well-worn example, the proposition:

There exist irrational numbersa,bsuch thata^{b}is rational.

A slick classical proof goes as follows. Either
√2^{√2} is
rational, in which case we take *a* = *b* =
√2;
or else
√2^{√2} is
irrational, in which case we take *a* =
√2^{√2} and
*b* =
√2
(see Dummett 1977,
10). But as it stands, this proof does not enable us to pinpoint which
of the two choices of the pair (*a*,*b*) has the required
property. In order to determine the correct choice of
(*a*,*b*), we would need to decide whether
√2^{√2} is rational or irrational, which is precisely to
employ our initial interpretation of disjunction with *P* the
statement
“√2^{√2} is rational”.

Here is another illustration of the difference between interpretations. Consider the following simple statement about the set ℜ of real numbers:

(*) ∀x∈ ℜ (x= 0 ∨x≠ 0),

where, for reasons that we divulge shortly, *x* ≠ 0 means
that we can find a rational number *r* with 0 < *r*
< |*x*|. A natural computational interpretation of (*) is
that we have a procedure which, applied to any real number *x*,
either tells us that *x*=0 or else tells us that *x* ≠
0. (For example, such a procedure might output 0 if *x*=0, and
output 1 if *x* ≠ 0.) However, because the computer can handle real
numbers only by means of finite rational approximations, we have the
problem of *underflow*, in which a sufficiently small positive
number can be misread as 0 by the computer; so there cannot be a
decision procedure that justifies the statement (*). In other words, we
cannot expect (*) to hold under our natural computational
interpretation of the quantifier
∀
and
the connective
∨.

Let's examine this from another angle. Let *G*(*n*)
act as shorthand for the statement “2*n* + 2 is a sum of
two primes”, where *n* ranges over the positive integers,
and define an infinite binary sequence **a** =
(*a*_{1},*a*_{2},…) as
follows:

a_{n}={ 0 if G( n) holds for allk≤n

1 if ¬G(n) holds for somek≤n.

There is no question that **a** is a computationally
well-defined sequence, in the sense that we have an algorithm for
computing *a*_{n} for each *n*: check
the even numbers 4,6,8,…,2*n*+2 to determine whether each
of them is a sum of two primes; in that case, set
*a*_{n}=0; in the contrary case, set
*a*_{n}=1. Now consider the real number whose
*n*^{th} binary digit is *a*_{n}
:

x= (0· a_{1}a_{2}a_{2}···)_{ 2}= 2 ^{−1}a_{1}+ 2^{−2}a_{2}+ ···=

∞

∑

n=12 ^{−n}a_{n}.

If (*) holds under our computational interpretation, then we can decide between the following two alternatives:

- 2
^{−1}*a*_{1}+ 2^{−2}*a*_{2}+ ··· = 0, which implies that*a*_{n}= 0 for every*n*; - we can find a positive integer
*N*such that 2^{−1}*a*_{1}+ 2^{−2}*a*_{2}+ ··· > 2^{−N}.

In the latter case, by testing
*a*_{1},…,*a*_{N}, we can
find *n* ≤ *N* such that
*a*_{n} = 1. Thus the computational
interpretation of (*) enables us to decide whether there exists
*n* such that *a*_{n} = 1; in other
words, it enables us to decide the status of the Goldbach
Conjecture.

The use of the Goldbach Conjecture here is purely dramatic. To avoid it, we define a function ƒ on the set of binary sequences as follows:

ƒ( a) ={ 0 if a_{n}= 0 for alln

1 ifa_{n}= 1 for somen.

The argument of the preceding paragraph can then be modified to show
that, under our computational interpretation, (*) provides us with a
procedure for calculating ƒ(**a**) for any
computationally well-defined binary sequence **a**. Now,
the computability of the function ƒ can be expressed informally by
the following:

Limited Principle of Omniscience (LPO):

For each binary sequence (a_{1},a_{2},…) eithera_{n}= 0 for allnor else there existsnsuch thata_{n}= 1,

which is generally regarded as an essentially nonconstructive principle, for several reasons. First, its recursive interpretation,

There is a recursive algorithm which, applied to any recursively defined binary sequence (a_{1},a_{2},…), outputs 0 ifa_{n}= 0 for alln, and outputs 1 ifa_{n}= 1 for somen,

is provably false within recursive function theory, even with classical logic (see Bridges & Richman 1987, Chapter 3); so if we want to allow a recursive interpretation of all our mathematics, then we cannot use LPO. Secondly, there is a model theory (Kripke models) in which it can be shown that LPO is not derivable in Heyting arithmetic — that is, Peano arithmetic using the computational interpretation of the connectives and quantifiers that we state in more detail in the next section (Bridges & Richman 1987, Chapter 7).

## 2. The Constructive Interpretation of Logic

It should, by now, be clear that a full-blooded computational development of mathematics disallows the idealistic interpretations of disjunction and existence upon which most classical mathematics depends. In fact, in order to work constructively, we need to return from the classical interpretations back to the natural, constructive ones, as follows.

∨ (or): to prove P∨Qwe must have either a proof ofPor a proof ofQ.∧ (and): to prove P∧Qwe must have a proof ofPand a proof ofQ.→ (implies): a proof of P→Qis an algorithm that converts a proof ofPinto a proof ofQ.¬ (not): to prove ¬ Pwe must show thatPimplies 0 = 1.∃ (there exists): to prove ∃ xP(x) we must construct an objectxand prove thatP(x) holds.∀ (for each/all): a proof of ∀ xP(x) is an algorithm that, applied to any objectx, proves thatP(x) holds.

These *BHK-interpretations* (the name reflects their origin
in the work of Brouwer, Heyting and Kolmogorov) can be made more
precise using Kleene's notion of *realizability*; see (Dummett
1977, 318–335; Beeson 1985, Chapter VII).

Why would we want to reinterpret logic in this way? First, there is
the desire to retain, as far as possible, computational interpretations
of our mathematics. Ideally, we are trying to develop mathematics in
such a way that if a theorem asserts the existence of an object
*x* with a property *P*, then the proof of the theorem
embodies algorithms for constructing *x* and for demonstrating,
by whatever calculations are necessary, that *x* has the
property *P*. Here are some examples of theorems, each followed
by an informal description of the requirements for its constructive
proof.

- For each real number
*x*, either*x*= 0 or*x*≠ 0.*Proof requirement*: An algorithm which, applied to a given real number*x*, would decide whether*x*= 0 or*x*≠ 0. Note that, in order to make this decision, the algorithm might use not only the data describing*x*but also the data showing that*x*is actually a real number. - Each nonempty subset
*S*of*R**that is bounded above has a least upper bound*.*Proof requirement*: An algorithm which, applied to a set*S*of real numbers, a member*s*of*S*, and an upper bound for*S*,- computes an object
*b*and shows that*b*is a real number; - shows that
*x*≤*b*for each*x*∈ S; and - given a real number
*b*′ <*b*, computes an element*x*of*S*such that*x*>*b*′.

- computes an object
- If ƒ is a continuous real-valued mapping on the closed
interval [0,1] such that ƒ(0)ƒ(1) < 0, then there exists
*x*such that 0 <*x*< 1 and ƒ(*x*) = 0.*Proof requirement*: An algorithm which, applied to the function ƒ, a modulus of continuity for ƒ, and the values ƒ(0) and ƒ(1),- computes an object
*x*and shows that*x*is a real number between 0 and 1, and - shows that ƒ(
*x*) = 0.

- computes an object
- If ƒ is a continuous real-valued mapping on the closed
interval [0,1] such that ƒ(0)ƒ(1) < 0, then for each
ε > 0 there exists
*x*such that 0 <*x*< 1 and |ƒ(*x*)| < ε.*Proof requirement*: An algorithm which, applied to the function ƒ, a modulus of continuity for ƒ, the values ƒ(0) and ƒ(1), and a positive number ε,- computes an object
*x*and shows that*x*is a real number between 0 and 1, and - shows that |ƒ(
*x*)| < ε.

- computes an object

We already have reasons for doubting that (A) has a constructive proof. If the
proof requirements for (B) can be fulfilled, then, given any mathematical
statement *P*,
we can apply our proof of (B) to the
set

{0} ∪ {x:x= 1 ∧ (P∨ ¬P)}

in order to determine its supremum σ. Computing σ with an
error < ½, we then determine whether σ = 0 or σ
= 1; the former case is ruled out, since it implies the contradiction
¬(*P* ∨ ¬*P*); so σ must equal 1, we
can easily find *N* such that *a*_{N} =
1, and therefore *P* ∨ ¬*P* holds. Thus (B)
implies the law of excluded middle.

However, in Bishop's constructive theory of the real numbers, based on Cauchy sequences with a preassigned convergence rate, we can prove the following:

Constructive Least-Upper-Bound Principle:

LetSbe a nonempty subset of ℜ that is bounded above. ThenShas a least upper bound if and only if it isorder located, in the sense that for all real numbers α, β with α < β, either β is an upper bound forSor else there existsx∈Swithx> α (Bishop & Bridges 1985, p. 37, Proposition (4.3)).

In passing, we mention an alternative development of the constructive theory of ℜ based on interval arithmetic; see Chapter 2 of Bridges & Vîta 2006.

Each of statements (C) and (D), which are classically equivalent, is
a version of the Intermediate Value Theorem. In these statements, a
*modulus of continuity* for ƒ is a set Ω of ordered
pairs (ε ,δ) of positive real numbers with the following
two properties:

- for each ε > 0 there exists δ > 0 such that (ε,δ) ∈Ω
- for each (ε,δ) ∈ Ω, and for all
*x*,*y*∈ [0,1] such that |*x*−*y*| < δ, we have |ƒ(*x*) − ƒ(*y*)| < ε.

Statement (C) is essentially nonconstructive, since it entails the following nonconstructive principle:

Lesser Limited Principle of Omniscience (LLPO):

For each binary sequence (a_{1},a_{2},…) with at most one term equal to 1, eithera_{n}= 0 for all evennor elsea_{n}= 0 for all oddn.

Statement (D), a weak form of (C), can be proved constructively, using an interval-halving argument of a standard type. The following stronger constructive intermediate value theorem, which suffices for most practical purposes, is proved using an approximate interval-halving argument:

Let ƒ be a continuous real-valued mapping on the closed interval [0,1] such that ƒ(0) and ƒ(1) have opposite signs. Suppose also that ƒ islocally nonzero, in the sense that for eachx∈ [0,1] and eachr> 0, there existsysuch that |x−y| <rand ƒ(y) ≠ 0. Then there existsxsuch that 0 <x< 1 and ƒ(x)=0.

The situation of the intermediate value theorem is typical of many
in constructive analysis, where we find one classical theorem with
several constructive versions, some or all of which may be equivalent
under classical logic. (See also, for example, Bridges *et al*.
1982.)

There is one omniscience principle whose constructive status is less clear than that of LPO and LLPO, namely, the following:

Markov's Principle (MP):

For each binary sequence (a_{n}), if it is contradictory that all the termsa_{n}equal 0, then there exists a term equal to 1.

This principle is equivalent to a number of simple classical propositions, including the following:

- For each real number
*x*, if it is contradictory that*x*equal 0, then*x*≠ 0 (in the sense we mentioned earlier). - For each real number
*x*, if it is contradictory that*x*equal 0, then there exists*y*∈ ℜ such that*xy*= 1. - For each one-one continuous mapping ƒ : [0,1] →
ℜ, if
*x*≠*y*, then ƒ(*x*) ≠ ƒ(*y*).

Markov's Principle represents an unbounded search: if you have a
proof that all terms *a*_{n} being 0 leads to a
contradiction, then, by testing the terms
*a*_{1},*a*_{2},*a*_{3},…
in turn, you are “guaranteed” to come across a term equal
to 1; but this guarantee does not extend to an assurance that you will
find the desired term before the end of the universe. Most
practitioners of constructive mathematics view Markov's Principle with
at least suspicion, if not downright disbelief. Such views are
reinforced by the observation that there is a Kripke Model showing that
MP is not derivable in Heyting arithmetic under our computational
interpretation of logic. (See Bridges & Richman 1987, 137–138.)

## 3. Varieties of Constructive Mathematics

The desire to retain the possibility of a computational interpretation is one motivation for using the constructive reinterpretations of the logical connective and quantifiers that we gave above; but it is not exactly the motivation of the pioneers of constructivism in mathematics. In this section we look at some of the different approaches to constructivism in mathematics over the past 125 years.

### 3.1 Intuitionistic Mathematics

In the late nineteenth century, certain individuals — most
notably Kronecker and Poincaré — had expressed doubts, or
even disapproval, of the idealistic, nonconstructive methods used by
some of their contemporaries; but it is in the polemical writings of
L.E.J. Brouwer
(1881–1966), beginning with his
Amsterdam doctoral thesis (1907) and continuing over the next
forty-seven years, that the foundations of a precise, systematic
approach to constructive mathematics were laid. In Brouwer's
philosophy, known as *intuitionism*, mathematics is a free
creation of the human mind, and an object exists if and only if it can
be (mentally) constructed. If one takes that philosophical stance, then
one is inexorably drawn to the foregoing constructive interpretation of
the logical connectives and quantifiers: for how could a proof of the
impossibility of the non-existence of a certain object *x*
describe a mental construction of *x*?

Brouwer was not the clearest expositor of his ideas, as is shown by the following quotation:

Mathematics arises when the subject of two-ness, which results from the passage of time, is abstracted from all special occurrences. The remaining empty form [the relation ofnton+1] of the common content of all these two-nesses becomes the original intuition of mathematics and repeated unlimitedly creates new mathematical subjects. (quoted in Kline 1972, pp. 1199–2000)

A modern precis of Brouwer's view was given by Errett Bishop (Bishop 1967, p. 2):

The primary concern of mathematics is number, and this means the positive integers. We feel about number the way Kant felt about space. The positive integers and their arithmetic are presupposed by the very nature of our intelligence and, we are tempted to believe, by the very nature of intelligence in general. The development of the positive integers from the primitive concept of the unit, the concept of adjoining a unit, and the process of mathematical induction carries complete conviction. In the words of Kronecker, the positive integers were created by God.

However obscure Brouwer's writings could be, one thing was always clear: for him, mathematics took precedence over logic. One might say, as Hermann Weyl does in the following passage, that Brouwer saw classical mathematics as flawed precisely in its use of classical logic without reference to the underlying mathematics:

According to [Brouwer's] view and reading of history, classical logic was abstracted from the mathematics of finite sets and their subsets. … Forgetful of this limited origin, one afterwards mistook that logic for something above and prior to all mathematics, and finally applied it, without justification, to the mathematics of infinite sets. This is the Fall and original sin of set theory, for which it is justly punished by the antinomies. It is not that such contradictions showed up that is surprising, but that they showed up at such a late stage of the game. (quoted in Kline 1972, p. 2001)

In particular, this misuse of logic led to nonconstructive existence proofs which, in Hermann Weyl's words, “inform the world that a treasure exists without disclosing its location”.

In order to describe the logic used by the intuitionist mathematician, it was necessary first to analyse the mathematical processes of the mind, from which analysis the logic could be extracted. In 1930, Brouwer's most famous pupil, Arend Heyting, published a set of formal axioms which so clearly characterise the logic used by the intuitionist that they have become universally known as the axioms for intuitionistic logic (Heyting 1930). These axioms captured the informal computational interpretations of the connectives and quantifiers that we gave earlier.

Intuitionistic mathematics diverges from other types of constructive
mathematics in its interpretation of the term “sequence”.
Normally, a sequence in constructive mathematics is given by a rule
which determines, in advance, how to construct each of its terms; such
a sequence may be said to be *lawlike* or
*predeterminate*. Brouwer generalised this notion of a sequence
to include the possibility of constructing the terms one-by-one, the
choice of each term being made freely, or subject only to certain
restrictions stipulated in advance. Most manipulations of sequences do
not require that they be predeterminate, and can be performed on these
more general *free choice sequences*.

Thus, for the intuitionist, a real number **x** =
(*x*_{1},*x*_{2},…) —
essentially, a Cauchy sequence of rational numbers — need not be
given by a rule: its terms
*x*_{1},*x*_{2},… , are simply
rational numbers, successively constructed, subject only to some kind
of Cauchy restriction such as the following one used by Bishop
(1967):

∀m∀n[|x_{m}−x_{n}| ≤ (1/m+ 1/n)]

Once free choice sequences are admitted into one's mathematics, so,
perhaps to one's initial surprise, are certain strong choice
principles. Let *P* be a subset of
**N**^{N} ×
**N** (where **N** denotes the set of natural
numbers and, for sets *A* and *B*,
*B*^{A} denotes the set of mappings from
*A* into *B*), and suppose that for each
**a**∈**N**^{N}
there exists *n*∈**N** such that
(**a**,*n*)∈*P*. From a constructive
point of view, this means that we have a procedure, applicable to
sequences, that computes n for any given **a**. According
to Brouwer, the construction of an element of
**N**^{N} is forever incomplete:
a generic sequence **a** is *purely extensional*,
in the sense that at any given moment we can know nothing about
**a** other than a finite set of its terms. It follows
that our procedure must be able to calculate, from some finite initial
sequence
(*a*_{0},…,*a*,_{N}) of
terms of **a**, a natural number *n* such that
*P*(**a**,*n*). If
**b**∈**N**^{N}
is any sequence such that *b*_{k} =
*a*_{k} for 0 ≤ *k* ≤ *N*,
then our procedure must return the same *n* for
**b** as it does for **a**. This means that
*n* is a continuous function of **a** with respect
to the topology on **N**^{N}
given by the metric

ρ : (a,b) inf{2^{−n}:a_{k}=b_{k}for 0 ≤k≤n}.

Thus we are led to the following *principle of continuous
choice*, which we divide into a continuity part and a choice part:

Continuous Choice 1 (CC1):

Any function fromN^{N}toNis continuous.

Continuous Choice 2 (CC2):

IfP⊆N^{N}×N, and for eacha∈N^{N}there existsn∈Nsuch that (a,n) ∈P, then there is a function ƒ :N^{N}→Nsuch that (a,ƒ(a)) ∈Pfor alla∈N^{N}.

If *P* and ƒ are as in CC2, then we say that ƒ is a
*choice function* for *P*.

The omniscience principles LPO and LLPO are demonstrably false under the hypotheses CC1-2; but MP is consistent with it. Among the remarkable consequences of CC1-2 are the following.

- Any function from N
^{N}or 2^{N}to a metric space is pointwise continuous. - Every mapping from a nonempty complete separable metric space to a metric space is pointwise continuous.
- Every map from the real line ℜ to itself is pointwise continuous.
- Let
*X*be a complete separable normed space,*Y*a normed space, and (*u*_{n}) a sequence of linear mappings from*X*to*Y*such that for each unit vector*x*of*X*,φ(

*x*) = sup{ ||*u*_{n}(*x*)|| :*n*∈**N**}exists. Then there exists

*c*>0 such that ||*u*_{n}(*x*)|| ≤*c*for all*n*∈**N**and all unit vectors*x*of*X*(“Uniform boundedness principle”).

Each of these statements appears to contradict known classical theorems. However, the comparison with classical mathematics should not be made superficially: in order to understand that there is no real contradiction here, we must appreciate that the meaning of such terms as “function” and even “real number” in intuitionistic mathematics is quite different from that in the classical setting.

Brouwer's introspection over the nature of functions and the continuum led him to a second principle, which, unlike that of continuous choice, is classically valid. This principle requires a little more background for its explanation.

For any set *S* we denote by *S*^{*} the set of
all finite sequences of elements of *S*, including the empty
sequence ( ). If α =
(*a*_{1},…,*a*_{n}) is
in *S*^{*}, then *n* is called the *length*
of α and is denoted by |α|. If *m*
∈ **N**, and α
∈ *S*^{N} or α
∈ *S*^{*} is of length at least *m*, then
we denote by
α¯(*m*)
the finite sequence consisting of the first *m* terms of α.
Note that
α¯(0)
= ( ).
If α ∈ *S*^{*} and
β=α¯(*m*)
for some *m*, we say that
α
is
an *extension* of β, and that β is a
*restriction* of
α.

A subset σ of *S* is said to be *detachable*
(from *S*) if

∀x∈S(x∈ σ ∨x∉ σ).

A detachable subset σ of **N**^{*} is called
a *fan* if

- it is closed under restriction: for each
α∈
**N**^{*}and each*n*, if α¯(*n*) ∈*S*, then α¯(*k*) ∈*S*whenever 0 ≤*k*≤*n*; and - for each
α∈σ,
the set
{ α¯

*n*:*n*∈**N**}is finite or empty, where α¯

*n*denotes the finite sequence obtained by adjoining the natural number*n*to the terms of α.

A *path* in a fan σ is a sequence
α,
finite or infinite, such that
α¯(*n*) ∈
σ for each applicable *n*. We say that a path
α
is *blocked* by a subset
*B* if some restriction of
α
is
in *B*; if no restriction of
α
is in *B*, we say that
α
*misses* *B*. A subset *B* of a fan
σ is called a *bar* for σ if each infinite path of
σ is blocked by *B*; a bar *B* for σ is
*uniform* if there exists *n*∈**N**
such that each path of length *n* is blocked by *B*.

At last we can state Brouwer's next principle of
intuitionism, *the fan theorem for detachable
bars*:

Fan Theorem (FT)_{D}:

Every detachable bar of a fan is uniform.

In its classical contrapositive form, FT_{D}
is known as
*König's Lemma*: if for every *n* there exists a
path of length *n* that misses *B*, then there exists an
infinite path that misses *B* (see Dummett 2000, 68–71). (Of
course, classically the condition of detachability is superfluous.) It
is simple to construct a Brouwerian counterexample to König's
Lemma.

Brouwer actually posited the fan theorem without the restriction of
detachability of the bar. Attempts to prove that more general fan
theorem constructively rely on an analysis of how we could know that a
subset is a bar, and led Brouwer to a notion of *bar
induction*, which we shall not describe here. We shall return to
fan theorems in Section 4.

Of the many applications of Brouwer's principles, the most famous is
his *uniform continuity theorem* (which follows from the
pointwise continuity consequences of CC1-2 together with FT):

Every mapping from a compact (that is, complete, totally bounded) metric space into a metric space is uniformly continuous.

The reader is warned once again to interpret this carefully within Brouwer's intuitionistic framework, and not to jump to the erroneous conclusion that intuitionism contradicts classical mathematics. It is more sensible to regard the two types of mathematics as incomparable. For further discussion, see the entry on intuitionistic logic.

Unfortunately — and perhaps inevitably, in the face of opposition from mathematicians of such stature as Hilbert — Brouwer's intuitionist school of mathematics and philosophy became more and more involved in what, at least to classical mathematicians, appeared to be quasi-mystical speculation about the nature of constructive thought, to the detriment of the practice of constructive mathematics itself. This unfortunate polarisation between the Brouwerians and the Hilbertians culminated in the notorious Grundlagenstreit of the 1920s, details of which can be found in the Brouwer biographies by van Dalen (1999, 2005) and van Stigt (1990).

### 3.2 Recursive Constructive Mathematics

In the late 1940s, the Russian mathematician A.A. Markov began the development of an alternative form of constructive mathematics (RUSS), which is, essentially, recursive function theory with intuitionistic logic (Markov 1954, Kushner 1985). In this variety the objects are defined by means of Gödel-numberings, and the procedures are all recursive; the main distinction between RUSS and the classical recursive analysis developed after, in 1936, the work of Turing, Church, and others clarified the nature of computable processes, is that the logic used in RUSS is intuitionistic. Thus RUSS may be described as “recursive mathematics with intuitionistic logic”.

One obstacle faced by the mathematician attempting to come to grips with RUSS is that, expressed in the language of recursion theory, it is not easily readable; indeed, on opening a page of Kushner's excellent lectures (1985), one might be forgiven for wondering whether this is analysis or logic. Fortunately, one can get to the heart of RUSS by an axiomatic approach due to Richman (1983) (see also Bridges & Richman 1987).

First, we define a set *S* to be *countable* if there
is a mapping from a detachable subset of **N** onto
*S*. By a *partial function* on **N** we
mean a mapping whose domain is a subset of **N**; if the
domain is **N** itself, then we call the function a
*total partial function* on **N**. Richman's
approach to RUSS is based on intuitionistic logic and a single axiom,
namely,

Computable Partial Functions (CPF):

There is an enumeration φ_{0},φ_{1},… of the set of all partial functions fromNtoNwith countable domains.

It is remarkable what can be deduced cleanly and quickly using this principle. For example, we can prove the following result, which almost immediately shows that LLPO, and hence LPO, are false in the recursive setting.

There is a total partial function ƒ :N×N→ {0,1} such that

- for each
mthere exists at most onensuch that ƒ(m,n) = 1; and- for each total partial function ƒ :
N→ {0,1}, there existm,kinNsuch that ƒ(m, 2k+ƒ(m)) = 1.

Of more interest, however, are results such as the following within RUSS.

**Specker's Theorem**: There exists a strictly increasing sequence (*r*_{1},*r*_{2},…) of rational numbers in the closed interval [0,1] such that for each*x*∈ ℜ there exist*N*∈**N**and δ > 0 such that |*x*−*r*_{n}| ≥ δ for all*n*≥*N*.- For each ε>0, there exists a sequence
(
*I*_{1},*I*_{2},…) of bounded open intervals in ℜ such that(i) ℜ ⊆ ∞

∪

*n*=1*I*_{n}, and(ii) *N*

∑

*n*=1| *I*_{n}| < ε for each*N*. - There exists a pointwise continuous function ƒ : [0,1] → ℜ that is not uniformly continuous.
- There exists a positive-valued uniformly continuous function ƒ : [0,1] → ℜ whose infimum is 0.

From a classical viewpoint, these results fit into place when one realises that words such as “function” and “real number” should be interpreted as “recursive function” and “recursive real number” respectively. Note that the second of these four is a strong recursive counterexample to the open—cover compactness property of the (recursive) real line; and the fourth is a recursive counterexample to the classical theorem that every uniformly continuous mapping of a compact set into ℜ attains its infimum.

### 3.3 Bishop's Constructive Mathematics

Progress in all varieties of constructive mathematics was relatively
slow throughout the next decade and a half. What was needed to raise
the profile of constructivism in mathematics was a top-ranking
classical mathematician to show that a thoroughgoing constructive
development of mathematics was possible without a commitment to
Brouwer's non-classical principles or to the machinery of recursive
function theory. This need was fulfilled in 1967, with the appearance
of Errett Bishop's monograph *Foundations of Constructive
Analysis* (1967), the product of an astonishing couple of years in
which, working in the informal but rigorous style used by normal
analysts, Bishop provided a constructive development of a large part of
twentieth-century analysis, including the Stone-Weierstrass Theorem,
the Hahn-Banach and separation theorems, the spectral theorem for
self-adjoint operators on a Hilbert space, the Lebesgue convergence
theorems for abstract integrals, Haar measure and the abstract Fourier
transform, ergodic theorems, and the elements of Banach algebra theory.
(See also Bishop & Bridges 1985.) Thus, at a stroke, he gave the
lie to the commonly-held view expressed so forcefully by Hilbert:

Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists. (Hilbert 1928)

Not only did Bishop's mathematics (BISH) have the advantage of readability — if you open Bishop's book at any page, what you see is clearly recognisable as analysis, even if, from time to time, his moves in the course of a proof may appear strange to one schooled in the use of the law of excluded middle — but, unlike intuitionistic or recursive mathematics, it admits many different interpretations. Intuitionistic mathematics, Markov's recursive constructive mathematics, and even classical mathematics all provide models of BISH. In fact, the results and proofs in BISH can be interpreted, with at most minor amendments, in any reasonable model of computable mathematics, such as, for example, Weihrauch's Type Two Effectivity Theory (Weihrauch 1996, 2000; Bauer 2005).

How is this multiple interpretability achieved? At least in part by
Bishop's refusal to pin down his primitive notion of
“algorithm” or, in his words, “finite routine”.
This refusal has led to the criticism that his approach lacks the
precision that a logician would normally expect of a foundational
system. However, this criticism can be overcome by looking more closely
at what practitioners of BISH actually do, as distinct from what Bishop
may have thought he was doing, when they prove theorems: in practice,
they are doing *mathematics with intuitionistic logic*.
Experience shows that the restriction to intuitionistic logic always
forces mathematicians to work in a manner that, at least informally,
can be described as algorithmic; so *algorithmic mathematics appears
to be equivalent to mathematics that uses only intuitionistic
logic*. If that is the case, then we can practice constructive
mathematics using intuitionistic logic on any reasonably defined
mathematical objects, not just some class of “constructive
objects”.

This view, more or less, appears to have first been put forward by Richman (1990, 1996). Taking the logic as the primary characteristic of constructive mathematics, it does not reflect the primacy of mathematics over logic that was part of the belief of Brouwer, Heyting, Markov, Bishop, and other pioneers of constructivism. On the other hand, it does capture the essence of constructive mathematics in practice.

Thus one might distinguish between the *ontological
constructivism* of Brouwer and others who are led to constructive
mathematics through a belief that mathematical objects are mental
creations, and the *epistemological constructivism* of Richman
and those who see constructive mathematics as characterised by its
methodology, based on the use of intuitionistic logic. Of course, the
former approach to constructivism inevitably leads to the latter; and
the latter is certainly not inconsistent with a Brouwerian
ontology.

### 3.4 Martin-Löf's Constructive Type Theory

Before ending our tour of varieties of modern constructive
mathematics, we should visit, if but briefly, a fourth variety, based
on Per Martin-Löf's type-theory (ML). In 1968, Martin-Löf
published his *Notes on Constructive Analysis*, based on
lectures he had given in Europe in 1966—68; so his involvement
with constructivism in mathematics goes back at least to the period of
Bishop's writing of *Foundations of Constructive Analysis*: the
former book is in the spirit of RUSS, rather than BISH; indeed, its
author did not have access to Bishop's book until his own manuscript
was finished. Martin-Löf later turned his attention to his theory
of types as a foundation for Bishop-style constructive
mathematics.

Here, in his own words, is an informal explanation of the ideas underlying ML:

We shall think ofmathematical objectsorconstructions. Every mathematical object is of a certain kind ortype[… and] is always given together with its type. […] A type is defined by describing what we have to do in order to construct an object of that type. […] Put differently, a type is well-defined if we understand […] what it means to be an object of that type. Thus, for instanceN→N[functions fromNtoN] is a type, not because we know particular number theoretic functions like the primitive recursive ones, but because we think we understand the notion of number theoretic functionin general. (1975)

In particular, in this system every proposition can be represented as a type: namely, the type of proofs of the proposition. Conversely, each type determines a proposition: namely, the proposition that the type in question is nonempty. So when we think of a certain type T as a proposition, we interpret the formula

x∈T

as “*x* is a proof of the proposition *T*”.

Martin-Löf goes on to construct new types, such as Cartesian products and disjoint unions, from old. For example, the Cartesian product

(Πx∈A)B(x)

is the type of functions that take an arbitrary object x of type A
into an object of type *B*(*x*). In the
propositions-as-proofs interpretation, where *B*(*x*)
represents a proposition, the above Cartesian product corresponds to
the universal proposition

(∀x∈A)B(x).

He distinguishes carefully between proofs and derivations: a
*proof object* is a witness to the fact that some proposition
has been proved; whereas a *derivation* is the record of the
construction of a proof object. Also, Martin-Löf exercises two
basic forms (one dare not say “types” here!) of
*judgement*. The first is a relation between proof objects and
propositions, the second a property of some propositions. In the first
case, the judgement is either one that a proof object *a* is a
witness to a proposition *A*, or else one that two proof objects
*a* and *b* are equal and both witness that *A*
has been proved. The first case of the second form of judgement states
that a proposition *A* is well-formed, and the second records
that two propositions *A* and *B* are equal.

There is a careful, and highly detailed, set of rules for formalising ML. We will not go into those here, but refer the reader to other sources such as Bridges & Reeves 1999. However, there is one further technical matter we would like to mention: the axiom of choice is derivable in ML.

The full axiom of choice can be stated as follows:

IfA,Bare nonempty sets, andSa subset ofA×Bsuch that

∀ x∈A∃y∈B((x,y) ∈S),(1) then there exists a choice function ƒ :

A→Bsuch that∀x∈A((x,ƒ(x)) ∈B).

Now, if this is to hold under a constructive interpretation, then
for a given *x*∈*A*, the value ƒ(*x*) of
the choice function will depend not only on *x* but also on the
data proving that *x* belongs to *A*. In general, we
cannot expect to produce a choice function of this sort. On the other
hand, the BHK interpretation of (1) is that there is an algorithm
A
which, applied to any given
*x* ∈ *A*, produces an element
*y* ∈ *B* such that (*x*,*y*) ∈
*S*. If *A* is a completely presented (or, in Bishop's
words, basic) set, one for which no work beyond the construction of
each element in the set is required to prove that the element does
indeed belong to *A*, then we might reasonably expect the
algorithm
A
to be a choice function. In
Bishop-style mathematics, basic sets are rare (**N** is
one). In Martin-Löf's type theory, *every set is completely
presented* and, in keeping with what we wrote above about the BHK
interpretation of (1), the axiom of choice is derivable therein. In
this connection, we should point the reader to the Goodman & Myhill
(1978) proof that the axiom of choice entails the law of excluded
middle (see also Problem 2 on page 58 of Bishop 1967). Clearly, the
Goodman-Myhill theorem applies under the assumption that not every set
is completely presented.

Every constructive proof embodies an algorithm that, in principle, can be extracted and recast as a computer program; moreover, the constructive proof is itself a verification that the algorithm is correct — that is, meets its specification. One major advantage of Martin-Löf's formal approach to constructive mathematics is that it greatly facilitates the extraction of programs from proofs. This has led to serious work on the implementation of constructive mathematics in various locations (see Martin-Löf 1980, Constable 1986, and Hayashi & Nakano 1988).

## 4. Constructive Reverse Mathematics

Over thirty years ago, Harvey Friedman initiated a research programme of
*reverse mathematics,* aiming to classify mathematical theorems
according to their equivalence to one of a small number of set-theoretic
principles (Friedman 1975). This classification reveals
interesting, and usually non-trivial, differences in proof-theoretic
complexity. For example, although the Ascoli-Arzelà theorem is used in
the standard proof of Peano's existence theorem for solutions of ordinary
differential equations (Hurewicz 1958, page 10), a
reverse-mathematical analysis shows that the former is equivalent to a
strictly stronger set-theoretic principle than the one equivalent to Peano's
theorem (Simpson 1984, Theorems 3.9 and 4.2). The
standard treatise on classical reverse mathematics is that of Simpson
(Simpson 1999).

Around the turn of this century, Veldman (Veldman 2005), in the
Netherlands, and Ishihara (Ishihara 2005, 2006), in Japan,
independently initiated a programme of *constructive *reverse
mathematics, CRM, based on intuitionistic, rather than classical,
logic. (Note, though, that the first published work in the modern era
of CRM is probably that of Julian and Richman (1984), which was twenty
years ahead of its time.) In this section of the article, we describe
a less formal approach to CRM, in the style and framework of BISH. The
aim of that CRM program is to classify the theorems in the three
standard models—CLASS, INT, and
RUSS—according to which principles we must, and need only,
add to BISH in order to prove them.

We stress that we restrict ourselves here to *informal*
CRM, in which we take for granted the principles
of function- and set-construction described in the first chapters
of (Bishop 1967, Bishop & Bridges 1985, Bridges & Richman
1987, Bridges & Vîta 2006), and we work in the informal,
though rigorous, style of the practising analyst, algebraist,
topologist, … .

In practice, CRM splits naturally into two parts. In the first of
these, we consider a theorem *T* of INT or RUSS, and try to
find some principle, valid in that model and other than *T*
itself, whose addition to BISH is necessary and sufficient for a
constructive proof of *T*. In the second part of CRM we deal
with a theorem *T* of CLASS that we suspect is nonconstructive,
and we try to prove that *T* is equivalent, over BISH, to one
of a number of known essentially-nonconstructive principles, such as
MP, LLPO, LPO, or LEM. For an example of this part of CRM, we mention
our earlier proof that the classical least-upper-bound principle is
equivalent to LEM.

Incidentally, there is a strong argument for Brouwer being the first to deal
with reverse-mathematical ideas: his *Brouwerian counterexamples*,
dating back to (Brouwer 1921), lie squarely in the
second part of CRM. Even if Brouwer did not state those
examples as logical equivalences, but as implications of the
type

P⇒ some nonconstructive principle,

one cannot but believe that he was aware that the right-hand-side implied the left in such cases.

To illustrate the first part of CRM, we now concentrate on theorems of the type

BISH ⊢ FT_{?}⇔T,

where FT_{?} is some form of Brouwer's fan
theorem, and *T* is a theorem of INT. To do
so, we need to distinguish between certain types of bar for
the *complete binary fan* 2^{*} (the set of
all finite sequences in {0,1}).

Let α ≡ (α_{1},α_{2},…)
be a finite or infinite binary sequence. The *concatenation* of
α with another string β is

α¯β ≡ (α_{1},α_{2},…,α_{n},β_{1},…,β_{m}).

For *b* in {0,1} we write α¯*b* rather than α¯(*b*).
By a *c*-*subset* of 2^{*}
we mean a subset *B* of 2^{*} such that

B= {u∈ 2^{*}: ∀v∈2^{*}(u¯v∈D}(2)

for some detachable subset *D* of 2^{*}. Every
detachable subset of 2^{*} is a *c*-subset. On the
other hand, by a Π10-*subset*
of 2^{*} we mean a subset *B* of 2^{*} with the
following property: there exists a detachable subset *S* of
2^{*} × **N** such that

∀u∈2^{*}∀n∈N((u,n) ∈S⇒ (u¯0,n) ∈S∧ (u¯1,n) ∈S)

and

B= {u∈ 2^{*}: ∀n∈N((u,n) ∈S)}.

Every *c*-subset *B* of 2^{*} is a
Π10-subset: simply take *S*
= *D* × **N**, where *D* is a
detachable subset of 2^{*} such that (1) holds.

If ? denotes a property of subsets of 2^{*}, then
Brouwer's *fan theorem for* ?-*bars*
tells us that every bar with the property ? is a uniform bar. We are
particularly interested in the fan theorem for detachable
bars (already discussed in Section 3.1):

FT_{D}: Every detachable bar of the complete binary fan is uniform,

the fan theorem for *c*-*bars*
(that is, bars that are *c*-subsets):

FT_{c}: Every c-bar of the complete binary fan is uniform,

the fan theorem for Π_{0}^{1}*-bars* (that
is, bars that are-subsets):

FT_{Π01}: Every Π_{0}^{1}-bar of the complete binary fan is uniform,

and the full fan theorem (already discussed in Section 3.1):

FT: Every bar of the complete binary fan is uniform.

Note that, relative to BISH,

FT ⇒ FT_{Π01}⇒ FT_{c}⇒ FT_{D},

but it is not known whether any of these implications can be reversed. However, Diener (2008) has shown that the negations of these four principles are equivalent over BISH.

Typically, we want to prove that
FT_{?} is equivalent,
over BISH, to the proposition that, for every
set *S* of an appropriate sort, some pointwise property of the
form

∀x∈S∃t∈TP(s,t)

actually holds uniformly in the form

∃t∈T∀s∈SP(s,t).

Our strategy for attacking this problem is two-fold. First, given a
set *S* of the appropriate sort, we construct a
?-subset *N* of 2^{*} such that

- if (2) holds, then
*B*is a bar, and - if
*B*is a uniform bar, then (3) holds.

This, though, is only half of the solution. To prove that the
implication from (3) to (2)
implies FT_{?}, we consider a
?-subset *B* of 2^{*} and construct a corresponding
set *S* such that

- if
*B*is a bar, then (2) holds, and - if (3) holds, then
*B*is a uniform bar.

The canonical example of such results is that of Julian and Richman
(1984), in which *S* is the set of values of a given uniformly
continuous mapping *f* : [0,1]
→ ℜ, *T* is the set of positive real
numbers, and

P(s,t) ≡ (s≥t)

The pointwise property we consider is

∀x∈[0,1]∃t>0(f(x) ≥t),

its uniform version being

∃t>0∀x∈[0,1](f(x) ≥t).

The Julian-Richman results are as follows.

Theorem 1:

Letf: [0,1] → ℜ be uniformly continuous. Then there exists a detachable subsetBof 2^{*}such that

- if
f(x) > 0 for each x ∈ [0,1], thenBis a bar, and- if
Bis a uniform bar, then inff> 0.

Theorem 2: LetBbe a detachable subset of 2^{*}. Then there exists a uniformly continuousf: [0,1] → ℜ such that

- if
Bis a bar, thenf(x) > 0 for eachx∈ [0,1], and- if inf
f> 0, thenBis a uniform bar.

The proofs of these two theorems are subtle and tricky; see either
Julian & Richman 1984 or Bridges & Richman 1987 (Chapter 6)
for details. New, but equally complex, proofs will appear in Berger
& Bridges 2009 The two Julian-Richman theorems together reveal
that, relative to BISH, the fan theorem
FT_{D} is equivalent to the statement:

POS:

Each positive-valued, uniformly continuous function on [0,1] has a positive infimum.

It follows that POS is derivable in INT, in which the full fan
theorem, not just FT_{D}, is a standard
principle. The situation is quiet the opposite in RUSS, where there
exist a detachable bar of 2^{*} that is not uniform and a
positive-valued, uniformly continuous function on [0,1] that has
infimum equal to 0; see Chapters 5 and 6 of Bridges & Richman
1987.

Recently, Berger (2006) solved the important problem of finding a form of the fan theorem that is equivalent, over BISH, to the uniform continuity theorem for [0,1]:

UCT_{[0,1]}:

Every pointwise continuous mapping of [0,1] into ℜ is uniformly continuous,

the proposition for which Brouwer originally developed his proof of
the fan theorem. (Note that UCT_{[0,1]} is
equivalent, relative to BISH, to the general uniform
continuity theorem for metric spaces: Every pointwise continuous
mapping of a complete, totally bounded metric space into a metric
space is uniformly continuous. See Loeb 2005 and Bridges & Diener
2007.) It is known that

BISH + UCT_{[0,1]}⊢ FT_{c}.

Also, Diener and Loeb (2008) have proved that

BISH + FT_{Π10}⊢ UCT_{[0,1]}.

However, we do not know if either of these implications can be replaced by a bi-implication.

For additional material on constructive reverse mathematics, see, for example, Berger & Schuster 2006, Bridges 2008, Ishihara (1992, 2005, 2006), and Veldman 2005.

## 5. Concluding Remarks

The traditional route taken by mathematicians wanting to analyse the
constructive content of mathematics is the one that follows classical
logic; in order to avoid decisions, such as whether or not a real
number equals 0, that cannot be made by a real computer, the
mathematician then has to keep within strict algorithmic boundaries
such as those formed by recursive function theory. In contrast, the
route taken by the constructive mathematician follows intuitionistic
logic, which automatically takes care of computationally inadmissible
decisions. This logic (together with an appropriate set-theoretic
framework) suffices to keep the mathematician within constructive
boundaries. Thus one is free to work in the natural style of an
analyst, algebraist (e.g., Mines *et al.* 1988), geometer,
topologist (e.g., Bridges & Vîta 2003), or other normal
mathematician, the only constraints being those imposed by
intuitionistic logic. As Bishop and others have shown, the traditional
belief promulgated by Hilbert and still widely held today, that
intuitionistic logic imposes such restrictions as to render the
development of serious mathematics impossible, is patently false: large
parts of deep modern mathematics can be, and have been, produced by
purely constructive methods. Moreover, the link between constructive
mathematics and programming holds great promise for the future
implementation and development of abstract mathematics on the
computer.

## Bibliography

### References

- Aberth, O., 1980,
*Computable Analysis*, New York: McGraw-Hill. - Aczel, P., and Rathjen, M., 2001,
*Notes on Constructive Set Theory*, Report No. 40, Institut Mittag-Leffler, Royal Swedish Academy of Sciences. - Beeson, M., 1985,
*Foundations of Constructive Mathematics*, Heidelberg: Springer-Verlag. - Berger, J., 2006, “The Logical Strength of the Uniform Continuity
Theorem”, in
*Logical Approaches to Computational Barriers*, A. Beckmann, U. Berger, B. Lowe, and J. V. Tucker (eds.), Heidelberg: Springer-Verlag. - Berger, J., and Bridges, D.S., 2007, “A fan-theoretic equivalent
of the antithesis of Specker's theorem”,
*Proc. Koninklijke Nederlandse Akad. Weten.*(Indag. Math. N.S.), 18 (2): 195–202. - Berger, J., and Bridges, D.S., 2009, “The Fan Theorem and
Positive-valued Uniformly Continuous Functions on Compact
Intervals”,
*New Zealand J. Math.*, to appear. - Berger, J., and Schuster, P.M., 2006, “Classifying Dini's
theorem”,
*Notre Dame J. Formal Logic*, 47: 253–262. - Bishop, E., 1967,
*Foundations of Constructive Analysis*, New York: McGraw-Hill. - –––, 1973,
*Schizophrenia in Contemporary Mathematics*,*Amer. Math. Soc. Colloquium Lectures*, Missoula: University of Montana; reprinted in*Errett Bishop: Reflections on Him and His Research*, Amer. Math. Soc. Memoirs 39. - Bishop, E. and Bridges, D., 1985,
*Grundlehren der math. Wissenschaften*, Heidelberg: Springer-Verlag. - Bridges, D., 1998, “Constructive Truth in Practice”, in
*Truth in Mathematics*, H. Dales and G. Oliveri (eds.), Oxford: Clarendon Press. - Bridges, D., 2008, “A Reverse Look at Brouwer's Fan Theorem”,
in
*One Hundred Years of Intuitionism (1907–2007)*, M. van Atten, P. Boldini, M. Bourdeau, G. Heinzmann (eds.), Basel: Birkhäuser Verlag. - Bridges, D., Calder, A., Julian, W., Mines. R. and Richman, F.,
1982, “Picard's Theorem”,
*Trans. Amer. Math. Soc.*, 269 (2): 513–520. - Bridges, D., and Diener, H., 2007, “The Pseudocompactness of [0,1]
is Equivalent to the Uniform Continuity Theorem”,
*J. Symbolic Logic*, 72 (4): 1379–1383. - Bridges, D., and Reeves, S., 1999, “Constructive mathematics, in
theory and programming practice”,
*Philosophia Mathematica*, 7 (1): 65—104. - Bridges, D., and Richman, F., 1987,
*Varieties of Constructive Mathematics*, London Math. Soc. Lecture Notes 97, Cambridge: Cambridge University Press. - Bridges, D. and Vîta, L., 2003, “Apartness spaces as a foundation
for constructive topology”,
*Ann. Pure Appl. Logic.*, 119 (1–3): 61–83. - –––, 2006,
*Techniques of Constructive Analysis*, Universitext, Heidelberg: Springer-Verlag. - Brouwer, L.E.J., 1907,
*Over de Grondslagen der Wiskunde*, Doctoral Thesis, University of Amsterdam; reprinted with additional material, D. van Dalen (ed.), by Matematisch Centrum, Amsterdam, 1981. - –––, 1908, “De onbetrouwbaarheid der logische principes”,
*Tijdschrift voor Wijsbegeerte*, 2: 152–158. - –––, 1921, “Besitzt jede reelle Zahl eine
Dezimalbruchentwicklung?”,
*Math. Ann.*, 83: 201–210. - –––, 1924, “Beweiss, dass jede volle Funcktion gleichmässig
stetig ist”,
*Proc. Koninklijke Nederlandse Akad. Weten.*, 27: 189–193. - –––, 1924A, “Bemerkung zum Beweise der gleichmässigen
Stetigkeit voller Funktionen”,
*Proc. Koninklijke Nederlandse Akad. Weten.*, 27: 644–646. - Constable, R.,
*et al*., 1986,*Implementing Mathematics with the Nuprl Proof Development System*, Englewood Cliffs, NJ: Prentice-Hall. - Diener, H., 2008,
*Compactness under Constructive Scrutiny*, Ph.D. Thesis, Christchurch: University of Canterbury. - Diener, H., and Loeb, I., 2009, “Sequences of Real Functions on
[0,1] in Constructive Reverse Mathematics”,
*J. Symbolic Logic*, to appear. - Dummett, Michael, 2000,
*Elements of Intuitionism*(Oxford Logic Guides, 39), Oxford: Clarendon Press. - Friedman, H., 1975, “Some systems of second order arithmetic and
their use”, in
*Proceedings of the 17th International Congress of Mathematicians*, (Vancouver, BC, 1974). - –––, 1977, “Set theoretic foundations for constructive
analysis”,
*Ann. Math.*, 105 (1): 1–28. - Goodman, N.D., and Myhill, J., 1978, “Choice Implies Excluded
Middle”,
*Zeit. Logik und Grundlagen der Math*, 24: 461. - Hayashi, S., and Nakano, H., 1988,
*PX: A Computational Logic*, Cambridge MA: MIT Press. - Heyting, A., 1930, “Die formalen Regeln der intuitionistischen
Logik”,
*Sitzungsber. der Preuss. Akad. Wiss. Berlin*, 42–56. - –––, 1971,
*Intuitionism — An Introduction*, 3rd edition, Amsterdam: North Holland. - Hilbert, D., 1925, “Über das Unendliche”,
*Mathematische Annalen*, 95: 161–190; translation, “On the Infinite”, by E. Putnam and G. Massey, in*Philosophy of Mathematics: Selected Readings*, P. Benacerraf and H. Putnam (eds.), Englewood Cliffs, NJ: Prentice Hall, 1964, pp. 134–151. - Hurewicz, W., 1958,
*Lectures on Ordinary Differential Equations*, Cambridge, MA: MIT Press. - Ishihara, H., 1992, “Continuity properties in constructive
mathematics”,
*J. Symbolic Logic*, 57 (2): 557–565. - –––, 2005, “Constructive Reverse Mathematics: Compactness
Properties”, in
*From Sets and Types to Analysis and Topology: Towards Practicable Foundations for Constructive Mathematics*, L. Crosilla and P. Schuster (eds.), Oxford: The Clarendon Press. - –––, 2006, “Reverse Mathematics in Bishop's Constructive
Mathematics”,
*Phil. Scientiae, Cahier Special*, 6: 43–59. - Kline, Morris, 1972.
*Mathematical Thought from Ancient to Modern Times*, Volume 3, Oxford: Clarendon Press. - Kushner, B., 1985,
*Lectures on Constructive Mathematical Analysis*, Providence, RI: Amer. Math. Soc. - Lietz, P., 2004,
*From Constructive Mathematics to Computable Analysis via the Realizability Interpretation*, Dr. rer. nat. dissertation, Universität Darmstadt, Germany. - Loeb, I., 2005, “Equivalents of the (Weak) Fan
Theorem”,
*Ann. Pure and Applied Logic*, 132: 51–66. - Julian, W., and Richman, F., 1984, “A Uniformly Continuous
Function on [0,1] that is Everywhere Different from its
Infimum”,
*Pacific J. Math.*, 111: 333–340. - Markov, A.A., 1954,
*Theory of Algorithms*, Trudy Mat. Istituta imeni V.A. Steklova, 42, Moskva: Izdatel'stvo Akademii Nauk SSSR. - Martin-Löf, P., 1968,
*Notes on Constructive Analysis*, Almquist & Wixsell, Stockholm. - –––, 1975, “An intuitionistic theory of types: predicative
part”, in
*Logic Colloquium 1973*, H.E. Rose and J.C. Shepherdson (eds.), Amsterdam: North-Holland, pp. 73-118. - –––, 1980, “Constructive mathematics and computer programming”,
in
*Proc. 6th. Int. Congress for Logic, Methodology and Philosophy of Science*, L. Jonathan Cohen (ed.), Amsterdam: North-Holland. - Mines, R., Richman, F., and Ruitenburg, W., 1988,
*A Course in Constructive Algebra*, Universitext, Heidelberg: Springer-Verlag. - Myhill, John, 1973, “Some Properties of Intuitionistic
Zermelo-Fraenkel Set Theory”, in
*Cambridge Summer School in Mathematical Logic*, A. Mathias and H. Rogers (eds.), Lecture Notes in Mathematics, 337, Heidelberg: Springer-Verlag, 206-231. - –––, 1975, “Constructive Set Theory”,
*J. Symbolic Logic*, 40 (3): 347–382. - Richman, Fred, 1983, “Church's Thesis Without Tears”,
*J. Symbolic Logic*, 48: 797–803. - –––, 1990, “Intuitionism as Generalization”,
*Philosophia Mathematica*, 5: 124–128. - –––, 1996, “Interview with a Constructive Mathematician”,
*Modern Logic*, 6: 247–271. - –––, 2000, “The Fundamental Theorem of Algebra: A Constructive
Treatment Without Choice”,
*Pacific J. Math.*, 196: 213–230. - Simpson, S.G., 1984, “Which Set Existence Axioms are Needed to
Prove the Cauchy/Peano Theorem for Ordinary Differential
Equations”,
*J. Symbolic Logic*, 49 (3): 783–802. - –––, 1999,
*Subsystems of Second Order Arithmetic*, Berlin: Springer-Verlag. Second edition to be published by the Association for Symbolic Logic. - Specker, E., 1949, “Nicht konstruktiv beweisbare Sätze der
Analysis”,
*J. Symbolic Logic*, 14: 145–158. - Troelstra, A.S., 1978, “Aspects of Constructive Mathematics”, in
*Handbook of Mathematical Logic*, J. Barwise (ed.), Amsterdam: North-Holland. - Troelstra, A.S., and van Dalen, D., 1988,
*Constructivism in Mathematics: An Introduction*(two volumes), Amsterdam: North Holland. - van Dalen, D., 1981,
*Brouwer's Cambridge Lectures on Intuitionism*, Cambridge: Cambridge University Press. - –––, 1999,
*Mystic, Geometer and Intuitionist: The Life of L.E.J. Brouwer*, vol. I, Oxford: Clarendon Press. - –––, 2005,
*Mystic, Geometer, and Intuitionist: The Life of L.E.J. Brouwer*, Volume 2, Oxford: Clarendon Press. - van Stigt, W.P., 1990,
*Brouwer's Intuitionism*, Amsterdam: North-Holland. - Veldman, W., 2005, “Brouwer's Fan Theorem as an Axiom and as a Contrast to Kleene's Alternative”, preprint, Radboud University, Nijmegen, Netherlands.
- Weihrauch, K., 1987,
*Computability*, Springer-Verlag, Heidelberg. - –––, 1996, “A Foundation for Computable Analysis”, in
*Combinatorics, Complexity, and Logic*, D. Bridges, C. Calude, J. Gibbons, S. Reeves, and I. Witten (eds.), Singapore: Springer-Verlag. - –––, 2000,
*Computable Analysis*, EATCS Texts in Theoretical Computer Science, Heidelberg: Springer-Verlag.

### Related Literature

- Heijenoort, Jean van, 1967,
*From Frege to Gödel: A Source Book in Mathematical Logic 1879–1931*, Cambridge, MA: Harvard University Press. - Hilbert, David, 1928, “Die Grundlagen der Mathematik”, Hamburger Mathematische Einzelschriften 5, Teubner, Leipzig. Reprinted in English translation in van Heijenoort 1967.

## Other Internet Resources

- Bauer, A., 2005, “Realizability as the connection between computable and constructive mathematics”.