# Intuitionism in the Philosophy of Mathematics

*First published Thu Sep 4, 2008; substantive revision Wed Aug 14, 2013*

Intuitionism is a philosophy of mathematics that was introduced by the Dutch mathematician L.E.J. Brouwer (1881–1966). Intuitionism is based on the idea that mathematics is a creation of the mind. The truth of a mathematical statement can only be conceived via a mental construction that proves it to be true, and the communication between mathematicians only serves as a means to create the same mental process in different minds.

This view on mathematics has far reaching implications for the daily
practice of mathematics, one of its consequences being that the principle of
the excluded middle, (*A* ∨ ¬*A*), is no longer
valid. Indeed, there are propositions, like the Riemann hypothesis, for
which there exists currently neither a proof of the statement nor of
its negation. Since knowing the negation of a statement in intuitionism
means that one can prove that the statement is not true, this implies
that both *A* and *¬A* do not hold
intuitionistically, at least not at this moment. The dependence of
intuitionism on time is essential: statements can become provable in
the course of time and therefore might become intuitionistically valid
while not having been so before.

Besides the rejection of the principle of the excluded middle, intuitionism strongly deviates from classical mathematics in the conception of the continuum, which in the former setting has the property that all total functions on it are continuous. Thus, unlike several other theories of constructive mathematics, intuitionism is not a restriction of classical reasoning; it contradicts classical mathematics in a fundamental way.

Brouwer devoted a large part of his life to the development of mathematics on this new basis. Although intuitionism has never replaced classical mathematics as the standard view on mathematics, it has always attracted a great deal of attention and is still widely studied today.

In this entry we concentrate on the aspects of intuitionism that set it apart from other branches of constructive mathematics, and the part that it shares with other forms of constructivism, such as foundational theories and models, is discussed only briefly.

- 1. Brouwer
- 2. Intuitionism
- 3. Mathematics
- 4. Constructivism
- 5. Meta-mathematics
- Bibliography
- Academic Tools
- Other Internet Resources
- Related Entries

## 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 Göttingen 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 Gödel, 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 schließe 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. The notion has become known in the literature as the

*creative 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.

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 the formalization of the notion of
creating subject, which was not formulated by Brouwer but only later
by others, the temporal aspect of intuitionism is incorporated in the
axioms (here □_{n}*A* denotes that the creating
subject experiences the truth of *A* at time *n*, or, in
other words, that it has a proof of *A* at
time *n*):

The first axiom is a form of the principle of the excluded middle concerning the knowledge of the creating subject. The second axiom clearly uses the fact that the creating subject is an idealization since it expresses that proofs will always be remembered. The last axiom is not one a mathematician using classical reasoning would adhere to. In fact, Gödel's incompleteness theorem indicates that the principle is false when □

(CS1)□ ∨ ¬□_{n}A_{n}A(it can be decided whether the creating subject knows A) (CS2)□ → □_{m}A_{m+n}A(what the creating subject knows remains known to him) (CS3)∃ n□↔_{n}AA(what is true will be discovered to be so by the creating subject, and it cannot know what is not true)

*would be interpreted as being provable in a reasonable proof system, which, however, is certainly not what Brouwer had in mind.*

_{n}A
Brouwer used arguments that involve a 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. One can, for example, given a
statement *A* that does not contain any reference to time,
i.e. no occurrence of □_{n}, define an infinite
sequence (what will later be called a choice sequence) according to
the following rule (Brouwer 1953):

α( n) = {0 if ¬□ _{n}A

1 if □_{n}A

From this follows the principle known as *Kripke's schema*,

∃α(A↔ ∃nα(n) = 1).

In van Dalen 1978 a model for the axioms of the creating subject is given in the context of arithmetic and choice sequences. Thus proving this notion to be consistent with intuitionistic arithmetic and certain parts of analysis.

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.

- ⊥ is not provable.
- A proof of
*A*∧*B*consists of a proof of*A*and a proof of*B*. - A proof of
*A*∨*B*consists of a proof of*A*or a proof of*B*. - A proof of
*A*→*B*is a construction which transforms any proof of*A*into a proof of*B*. - A proof of ∃
*xA*(*x*) is given by presenting an element*d*of the domain and a proof of*A*(*d*). - A proof of ∀
*xA*(*x*) is a construction which transforms every proof that*d*belongs to the domain into a proof of*A*(*d*).

The negation *¬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 *¬A* is equivalent to *A* →
⊥. 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* ∨
*¬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* ∨
*¬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* ∨ *¬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 ∧ B → A |
A ∧ B → B |
A → A ∨ B |
B → A ∨ B |

A → (B → A) |
∀xA(x) →
A(t) |
A(t) →
∃xA(x) |
⊥ → A |

(A → (B → C)) →
((A → B) → (A →
C)) |
|||

A → (B
→ A ∧ B) |
(A → C)
→((B →
C) → (A ∨ B → C)) |
||

∀x(B
→ A(x)) → (B →
∀xA(x)) |
∀x(A(x)
→ B) → (∃xA(x)
→ B) |

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

fromAand (A→B) inferB,

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:

(DP)IQC⊢A∨B⇒ IQC⊢Aor IQC⊢B.

This principle is clearly violated in classical logic, because classical logic
proves (*A*∨*¬A*) also for formulas that are
independent of the logic, i.e. for which both *A* and
*¬A*. are not a tautology. The inclusion of the principle
Ex Falso Sequitur Quodlibet, (⊥→*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 λ-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* ∨ ¬*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}2 ^{−n}if ∀m≤nA(m)

2^{−m}if ¬A(m) ∧m≤n∧∀k<mA(k).

Here *A*(*n*) is a decidable property for which
∀*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
¬*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; ∀*n**A*(*n*) then
expresses the (original) Goldbach conjecture that every number greater
than 2 is the sum of three primes. The sequence
<*r*_{n}> defines a real number *r* for
which the statement *r* = 0 is equivalent to the statement
∀*n*A(*n*). It follows that the statement
(*r* = 0 ∨ *r* ≠ 0) does not hold, and therefore
that the law of trichotomy ∀*x*(*x*
< *y* ∨ *x* =
*y* ∨ *y* < *x*) 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 couterexample to the principle of the excluded
middle, since ∀*n**A*(*n*) as above is at
present not known to be true or false, and thus we cannot assert
∀*n**A*(*n*)∨¬∀*n**A*(*n*)
intuitionistically, at least not at this moment. But the refutation of
this statement,
¬(∀*n**A*(*n*)∨¬∀*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 ¬*B* and ¬¬*B* hold (and
thus also from *B* and ¬*B*). In other words,
¬¬(*B*∨¬*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) = {0 if r≥0

1 ifr< 0

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* ≤ 0 ∨ 0 < *r*)
has not been decided, as in the example above. Define the uniformly
continuous function *f* on [0,3] by

f(x) = min(x−1,0) + 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
≤ *x* or *x* ≤ 2. Since *f* equals
*r* on [1,2], in the first case *r* ≤ 0 and in the
second case 0 ≤ *r*, contradicting the undecidability of the
statement (*r* ≤ 0 ∨ 0 ≤ *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 functionfon an interval [a,b] witha<b, for everycbetweenf(a) andf(b), the following holds:∀n∃x∈[a,b] |f(x) −c| < 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 presented 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:

(WC-N)∀α∃nA(α,n) → ∀α∃m∃n∀β∈α(m)A(β,n),

where *n* and *m* range over natural numbers, α
and β over choice sequences, and
β∈α(m)
means that the first *m* numbers of α and β are
equal, and N refers to the natural numbers. 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
∀α∃*n*A(α,*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(α,*n*) holds has to be made after
only a finite initial segment of α is known. For we do not know
how α will proceed in time, and we therefore have to base the
choice of *n* on the initial segment of α that is known
at that point in time where we wish to fix *n*. This implies
that for every lawless sequence β with the same initial segment
as α, A(β,*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 α, 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 ∀β∈α(*m*)
*A*(β,*n*), could be made explicit. Thus
∀α∃*n**A*(α,*n*) implies
the existence of a continuous functional Φ that for every α
produces the *m* that fixes the length of α on the basis
of which *n* is chosen. More formally, let *CF* be the class of
continuous functionals Φ that assign natural numbers to infinite
sequences, i.e. that satisfy

∀α∃m∀β∈α(m) Φ(α) = Φ(β).

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

(C-N)∀α∃nA(α,n) → ∃Φ∈CF∀αA(α,Φ(α)).

There exist stronger forms of continuity that occur in intuitionistic analysis and the theory of lawless sequences.

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:

¬∀α (∀nα(n) = 0 ∨ ¬∀nα(n) = 0).

Here α(*n*) denotes the *n*-th element of α.
To see that this negations holds, suppose, arguing by contradiction, that ∀α (∀*n*α(*n*)
= 0 ∨ ¬∀*n*α(*n*) = 0) holds. This
implies that

∀α∃k( (∀nα(n) = 0 ∧k= 0) ∨ (¬∀nα(n) = 0 ∧k= 1) ).

By the weak continuity axiom, for α consisting of only zeros
there exists a number *m* that fixes the choice of *k*,
which means that for all
β∈α(*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*_{α} that is the limit
of the sequence *r*_{α} given in the section on
weak counterexamples, where the *A*(*m*) in the
definition is taken to be the statement α(*m*) = 0. Then
the refutation above implies that
¬∀α(*r*_{α} = 0 ∨
*r*_{α} ≠ 0), and it thereby refutes the law of
trichotomy,

∀x(x<y∨x=y∨y<x).

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

Theorem(C-N)

Every total real function is continuous.

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

f(x) = {0 if xis a rational number

1 ifxis an irrational number

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 (* denotes concatenation and
*f*(α(*n*))
denotes the value of *f* on the code of
the finite sequence
α(*n*)):

∀α∃nf(α(n)) > 0 ∀n∀m(f(n) > 0 →f(n*m) =f(n)).

Intuitively, if *f* represents Φ then
*f*(α(*n*)) = 0 means that
α(*n*) is not
long enough to compute Φ(α), and
*f*(α(*n*))
= *m+1* means that
α(*n*)
is long enough to compute Φ(α) and that
the value of Φ(α) is *m*. If *K* denotes the
class of neighborhood functions, then the continuity axiom
**(C-N)** can be rephrased as

∀α∃nA(α,n) → ∃f∈K∀m(f(m) > 0 → ∀β∈mA(β,f(m−1))),

where β∈*m* means that
the code of the initial segment of β 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
König'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*.

(FAN)∀α∈T∃nA(αn) → ∃m∀α∈T∃n≤mA(αn).

Here α∈*T* means that
α is a branch of *T*.
**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:

(BI_{D})[∀α∀ n(A(αn) ∨ ¬A(αn)) ∧∀α∃ nA(αn) ∧∀α∀ n(A(αn) →B(αn)) ∧∀α∀ n(∀mB(αn * m) →B(αn))] →Bε.

Here ε stands for the empty sequence, * 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 *IK* be the inductively defined class of
neighborhood functions, consisting of all constant non-zero sequences
λ*m*.*n*+1, and such that if *f*(0) = 0
and λ*m*.*f*(*x***m*)
∈ *IK* for all
*x*, then *f* ∈*IK*. The
statement *K* = *IK*, that is, that the neighborhood
functions can be generated inductively, is equivalent
to **BI**.

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.

X= {x∈{0,1} |x= 0 ∨ (x= 1 ∧A)}Y= {x∈{0,1} |x= 1 ∨ (x= 0 ∧A)}

The existence of a choice function *f*: {X,Y} → {0,1}
choosing an element from *X* and *Y* would imply
(*A* ∨ ¬*A*). For if *f*(*X*) ≠
*f*(*Y*), it follows that *X* ≠ *Y*, and
hence ¬*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:

(AC-N)∀R⊆ N × N (∀m∃nmRn→ ∃α∀mmRα(m) ).

Here N stands for the set of natural numbers. 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 α on the natural numbers can be
constructed step-by-step: first an element *m*_{0} is
chosen such that *0Rm _{0}*, which will be
the value of α(0), then an element

*m*

_{1}is chosen such that

*1Rm*, which will be the value of α(1), and so on.

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

(DC-N)∀R⊆ N × N (∀m∃nmRn→∀k∃α ∈ N^{N}(α(0) =k∧

∀i≥ 0 α(i)Rα(i+1))).

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 Émile 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-Löf 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:

(NEP)HA⊢∃xA(x) ⇒ ∃n∈NHA⊢A(n).

That this property does not hold in
**PA**
follows from the fact that
**PA**
proves ∃*x*
(*A*(*x*) ∨
∀*x*¬*A*(*x*)). 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* codes a terminating computation of
the program with code *e* on input *e*. If for every
*x* there would exist a number *n* such that
**PA**⊢*T*(*e,e,n*) ∨
∀*x*¬*T*(*e,e,x*), 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

(MR)HA⊢∀x(A(x) ∨ ¬A(x)) ∧ ¬¬∃xA(x) ⇒HA⊢∃xA(x)

is a principle that holds both classically and intuitionistically, but
only for **HA** the proof
of this fact is nontrivial. Since
**HA** proves the law of the excluded middle
for every primitive recursive predicate, it follows that for such
*A* the derivability of
¬¬∃*x**A*(*x*) in
**HA** implies the derivability of
∃*x**A*(*x*) as well. From this it follows
that **PA** is
Π^{0}_{2}-conservative over
**HA**, that is, for primitive recursive
*A*,

Thus the class of provably recursive functions ofPA⊢∀x∃y(A(x,y) ⇒HA⊢∀x∃y(A(x,y).

**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 Gödel's Dialectica interpretation (Gödel
1958, Kreisel 1959), Kleene realizability (Kleene 1965), or type
theories (Martin-Löf 1984). In these interpretations the
functionals underlying constructive statements, such as for example the
function assigning a *y* to every *x* in
∀*x*∃*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: for
*A*(α) not containing other nonlawlike parameters
besides α,

A(α) → ∃n∀β ∈α(n)A(β).

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 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-Löf 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.5 Reverse mathematics

In reverse mathematics one tries to establish for mathematical theorems which axioms are needed to prove them. In intuitionsistic 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 (Other Internet Resources), 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 intuitionsistic 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.

## Bibliography

- Aczel, P., 1978, ‘The type-theoretic interpretation of
constructive set theory,’ in
*Logic Colloquium '77*, A. Macintyre, L. Pacholski, J. Paris (eds.), North-Holland. - van Atten, M., 2004,
*On Brouwer*, (Wadsworth Philosophers Series), Belmont: Wadsworth/Thomson Learning. - –––, 2007,
*Brouwer meets Husserl (On the phenomenology of choice sequences)*, Dordrecht: Springer. - –––, 2008, ‘On the hypothetical judgement
in the history of intuitionistic logic,’ in
*Logic, Methodology, and philosophy of science XIII: Proceedings of the 2007 International Congress in Beijing*, C. Glymour and W. Wang and D. Westerståhl (eds.), London: King's College Publications. - van Atten, M. and D. van Dalen, 2002, ‘Arguments for the
continuity principle,’
*Bulletin of Symbolic Logic*, 8(3): 329–374. - Beth, E.W., 1956, ‘Semantic construction of intuitionistic
logic,’
*KNAW Afd. Let. Med., Nieuwe serie*, 19/11: 357–388. - Brouwer, L.E.J., 1975,
*Collected works I*, A. Heyting (ed.), Amsterdam: North-Holland. - –––, 1976,
*Collected works II*, H. Freudenthal (ed.), Amsterdam: North-Holland. - –––, 1905,
*Leven, kunst en mystiek*, Delft: Waltman. - –––, 1907,
*Over de grondslagen der wiskunde*, Ph.D. Thesis, University of Amsterdam, Department of Physics and Mathematics. - –––, 1912, ‘Intuïtionisme en formalisme’,
Inaugural address at the University of Amsterdam, 1912. Also in
*Wiskundig tijdschrift*, 9, 1913. - –––, 1925, ‘Zur Begründung der
intuitionistischen Mathematik I,’
*Mathematische Annalen*, 93: 244–257. - –––, 1925, ‘Zur Begründung der
intuitionistischen Mathematik II,’
*Mathematische Annalen*, 95: 453–472. - –––, 1948, ‘Essentially negative
properties’,
*Indagationes Mathematicae*, 10: 322–323. - –––, 1952, ‘Historical background,
principles and methods of intuitionism,’
*South African Journal of Science*, 49 (October-November): 139-146. - –––, 1953, ‘Points and
Spaces,’
*Canadian Journal of Mathematics*, 6: 1–17. - –––, 1981,
*Brouwer's Cambridge lectures on intuitionism*, D. van Dalen (ed.), Cambridge: Cambridge University Press, Cambridge. - –––, 1992,
*Intuitionismus*, D. van Dalen (ed.), Mannhein: Wissenschaftsverlag. - Brouwer, L.E.J. and C.S. Adama van Scheltema, 1984,
*Droeve snaar, vriend van mij – Brieven*, D. van Dalen (ed.), Amsterdam: Uitgeverij de Arbeiderspers. - Coquand, T., 1995, ‘A constructive topological proof of van
der Waerden's theorem,’
*Journal of Pure and Applied Algebra*, 105: 251–259. - van Dalen, D., 1978, ‘An interpretation of intuitionistic
analysis’,
*Annals of Mathematical Logic*, 13: 1–43. - –––, 1997, ‘How connected is the
intuitionistic continuum?,’
*Journal of Symbolic Logic*, 62(4): 1147–1150. - –––, 1999/2005,
*Mystic, geometer and intuitionist*, Volumes I (1999) and II (2005), Oxford: Clarendon Press. - –––, 2001,
*L.E.J. Brouwer (een biografie)*, Amsterdam: Uitgeverij Bert Bakker. - –––, 2004, ‘Kolmogorov and Brouwer on constructive
implication and the Ex Falso rule’
*Russian Math Surveys*, 59: 247–257. - van Dalen, D. (ed.), 2001,
*L.E.J. Brouwer en de grondslagen van de wiskunde*, Utrecht: Epsilon Uitgaven. - Diaconescu, R., 1975, ‘Axiom of choice and
complementation,’ in
*Proceedings of the American Mathematical Society*, 51: 176–178. - Fourman, M., and R. Grayson, 1982, ‘Formal spaces,’
in
*The L.E.J. Brouwer centenary symposium*, A.S. Troelstra and D. van Dalen (eds.), Amsterdam: North-Holland. - Gentzen, G., 1934, ‘Untersuchungen über das logische
Schließen I, II,’
*Mathematische Zeitschrift*, 39: 176–210, 405–431. - Gödel, K., 1958, ‘Über eine bisher noch nicht
benützte Erweiterung des finiten Standpunktes,’
*Dialectia*, 12: 280–287. - Heyting, A., 1930, ‘Die formalen Regeln der
intuitionistischen Logik,’
*Sitzungsberichte der Preussischen Akademie von Wissenschaften. Physikalisch-mathematische Klasse*, 42–56. - –––, 1956,
*Intuitionism, an introduction*, Amsterdam: North-Holland. - van der Hoeven, G., and I. Moerdijk, 1984, ‘Sheaf models for
choice sequences,’
*Annals of Pure and Applied Logic*, 27: 63–107. - Kleene, S.C., and R.E. Vesley, 1965,
*The foundations of intuitionistic mathematics*, Amsterdam: North-Holland. - Kreisel, G., 1959, ‘Interpretation of analysis by means of
constructive functionals of finite type,’ in
*Constructivity in mathematics*, A. Heyting (ed.), Amsterdam: North-Holland. - –––, 1962, ‘On weak completeness of intuitionistic
predicate logic,’
*Journal of Symbolic Logic*, 27: 139–158. - –––, 1968, ‘Lawless sequences of natural
numbers,’
*Compositio Mathematica*, 20: 222–248. - Kripke, S.A., 1965, ‘Semantical analysis of intuitionistic
logic’, in
*Formal systems and recursive functions*, J. Crossley and M. Dummett (eds.), Amsterdam: North-Holland. - Lubarsky, R., F. Richman, and P. Schuster 2012, ‘The Kripke
schema in metric topology’,
*Mathematical Logic Quarterly*, 58(6): 498–501. - Maietti, M.E., and G. Sambin, 2007, ‘Toward a minimalist
foundation for constructive mathematics,’ in
*From sets and types to topology and analysis: toward a minimalist foundation for constructive mathematics*, L. Crosilla and P. Schuster (eds.), Oxford: Oxford University Press. - Martin-Löf, P., 1970,
*Notes on constructive mathematics*, Stockholm: Almqvist & Wiskell. - –––, 1984,
*Intuitionistic type theory*, Napoli: Bibliopolis. - Moschovakis, J.R., 1986, ‘Relative lawlessness in
intuitionistic analysis,’
*Journal of Symbolic Logic*, 52(1): 68–87. - Myhill, J., 1975, ‘Constructive set
theory,’
*Journal of Symbolic Logic*, 40: 347–382. - Niekus, J., 2010,‘Brouwer's incomplete objects’
*History and Philosophy of Logic*31: 31–46. - van Oosten, J., 2008,
*Realizability: An introduction to its categorical side*, (Studies in Logic and the Foundations of Mathematics: Volume 152), Amsterdam: Elsevier. - Sambin, G., 1987, ‘Intuitionistic formal spaces,’
in
*Mathematical Logic and its Applications*, D. Skordev (ed.), New York: Plenum. - Scott, D., 1968, ‘Extending the topological interpretation
to intuitionistic analysis,’
*Compositio Mathematica*, 20: 194–210. - –––, 1970, ‘Extending the topological
interpretation to intuitionistic analysis II’,
in
*Intuitionism and proof theory*, J. Myhill, A. Kino, and R. Vesley (eds.), Amsterdam: North-Holland. - Tarski, A., 1938, ‘Der Aussagenkalkül und die Topologie,’
*Fundamenta Mathematicae*, 31: 103–134. - Troelstra, A.S., 1973,
*Metamathematical investigations of intuitionistic arithmetic and analysis*, (Lecture Notes in Mathematics: Volume 344), Berlin: Springer. - –––, 1977,
*Choice sequences*(Oxford Logic Guides), Oxford: Clarendon Press. - Troelstra, A.S., and D. van Dalen, 1988,
*Constructivism I and II*, Amsterdam: North-Holland. - Veldman, W., 1976, ‘An intuitionistic completeness theorem
for intuitionistic predicate logic,’
*Journal of Symbolic Logic*, 41(1): 159–166. - –––, 1999, ‘The Borel hierarchy and the projective hierarchy in intuitionistic mathematics,’ Report Number 0103, Department of Mathematics, University of Nijmegen. [available online]
- –––, 2004, ‘An intuitionistic proof of Kruskal's
theorem,’
*Archive for Mathematical Logic*, 43(2): 215–264. - –––, 2009,
‘Brouwer's Approximate Fixed-Point Theorem is Equivalent to Brouwer's Fan Theorem,’
in
*Logicism, Intuitionism, and Formalism - Synthese Library*341, S. Lindström, E. Palmgren, K. Segerberg, V. Stoltenberg-Hansen (eds.): 277–299. - Weyl, H., 1921, ‘Über die neue Grundlagenkrise der
Mathematik,’
*Mathematische Zeitschrift*, 10: 39–70.

## Academic Tools

How to cite this entry. Preview the PDF version of this entry at the Friends of the SEP Society. Look up this entry topic at the Indiana Philosophy Ontology Project (InPhO). Enhanced bibliography for this entry at PhilPapers, with links to its database.

## Other Internet Resources

- Veldman, W., 2011, ‘Brouwer's Fan Theorem as an axiom and as a contrast to Kleene's Alternative,’ online manuscript, arXiv:1106.2738.
- Luitzen Egbertus Jan Brouwer, biography at Mac Tutor History of Mathematics website.