## 1. Brouwer



Luitzen Egbertus Jan Brouwer was born in Overschie, the Netherlands.
He studied mathematics and physics at the University of Amsterdam,
where he obtained his PhD in 1907. In 1909 he became a lecturer at the
same university, where he was appointed full professor in 1912, a
position he held until his retirement in 1951. Brouwer was a brilliant
mathematician who did ground-breaking work in topology and became
famous already at a young age. All his life he was an independent mind
who pursued the things he believed in with ardent vigor, which brought
him in conflict with many a colleague, most notably with David
Hilbert. He had admirers as well, and in his house "the
hut" in Blaricum he welcomed many well-known mathematicians of
his time. To the end of his life he became more isolated, but his
belief in the truth of his philosophy never wavered. He died in a car
accident at the age of 85 in Blaricum, seven years after the death of
his wife Lize Brouwer. 



At the age of 24 Brouwer wrote the book *Life, Art and
Mysticism* (Brouwer 1905), whose solipsistic content foreshadows
his philosophy of mathematics. In his dissertation the foundations of
intuitionism are formulated for the first time, although not yet under
that name and not in their final form. In the first years after his
dissertation most of Brouwer's scientific life was devoted to
topology, an area in which he is still known for his theory of
dimension and his fixed point theorem. This work is part of classical
mathematics; according to Brouwer's later view, his fixed point
theorem does not hold, although an analogue cast in terms of
approximations can be proved to hold according to his principles.



From 1913 on, Brouwer increasingly dedicated himself to the
development of the ideas formulated in his dissertation into a full
philosophy of mathematics. He not only refined the philosophy of
intuitionism but also reworked mathematics, especially the theory of
the continuum and the theory of sets, according to these principles.
By then, Brouwer was a famous mathematician who gave influential
lectures on intuitionism at the scientific meccas of that time,
Cambridge, Vienna, and Gottingen among them. His philosophy was
considered awkward by many, but treated as a serious alternative to
classical reasoning by some of the most famous mathematicians of his
time, even when they had a different view on the matter. Kurt
Godel, who was a Platonist all his life, was one of them. Hermann
Weyl at one point wrote "So gebe ich also jetzt meinen eigenen
Versuch Preis und schliesse mich Brouwer an" (Weyl 1921,
56). And although he rarely practised intuitionistic mathematics later
in life, Weyl never stopped admiring Brouwer and his intuitionistic
philosophy of mathematics.



The life of Brouwer was laden with conflicts, the most famous one
being the conflict with David Hilbert, which eventually led to
Brouwer's expulsion from the board of the *Mathematische
Annalen*. This conflict was part of the *Grundlagenstreit*
that shook the mathematical society at the beginning of the 20th
century and that emerged as a result of the appearance of paradoxes
and highly nonconstructive proofs in mathematics. Philosophers and
mathematicians were forced to acknowledge the lack of an
epistemological and ontological basis for mathematics. Brouwer's
intuitionism is a philosophy of mathematics that aims to provide such
a foundation.


## 2. Intuitionism


### 2.1 The two acts of intuitionism



According to Brouwer mathematics is a languageless creation of the
mind. Time is the only a priori notion, in the Kantian sense. Brouwer
distinguishes two *acts of intuitionism*:



The first act of intuitionism is: 



> 
> Completely separating mathematics from mathematical language and hence
> from the phenomena of language described by theoretical logic,
> recognizing that intuitionistic mathematics is an essentially
> languageless activity of the mind having its origin in the perception
> of a move of time. This perception of a move of time may be described
> as the falling apart of a life moment into two distinct things, one of
> which gives way to the other, but is retained by memory. If the twoity
> thus born is divested of all quality, it passes into the empty form of
> the common substratum of all twoities. And it is this common
> substratum, this empty form, which is the basic intuition of
> mathematics. (Brouwer 1981, 4-5)
> 



As will be discussed in the section on mathematics, the first act of
intuitionism gives rise to the natural numbers but implies a severe
restriction on the principles of reasoning permitted, most notably the
rejection of the principle of the excluded middle. Owing to the
rejection of this principle and the disappearance of the logical basis
for the continuum, one might, in the words of Brouwer, "fear
that intuitionistic mathematics must necessarily be poor and anaemic,
and in particular would have no place for analysis" (Brouwer
1952, 142). The second act, however, establishes the existence of the
continuum, a continuum having properties not shared by its classical
counterpart. The recovery of the continuum rests on the notion of
choice sequence stipulated in the second act, i.e. on the existence of
infinite sequences generated by free choice, which therefore are not
fixed in advance.



The second act of intuitionism is:



> 
> Admitting two ways of creating new mathematical entities: firstly in
> the shape of more or less freely proceeding infinite sequences of
> mathematical entities previously acquired ...; secondly in the
> shape of mathematical species, i.e. properties supposable for
> mathematical entities previously acquired, satisfying the condition
> that if they hold for a certain mathematical entity, they also hold
> for all mathematical entities which have been defined to be
> "equal" to it .... (Brouwer 1981, 8)
> 



The two acts of intuitionism form the basis of Brouwer's
philosophy; from these two acts alone Brouwer creates the realm of
intuitionistic mathematics, as will be explained below. Already from
this basic principles it can be concluded that intuitionism differs
from Platonism and formalism, because neither does it assume a
mathematical reality outside of us, nor does it hold that mathematics
is a play with symbols according to certain fixed rules. In
Brouwer's view, language is used to exchange mathematical ideas
but the existence of the latter is independent of the former. The
distinction between intuitionism and other constructive views on
mathematics according to which mathematical objects and arguments
should be computable, lies in the freedom that the second act allows
in the construction of infinite sequences. Indeed, as will be
explained below, the mathematical implications of the second act of
intuitionism contradict classical mathematics, and therefore do not
hold in most constructive theories, since these are in general part of
classical mathematics.



Thus Brouwer's intuitionism stands apart from other philosophies
of mathematics; it is based on the awareness of time and the
conviction that mathematics is a creation of the free mind, and it
therefore is neither Platonism nor formalism. It is a form of
constructivism, but only so in the wider sense, since many
constructivists do not accept all the principles that Brouwer believed
to be true.


### 2.2 The Creating Subject



The two acts of intuitionism do not in themselves exclude a
psychological interpretation of mathematics. Although Brouwer only
occasionally addressed this point, it is clear from his writings that
he did consider intuitionism to be independent of psychology.
Brouwer's introduction of the *Creating Subject* (Brouwer
1948) as an idealized mind in which mathematics takes place already
abstracts away from inessential aspects of human reasoning such as
limitations of space and time and the possibility of faulty arguments.
Thus the intersubjectivity problem, which asks for an explanation of
the fact that human beings are able to communicate, ceases to exist,
as there exists only one Creating Subject. In the literature, also the
name *Creative Subject* is used for Creating Subject, but here
Brouwer's terminology is used. In (Niekus 2010), it is argued
that Brouwer's Creating Subject does not involve an idealized
mathematician. For a phenomenological analysis of the Creating Subject
as a transcendental subject in the sense of Husserl see (van Atten
2007). 



Brouwer used arguments that involve the Creating Subject to construct
counterexamples to certain intuitionistically unacceptable statements.
Where the weak counterexamples, to be discussed below, only show that
certain statements cannot, at present, be accepted intuitionistically,
the notion of the idealized mind proves certain classical principles
to be false. An example is given in Section 5.4 on the formalization
of the notion of the Creating Subject. There it is also explained that
the following principle, known as *Kripke's Schema*, can
be argued for in terms of the Creating Subject: 

 

\[\tag{\({\bf KS}\)}
\exists \alpha(A \leftrightarrow \exists n\, \alpha(n) = 1). 
\]


In **KS**, \(A\) ranges over formulas and \( \alpha\) ranges over
choice sequences, which are sequences of natural numbers produced by
the Creating Subject, who chooses their elements one-by-one. Choice
sequences and Kripke's Schema are discussed further in Section
3.4.



In most philosophies of mathematics, for example in Platonism,
mathematical statements are tenseless. In intuitionism truth and
falsity have a temporal aspect; an established fact will remain so,
but a statement that becomes proven at a certain point in time lacks a
truth-value before that point. In said formalization of the notion of
Creating Subject, which was not formulated by Brouwer but only later
by others, the temporal aspect of intuitionism is conspicuously
present. 



Important as the arguments using the notion of Creating Subject might
be for the further understanding of intuitionism as a philosophy of
mathematics, its role in the development of the field has been less
influential than that of the two acts of intuitionism, which directly
lead to the mathematical truths Brouwer and those coming after him
were willing to accept.


## 3. Mathematics



Although Brouwer's development of intuitionism played an
important role in the foundational debate among mathematicians at the
beginning of the 20th century, the far reaching implications of his
philosophy for mathematics became only apparent after many years of
research. The two most characteristic properties of intuitionism are
the logical principles of reasoning that it allows in proofs and the
full conception of the intuitionistic continuum. Only as far as the
latter is concerned, intuitionism becomes incomparable with classical
mathematics. In this entry the focus is on those principles of
intuitionism that set it apart from other mathematical disciplines,
and therefore its other constructive aspects will be treated in less
detail. 


### 3.1 The BHK-interpretation



In intuitionism, knowing that a statement *A* is true means
having a proof of it. In 1934 Arend Heyting, who had been a student of
Brouwer, introduced a form of what became later known as the
*Brouwer-Heyting-Kolmogorov-interpretation*, which captures the
meaning of the logical symbols in intuitionism, and in constructivism
in general as well. It defines in an informal way what an
intuitionistic proof should consist of by indicating how the
connectives and quantifiers should be interpreted. 


* \(\bot\) is not provable.
* A proof of \(A\wedge B\) consists of a proof of \(A\) and a proof
of \(B\).
* A proof of \(A \vee B\) consists of a proof of \(A\) or a proof of
\(B\).
* A proof of \(A \rightarrow B\) is a construction which transforms
any proof of \(A\) into a proof of \(B\).
* A proof of \(\exists x A(x)\) is given by presenting an element
\(d\) of the domain and a proof of \(A(d)\).
* A proof of \(\forall x A(x)\) is a construction which transforms
every proof that \(d\) belongs to the domain into a proof of
\(A(d)\).



The negation \(\neg A\) of a formula \(A\) is proven once it has been
shown that there cannot exist a proof of \(A\), which means providing
a construction that derives falsum from any possible proof of \(A\).
Thus \(\neg A\) is equivalent to \(A \rightarrow \bot\). The
BHK-interpretation is not a formal definition because the notion of
construction is not defined and therefore open to different
interpretations. Nevertheless, already on this informal level one is
forced to reject one of the logical principles ever-present in
classical logic: the principle of the excluded middle \((A\vee \neg
A)\). According to the BHK-interpretation this statement holds
intuitionistically if the Creating Subject knows a proof of \(A\) or a
proof that \(A\) cannot be proved. In the case that neither for \(A\)
nor for its negation a proof is known, the statement \((A \vee \neg
A)\) does not hold. The existence of open problems, such as the
Goldbach conjecture or the Riemann hypothesis, illustrates this fact.
But once a proof of \(A\) or a proof of its negation is found, the
situation changes, and for this particular \(A\) the principle \((A
\vee \neg A)\) is true from that moment on.


### 3.2 Intuitionistic logic



Brouwer rejected the principle of the excluded middle on the basis of
his philosophy, but Arend Heyting was the first to formulate a
comprehensive logic of principles acceptable from an intuitionistic
point of view. Intuitionistic logic, which is the logic of most other
forms of constructivism as well, is often referred to as
"classical logic without the principle of the excluded
middle". It is denoted by IQC, which stands for Intuitionistic
Quantifier Logic, but other names occur in the literature as well. A
possible axiomatization in Hilbert style consists of the
principles




|  |  |  |  |
| --- | --- | --- | --- |
| \(A \wedge B \rightarrow A\) | \(A \wedge B \rightarrow B\) | \(A \rightarrow A \vee B\) | \(B \rightarrow A \vee B\) |
| \(A \rightarrow (B \rightarrow A)\) | \(\forall x A(x) \rightarrow A(t)\) | \(A(t) \rightarrow \exists x A(x)\) | \(\bot \rightarrow A\) |
| \((A \rightarrow (B \rightarrow C))
\rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))\) |
| \(A \rightarrow (B \rightarrow A
\wedge B)\) |
| \((A \rightarrow C) \rightarrow ( (B
\rightarrow C) \rightarrow (A \vee B \rightarrow C))\) |
| \(\forall x (B \rightarrow A(x))
\rightarrow (B \rightarrow \forall x A(x))\) | \(\forall x (A(x) \rightarrow B)
\rightarrow (\exists x A(x) \rightarrow B)\) |



with the usual side conditions for the last two axioms, and the rule
Modus Ponens, 

 

\[
 \text{from \(A\) and \((A \rightarrow B)\) infer \(B\)},
\]


as the only rule of inference. Intuitionistic logic has been an object
of investigation ever since Heyting formulated it. Already at the
propositional level it has many properties that sets it apart from
classical logic, such as the Disjunction Property: 

 

\[\tag{\({\bf DP}\)} 
{\bf IQC} \vdash A \vee B \text{ implies }{\bf IQC} \vdash A \text{ or } {\bf IQC} \vdash B.
\]


This principle is clearly violated in classical logic, because
classical logic proves \((A \vee \neg A)\) also for formulas that are
independent of the logic, i.e. for which both \(A\) and \(\neg A\) are
not a tautology. The inclusion of the principle Ex Falso Sequitur
Quodlibet, \((\bot \rightarrow A)\), in intuitionistic logic is a
point of discussion for those studying Brouwer's remarks on the
subject; in van Atten 2008, it is argued that the principle is not
valid in Intuitionism and that the logical principles valid according
to Brouwer's views are those of relevance logic. See van Dalen
2004 for more on Brouwer and Ex Falso Sequitur Quodlibet. 



Although till today all the logic used in intuitionistic reasoning is
contained in **IQC**, it is in principle conceivable that at some
point there will be found a principle acceptable from the
intuitionistic point of view that is not covered by this logic. For
most forms of constructivism the widely accepted view is that this
will not ever be the case, and thus **IQC** is considered to be
*the* logic of constructivism. For intuitionism the situation
is less clear because it cannot be excluded that at some point our
intuitionistic understanding might lead us to new logical principles
that we did not grasp before. 



One of the reasons for the widespread use of intuitionistic logic is
that it is well-behaved both from the proof-theoretic as the
model-theoretic point of view. There exist a great many proof systems
for it, such as Gentzen calculi and natural deduction systems, as well
as various forms of semantics, such as Kripke models, Beth models,
Heyting algebras, topological semantics and categorical models.
Several of these semantics are, however, only classical means to study
intuitionistic logic, for it can be shown that an intuitionistic
completeness proof with respect to them cannot exist (Kreisel 1962).
It has, however, been shown that there are alternative but a little
less natural models with respect to which completeness does hold
constructively (Veldman 1976). The constructive character of
intuitionistic logic becomes particularly clear in the Curry-Howard
isomorphism that establishes a correspondence between derivations in
the logic and terms in simply typed \(\lambda\)-calculus, that is,
between proofs and computations. The correspondence preserves
structure in that reduction of terms correspond to normalization of
proofs. 


### 3.3 The natural numbers



The existence of the natural numbers is given by the first act of
intuitionism, that is by the perception of the movement of time and
the falling apart of a life moment into two distinct things: what was,
1, and what is together with what was, 2, and from there to 3, 4, ...
In contrast to classical mathematics, in intuitionism all infinity is
considered to be potential infinity. In particular this is the case
for the infinity of the natural numbers. Therefore statements that
quantify over this set have to be treated with caution. On the other
hand, the principle of induction is fully acceptable from an
intuitionistic point of view.



Because of the finiteness of a natural number in contrast to, for
example, a real number, many arithmetical statements of a finite
nature that are true in classical mathematics are so in intuitionism
as well. For example, in intuitionism every natural number has a prime
factorization; there exist computably enumerable sets that are not
computable; \((A \vee \neg A)\) holds for all quantifier free
statements \(A\). For more complex statements, such as van der
Waerden's theorem or Kruskal's theorem, intuitionistic
validity is not so straightforward. In fact, the intuitionistic proofs
of both statements are complex and deviate from the classical proofs
(Coquand 1995, Veldman 2004).



Thus in the context of the natural numbers, intuitionism and classical
mathematics have a lot in common. It is only when other infinite sets
such as the real numbers are considered that intuitionism starts to
differ more dramatically from classical mathematics, and from most
other forms of constructivism as well.


### 3.4 The continuum



In intuitionism, the continuum is both an extension and a restriction
of its classical counterpart. In its full form, both notions are
incomparable since the intuitionistic real numbers possess properties
that the classical real numbers do not have. A famous example, to be
discussed below, is the theorem that in intuitionism every total
function on the continuum is continuous. That the intuitionistic
continuum does not satisfy certain classical properties can be easily
seen via *weak counterexamples*. That it also contains
properties that the classical reals do not posses stems from the
existence, in intuitionism, of *choice sequences*.


#### Weak counterexamples



The *weak counterexamples*, introduced by Brouwer in 1908, are
the first examples that Brouwer used to show that the shift from a
classical to an intuitionistic conception of mathematics is not
without consequence for the mathematical truths that can be
established according to these philosophies. They show that certain
classical statements are presently unacceptable from an intuitionistic
point of view. As an example, consider the sequence of real numbers
given by the following definition: 

 

\[
r\_n = 
 \begin{cases}
 2^{-n} \text{ if } \forall m \leq n A(m) \\
 2^{-m} \text{ if } \neg A(m) \wedge m \leq n \wedge \forall k \lt m A(k). 
 \end{cases}
\]


Here \(A(n)\) is a decidable property for which \(\forall n A(n)\) is
not known to be true or false. Decidability means that at present for
any given \(n\) there exists (can be constructed) a proof of \(A(n)\)
or of \(\neg A(n)\). At the time of this writing, we could for example
let \(A(n)\) express that \(n\), if greater than 2, is the sum of
three primes; \(\forall n A(n)\) then expresses the (original)
Goldbach conjecture that every number greater than 2 is the sum of
three primes. The sequence \(\langle r\_n \rangle\) defines a real
number \(r\) for which the statement \(r=0\) is equivalent to the
statement \(\forall n A(n)\). It follows that the statement \((r = 0
\vee r \neq 0)\) does not hold, and therefore that the law of
trichotomy \(\forall x(x \lt y \vee x=y \vee x \gt y)\) is not true on
the intuitionistic continuum.



Note the subtle difference between "\(A\) is not
intuitionistically true " and "\(A\) is intuitionistically
refutable": in the first case we know that \(A\) cannot have an
intuitionistic proof, the second statement expresses that we have a
proof of !*A*, i.e. a construction that derives falsum from
any possible proof of \(A\). For the law of trichotomy we have just
shown that it is not intuitionistically true. Below it will be shown
that even the second stronger form saying that the law is refutable
holds intuitionistically. This, however, is not true for all
statements for which there exist weak counterexamples. For example,
the Goldbach conjecture is a weak counterexample to the principle of
the excluded middle, since \(\forall n A(n)\) as above is at present
not known to be true or false, and thus we cannot assert \(\forall n
A(n) \vee \neg \forall n A(n)\) intuitionistically, at least not at
this moment. But the refutation of this statement, \(\neg (\forall n
A(n) \vee \neg \forall n A(n))\), is not true in intuitionism, as one
can show that for any statement \(B\) a contradiction can be derived
from the assumption that \(\neg B\) and \(\neg\neg B\) hold (and thus
also from \(B\) and \(\neg B\)). In other words, \(\neg\neg (B \vee
\neg B)\) is intuitionistically true, and thus, although there exist
weak counterexamples to the principle of the excluded middle, its
negation is false in intuitionism, that is, it is intuitionistically
refutable.



The existence of real numbers \(r\) for which the intuitionist cannot
decide whether they are positive or not shows that certain classically
total functions cease to be so in an intuitionistic setting, such as
the piecewise constant function

 

\[
f(r) = 
 \begin{cases}
 0 \text{ if } r \geq 0 \\
 1 \text{ if } r \lt 0. 
 \end{cases}
\]


There exist weak counterexamples to many classically valid statements.
The construction of these weak counterexamples often follow the same
pattern as the example above. For example, the argument that shows
that the intermediate value theorem is not intuitionistically valid
runs as follows. Let \(r\) be a real number in [[?]1,1] for which
\((r\leq 0 \vee 0 \lt r)\) has not been decided, as in the example
above. Define the uniformly continuous function \(f\) on \([0,3]\)
by

 

\[
 f(x) = \text{min}(x-1,0) + \text{max}(0,x-2) + r.
\]


Clearly, \(f(0) = -1 +r\) and \(f(3) = 1 + r\), whence \(f\) takes the
value 0 at some point \(x\) in [0,3]. If such \(x\) could be
determined, either \(1 \leq x\) or \(x \leq 2\). Since \(f\) equals
\(r\) on \([1,2]\), in the first case \(r \leq 0\) and in the second
case \(0\leq r\), contradicting the undecidability of the statement
\((r\leq 0 \vee 0 \leq r)\).



These examples seem to indicate that in the shift from classical to
intuitionistic mathematics one loses several fundamental theorems of
analysis. This however is not so, since in many cases intuitionism
regains such theorems in the form of an analogue in which existential
statements are replaced by statements about the existence of
approximations within arbitrary precision, as in this classically
equivalent form of the intermediate value theorem that is
constructively valid:



> 
> 
> **Theorem**. For every continuous real-valued function
> \(f\) on an interval \([a,b]\) with \(a \lt b\), for every \(c\)
> between \(f(a)\) and \(f(b)\), the following holds:
> 
>  
> 
> \[
>  \forall n \exists x \in [a,b] \, |f(x)-c| \lt 2^{-n}.
> \]
> 
> 



Weak counterexamples are a means to show that certain mathematical
statements do not hold intuitionistically, but they do not yet reveal
the richness of the intuitionistic continuum. Only after
Brouwer's introduction of choice sequences did intuitionism
obtain its particular flavor and became incomparable with classical
mathematics.


#### Choice sequences


Choice sequences were introduced by Brouwer to capture the
intuition of the continuum. Since for the intuitionist all infinity is
potential, infinite objects can only be grasped via a process that
generates them step-by-step. What will be allowed as a legitimate
construction therefore decides which infinite objects are to be
accepted. For example, in most other forms of constructivism only
computable rules for generating such objects are allowed, while in
Platonism infinities are considered to be completed totalities whose
existence is accepted even in cases when no generating rules are
known.



Brouwer's second act of intuitionism gives rise to choice
sequences, that provide certain infinite sets with properties that are
unacceptable from a classical point of view. A choice sequence is an
infinite sequence of numbers (or finite objects) created by the free
will. The sequence could be determined by a law or algorithm, such as
the sequence consisting of only zeros, or of the prime numbers in
increasing order, in which case we speak of a *lawlike*
sequence, or it could not be subject to any law, in which case it is
called *lawless*. Lawless sequences could for example be
created by the repeated throw of a coin, or by asking the Creating
Subject to choose the successive numbers of the sequence one by one,
allowing it to choose any number to its liking. Thus a lawless
sequence is ever unfinished, and the only available information about
it at any stage in time is the initial segment of the sequence created
thus far. Clearly, by the very nature of lawlessness we can never
decide whether its values will coincide with a sequence that is
lawlike. Also, the free will is able to create sequences that start
out as lawlike, but for which at a certain point the law might be
lifted and the process of free choice takes over to generate the
succeeding numbers, or vice versa.



According to Brouwer every real number is represented by a choice
sequence, and the choice sequences enabled him to capture the
intuitionistic continuum via the controversial continuity axioms.
Brouwer first spoke of choice sequences in his inaugural address
(Brouwer 1912), but at that time he did not yet treat them as a
fundamental part of his mathematics. Gradually they became more
important and from 1918 on Brouwer started to use them in a way
explained in the next section. 


### 3.5 Continuity axioms



The acceptance of the notion of choice sequence has far-reaching
implications. It justifies, for the intuitionist, the use of the
continuity axioms, from which classically invalid statements can be
derived. The weakest of these axioms is the weak continuity axiom:


 

\[\tag{\({\bf WC\mbox{-}N}\)}
\forall\alpha\exists n A(\alpha,n) \rightarrow 
\forall\alpha\exists m\exists n \forall\beta\in\alpha(\overline{m})A(\beta,n).
\]


Here \(n\) and \(m\) range over natural numbers, \(\alpha\) and
\(\beta\) over choice sequences, and \(\beta\in\alpha(\overline{m})\)
means that the first \(m\) elements of \(\alpha\) and \(\beta\) are
equal. Although until now there has never been given a completely
satisfactory justification of most continuity axioms for arbitrary
choice sequences, not even by Brouwer, when restricted to the class of
lawless sequences arguments supporting the validity of the weak
continuity axiom run as follows. When could a statement of the form
\(\forall\alpha\exists n A(\alpha,n)\) be established by the
intuitionist? By the very nature of the notion of lawless sequence,
the choice of the number \(n\) for which \(A(\alpha,n)\) holds has to
be made after only a finite initial segment of \(\alpha\) is known.
For we do not know how \(\alpha\) will proceed in time, and we
therefore have to base the choice of \(n\) on the initial segment of
\(\alpha\) that is known at that point in time where we wish to fix
\(n\). This implies that for every lawless sequence \(\beta\) with the
same initial segment as \(\alpha\), \(A(\beta,n)\) holds as well. 



The weak continuity axiom has been shown to be consistent, and is
often applied in a form that can be justified, namely in the case in
which the predicate \(A\) only refers to the values of \(\alpha\), and
not to the higher order properties that it possibly possesses. The
details of the argument will be omitted here, but it contains the same
ingredients as the justification of the principle for lawless
sequences, and can be found in van Atten and van Dalen 2002.



Weak continuity does not exhaust the intuitionists' intuition
about the continuum, for given the weak continuity axiom, it seems
reasonable to assume that the choice of the number \(m\) such that
\(\forall\beta\in\alpha(\overline{m})A(\beta,n)\), could be made
explicit. Thus \(\forall\alpha\exists n A(\alpha,n)\) implies the
existence of a continuous functional \(\Phi\) that for every
\(\alpha\) produces the \(m\) that fixes the length of \(\alpha\) on
the basis of which \(n\) is chosen. More formally, let
\(\mathcal{CF}\) be the class of continuous functionals \(\Phi\) that
assign natural numbers to infinite sequences, i.e. that satisfy



\[ \forall\alpha\exists
 m\forall\beta\in\alpha(\overline{m})\Phi(\alpha)=\Phi(\beta). \]


The full axiom of continuity, which is an extension of the weak
continuity axiom, can then be expressed as: 

 

\[\tag{\({\bf C\mbox{-}N}\)}
\forall\alpha\exists n A(\alpha,n) \rightarrow 
\exists \Phi \in \mathcal{CF}\,\forall\alpha A(\alpha,\Phi(\alpha)).
\]


Through the continuity axiom certain weak counterexamples can be
transformed into genuine refutations of classically accepted
principles. For example, it implies that the quantified version of the
principle of the excluded middle is false:

 

\[
 \neg\forall\alpha(\forall n\alpha (n)=0 \vee \neg \forall n\alpha (n)=0).
\]


Here \(\alpha(n)\) denotes the \(n\)-th element of \(\alpha\). To see
that this negations holds, suppose, arguing by contradiction, that
\(\neg\forall\alpha(\forall n\alpha (n)=0 \vee \neg \forall n\alpha
(n)=0)\) holds. This implies that 

 

\[
 \forall\alpha\exists k((\forall n\alpha (n)=0 \wedge k=0) \vee 
 (\neg \forall n\alpha (n)=0 \wedge k=1)).
\]


By the weak continuity axiom, for \(\alpha\) consisting of only zeros
there exists a number \(m\) that fixes the choice of \(k\), which
means that for all \(\beta\in\alpha(\overline{m})\), \(k=0\). But the
existence of sequences whose first \(m\) elements are 0 and that
contain a 1 show that this cannot be.



This example showing that the principle of the excluded middle not
only does not hold but is in fact false in intuitionism, leads to the
refutation of many basic properties of the continuum. Consider for
example the real number \(r\_\alpha\) that is the limit of the sequence
consisting of the numbers \(r\_n\) as given in the section on weak
counterexamples, where the \(A(m)\) in the definition is taken to be
the statement \(\alpha(m)=0\). Then the refutation above implies that
\(\neg\forall\alpha(r\_\alpha=0 \vee r\_\alpha\neq 0)\), and it thereby
refutes the law of trichotomy:

 

\[
 \forall x (x \lt y \vee x=y \vee y \lt x).
\]


The following theorem is another example of the way in which the
continuity axiom refutes certain classical principles. 



> 
>  **Theorem**  \({\bf (C\mbox{-}N)}\) Every total real
> function is continuous.
> 



Indeed, a classical counterexample to this theorem, the nowhere
continuous function 

\[
 f(x) = 
 \begin{cases}
 0 \text{ if \(x\) is a rational number } \\
 1 \text{ if \(x\) is an irrational number} 
 \end{cases}
\]

 is not a legitimate function from the
intuitionistic point of view since the property of being rational is
not decidable on the real numbers. The theorem above implies that the
continuum is not decomposable, and in van Dalen 1997, it is shown that
this even holds for the set of irrational numbers.



The two examples above are characteristic for the way in which the
continuity axioms are applied in intuitionistic mathematics. They are
the only axioms in intuitionism that contradict classical reasoning,
and thereby represent the most colorful as well as the most
controversial part of Brouwer's philosophy.


#### Neighborhood Functions



There is a convenient representation of continuous functionals that
has been used extensively in the literature, though not by Brouwer
himself. Continuous functionals that assign numbers to infinite
sequences can be represented by *neighborhood functions*, where
a neighborhood function \(f\) is a function on the natural numbers
satisfying the following two properties (\(\cdot\) denotes
concatenation and \(f(\alpha(\overline{n}))\) denotes the value of
\(f\) on the code of the finite sequence
\(\alpha(\overline{n})\)).

 

\[
 \alpha\exists n f(\alpha(\overline{n})) \gt 0 \ \ \ \ 
 \forall n\forall m (f(n) \gt 0 \rightarrow f(n\cdot m) = f(n)). 
\]


Intuitively, if \(f\) represents \(\Phi\) then
\(f(\alpha(\overline{n}))=0\) means that \(\alpha(\overline{n})\) is
not long enough to compute \(\Phi(\alpha)\), and
\(f(\alpha(\overline{n}))=m+1\) means that \(\alpha(\overline{n})\) is
long enough to compute \(\Phi(\alpha)\) and that the value of
\(\Phi(\alpha)\) is \(m\). If \(\mathcal{K}\) denotes the class of
neighborhood functions, then the continuity axiom \({\bf C\mbox{-}N}\)
can be rephrased as 

\[
 \forall \alpha\exists n A(\alpha,n) \rightarrow 
 \exists f \in \mathcal{K}\, \forall m(f(m) \gt 0 \rightarrow 
 \forall \beta \in m A(\beta,f(m-1))), 
\]

 



where \(\beta \in m\) means that the code of the initial segment of
\(\beta\) is \(m\).


### 3.6 The bar theorem



Brouwer introduced choice sequences and the continuity axioms to
capture the intuitionistic continuum, but these principles alone do
not suffice to recover that part of traditional analysis that Brouwer
considered intuitionistically sound, such as the theorem that every
continuous real function on a closed interval is uniformly continuous.
For this reason Brouwer proved the so-called bar theorem. It is a
classically valid statement, but the proof Brouwer gave is by many
considered to be no proof at all since it uses an assumption on the
form of proofs for which no rigorous argument is provided. This is the
reason that the bar theorem is also referred to as the bar principle.




The most famous consequence of the bar theorem is the fan theorem,
which suffices to prove the aforementioned theorem on uniform
continuity, and which will be treated first. Both the fan and the bar
theorem allow the intuitionist to use induction along certain
well-founded sets of objects called spreads. A *spread* is the
intuitionistic analogue of a set, and captures the idea of infinite
objects as ever growing and never finished. A spread is essentially a
countably branching tree labelled with natural numbers or other finite
objects and containing only infinite paths.



A *fan* is a finitely branching spread, and the fan principle
expresses a form of compactness that is classically equivalent to
Konig's lemma, the classical proof of which is unacceptable
from the intuitionistic point of view. The principle states that for
every fan \(T\) in which every branch at some point satisfies a
property \(A\), there is a uniform bound on the depth at which this
property is met. Such a property is called a *bar* for
\(T\).

 

\[\tag{\({\bf FAN}\)}
\forall \alpha \in T\exists n A(\alpha(\overline{n})) \rightarrow 
\exists m \forall \alpha \in T \exists n \leq m A(\alpha(\overline{n})).
\]


Here \(\alpha \in T\) means that \(\alpha\) is a branch of \(T\). The
principle **FAN** suffices to prove the theorem mentioned
above: 



> 
> **Theorem** (**FAN**) Every continuous real
> function on a closed interval is uniformly continuous.
> 



Brouwer's justification for the fan theorem is his bar principle
for the universal spread:

 

\[\tag{\({\bf BI}\)}
\begin{align}
& [\forall\alpha\forall n \big( A(\alpha(\overline{n})) \vee \neg A(\alpha(\overline{n})) \big)
 \wedge \forall\alpha\exists n A(\alpha(\overline{n}))\ \wedge\\
&\quad \forall\alpha\forall n \big( A(\alpha(\overline{n})) \rightarrow
 B(\alpha(\overline{n})) \big)\ \wedge \\
&\quad \forall\alpha\forall n \big(
 \forall mB(\alpha(\overline{n})\cdot m) \rightarrow
 B(\alpha(\overline{n})) \big)] \rightarrow B(\varepsilon).
\end{align} 
\]


Here \(\varepsilon\) stands for the empty sequence, \(\cdot\) for
concatenation, **BI** for Bar Induction, and the
subscript **D** refers to the decidability of the
predicate \(A\). The bar principle provides intuitionism with an
induction principle for trees; it expresses a well-foundedness
principle for spreads with respect to decidable properties. Extensions
of this principle in which the decidability requirement is weakened
can be extracted from Brouwer's work but will be omitted here.
Continuity and the bar principle are sometimes captured in one axiom
called the *bar continuity axiom*.



There is a close connection between the bar principle and the
neighborhood functions mentioned in the section on continuity axioms.
Let \(\mathcal{IK}\) be the inductively defined class of neighborhood
functions, consisting of all constant non-zero sequences \(\lambda
m.n+1\), and such that if \(f(0)=0\) and \(\lambda m.f(x\cdot m)\in
\mathcal{IK}\) for all \(x\), then \(f \in \mathcal{IK}\). The
statement \(\mathcal{K}=\mathcal{IK}\), that is, the statement that
the neighborhood functions can be generated inductively, is equivalent
to **BID**. 



Brouwer's proof of the bar theorem is remarkable in that it uses
well-ordering properties of *hypothetical* proofs. It is based
on the assumption that any proof that a property *A* on
sequences is a bar can be decomposed into a *canonical proof*
that is well-ordered. Although it is classically valid,
Brouwer's proof of the principle shows that the reason for
accepting it as a valid principle in intuitionism differs
fundamentally from the argument supporting its acceptability in
classical mathematics.


### 3.7 Choice axioms



The axiom of choice in its full form is unacceptable from a
constructive point of view, at least in the presence of certain other
central axioms of set theory, such as extensionality (Diaconescu
1975). For let \(A\) be a statement that is not known to be true or
false. Then membership of the following two sets is undecidable. 



\[

\begin{align}
 X &= \{ x \in \{0,1\} \mid x=0 \vee (x=1 \wedge A) \} \\
 Y &= \{ y \in \{0,1\} \mid y=1 \vee (y=0 \wedge A) \}
\end{align}

\]


The existence of a choice function \(f:\{X,Y\} \rightarrow \{0,1\}\)
choosing an element from \(X\) and \(Y\) would imply \((A \vee \neg
A)\). For if \(f(X)\neq f(Y)\), it follows that \(X\neq Y\), and hence
\(\neg A\), whereas \(f(X)=f(Y)\) implies \(A\). Therefore a choice
function for \(\{X,Y\}\) cannot exist. 



There are, however, certain restrictions of the axiom that are
acceptable for the intuitionist, for example the *axiom of
countable choice*, also accepted as a legitimate principle by the
semi-intuitionists to be discussed below:

 

\[\tag{\({\bf AC\mbox{-}N}\)}
\forall R \subseteq \mathbb{N} \times \mathbb{N} \big( 
 \forall m\exists n\, mRn \rightarrow 
 \exists \alpha \in \mathbb{N}^\mathbb{N} \forall m\, mR\alpha(m) \big).
\]


This scheme may be justified as follows. A proof of the premise should
provide a method that given \(m\) provides a number \(n\) such that
\(mRn\). Thus the function \(\alpha\) on the natural numbers
\(\mathbb{N}\) can be constructed step-by-step: first an element
\(m\_0\) is chosen such that \(0Rm\_0\), which will be the value of
\(\alpha(0)\). Then an element \(m\_1\) is chosen such that \(1Rm\_1\),
which will be the value of \(\alpha(1)\), and so on. 



Several other choice axioms can be justified in a similar way. Only
one more will be mentioned here, the axiom of dependent choice:



\[\tag{\({\bf DC\mbox{-}N}\)}
\begin{align}
 \forall R \subseteq
 \mathbb{N} \times \mathbb{N} \big( \forall m\exists n\, mRn
 \rightarrow& \forall k \exists \alpha \in \mathbb{N}^\mathbb{N} \big(
 \alpha(0)=k\ \wedge\\
& \forall i\geq 0\, \alpha(i)R\alpha(i+1) \big) \big).
\end{align}\]


Also in classical mathematics the choice axioms are treated with care,
and it is often explicitly mentioned how much choice is needed in a
proof. Since the axiom of dependent choice is consistent with an
important axiom in classical set theory (the axiom of determinacy)
while the full axiom of choice is not, special attention is payed to
this axiom and in general one tries to reduce the amount of choice in
a proof, if choice is present at all, to dependent choice. 


### 3.8 Descriptive set theory, topology, and topos theory



Brouwer was not alone in his doubts concerning certain classical forms
of reasoning. This is particularly visible in descriptive set theory,
which emerged as a reaction to the highly nonconstructive notions
occurring in Cantorian set theory. The founding fathers of the field,
including Emile Borel and Henri Lebesgue as two of the main
figures, were called *semi-intuitionists*, and their
constructive treatment of the continuum led to the definition of the
Borel hierarchy. From their point of view a notion like the set of all
sets of real numbers is meaningless, and therefore has to be replaced
by a hierarchy of subsets that do have a clear description. 



In Veldman 1999, an intuitionistic equivalent of the notion of Borel
set is formulated, and it is shown that classically equivalent
definitions of the Borel sets give rise to a variety of
intuitionistically distinct classes, a situation that often occurs in
intuitionism. For the intuitionistic Borel sets an analogue of the
Borel Hierarchy Theorem is intuitionistically valid. The proof of this
fact makes essential use of the continuity axioms discussed above and
thereby shows how classical mathematics can guide the search for
intuitionistic analogues that, however, have to be proved in a
completely different way, sometimes using principles unacceptable from
a classical point of view.



Another approach to the study of subsets of the continuum, or of a
topological space in general, has appeared through the development of
formal or abstract topology (Fourman 1982, Martin-Lof 1970,
Sambin 1987). In this constructive topology the role of open sets and
points is reversed; in classical topology an open set is defined as a
certain set of points, in the constructive case open sets are the
fundamental notion and points are defined in terms of them. Therefore
this approach is sometimes referred to as point-free topology.



Intuitionistic functional analysis has been developed far and wide by
many after Brouwer, but since most approaches are not strictly
intuitionistic but also constructive in the wider sense, this research
will not be addressed any further here.


## 4. Constructivism



Intuitionism shares a core part with most other forms of
constructivism. Constructivism in general is concerned with
constructive mathematical objects and reasoning. From constructive
proofs one can, at least in principle, extract algorithms that compute
the elements and simulate the constructions whose existence is
established in the proof. Most forms of constructivism are compatible
with classical mathematics, as they are in general based on a stricter
interpretation of the quantifiers and the connectives and the
constructions that are allowed, while no additional assumptions are
made. The logic accepted by almost all constructive communities is the
same, namely intuitionistic logic. 



Many existential theorems in classical mathematics have a constructive
analogue in which the existential statement is replaced by a statement
about approximations. We saw an example of this, the intermediate
value theorem, in the section on weak counterexamples above. Large
parts of mathematics can be recovered constructively in a similar way.
The reason not to treat them any further here is that the focus in
this entry is on those aspects of intuitionism that set it apart from
other constructive branches of mathematics. For a thorough treatment
of constructivism the reader is referred to the corresponding entry in
this encyclopedia.


## 5. Meta-mathematics



Although Brouwer developed his mathematics in a precise and
fundamental way, formalization in the sense as we know it today was
only carried out later by others. Indeed, according to Brouwer's
view that mathematics unfolds itself internally, formalization,
although not unacceptable, is unnecessary. Others after him thought
otherwise, and the formalization of intuitionistic mathematics and the
study of its meta-mathematical properties, in particular of arithmetic
and analysis, have attracted many researchers. The formalization of
intuitionistic logic on which all formalizations are based has already
been treated above. 


### 5.1 Arithmetic



Heyting Arithmetic **HA** as formulated by Arend Heyting
is a formalization of the intuitionistic theory of the natural numbers
(Heyting 1956). It has the same non-logical axioms as Peano Arithmetic
**PA** but it is based on intuitionistic logic. Thus it
is a restriction of classical arithmetic, and it is the accepted
theory of the natural numbers in almost all areas of constructive
mathematics. Heyting Arithmetic has many properties that reflect its
constructive character, for example the Disjunction Property that
holds for intuitionistic logic too. Another property of
**HA** that **PA** does not share is the
numerical existence property: (\(\overline{n}\) is the numeral
corresponding to natural number \(n\)) 

 

\[\tag{\({\bf NEP}\)}
{\bf HA} \vdash \exists x A(x) \Rightarrow 
\exists n \in {\mathbb N} \, {\bf HA} \vdash A(\overline{n}). 
\]


That this property does not hold in **PA** follows from
the fact that **PA** proves \(\exists x (A(x) \vee
\forall y \neg A(y))\). Consider, for example, the case that \(A(x)\)
is the formula \(T(e,e,x)\), where \(T\) is the decidable Kleene
predicate expressing that \(x\) is the code of a terminating
computation of the program with code \(e\) on input \(e\). If for
every \(e\) there would exist a number \(n\) such that \({\bf
PA}\vdash T(e,e,n) \vee \forall y \neg T(e,e,y)\), then by checking
whether \(T(e,e,n)\) holds it would be decided whether a program \(e\)
terminates on input \(e\). This, however, is in general undecidable.




Markov's rule is a principle that holds both classically and
intuitionistically, but only for **HA** the proof of this
fact is nontrivial: 

 

\[\tag{\({\bf MR}\)}
{\bf HA} \vdash \forall x (A(x) \vee \neg A(x)) \wedge 
\neg\neg\exists x A(x) \Rightarrow {\bf HA}
 \vdash \exists x A(x).
\]


Since **HA** proves the law of the excluded middle for
every primitive recursive predicate, it follows that for such \(A\)
the derivability of \(\neg\neg \exists x A(x)\) in **HA**
implies the derivability of \(\exists x A(x)\) as well. From this it
follows that **PA** is \(\Pi^0\_2\)-conservative over
**HA**. That is, for primitive recursive \(A\):

\[
 {\bf PA} \vdash \forall x \exists y A(x,y) 
 \Rightarrow 
 {\bf HA} \vdash \forall x \exists y A(x,y).
\]

 Thus the class of provably recursive functions of
**HA** coincides with the class of provably recursive
functions of **PA**, a property that, on the basis of the
ideas underlying constructivism and intuitionism, may not come as a
surprise. 


### 5.2 Analysis



The formalization of intuitionistic mathematics covers more than
arithmetic. Large parts of analysis have been axiomatized from a
constructive point of view (Kleene 1965, Troelstra 1973). The
constructivity of these systems can be established using functional,
type theoretic, or realizability interpretations, most of them based
on or extensions of Godel's Dialectica interpretation
(Godel 1958, Kreisel 1959), Kleene realizability (Kleene 1965),
or type theories (Martin-Lof 1984). In these interpretations the
functionals underlying constructive statements, such as for example
the function assigning a \(y\) to every \(x\) in \(\forall x\exists y
A(x,y)\), are made explicit in various ways.



In (Scott 1968 and 1970), a topological model for the second-order
intuitionistic theory of analysis is presented where the reals are
interpreted as continuous functions from Baire space into the
classical reals. In this model Kripke's Schema as well as
certain continuity axioms hold. In (Moschovakis 1973), this method is
adapted to construct a model of theories of intuitionistic analysis in
terms of choice sequences. Also in this model Kripke's Schema
and certain continuity axioms hold. In (Van Dalen 1978) Beth models
are used to provide a model of arithmetic and choice sequences that
satisfy choice schemata, instances of weak continuity and
Kripke's Schema. In this model the domains at every node are the
natural numbers, so that one does not have to use nonstandard models,
as in the case of Kripke models. Moreover, the axioms
**CS1-3** of the creating subject can be
interpreted in it, thus showing this theory to be consistent. 


### 5.3 Lawless sequences



There exist axiomatizations of the lawless sequences, and they all
contain extensions of the continuity axioms (Kreisel 1968, Troelstra
1977). In particular in the form of the Axiom of Open Data stating
that for \(A(\alpha)\) not containing other nonlawlike parameters
besides \(\alpha\): 

 

\[

 A(\alpha) \rightarrow \exists n \forall \beta \in \alpha (\overline{n}) A(\beta). 

\]


In (Troelstra 1977), a theory of lawless sequences is developed (and
justified) in the context of intuitionistic analysis. Besides axioms
for elementary analysis it contains, for lawless sequences,
strengthened forms of the axioms of open data, continuity,
decidability and density (density says that every finite sequence is
the initial segment of a lawless sequence). What is especially
interesting is that in these theories quantifiers over lawless
sequences can be eliminated, a result that can also be viewed as
providing a model of lawlike sequences for such theories. Other
classical models of the theory of lawless sequences have been
constructed in category theory in the form of sheaf models (van der
Hoeven and Moerdijk 1984). In (Moschovakis 1986), a theory for choice
sequences relative to a certain set of lawlike elements is introduced,
along with a classical model in which the lawless sequences turn out
to be exactly the generic ones.


### 5.4 Formalization of the Creating Subject



The Creating Subject, introduced in Section 2.2, can generate choice
sequences, which are some of the most important and complicated
mathematical entities of Brouwer's Intuitionism. Several
philosophers and mathematicians have tried to develop the theory of
the Creating Subject further mathematically as well as
philosophically. 



In the formalization of the notion of the Creating Subject its
temporal aspect is formalized using the notation \(\Box\_n A\), that
denotes that the Creating Subject has a proof of A at time n (in some
other formulations: experiences the truth of \(A\) at time \(n\)).
Georg Kreisel (1967) introduced the following three axioms for the
Creating Subject, which taken together are denoted by **CS**:



\[\begin{align}
\tag{\({\bf CS1}\)}
& \Box\_n A \vee \neg \Box\_n A \\ 
& \mbox{(at time \(n\), it can be decided whether the Creating Subject} \\ 
& \mbox{ has a proof of A)} \\ 
\tag{\({\bf CS2}\)}
& \Box\_m A \rightarrow \Box\_{m+n}A \\ 
& \mbox{(the Creating Subject never forgets what it has proven)} \\ 
\tag{\({\bf CS3}\)}
& (\exists n \Box\_n A \rightarrow A) \wedge (A \rightarrow \neg\neg \exists n \Box\_n A)\\ 
& \mbox{(the Creating Subject only proves what is true and no} \\ 
& \mbox{ true statement can be impossible to prove for the} \\ 
& \mbox{ Creating Subject)}\\
\end{align}\]


In the version of Anne Troelstra (1969) the last axiom is strengthened
to 

 

\[\begin{align}
\tag{\({\bf CS3}^+\)}
& \exists n \Box\_n A \leftrightarrow A \\ 
& \mbox{(the Creating Subject only proves what is true and what} \\ 
& \mbox{ is true will be proved by the Creating Subject at some} \\
& \mbox{ point)}
\end{align}\]


The first axiom **CS1** is uncontroversial: at any point in time,
it can be established whether the Creating Subject has a proof of a
given statement or not. The second axiom **CS2** clearly uses the
fact that the Creating Subject is an idealization since it expresses
that proofs will always be remembered. The last axiom **CS3** is
the most disputed part of the formalization of the Creating Subject,
or better, its second conjunct \((A \rightarrow \neg\neg\exists n\Box\_n A)\)
is, which was given the name *Axiom of Christian Charity* by
Kreisel. Goran Sundholm (2014), for example, argues that Axiom of
Christian Charity is not acceptable from a constructive point of view.
And Godel's incompleteness theorem even implies that the
principle is false when \(\Box\_n A\) would be interpreted as being
provable in a sufficiently strong proof system, which, however, is
certainly not the interpretation that Brouwer had in mind. 



Given a statement \(A\) that does not contain any reference to time,
i.e. no occurrence of \(\Box\_n\), one can define a choice sequence
according to the following rule (Brouwer 1953): 

 

\[
 \alpha (n) = \left\{ \begin{array}{ll}
 0 & \mbox{ if \(\neg \Box\_n A\)} \\
 1 & \mbox{ if \(\Box\_n A\). } 
 \end{array} \right.
\]


From this follows the principle known as Kripke's Schema
**KS**, introduced in Section 2.2, a principle that unlike the
axioms of the theory of the Creating Subject, contains no explicit
reference to time: \(\exists \alpha (A \leftrightarrow \exists n
\alpha(n) = 1)\).



Using Kripke's Schema, the weak counter example arguments can be
expressed formally without any reference to the Creating Subject. The
following example is taken from (van Atten 2018). Let A be a statement
for which at present \(\neg A \vee \neg\neg A\) is not known to hold.
Using **KS** one obtains choice sequences \(\alpha\_1\) and
\(\alpha\_2\) such that 

 

\[ \neg A \leftrightarrow \exists n \alpha\_1(n) = 1 \ \ \ \ \neg\neg A
 \leftrightarrow \exists n \alpha\_2(n) = 1. \]


Associate with these two sequences the real numbers \(r\_0\) and
\(r\_1\), where for \(i=0,1\): 

 

\[
r\_i(n) = 
 \begin{cases}
 0 & \text{ if \(\alpha\_i(n)\neq 1\)} \\
 (-1)^i2^{-m} & \begin{align} &\text{if for some \(m\leq n\), \(\alpha\_i(m)=1\) and } \\
 & \text{for no \(k \lt m\), \(\alpha\_i(k)=1.\)} 
 \end{align}
 \end{cases}
\]


Then for \(r=r\_0 + r\_1\), statement \(\neg A \vee \neg\neg A\) is
implied by \((r\gt 0\vee r\lt 0)\), which shows that \((r\gt 0\vee
r\lt 0)\) cannot be proved. 



In (van Dalen 1978) a model is constructed of the axioms for the
Creating Subject in the context of arithmetic and choice sequences,
thus proving them to be consistent with intuitionistic arithmetic and
certain parts of analysis. In (van Dalen 1982), **CS** is proven to
be conservative over Heyting Arithmetic. Mathematical consequences of
Kripke's Schema can be found in (van Dalen 1997), where it is
shown that **KS** and the continuity axioms reject Markov's
principle, while **KS** together with Markov's principle
implies the principle of the excluded middle. 



Kripke has shown that **KS** implies the existence of nonrecursive
functions, a result not published by him but by Kreisel (1970).
Clearly, this implies that the theory **CS** also implies the
existence of a nonrecursive function. A possible argument for
**CS** runs as follows. Suppose \(X\) is a noncomputable but
computably enumerable set and define the function \(f\) as
follows:

 

\[
 f(m,n) = 
 \begin{cases}
 0 & \text{ if not \(\Box\_m (n \not\in X)\)} \\
 1 & \text{ if \(\Box\_m (n \not\in X)\).} 
 \end{cases}
\]


Then it follows that \(n\not\in X\) if and only if \(f(m,n)=1\) for
some natural number \(m\), which implies that \(f\) cannot be
computable. For if so, the complement of \(X\) would be computably
enumerable, implying the computability of \(X\). Since \(f\) is a
function from the intuitionistic point of view, this establishes that
in Intuitionism not all functions are computable. 


### 5.5 Foundations



Formalizations that are meant to serve as a foundation for
constructive mathematics are either of a set-theoretic (Aczel 1978,
Myhill 1975) or type-theoretic (Martin-Lof 1984) nature. The
former theories are adaptations of Zermelo-Fraenkel set theory to a
constructive setting, while in type theory the constructions implicit
in constructive statements are made explicit in the system. Set theory
could be viewed as an extensional foundation of mathematics whereas
type theory is in general an intensional one. 



In recent years many models of parts of such foundational theories for
intuitionistic mathematics have appeared, some of them have been
mentioned above. Especially in topos theory (van Oosten 2008) there
are many models that capture certain characteristics of intuitionism.
There are, for example, topoi in which all total real functions are
continuous. Functional interpretations such as realizability as well
as interpretations in type theory could also be viewed as models of
intuitionistic mathematics and most other constructive theories.


### 5.6 Reverse mathematics



In reverse mathematics one tries to establish for mathematical
theorems which axioms are needed to prove them. In intuitionistic
reverse mathematics one has a similar aim, but then with respect to
intuitionistic theorems: working over a weak intuitionistic theory,
axioms and theorems are compared to each other. The typical axioms
with which one wishes theorems to compare are the fan principle and
the bar principle, Kripke's schema and the continuity
axioms.



In (Veldman 2011), equivalents of the fan principle over a basic
theory called Basic Intuitionistic Mathematics are studied. It is
shown that the fan principle is equivalent to the statement that the
unit interval [0,1] has the Heine-Borel property, and from this many
other equivalents are derived. In (Veldman 2009), the fan principle is
shown to also be equivalent to Brouwer's Approximate Fixed-Point
Theorem. In (Lubarsky et al. 2012), reverse mathematics is applied to
a form of Kripke's schema, which is shown to be equivalent to
certain topological statements.



There are many more of such examples from intuitionistic reverse
mathematics. Especially in the larger field of constructive reverse
mathematics there are many results of this nature that are also
relevant from the intuitionistic point of view.


## 6. Philosophy



Brouwer build his Intuitionism from the ground up and did
not comment much on the relation between Intuitionism and other
existing philosophies, but others after him did. Some of these
connections are discussed in this section, in particular the way in
which intuitionistic principles can be justified in terms of other
philosophies.


### 6.1 Phenomenology



The connection between Intuitionism and Phenomenology, the philosophy
developed by Edmund Husserl, has been investigated by several authors,
during Brouwer's lifetime as well as decades later. Hermann Weyl
was among the first to discuss the relation between Brouwer's
ideas and the phenomenological view on mathematics. Like Brouwer, Weyl
speaks in his book *Das Kontinuum* (Chapter 2) about the
*intuitive continuum*, but Weyl's notion is based on the
phenomenology of (the consciousness of) time. Weyl later feels that
Brouwer's development of real analysis is more faithful to the
idea of the intuitive continuum than his own (Weyl 1921) and therefore
places himself at Brouwer's side, at least regarding this aspect
(van Atten 2002).



Van Atten (2003 en 2007) uses phenomenology to justify choice
sequences as mathematical objects. The author (2002) is critical about
Brouwer's justification of choice sequences, which is the motive
to look for a philosophical justification elsewhere. Choice sequences
occur in the work of Becker (1927) and Weyl, but they differ from
Brouwer's notion, and Husserl never discussed choice sequences
publicly. Van Atten explains how the *homogeneity* of the
continuum accounts for its inexhaustibility and nonatomicity, two key
properties of the intuitive continuum according to Brouwer. Using the
fact that these two essential properties are present in the definition
of choice sequences, one arrives at a phenomenological justification
of them. 


### 6.2 Wittgenstein



On March 10, 1928, Brouwer lectured in Vienna on his intuitionistic
foundations of mathematics. Ludwig Wittgenstein attended that lecture,
persuaded by Herbert Feigl, who afterwards wrote about the hours he
spent with Wittgenstein and others after the lecture: *a great
event took place. Suddenly and very volubly Wittgenstein began talking
philosophy - at great length. Perhaps this was the turning
point, for ever since that time, 1929, when he moved to Cambridge
University, Wittgenstein was a philosopher again, and began to exert a
tremendous influence*.



Others dispute that Brouwer's lecture influenced
Wittgenstein's thinking (Hacker 1986, Hintikka 1992, Marion
2003). In how far, if at all, Wittgenstein was influenced by
Brouwer's ideas is not entirely clear, but there certainly are
interesting agreements and disagreements between their views. Marion
(2003) argues that Wittgenstein's conception of mathematics as
described in the Tractatus is very close to that of Brouwer, and that
Wittgenstein agrees with the rejection of the Law of Excluded Middle
(1929 manuscript, pp 155-156 in Wittgenstein 1994) but disagrees
with Brouwer's arguments against it. Marion (2003) claims that
Wittgenstein's stance is more radical than Brouwer's in
that in the former's view the lack of validity of the Law of
Excluded Middle in mathematics is a distinguishing feature of all
mathematical propositions (as opposed to empirical propositions) and
not only a particularity of the mathematics of the infinite, as it is
for Brouwer.



Veldman (forthcoming) discusses several points of (dis)agreement between
Brouwer and Wittgenstein, such as the danger of logic, which,
according to both, may lead to constructions without mathematical
content. One of the disagreements raised in the paper concerns
Wittgenstein's view that mathematics is a common undertaking,
which is in stark contrast to Brouwer's Creating Subject and his
view that mathematics is a languageless activity. 


### 6.3 Dummett



The British philosopher Michael Dummett (1975) developed a
philosophical basis for Intuitionism, in particular for intuitionistic
logic. Dummett explicitly states that his theory is not an exegesis of
Brouwer's work, but a possible philosophical theory for (in his
words) *repudiating classical reasoning in mathematics in favor of
intuitionistic reasoning*.



Dummett's approach starts with the idea that the choice for one
logic over another must necessarily lie in the meaning one attaches to
logical statements. In the theory of meaning that Dummett uses, which
is based on Wittgenstein's ideas about language and in
particular on his idea that *meaning is use*, the meaning of a
sentence is determined by the way in which the sentence is used. The
meaning of a mathematical statement manifests itself in the use made
of it, and the *understanding* of it is the knowledge of the
capacity to use the statement. This view is supported by the way in
which we acquire mathematical knowledge. When we learn a mathematical
notion we learn how to use it: how to compute it, prove it or infer
from it. And the only way to establish that we have grasped the
meaning of a mathematical statement lies in our proficiency in making
correct use of the statement. 



Given this view on meaning, the central notion in the theory of
meaning for mathematics is not, as in Platonism, truth, but
*proof*; the understanding of a mathematical statement consists
in the ability to recognize a proof of it when one is presented with
one. This then, as Dummett argues, leads to the adoption of
intuitionistic logic as the logic of mathematical reasoning. 



Interestingly, as Dummett (1975) remarks himself, his theory of
meaning is far apart from Brouwer's ideas on mathematics as an
essentially languageless activity. So that there are at least two
quite different lines of thought that lead to the adoption of
intuitionistic logic over classical logic, the one developed by
Brouwer and the one argued for by Dummett. Dummett's work on
Intuitionism has been commented on by various philosophers such as Dag
Prawitz (1977), Parsons (1986) and Richard Tieszen (1994 en 2000). 


### 6.4 Finitism



Various forms of *Finitism* are based on a similar view as the
one expressed by Dummett, but in which the constructions that are
allowed to prove mathematical statements are required to exist not
only in principle, but also in practice. Depending on the the precise
implementation of the latter notion one arrives at different forms of
Finitism, such as the *Ultra-Intuitionism* developed by
Alexander Yessenin-Volpin (1970) and the *Strict Finitism*
developed by Crispin Wright (1982).