 # Constructive Mathematics

Constructive Mathematics

Constructive mathematics is positively characterized by the requirement that proof be algorithmic. Loosely speaking, this means that when a (mathematical) object is asserted to exist, an explicit example is given: a constructive existence proof demonstrates the existence of a mathematical object by outlining a method of finding (“constructing”) such an object. The emphasis in constructive theory is placed on hands-on provability, instead of on an abstract notion of truth. The classical concept of validity is starkly contrasted with the constructive notion of proof. An implication (A⟹B) is not equivalent to a disjunction (¬A∨B), and neither are equivalent to a negated conjunction (¬(A∧¬B)). In practice, constructive mathematics may be viewed as mathematics done using intuitionistic logic.

With the advent of the computer, much more emphasis has been placed on algorithmic procedures for obtaining numerical results, and constructive mathematics has come into its own. For, a constructive proof is exactly that: an algorithmic procedure for obtaining a conclusion from a set of hypotheses.

The historical and philosophical picture is complex; various forms of constructivism have developed over time. Presented here is a brief introduction to several of the more widely accepted approaches, and is by no means comprehensive.

Motivation and History
An Example
Constructivism as Philosophy
The BHK Interpretation
Constructive Methods in Mathematics
Early History
The Axiom of Choice
Intuitionism
Brouwerian Counterexamples
The Fan Theorem
Constructive Recursive Mathematics
Surprises
Bishop’s Constructive Mathematics
Proof Readability and Preservation of Numerical Meaning
The Axiom of Choice in BISH
Martin-Löf Type Theory
The Axiom of Choice is Provable
Constructive Reverse Mathematics
Summary
Some Further Remarks
References
1. Motivation and History

The origin of modern constructive mathematics lies in the foundational debate at the turn of the 20th Century. At that time, the German mathematician David Hilbert established some very deep and far-reaching existence theorems using non-constructive methods. Around the same time, the Dutch mathematician L.E.J. Brouwer became philosophically convinced that the universal validity of contradiction proofs for existence proofs was unwarranted—despite his early work in establishing the non-constructive fixed point theorem which now bears his name.

It is often the case that a classical theorem becomes more enlightening when seen from the constructive viewpoint (we meet an example of such a case—the least upper bound principle—in Section 1d. It would, however, be unfair to say that constructive mathematics is revisionist in nature. Indeed, Brouwer proved his Fan Theorem (see Section 2b) intuitionistically in 1927 (Brouwer, 1927), but the first proof of König’s Lemma (its classical equivalent) only appeared in 1936 (König, 1936). It is ironic that the Brouwer’s intuitionist position (see Section 2) has become known as anti-realist since it demands that every object be explicitly constructible.

a. An example

Here is an example of a non-constructive proof that is commonly encountered in the literature:

Proposition.

The proof is non-constructive because even though it shows that the non-existence of such numbers would be contradictory, it leaves us without the knowledge of which choice of
a
and
b
satisfy the theorem. There is a (simple) constructive proof of this theorem: set
a=
2

and
b=
log
2
9
(in the full constructive proof, a little work first needs to be done to demonstrate that
a
and
b
are, in fact, irrational). A fully constructive proof that
2

is properly irrational (that is, positively bounded away from every rational number) may be found in Bishop (1973). This clarifies the choice of words in the proposition above. It is further possible to show that
2

2

is in fact irrational, but this is not done by the proof presented here. (An early mention of the above illustrative example in the literature is in Dummett (1977, p. 10).)

b. Constructivism as philosophy

Constructive mathematics is often mis-characterized as classical mathematics without the axiom of choice (see Section 1f); or classical mathematics without the Law of Excluded Middle. But seen from within the discipline, constructive mathematics is positively characterized by a strict provability requirement. The consequences of adopting this stance—and rigorously implementing it—are far-reaching, as will be seen.

There are two conditions which are fundamental to every constructivist philosophy:

The notion of `truth’ is not taken as primitive; rather, a proposition is considered true only when a proof for the proposition is produced.
The notion of `existence’ is taken to be constructibility: when an object is proved to exist, the proof also exhibits how to find it.

To assert that
P
, then, is to produce a proof that
P
. Likewise, to assert that
¬P
is to prove that the assumption of
P
leads to a contradiction. Very quickly, one realizes that the Principle of Excluded Middle (PEM; Latin tertium non datur or principium tertii exclusi) leads to trouble:

PEM: For any statement
P
, either
P
or
¬P
.

The assertion of PEM constructively amounts to claiming that, for any given statement
P
, either there is a proof of
P
, or there is a proof that
P

The Collatz conjecture. Define
f:N→N
by the rule:

f(n)={
n/2
3n+1
if n is even,
if n is odd.

Then for each natural number
n
, that is for each n in {1,2,3,…}, there exists a natural number
k
such that
f
k
(n)=1
.

At the time of writing this article, the Collatz conjecture remains unsolved. To claim that there is a proof of it is erroneous; likewise to claim that there is a proof that it leads to a contradiction is also erroneous. In fact, in Brouwer’s view (see Section 2), to assert PEM is to claim that any mathematical problem has a solution. Thus there are good philosophical grounds for rejecting PEM.

c. The BHK interpretation

The following interpretation of logical connectives is now known as the Brouwer-Heyting-Kolmogorov (BHK) interpretation, and is widely accepted by constructivists.

Statement Interpretation

P
We have a proof of
P
.

P∧Q
We have both a proof of
P
and a proof of
Q
.

P∨Q
We have either a proof of
P
or a proof of
Q
.

P⟹Q
We have an algorithm that converts any proof of
P
into a proof of
Q
.

¬P
We have a proof that
P⟹⊥
, where

is absurd (for example,
0=1
).

x∈A
P(x)
We have an algorithm which computes an object
x∈A
and confirms that
P(x)
.

x∈A
P(x)
We have an algorithm which, given any object
x
, together with the data that
x∈A
, shows that
P(x)
holds.

In particular, the interpretations for
¬,∨,⟹
and

are worth emphasizing: each of these has the very strict requirement that a proof of such a statement will consist of a decision procedure—in other words, every constructive proof contains, in principle, an algorithm.

The BHK interpretation characterizes a logic called intuitionistic logic. Every form of constructive mathematics has intuitionistic logic at its core; different schools have different additional principles or axioms given by the particular approach to constructivism.

d. Constructive methods in mathematics

Upon adopting only constructive methods, we lose some powerful proof tools commonly used in classical mathematics. We have already seen that the Principle of Excluded Middle is highly suspect from the constructivist viewpoint, as (under the BHK interpretation) it claims the existence of a universal algorithm to determine the truth of any given statement. This is not to say that PEM is constructively false, however. Both Russian recursive mathematics (in which PEM is provably false) and classical mathematics (in which it is logically true) are in a sense models, or interpretations, of constructive mathematics. So in a way, PEM is independent of constructive mathematics. Note, however, that if one is given a statement, it may be possible to prove PEM concerning that particular statement—such statements are called decidable. The point is that there is no general constructive method for doing so for all statements.

If PEM is not universally valid we also lose universal applicability of any mode of argument which validates it. For example, double negation elimination, or proof by contradiction. Again, it must be emphasized that it is only the universal applicability which is challenged: proof by contradiction is constructively just fine for proving negative statements; and double negation elimination is just fine for decidable statements.

However these limitations are in fact often advantages. In a lot of cases, constructive alternatives to non-constructive classical principles in mathematics exist, leading to results which are often constructively stronger than their classical counterpart. For example, the classical least upper bound principle (LUB) is not constructively provable:

LUB: Any nonempty set of real numbers that is bounded from above has a least upper bound.

The constructive least upper bound principle, by contrast, is constructively provable (Bishop & Bridges, 1985, p. 37):

CLUB: Any order-located nonempty set of reals that is bounded from above has a least upper bound.

A set is order-located if given any real
x
, the distance from
x
to the set is computable.
It is quite common for a constructive alternative to be classically equivalent to the classical principle; and, indeed, classically every nonempty set of reals is order-located.

To see why LUB is not provable, we may consider a so-called Brouwerian counterexample (see Section 2a), such as the set

S={x∈R:(x=2)∨(x=3∧P)}

where
P
is some as-yet unproven statement, such as Goldbach’s conjecture that every even number greater than 2 is the sum of two prime numbers. (There may be some philosophical problems with this set; however these do not matter for the purpose of this example. Section 2a has a much “cleaner”, though more technically involved, example.) If the set
S
had a computable least upper bound, then we would have a quick proof of the truth or falsity of Goldbach’s conjecture. A Brouwerian counterexample is an example which shows that if a certain property holds, then it is possible to constructively prove a non-constructive principle (such as PEM); and thus the property itself must be essentially non-constructive.

e. Early history

In the late 19th century, the mathematical community embarked on a search for foundations: unquestionable solid ground on which mathematical theorems could be proved. An early exemplar of this search is Kronecker’s 1887 paper “Über den Zahlbegriff” (“On the Concept of Number”) (Kronecker, 1887), where he outlines the project of arithmetization (that is, founding on the fundamental notion of number) of analysis and algebra. It is perhaps in this work that we see the earliest instance of the constructive manifesto in mathematical practice. Kronecker was famously quoted by Weber (1893) as saying “Die ganzen Zahlen hat der liebe Gott gemacht, alles andere ist Menschenwerk.” (“The integers were made by God; all else is the work of man.”)

It has been said that “almost all mathematical proofs before 1888 were essentially constructive.” (Beeson, 1985, p. 418). This is not to say that constructive mathematics, as currently conceived of, was common practice; but rather that the natural interpretation of existence of the time was existence in the constructive sense. As mathematical concepts have changed over time, however, old proofs have taken on new meaning. There are thus plenty of examples of results which are today regarded as essentially non-constructive, but seen within the context of the period during which they were written, the objects of study that the authors had in mind allowed proofs of a constructive nature. One good example of this is Cauchy’s 1821 proof of the Intermediate Value Theorem (Cauchy, 1821; in Bradley & Sandifer, 2009, pp. 309–312); the classical interval-halving argument. The concept of “function” has, since then, expanded to include objects which allow for Brouwerian counterexamples (see Section 2a).

The first major systematic development of a constructive approach to mathematics is that of Brouwer and the intuitionists, introduced in the next major section. Some notable forerunners (who should perhaps not be thought of as intuitionists themselves) were Henri Poincaré, who argued that mathematics is in a way more immediate than logic, and Emile Borel, who maintained that the only objects that concern science are those that can be effectively defined (Borel, 1914). Poincaré argues that intuition is a necessary component of mathematical thought, rejects the idea of an actual infinite, and argues that mathematical induction is an unprovable fact (Poincaré, 1908).

As a result of techniques from ZF set theory, rigorous proofs have over time taken on non-constructive aspects. David Hilbert, contemporary of Brouwer and an opponent of Brouwer’s philosophy, deserves particular mention, since he was an early pioneer of highly non-constructive techniques. The debate between Brouwer and Hilbert grew fierce and controversial, which perhaps added fuel to the development of both constructivism (à la Brouwer) and formalism (à la Hilbert) (see, for example, van Heijenoort, 1976). The spectacular 1890 proof by Hilbert of his famous basis theorem (Hilbert, 1890), showing the existence of a finite set of generators for the invariants of quantics, was greeted by the German mathematician Gordan with another now-(in)famous phrase: “Das ist nicht Mathematik. Das ist Theologie.” (“That is not Mathematics. That is Theology.”) This is perhaps the most dramatic example of a non-constructive proof, relying on PEM in an infinite extension.

The method Hilbert exhibited there has become widely accepted by the mathematics community as a pure existence proof (that is, proving that non-existence of such an object was contradictory without actually exhibiting the object); however it was not admissible as a constructive technique. Weyl, one of Hilbert’s students (who Hilbert would eventually “lose”—perhaps temporarily—to intuitionism) commented on pure existence proofs, that they “inform the world that a treasure exists without disclosing its location” (Weyl, 1946). The Axiom of Choice, perhaps due in part to its regular use in many non-constructive proofs (and heavily implicated in many of Hilbert’s most influential proofs), has been accused of being the source of non-constructivity in mathematics.

f. The Axiom of Choice

The Axiom of Choice (AC) has been controversial to varying degrees in mathematics ever since it was recognized by Zermelo (1904). Loosely, it states that given a collection of non-empty sets, we can choose exactly one item from each set.

AC: If to each
x
in
A
there corresponds a
y
in
B
, then there is a function
f
such that
f(x)
is in
B
whenever
x
is in
A
.

Formally, given non-empty sets
A
and
B
, the Axiom may be stated as:

x∈A

y∈B
P(x,y)⟹

f∈
B
A

x∈A
P(x,f(x)).

Intuitively, this seems almost trivial, and the case where the non-empty sets are finite in size is indeed so, since one does not need the axiom of choice to prove that such a choice can be made in most formulations of set theory. However it becomes less clear when the size of the sets involved is very large or somehow not easily determined. In such cases, a principled, functional choice may not necessarily be made. Even in classical mathematics, the axiom of choice is occasionally viewed with some suspicion: it leads to results that are surprising and counterintuitive, such as the Banach-Tarski paradox: using the axiom of choice allows one to take a solid sphere in 3-dimensional space, decompose it into a finite number of non-overlapping pieces, and reassemble the pieces (using only rotations and translations) into two solid spheres, each with volume identical to the original sphere. Due to its controversial nature, many mathematicians will explicitly state when and where in their proof AC has been used.

Nonetheless, the BHK interpretation of the quantifiers seems to invite one to think about the existential quantifier

y∈B
as defining the choice function, and so it would seem very natural to adopt AC from the constructive point of view (see, however, the discussion in Sections 4b and 5a). But consider the set
S
given by

S={x∈Z:(x=0∧P)∨(x=1∧¬P)}

for some syntactically correct statement
P
. This set is not empty, since if it were then both
P
and
¬P
would have to be false; so
¬P∧¬¬P
S
cannot contain both
0
and
1
. But suppose that we had an algorithmic procedure which (in a finite time) returns an element of
S
for us. If it returns
0
, then we know that
P
must be true; whereas if it returns
1
then we know that
P
must be false—and thus we will have proved that
P∨¬P
. We may repeat this for any statement, and so this amounts to a (constructive) proof of the universal applicability of PEM. And as we have seen, universal applicability of PEM is not constructively acceptable. Thus, while the set
S
is non-empty, we cannot necessarily exhibit any of its members either. A set which has constructible members is called inhabited, and the distinction between inhabited and non-empty sets is key in constructive set theories. Related is the issue of the size of
S
; since
S
is not empty, its size is not
0
, but since
S
is not (necessarily) inhabited, its size is no other natural number either—
S
is an at-most-singleton set. It is a consquence of AC, in fact, that every non-empty set is inhabited.

It is no coincidence that the symbolic form of AC suggests that it is essentially a quantifier swap: AC states that if to each element of
A
an element of
B
can be assigned, then it can be done so in a systematic (algorithmic) way. It is thus a kind of uniformity principle.

The example set
S
above is known as a Brouwerian example (although most of Brouwer’s examples of this sort were a little more specific—see below). It is to intuitionism, Brouwer’s philosophy of mathematics, that we now turn.

2. Intuitionism

If there is a name synonymous with constructive mathematics, it is L.E.J. Brouwer (Luitzen Egbertus Jan Brouwer; Bertus to his friends). In his doctoral thesis, Over de Grondslagen der Wiskunde (On the Foundations of Mathematics; Brouwer, 1907), Brouwer began his program of laying the foundations of constructive mathematics in a systematic way. Brouwer’s particular type of constructive mathematics is called “intuitionism” or “intuitionistic mathematics” (not to be confused with intuitionistic logic; recall Section 1c).

Shortly after the presentation of his thesis, Brouwer wrote a paper entitled “De onbetrouwbaarheid der logische principes” (“The Untrustworthiness of the Principles of Logic”; Brouwer, 1908), in which he challenged the absolute validity of classical logic: “De vraag naar de geldigheid van het principium tertii exclusi is dus aequivalent met de vraag naar de mogelijkheid van onoplosbare wiskundige problemen.” (“The question of validity of the principle of excluded third is equivalent to the question of the possibility of unsolvable mathematical problems.”; Brouwer, 1908, p. 156) In other words, PEM is valid only if there are no unsolvable mathematical problems.

In intuitionistic mathematics, mathematics is seen as a free creation of the human mind: a (mathematical) object exists just in case it can be (mentally) constructed. This immediately justifies the BHK interpretation, since any existence proof cannot be a proof-by-contradiction—the contradiction leaves us without a construction of the object.

According to Brouwer, the natural numbers and (perhaps surprisingly) the continuum, are primitive notions given directly by intuition alone. This connects to the idea of what Brouwer called free choice sequence, a generalization of the notion of sequence. It is perhaps ironic that when Brouwer initially encountered the idea of a free choice sequence, which had been a mathematical curiosity at the time, he rejected such sequences as non-intuitionistic (Brouwer, 1912). However, soon afterward he accepted them and was the first to discover how important they were to practical constructive mathematics (Brouwer, 1914). This is one of two major aspects which distinguishes intuitionistic mathematics from other kinds of constructive mathematics (the second being Brouwer’s technique of bar induction, which we do not explain in great depth here; though see Section 2b).

A free choice sequence is given by a constructing agent (Brouwer’s creative subject), who is at any stage of the progression of a sequence free to choose (or subject to mild restrictions) the next member of the sequence. For example, if one is asked to produce a binary free choice sequence, one may start “
000…0
” for a hundred digits, and then (perhaps unexpectedly) freely choose “
1
” as the next digit. A real number, classically thought of as a (converging) Cauchy sequence, thus need not be given by a determinate rule; instead, it is only subject to a Cauchy restriction (that is, some rate of convergence).

The idea of a free choice sequence leads to some very strong commitments. Not immediately obvious is the principle of continuous choice. It states:

If
P⊆
N
N
×N
and for each
x
in
N
N
there exists
n
in
N
such that
(x,n)
is in
P
, then there is a choice function
f:
N
N
→N
such that
(x,f(x))
is in
P
for all
x
in
N
N
.

The notation
B
A
, where
A
and
B
are sets, denotes the collection of functions from
A
to
B
. So
N
N
denotes the collection of functions from natural numbers to natural numbers; the arguments
x
in question are thus actually functions
x:N→N
. One may conceive of these (as Brouwer did) as sequences of natural numbers; further technical details are omitted.

Intuitively, the principle arises from the following considerations. Let
P⊆
N
N
×N
and suppose that we have a procedure that we may apply to any given sequence
x=
x
1
,
x
2
,
x
3
,…
of natural numbers which computes an index
n
such that
(x,n)∈P
—that is,
P
is a set in which every sequence of natural numbers is (constructively) paired with some natural number. Under the intuitionist’s view, at any given moment we may have only a finite number of terms of
x
at hand. The procedure which computes
n
such that
(x,n)∈P
must thus do so after being given only a finite initial fragment of
x
; say
x
1
,
x
2
,…,
x
m
. Now if we are given another sequence
y
, if the first
m
terms of
y
are the same as those of
x
(that is, if
y
is “close” to
x
in some sense), then the procedure must return the same value of
n
for
y
as it would give for
x
. The procedure is thus a continuous function (the choice function) from
N
N
to
N
.

The principle of continuous choice is a restricted form of the classical axiom of choice (see Section 1f). This principle (together with the BHK interpretation) gives rise to a number of very strong consequences—perhaps the most (in)famous being that every function
f:R→R
which maps the real line into itself is pointwise continuous.

If this seems outlandish, then remember that in intuitionistic mathematics the very ideas of “function” and “real number” are different from their classical counterparts. We now discuss a technique that originated with Brouwer which justifies, to some extent, these conceptions.

a. Brouwerian counterexamples

As we have seen, Brouwer rejected the principle of excluded middle. The intuitionist school further rejects appeal to so-called omniscience principles; logical principles which allow one to decide the truth of predicates over an infinite number of things. An illuminating example of such a principle is the limited principle of omniscience (LPO), which states that:

For each binary sequence
a
1
a
2
a
3

, either
a
n
=0
for all natural numbers
n
or there exists a natural number
n
such that
a
n
=1
.

In symbols LPO states that, for any given binary sequence
a
1
a
2
a
3

, the following statement is decidable:

∀n(
a
n
=0)∨∃n(
a
n
=1).

For one familiar with computability, the above statement will already appear problematical. It says that there is an algorithm which, given an arbitrary binary sequence will in finite time determine either that all the terms in
α
are zero, or it will output an
n
such that
a
n
=1
. Since computers have a finite memory capacity, the problem of loss of significance (or underflow) occurs: the computer carrying out the calculation may not carry enough digits of the sequence to determine whether a
1
occurs or not (though see Section 3).

However, (modern) computational issues aside, this was not the problem seen by the intuitionist. To Brouwer, the possible existence of choice sequences made this statement unacceptable. Since a constructing agent is free to insert a
1
while constructing a sequence at any stage of the construction, there is no a priori bound on how many terms one may need to search in order to establish the presence, or lack of, a
1
.

Thus we see that the lesser principle of omniscience does not apply to binary sequences in intuitionist mathematics. Let us now turn to the real numbers. The decimal expansion of
π
is a favourite example. There are well-known algorithms for computing
π
to arbitrary precision, limited only by the power of the device on which the algorithms run. At the time of writing this article, it is unkown whether a string of 100 successive
0
s (that is,
000…0
, with 100 digits) appears in the decimal expansion of
π
. It is known that
π
does not have a terminating decimal expansion (so it does not finish in all
0
s) and that it has no systematic repetition (since it is not a rational number).

But suppose we define a real number
x
by the expansion

x=

n=1

(−
1
2
)
n
a
n

where
a
n
is defined as

a
n
={
0
1
if a hundred consecutive 0s have not occurred by the nth digit of π‘s expansion
otherwise.

The number
x
is constructible: we have prescribed an algorithm for computing it to any desired precision. It also has a Cauchy condition—the
1/
2
n
part—which ensures it converges. However, we now have a problem as regards the sign of
x
: if a hundred consecutive
0
s never occur in the decimal expansion of
π
, then
x=0
. If a hundred consecutive
0
s do occur in the decimal expansion of
π
, and the hundredth such
0
occurs in an odd place, then
x<0 ; whereas if it occurs in an even place then x>0
. So if we have an answer to the question whether such a string occurs in the decimal expansion of
π
, then we can determine whether
x=0
or not; however, since we do not have an answer, we cannot conclude that
x>0
, or
x=0
, or