# Intuitionism: an inspiration?

Wim Veldman  Institute for Mathematics, Astrophysics and Particle Physics,
Faculty of Science, Radboud University Nijmegen, Postbus 9010, 6500 GL
Nijmegen, the Netherlands<EMAIL_ADDRESS>
τοιγὰρ ἐγὼ τοι, ξεῖνε, μάλ’ ἀτρεϰέως ἀγορε´υςω

Well then, let me you, stranger, precisely explain these matters

Od. $\alpha$ 214

##  1\. Introduction

###  1.1. Topology and foundations

We want to introduce the reader to the intuitionistic view of mathematics
proposed, developed and defended by the Dutch mathematician L.E.J. Brouwer
(1881-1966)111The title of the paper is taken from an exclamation by the
philosopher L. Wittgenstein, see [64]..

Brouwer obtained his fame as a mathematician by a number of very important
results in topology such as the Dimension Theorem:

> For all positive integers $m,n$,
> if there is a homeomorphism from $[0,1]^{m}$ to $[0,1]^{n}$, then $m=n$,

and the closely related Brouwer Fixed-point Theorem:

> For each positive integer $n$, for every continuous function $f$ from
> $[0,1]^{n}$ to $[0,1]^{n}$, there exists $p$ in $[0,1]^{n}$ such that
> $f(p)=p$.

These results were obtained in 1911.

Brouwer had started thinking on the foundations of mathematics earlier than
that. In his dissertation from 1907, see [9], he wrestled already with the
concept of the continuum. In a famous paper from 1908, see [10], he attacked
the principle of the excluded third $X\;\vee\;\neg X$.

###  1.2. Against the formalists

In his inaugural lecture at the University of Amsterdam in 1912, entitled:
‘Intuitionism and Formalism’, see [11], Brouwer declares himself an opponent
of the formalists. The formalists, in Brouwer’s words, explain the exactness
and precision of the statements of mathematics by describing mathematics as a
game with meaningless strings of symbols according to very strict and precise
rules. The game may turn out to be useful for certain purposes, and then may
give ‘a vague sensation of delight’, but these other purposes are not the
concern of the mathematician. In the formalist’s ‘game’, there is no place for
truth, only for correctness.

Brouwer most emphatically did not want to explain away the meaningfulness of
mathematical statements and the experience of truth. In his intuitionistic
view, the source of mathematical exactness is not to be found ‘on paper’ but
‘in the human intellect’.

###  1.3. I. Kant

Brouwer was inspired by the philosopher I. Kant (1724-1804) who described the
simple theorem ‘7+5=12’ as the result of a construction in ‘pure intuition’.

Pure intuition has to be distinguished from observation by the senses. In
Kant’s terms, it is the ‘form’ of all observations by the senses, and, as
such, independent of all individual observations by the senses, i.e. a priori.

It is very important that one has to do something in order to come to the
insight of the truth of ‘7+5=12’: counting 1, 2, 3, $\dots,7$ and then,
continuing, putting 1 below 8, 2 below 9, 3 below 10, 4 below 11, and,
finally, 5 below 12. This is why Kant holds the mathematical judgment ‘7+5=12’
is not analytic, i.e. a matter of logic, but synthetic, see [37, §2c], i.e.,
going beyond logic, and, one might perhaps say, a product of some activity by
the judging subject.

###  1.4. Languageless constructions

For the intuitionistic mathematician, every mathematical theorem is, like
‘7+5=12’, the result of a construction in pure intuition. The successful
completion of this construction, the proof of the theorem, gives joy and a
sense of beauty, and one wants to tell one’s friends.

A construction in pure intuition is languageless. Language comes in if I want
to preserve the memory of the construction for myself, or if I want to make an
attempt to explain to my fellow mathematician what I did, in the hope she will
be able to do something similar. Language is not trustworty: it always may
fail to do what one expects it to do, as we all know from our experience as
unsuccessful teachers and forgetful researchers.

There is no such thing as an exact linguistic description of a mathematical
construction. The linguistic description only is the accompaniment of an act
of understanding, either between me and one of my former selves, or between me
and a fellow mathematician.

Nevertheless, it is our task to study the language of mathematics carefully
and to find out where it perhaps may be improved. Although it is impossible we
express ourselves in a perfect way, we always have to try to do better than we
did until now.

###  1.5. Intuitionistic mathematics is constructive mathematics

Intuitionistic mathematics is not a new, alternative kind of mathematics.
Mathematics is intuitionistic mathematics. Brouwer’s revolution is a call for
reflection. A sharpened awareness of what it is we do when doing mathematics
makes us more careful and more precise and, thereby, hopefully, better
mathematicians.

Intuitionistic mathematics is constructive mathematics. The reason is that
mathematics itself essentially is constructive although this fact has been
obscured by our mistaken trust in (classical) logic.

Thinking of Brouwer’s ability in topology one may reflect that a continuous
function $f$ from $[0,1]^{m}$ to $[0,1]^{n}$ has the property that, for each
$p$ in $[0,1]^{m}$, one may effectively find approximations of the function
value $f(p)$ from approximations of the argument $p$. Continuous functions are
constructive functions: there is a deep connection between Brouwer’s
foundational interests and his topological concerns.

###  1.6. The contents of the paper

The paper is divided into 21 Sections. Section 2 treats the basic intuition
giving rise to the nonnegative integers. Section 3 is a short reflection on
theorems and their proofs. In Sections 4-6, we consider three famous results,
that usually are taken to be negative statements although they are not
negative at all. In Section 4, we have a look at Euclid’s theorem that there
are infinitely many primes. In Section 5, we consider the theorem that
$\sqrt{2}$ is irrational. In Section 6, we introduce the reals and Cantor’s
theorem that there are uncountably many of them. In Section 7, we introduce
reals oscillating around $0$: if $x$ is such a number, one is unable to make
out if $x<0$, $x=0$ or $x>0$. Section 8 explains the reasons for interpreting
the logical constants constructively and rejecting the principle of the
excluded third $X\vee\neg X$. In Section 9 we study a basic result of real
analysis: the Intermediate Value Theorem. The theorem is an existential
statement that fails when taken at its constructive face value, but, if
suitably reformulated and adapted, leads to several true and useful results.
Finding such reconstructions of a constructively invalid result is part of the
intuitionistic program.

Intuitionistic mathematicians hold that every real function is (pointwise)
continuous. In Section 10, we treat the preliminary observation that a real
function can not have a positive discontinuity. In Section 11, we go into the
intuitionistic meaning of negation. In Section 12, we introduce the Continuity
Principle, an axiom used by Brouwer and we show that this axiom leads to the
positive result that real functions are (pointwise) continuous.

In Section 13, we introduce the Fan Theorem, a theorem that perhaps, like the
Continuity Principle, should be called an axiom: we discover Brouwer’s
‘proof’: most of us would call it a philosophical argument. One should note,
however, that, as long as we do not organize our mathematical results in a
formal way, it is difficult to distinguish axioms from theorems. As we shall
see, the Fan Theorem implies that a real function from $[0,1]$ to
$\mathcal{R}$ is not only pointwise but even uniformly continuous. As an
aside, we prove that the Fan Theorem fails to be true in computable analysis.
In Section 14, we go into the rôle of the Fan Theorem in game theory.

In Section 15, we consider Brouwer’s Thesis on Bars in
$\mathcal{N}=\omega^{\omega}$, formulated as a Principle of Bar Induction. The
Thesis on Bars in $\mathcal{N}$ implies the Fan Theorem but is a far stronger
statement. We show how the argument for the Fan Theorem extends to the Thesis
on Bars in $\mathcal{N}$. As an application we prove, in Section 16, the
Principle of Open Induction in $[0,1]$. In Section 17 we give a second
formulation of Brouwer’s Thesis. This second formulation uses stumps:
inductively generated sets of finite sequences of natural numbers, whose rôle
may be compared to the rôle of countable ordinals in classical, non-
intuitionistic analysis. As an application we give, in Section 18, an
intuitionistic formulation and proof of the Clopen Ramsey Theorem, itself an
impressive extension of Ramsey’s result from 1928. The proof of this
intuitionistic theorem has not been published before. In Section 19 we study
Borel sets. Because of the failure of De Morgan’s Law $\neg\forall n\neg
P(n)]\rightarrow\exists n[P(n)]$, the subject of descriptive set theory needs
a complete reconstruction. In Section 20 we reflect on the notion of a finite
subset of the set $\mathbb{N}$ of the non-negative integers. This mathematical
notion may be made intuitionistically precise in uncountably many ways. It is
a perfect illustration of the subtlety and expressivity the language of
mathematics has obtained from Brouwer’s intervention.

In Section 21, we briefly describe how E. Bishop, who founded his own school
of constructive analysis in the 1960’s, treated Brouwer’s legacy, and how also
P. Martin-Löf’s view on constructive mathematics was influenced by Brouwer.

Many Sections may be read independently from other Sections.

##  2\. The basic intuition

###  2.1. If you don’t become like little children $\ldots$

222Matthew 18:3

Mathematics is a child’s game and each of us, from his tender days, is
familiar with the infinite sequence:

$0,\;1,\;2,\;3,\dots$

The sequence of these natural numbers or non-negative integers has no end.

No end? Can we always go on? Yes, yes, we can always go on!

We never die, or get tired of the game. Please, do not plague us with such
silly objections.

We courageously stick to the fascinating perspective of the never finished
infinite.

###  2.2. Induction and recursion

The function $\mathsf{S}$ produces, given any non-negative integer $n$, the
next one, $\mathsf{S}(n)$:

$\mathsf{S}(0)=1,\;\mathsf{S}(1)=2,\;\mathsf{S}(2)=3,\ldots$

Let $P$ be a property of non-negative integers such that one has a proof of
$P(0)$, and, for each $n$, a proof of $P\bigl{(}\mathsf{S}(n)\bigr{)}$ from
$P(n)$, i.e. a proof of $P(1)$ from $P(0)$, a proof of $P(2)$ from $P(1)$, a
proof of $P(3)$ from $P(2)$, and so on. One then proves, step by step, first
$P(1)$, then $P(2)$, then $P(3)$, and so on, that is, one proves, for each
$n$, $P(n)$. We see this happening although the process is never finished.

The principle of complete induction on the non-negative integers thus is
obvious.

Suppose one defines: for each $m$, $m+0=m$ and for each $n$,
$m+\mathsf{S}(n)=\mathsf{S}(m+n)$. One then calculates, first
$m+1=m+\mathsf{S}(0)$, then $m+2=m+\mathsf{S}(1)$, then
$m+3=m+\mathsf{S}(2)$, and so on, and, in this way, one finds, for each $n$,
the meaning of $m+n$.

This also is obvious.

###  2.3. The ‘logicist’ attempt to ‘prove’ induction

In the nineteenth century, G. Frege and R. Dedekind tried to define the non-
negative integers, logically or set-theoretically, and then to prove the
principle of complete induction and the possibility of defining functions by
recursion.

Brouwer considered such attempts futile and misleading.

###  2.4. Awakening consciousness

Brouwer spent a lot of thought on finding the origin of the idea of the non-
negative integers, see for instance [14].

A first thing, then a next thing, then another thing, and again another thing
$\ldots$

Mark the beginning: a first thing, then a next thing. Brouwer called it the
basic intuition of two-ity. He saw it happening in an awakening of slumbering
consciousness, a shift of attention, a moment’s reflection, or a move of time:
here I am, and now I see: ‘here I am’, and that is two things. Iterating this
shift of attention, I obtain three things, four things, and so on.

One is reminded of R. Dedekind’s proof of [23, Theorem 66]: There exist
infinite sets, for instance, the ‘world of my thoughts, meine Gedankenwelt’.
Dedekind invokes a function $s\mapsto s^{\prime}$ that associates to every
thought $s$ of mine the thought $s^{\prime}$: ‘I am thinking of $s$’ and
concludes, from the fact that this function should be one-to-one and non-
surjective, the latter because ‘I myself, mein eigenes Ich’ am a thought of
mine not of the form $s^{\prime}$, that I have infinitely many thoughts.

As we mentioned already, Brouwer refers to Kant. Kant held that the concepts
of ‘time’ and ‘space’, the ‘forms’ of ‘inner sense’ and ‘outer sense’,
respectively, are apriori concepts, that is, independent from every
observation by the senses. These apriori concepts are studied by mathematics,
in its two divisions: ‘arithmetic’ and ‘geometry’. Brouwer wants to maintain
Kant’s conviction about the apriori character of ‘time’ but rejects the
apriori character of ‘space’. This is partly because Kant believed space to be
Euclidean, and, after Kant, one had the non-euclidean revolution. Also,
geometry may be ‘arithmetized’ and be robbed of its status as an independent
discipline.

###  2.5. The ‘set’ $\mathbb{N}$

We use $\mathbb{N}$ to denote the set of the nonnegative integers. This ‘set’
is a well-understood totality but an ongoing project, in no sense finished or
complete. We use $m,n,\ldots,s,t,\ldots$ as variables over $\mathbb{N}$.

##  3\. Theorems and their proofs

###  3.1. Mere announcements

One does not understand a mathematical theorem immediately upon hearing its
statement. The statement of the theorem is only a preliminary announcement, a
partial communication, a promise. Its full meaning will unfold itself in the
proof, and understanding this full meaning is reserved for someone who takes
the trouble to go through the proof and to reconstruct it for herself.

###  3.2. No to ‘Platonism’

The statement of a theorem tells us that some mental construction has been
succesfully completed. It is not reporting a fact one might ‘observe’ in a
mathematical reality lying outside us.
The latter view has been strongly defended by Plato (427-347 B.C.). He
believed that the contemplation of the timeless mathematical reality, that one
approaches with the mind and not with the senses and that one should not touch
with one’s fingers333See Plato, Politeia (the Republic) VII 527a., would
prepare us for the contemplation of what is the true interest of the
philosopher: the timeless reality of the ‘Ideas’.

The intuitionistic mathematician rejects this view. In the ancient debate
between Speusippus (405-338 B.C.) and Menaechmus (380-320 B.C.) as reported by
Proclus (410-485), she would definitely have sided with Menaechmus. Speusippus
held that every ‘problem’ essentially is a ‘theorem’, i.e. a truth to behold,
whereas Menaechmus defended the view that every ‘theorem’ essentially is a
‘problem’, i.e. a construction to find and carry out.444The 48 propositions of
the First Book of Euclid’s Elements (300 B.C.) are divided into 34 ‘theorems’
and 14 ‘problems’. Proclus, in his wisdom, judged that both views contain some
truth555‘Both parties are right’, see [45, Prologue, Part Two, $\S$ 78], and,
indeed, one might say, both views try to explain a part of our mathematical
experience.
In our days, many mathematicians still feel they are discovering hard facts
not of their own making. They prefer a so-called realistic view, reminiscent
of Plato’s, while admitting it is difficult to give a convincing account of
the mathematical reality see [35, p. 123].

As to Brouwer’s formalist adversaries, some of them develop their formalisms
with an eye to ‘reality’ while others, like Brouwer himself, keep far from it.
A famous defender of the realistic point of view is K. Gödel (1906-1972). The
formula $\mathsf{CH}$ in the language of set theory that is taken to represent
Cantor’s famous continuum hypothesis666In an intuitionistic context, the
classical continuum hypothesis has no immediate meaning. One may however study
meaningful statements that seem to come close tot it, see [29] and [65,
Sections 7 and 8]. has been shown, by Gödel himself in 1938, and by P. Cohen
in 1963, respectively, not to be refuted and not to be proven by the rules of
first-order predicate logic from the formulas accepted as representing ‘the’
axioms of set theory, provided the latter do not give a contradiction. Gödel
observed, even before Cohen proved his result, that this fact does not solve
the problem: we still have to find out if $\mathsf{CH}$ holds in the
mathematical universe, see [30]777“Of course it is happening inside your head,
Harry, but why on earth should that mean that it is not real?” Dumbledore in:
J.K. Rowling, Harry Potter and the Deathly Hallows .

The intuitionistic mathematician discards the realistic view: he believes it
is wrong and harmful for the practice of mathematics.

###  3.3. Propositions (as yet) without proof

From our intuitionistic perspective, it seems impossible to fully understand a
proposition that has (as yet) no proof. We like to say, however, that we also
‘understand’ the proposition ‘$0=1$’, in the sense that we see this
proposition never will have a proof.

Besides, propositions that are only partially understood in the sense that we
have as yet no proof and also do not see that we never will have one, have an
important part to play in mathematics. Let us consider an example.

Studying Euclid’s proof that there are infinitely many primes888See Section
4., one comes to understand the statement: ‘there are infinitely many primes’
and to enjoy its beauty and depth. One now may ask: ‘Are there also infinitely
many twin primes, i.e. prime numbers $p$ such that also $p+2$ is prime?’. By
analogy, we have some understanding of the latter proposition. We can imagine
what a proof of this proposition might be and, in this sense, catch its
meaning, although, up to now, no proof or refutation has been found.

By his exemplary proof, Euclid suggests us how to (partially) understand other
propositions of the form ‘there are infinitely many numbers $n$ such that
$P(n)$’.

###  3.4. Negative theorems

There is a large supply of theorems whose statement is negative. Such theorems
report us that a construction of a kind we hoped for is impossible. We obtain
such conclusions imagining ourselves possessed of a construction of the
required kind and seeing that we then could prove $0=1$. We hastily retreat,
admitting we were imagining the impossible.

Indeed, when constructing proofs, we often use our imagination. We make
temporary extra assumptions for the sake of the argument, that later perhaps
will have to be given up. G. Gentzen (1909-1945), the inventor of ‘Natural
Deduction’, put great emphasis on this fact. Gentzen was inspired by Brouwer,
see [27, Section II, $\S 3$].

In a sense, propositions with a negative conclusion are second-rank. They tell
us about a lost hope, a failure. Fortunately, many mathematical theorems are
unnecessarily negative. Their negative formulation is caused by laziness or
lack of attention. The intuitionistic mathematician likes to find the positive
content of seemingly negative statements.

In Sections 4, 5 and 6, trying to make this clear, we give some examples.

##  4\. Infinitely many prime numbers

The following theorem is due to Euclid, see [25, Book IX, Proposition 20]. It
is important and rewarding to study the proof in the original.

######  Theorem 1.

The prime numbers are more than every quantity of prime numbers given
beforehand.

###### Proof.

Let the prime numbers given beforehand be $A,B,C$. I say that there are more
prime numbers than $A,B,C$. Let the least number measured by999the least
common multiple of $A,B,C$ be taken, and let it be $DE$, and let the unit $DF$
be added to it; we thus obtain $EF$. $EF$ is prime or $EF$ is not
prime101010Euclid makes this case distinction as he did not consider a number
to be a divisor of itself.. First, let it be prime. Then the prime numbers
$A,B,C,EF$ are more than $A,B,C$. Next, let $EF$ be not prime. Then there is a
prime number that measures $EF$. Let it be $G$. I say $G$ is not the same with
any of $A,B,C$. For, if possible, let it be so. Now $A,B,C$ measure $DE$ and
thus also $G$ measures $DE$. But the number $G$ also measures $EF$ and thus
the _number_ $G$ measures the remainder $DF$ which is a _unit_ , and that is
absurd. So $G$ is not the same with any of $A,B,C$. Thus prime numbers
$A,B,C,G$ are found which are more than than the quantity of prime numbers
$A,B,C$ given beforehand. ∎

We now paraphrase Euclid’s proof in contemporary terms. Euclid explains us,
how, given any finite list $q_{0},q_{1},\ldots,q_{n-1}$ of prime numbers, one
produces a prime number $q$ that is not on the list: consider $c:=$ the least
common multiple of $q_{0},q_{1},\ldots,q_{n-1}$. If $c$ is prime, take $q:=c$.
If $c$ is not prime, determine the least number $q>1$ that divides $c$. Then
$q$ is prime, and, for every $i<n$, $q\neq q_{i}$.

One may seriously wonder if this paraphrase is better than the original.

Note that Euclid only treats the case: $n=3$. He of course expects the reader
to pick up the general idea from this exemplary case. The reader must be
willing to understand him. This is a conditio sine qua non for every written
proof.

Also note that Euclid provides an algorithm: he demonstrates how, given any
finite list of prime numbers, one calculates a prime number that still is
missing.

Most importantly, as we observed already in the previous Section, Euclid in a
way lays down the meaning of the word ‘infinite’. His proof suggests how to
understand a proposition of the form: ‘there are infinitely many numbers
satisfying $A$’. One may prove such a thing by doing something like he does in
the case of the prime numbers.

Sometimes, a description of Euclid’s proof is given that does no justice to
the argument. According to this description, one is invited to assume: there
is a finite list containing all the primes. Euclid then reduces this
assumption to absurdity and forces one to admit that the initial assumption is
false: there is no such finite list, which is to say: there are not finitely
many primes.

G.H. Hardy, a great mathematician and a convinced platonist, has this view,
see [35, Section 12]. In the context of Euclid’s theorem, he calls reductio ad
absurdum ‘one of a mathematician’s finest weapons’, but adds a footnote
stating: ‘The proof can be arranged so as to avoid a _reductio_ and logicians
of some schools would prefer that it should be.’

##  5\. $\sqrt{2}$ is irrational

The theorem that $\sqrt{2}$ is irrational is also due to the Greeks and dates
from 450 B.C.. In those days, mathematicians sometimes were called ‘those who
know about the odd and the even’. The theorem uses the following

######  Lemma 2.

For all positive integers $n$, if $n$ is odd, then $n^{2}$ is odd.

###### Proof.

Find $p$ such that $n=2p+1$. Then
$n^{2}=(2p+1)(2p+1)=4p^{2}+4p+1=2(2p^{2}+2p)+1$. ∎

######  Theorem 3.

There are no positive integers $m,n$ such that $\sqrt{2}=\frac{m}{n}$.

###### Proof.

Suppose there are. Find such $m,n$ and assume: at least one of $m,n$ is odd.
Then $\sqrt{2}=\frac{m}{n}$, so $2n^{2}=m^{2}$, so $m^{2}$ is even and, by
Lemma 2, also $m$ is even and $4$ divides $m^{2}=2n^{2}$, so $n^{2}$ is even
and, again by Lemma 2, $n$ is even. We thus see: both $m,n$ are even.
Contradiction. ∎

Already in ancient times, some people worried about this proof, in particular
about the sentence: ‘Suppose there are.’. How is it possible to suppose that
$\sqrt{2}$ is rational? ‘Suppose’ must mean something like ‘Imagine’. How can
one make a clear mental picture of a fact that will turn out to be false? How
to imagine the impossible?

In particular, Parmenides (fl. 475 B.C.) and Zeno (fl. 450 B.C.), leading
members of the Eleatic school of philosophy, felt this difficulty. The Dutch
mathematician G.F.C. Griss (1898-1953) shared their concern and suggested to
Brouwer to remove the proposition without proof, negation and the empty set
from the discourse of mathematics. He started a redevelopment of
intuitionistic mathematics, see, for instance, [33]. Brouwer did not want to
go into his suggestion, and offered the somewhat surprising argument that,
following it, one would impoverish the subject, see [13]. Nevertheless, in
intuitionistic, and, more generally, in constructive mathematics, one avoids
negation as much as possible, also for the reason that negative results lack
constructive content.

The negatively formulated Theorem 3 may be replaced by a positive and
affirmative result, as follows.

######  Definition 1.

A real number $x$ is _positively irrational_ if and only if, given any
rational number $q=\frac{m}{n}$ one may effectively find a positive integer
$p$ such that $|x-\frac{m}{n}|\geq\frac{1}{p}$.

######  Theorem 4.

$\sqrt{2}$ is positively irrational.

###### Proof.

Let $m,n$ be given. Note $2n^{2}\neq m^{2}$, and therefore:
$|2n^{2}-m^{2}|\geq 1$ and $|2-\frac{m^{2}}{n^{2}}|\geq\frac{1}{n^{2}}$, that
is $|\sqrt{2}+\frac{m}{n}|\cdot|\sqrt{2}-\frac{m}{n}|\geq\frac{1}{n^{2}}$. If
$\frac{m}{n}>2$, then $\frac{m}{n}-\sqrt{2}>\frac{1}{2}$ and, if
$\frac{m}{n}\leq 2$, then $|\sqrt{2}+\frac{m}{n}|<4$ and
$|\sqrt{2}-\frac{m}{n}|>\frac{1}{4n^{2}}$. ∎

##  6\. Uncountably many reals

We sketch how to treat integers and rationals and then define the notion of a
real number, essentially like G. Cantor (1845-1918) did it, and Brouwer after
him.

###  6.1. Integers and rationals

One first introduces, on the set $\mathbb{N}$ of the natural numbers, the
operations $+,\cdot,exp$ and the relations $<,\leq$ by recursive definitions,
as suggested in Section 2, and proves, by induction, their well-known nice
properties. One then defines a pairing function from
$\mathbb{N}\times\mathbb{N}$ to $\mathbb{N}$, for instance the function
$(m,n)=2^{m}(2n+1)-1$, with inverse functions
$K,L:\mathbb{N}\rightarrow\mathbb{N}$. We will write $m^{\prime}=K(m)$ and
$m^{\prime\prime}=L(m)$, so, for each $m$, $m=(m^{\prime},m^{\prime\prime})$.

Then an equivalence relation $=_{\mathbb{Z}}$ on $\mathbb{N}$ is introduced
by:
$m=_{\mathbb{Z}}n\leftrightarrow
m^{\prime}+n^{\prime\prime}=m^{\prime\prime}+n^{\prime}$. Integers, for us,
are just natural numbers and not, as in the usual treatment, the equivalence
classes of the relation $=_{\mathbb{Z}}$. Functions and relations on
$\mathbb{Z}$ are functions and relations on $\mathbb{N}$ that respect the
relation $=_{\mathbb{Z}}$. The functions $+_{\mathbb{Z}},\cdot_{\mathbb{Z}}$,
the relations $<_{\mathbb{Z}},\leq_{\mathbb{Z}}$,and the special elements
$0_{\mathbb{Z}},1_{\mathbb{Z}}$ are defined in the way one would expect.

One then defines
$\mathbb{Q}:=\\{m\mid\neg(m^{\prime\prime}=_{\mathbb{Z}}0_{\mathbb{Z}})\\}$.
An equivalence relation $=_{\mathbb{Q}}$ is introduced on $\mathbb{Q}$ by:
$m=_{\mathbb{Q}}n\leftrightarrow
m^{\prime}\cdot_{\mathbb{Z}}n^{\prime\prime}=_{\mathbb{Z}}m^{\prime\prime}\cdot_{\mathbb{Z}}n^{\prime}$.
Rationals, for us, are just natural numbers, but, whenever we consider natural
numbers as rationals, we respect $=_{\mathbb{Q}}$. The functions
$+_{\mathbb{Q}},\cdot_{\mathbb{Q}}$, the relations
$<_{\mathbb{Q}},\leq_{\mathbb{Q}}$, and the special elements
$0_{\mathbb{Q}},1_{\mathbb{Q}}$ are defined straightforwardly.

In general, we omit the subscripts ‘Z’, ‘Q’ unless we fear for confusion,

It is important to realize that all functions and relations mentioned so far
are algorithmic. We learned the algorithms at elementary school and know, for
instance, how to find out, given rationals $p,q$, if $p=_{\mathbb{Q}}q$ or
not.

###  6.2. Real numbers

We now are ready to introduce the reals.

######  Definition 2.

A real number is an _approximation process_ , an infinite sequence
$x=x(0),x(1),\ldots$ of pairs
$x(n)=\bigl{(}x^{\prime}(n),x^{\prime\prime}(n)\bigr{)}$ of rationals such
that

  1. (i)

_$x$ is shrinking:_ for all $n$, $x^{\prime}(n)\leq x^{\prime}(n+1)\leq
x^{\prime\prime}(n+1)\leq x^{\prime\prime}(n)$ and

  2. (ii)

_$x$ is dwindling:_ for all $m$, there exists $n$ such that
$x^{\prime\prime}(n)-x^{\prime}(n)\leq\frac{1}{2^{m}}$.

$\mathcal{R}$ is the set of all real numbers. We use $x,y,\ldots$ as variables
over $\mathcal{R}$.

Brouwer gave Cantor’s notion his own colouring.
Every real number $x=x(0),x(1),\ldots$ is an infinite sequence of successive
approximations, and, like the infinite sequence $0,1,2,\ldots$ itself, never
finished and always under construction. Even if an algorithm has been given
determing the successive values of $x$, the finding of these successive values
keeps us busy forever. The number is the process of approximation itself: it
makes no sense to ask for the limit point that the successive approximations
are striving for.

For all reals $x$, for all rationals $p,q$, for all $n$, if
$p<_{\mathbb{Q}}x^{\prime}(n)<_{\mathbb{Q}}x^{\prime\prime}(n)<_{\mathbb{Q}}q$,
we say that $(p,q)$ is an approximation of $x$ of precision
$q-_{\mathbb{Q}}p$.

######  Definition 3.

For all real numbers $x,y$, we define:

$x<_{\mathcal{R}}y$ ($x$ _is smaller than $y$_) if and only if $\exists
n[x^{\prime\prime}(n)<_{\mathbb{Q}}y^{\prime}(n)]$, and:

$x\leq_{\mathcal{R}}y$ (_$x$ is not greater than $y$_) if and only if $\forall
n[x^{\prime}(n)\leq_{\mathbb{Q}}y^{\prime\prime}(n)]$, and:

$x\;\\#_{\mathcal{R}}\;y$ ($x$ _is apart from_ $y$) if and only if either
$x<_{\mathcal{R}}y$ or $y<_{\mathcal{R}}x$, and:

$x=_{\mathcal{R}}y$ (_$x$ coincides with $y$_) if and only if
$x\leq_{\mathcal{R}}y$ and $y\leq_{\mathcal{R}}x$.

We suppress the subscript ‘R’ if we expect that, doing so, we will not confuse
the reader.

Traditionally, our ‘real numbers’ would be called ‘number generators’.
The name ‘real number’ would then be reserved for equivalence classes of the
form
$[x]=\\{y\in\mathcal{R}\mid y=_{\mathcal{R}}x\\}$.
Also Brouwer does so, using the terms ‘point’ and ‘point kernel’.

We will not make this distinction but will only consider operations and
relations on $\mathcal{R}$ that respect the equivalence relation
$=_{\mathcal{R}}$.

The relations $<_{\mathcal{R}}$ and $\\#_{\mathcal{R}}$ are positive
relations. From a constructive point of view, they are more important than the
relations $\leq_{\mathcal{R}}$ and $=_{\mathcal{R}}$. The latter two relations
are negative, and, moreover, expressible in terms of the positive relations,
as: $x\leq_{\mathcal{R}}y\leftrightarrow\neg(y<_{\mathcal{R}}x)$ and:
$x=_{\mathcal{R}}y\leftrightarrow\neg(x\;\\#_{\mathcal{R}}\;y)$. Given real
numbers $x,y$ one may prove: ‘$x=_{\mathcal{R}}y$’ by assuming:
‘$x\;\\#_{\mathcal{R}}\;y$’ and obtaining a contradiction.

It is important that the positive relations $<_{\mathcal{R}}$ and
$=_{\mathcal{R}}$ are co-transitive, i.e.
$x<_{\mathcal{R}}y\rightarrow(x<_{\mathcal{R}}z\;\vee\;z<_{\mathcal{R}}y)$ and
$x\;\\#_{\mathcal{R}}\;y\rightarrow(x\;\\#_{\mathcal{R}}\;z\;\vee\;z\;\\#_{\mathcal{R}}\;y)$.

It suffices to prove this for the first relation.
Given $x,y,z$ such that $x<_{\mathcal{R}}y$, find $n$ such that
$z^{\prime\prime}(n)-z^{\prime}(n)<_{\mathbb{Q}}y^{\prime}(n)-x^{\prime\prime}(n)$
and decide: either $x^{\prime\prime}(n)<_{\mathbb{Q}}z^{\prime}(n)$ and
$x<_{\mathcal{R}}z$ or: $z^{\prime\prime}(n)<_{\mathbb{Q}}y^{\prime}(n)$ and
$z<_{\mathcal{R}}y$.

###  6.3. Cantor’s proof

In 1873, Cantor proves the following, see [19, §2]:

######  Theorem 5.

For every infinite sequence $x_{0},x_{1},\dots$ of reals, there exists a real
$x$ apart from every real in the sequence, that is:
$x\;\\#_{\mathcal{R}}\;x_{0},x\;\\#_{\mathcal{R}}\;x_{1},\ldots$

###### Proof.

Let an infinite sequence $x_{0},x_{1},x_{2},\ldots$ of reals be given.

Define $x=x(0),x(1),\ldots$, as follows, step by step.

First, define $x(0)=(0,1)$.

Now assume $x(n)$ has been defined and
$x^{\prime\prime}(n)-x^{\prime}(n)=_{\mathbb{Q}}\frac{1}{3^{n}}$.

Find $m_{0}:=$ the least $m$ such that
$x_{n}^{\prime\prime}(m)-x_{n}^{\prime}(m)<_{\mathbb{Q}}\frac{1}{3^{n+1}}$.

Note: either
$\frac{2}{3}x^{\prime}(n)+_{\mathbb{Q}}\frac{1}{3}x^{\prime\prime}(n)<_{\mathbb{Q}}x_{n}^{\prime}(m_{0})$
or
$x_{n}^{\prime\prime}(m_{0})<_{\mathbb{Q}}\frac{2}{3}x^{\prime}(n)+_{\mathbb{Q}}\frac{1}{3}x^{\prime\prime}(n)$.

If
$\frac{2}{3}x^{\prime}(n)+_{\mathbb{Q}}\frac{1}{3}x^{\prime\prime}(n)<_{\mathbb{Q}}x_{n}^{\prime}(m_{0})$,
define:
$x(n+1):=\bigl{(}x^{\prime}(n),\frac{2}{3}x^{\prime}(n)+\frac{1}{3}x^{\prime\prime}(n)\bigr{)}$
and, if not, define
$x(n+1):=\bigl{(}\frac{1}{3}x^{\prime}(n)+\frac{2}{3}x^{\prime\prime}(n),x^{\prime\prime}(n)\bigr{)}$.

By this choice of $x(n+1)$, we ensure
$x^{\prime\prime}(n+1)-x^{\prime}(n+1)=_{\mathbb{Q}}\frac{1}{3^{n+1}}$ and
$x\;\\#_{\mathcal{R}}\;x_{n}$. ∎

Our constructive argument differs but little from Cantor’s. Cantor makes it
perfectly clear how, given any countable list $x_{0},x_{1},\ldots,$ of reals,
one produces a real positively different from every real on the list.

We thus see that the statement ‘$\mathcal{R}$ is uncountable’, essentially, is
a positive statement.

Note that, by his exemplary proof, Cantor suggest to us how we should
understand and prove a proposition of the form ‘$A\subseteq\mathcal{R}$ is
uncountable’.

One defines operations $+_{\mathcal{R}}$ and $\cdot_{\mathcal{R}}$ on
$\mathcal{R}$ by:
for all $n$,
$(x+_{\mathcal{R}}\;y)(n):=\bigl{(}x^{\prime}(n)+_{\mathbb{Q}}y^{\prime}(n),x^{\prime\prime}(n)+_{\mathbb{Q}}y^{\prime\prime}(n)\bigr{)}$
and
$(x\cdot_{\mathcal{R}}y)(n)=\bigl{(}\min_{\mathbb{Q}}(x^{\prime}(n)\cdot_{\mathbb{Q}}y^{\prime}(n),x^{\prime}(n)\cdot_{\mathbb{Q}}y^{\prime\prime}(n),x^{\prime\prime}(n)\cdot_{\mathbb{Q}}y^{\prime}(n),x^{\prime\prime}(n)\cdot_{\mathbb{Q}}y^{\prime\prime}(n)),\\\
\max_{\mathbb{Q}}(x^{\prime}(n)\cdot_{\mathbb{Q}}y^{\prime}(n),x^{\prime}(n)\cdot_{\mathbb{Q}}y^{\prime\prime}(n),x^{\prime\prime}(n)\cdot_{\mathbb{Q}}y^{\prime}(n),x^{\prime\prime}(n)\cdot_{\mathbb{Q}}y^{\prime\prime}(n))\bigr{)}$.

Also subtraction and an absolute value function $x\mapsto|x|$ may be defined.

For every rational $q$, we define $q_{\mathcal{R}}$ in $\mathcal{R}$ such
that, for all $n$,
$q_{\mathcal{R}}(n)=(q-_{\mathbb{Q}}\frac{1}{2^{n}},q+_{\mathbb{Q}}\frac{1}{2^{n}})$.

We omit subscripts ‘R’ where we think it does no harm to do so.

##  7\. Fugitive integers and oscillating reals

The following definition lies at the basis of many counterexamples in
Brouwer’s style to various mathematical results that do not stand a
constructive reading.

We consider the decimal expansion of $\pi$, evaluating it step by step,
hunting for the first block of 99 consecutive 9’s. We would like to define
$k_{99}$ as the least number $n$ such that at the places $n,n+1,\ldots n+98$
in the decimal expansion of $\pi$ we find the value $9$, but we have to be
careful as we do not know if such a number $n$ exists.

######  Definition 4 (The fugitive ‘number’ $k_{99}$).

Let $d=d(0),d(1),\ldots$ be the decimal expansion of $\pi$, that is: $d$ is
the function from $\mathbb{N}$ to $\\{0,1,\ldots,9\\}$ such that
$\pi=3+\sum_{n=0}^{\infty}d(n)\cdot 10^{-n-1}$.

For each $n$, we define:

$k_{99}\leq n$ if and only if $\exists j\leq n\forall i<99[d(j+i)=9]$, and:

$n<k_{99}$ if and only if $\forall j\leq n\exists i<99[d(i+j)\neq 9]$, and:

$n=k_{99}$ if and only if $k_{99}\leq n$ and $\forall j<n[j<k_{99}]$.

Note that we do not define a natural number $k_{99}$ but only the meaning of
an expression like ‘$k_{99}\leq n$’.

Also note that, for each $n$, one may find out, for each of the propositions
‘$k_{99}\leq n$’, ‘$n<k_{99}$’, and ‘$n=k_{99}$’, if they are true or not, by
simply calculating the first $n$ values of the decimal expansion of $\pi$.

The statement ‘$P:=\exists n[n=k_{99}]$’ is a prime example of an undecided
proposition, i.e. we do not have a proof of $P$, but we also do not have a
proof that we never will find one, and we have no procedure to find either one
of these proofs in finitely many steps.

The problem of the 99 9’s in the decimal expansion of $\pi$ is not important
in itself. It only is a pedagogical example, showing that we have no method to
solve this kind of problems. Should someone, by historical accident, find the
99 9‘s, then one easily formulates a similar proposition that is still
undecided.

######  Definition 5 (The ‘oscillating’ reals $\rho_{0},\rho_{1},\rho_{2}$).

We define real numbers $0_{\mathcal{R}}$, $\rho_{0},\rho_{1}$ and $\rho_{2}$,
as follows.

$0_{\mathcal{R}}$ is the real number such that, for all $n$,
$0_{\mathcal{R}}(n)=(-\frac{1}{2^{n}},\frac{1}{2^{n}})$.

$\rho_{0}=(\frac{1}{2})^{k_{99}}$ is the real number such that, for all
$n<k_{99}$, $\rho_{0}(n):=(-\frac{1}{2^{n}},\frac{1}{2^{n}})$, and, for all
$n\geq k_{99}$, $\rho_{0}(n):=(\frac{1}{2^{k_{99}}},\frac{1}{2^{k_{99}}})$.

$\rho_{1}=(-\frac{1}{2})^{k_{99}}$ is the real number such that, for all
$n<k_{99}$, $\rho_{1}(n)=(-\frac{1}{2^{n}},\frac{1}{2^{n}})$, and, for all
$n\geq k_{99}$, if $k_{99}$ is even, then
$\rho_{1}(n):=(\frac{1}{2^{k_{99}}},\frac{1}{2^{k_{99}}})$, and, if $k_{99}$
is odd, then $\rho_{1}(n):=(-\frac{1}{2^{k_{99}}},-\frac{1}{2^{k_{99}}})$.

Finally, $\rho_{2}:=\rho_{0}+_{\mathcal{R}}\rho_{1}$.

Now note the following:

(1) $0_{\mathcal{R}}=_{\mathcal{R}}\rho_{0}\leftrightarrow\forall
n[n<k_{99}]$, and we have no proof of ‘$\forall n[n<k_{99}]$’.

Also: $\neg(0_{\mathcal{R}}=_{\mathcal{R}}\rho_{0})\leftrightarrow\neg\forall
n[n<k_{99}]$, and we have no proof of ‘$\neg\forall n[n<k_{99}]$’.

Finally: $0_{\mathcal{R}}<_{\mathcal{R}}\rho_{0}\leftrightarrow\exists
n[n=k_{99}]$, and we have no proof of ‘$\exists n[n=k_{99}]$’.

We thus see that, in general, given real numbers $x,y$, we have no means of
proving one of the propositions ‘$x=_{\mathcal{R}}y$’,
‘$\neg(x=_{\mathcal{R}}y)$’ , ‘$x<_{\mathcal{R}}y$’.

(2) Note: $0_{\mathcal{R}}\leq_{\mathcal{R}}\rho_{0}$, but, as we saw, we have
no proof of ‘$0_{\mathcal{R}}=_{\mathcal{R}}\rho_{0}$’, nor of
‘$0_{\mathcal{R}}<_{\mathcal{R}}\rho_{0}$’.

We thus see that, in general, given real numbers $x,y$ such that
$x\leq_{\mathcal{R}}y$, we have no means of proving either one of the
propositions ‘$x=_{\mathcal{R}}y$’ or ‘$x<_{\mathcal{R}}y$’.

(3) Note: $0_{\mathcal{R}}\leq_{\mathcal{R}}\rho_{1}\leftrightarrow\forall
n[n=k_{99}\rightarrow\exists m[n=2m]]$, and we have no proof of: ‘$\forall
n[n=k_{99}\rightarrow\exists m[n=2m]]$’.

Note: $\rho_{1}\leq_{\mathcal{R}}0_{\mathcal{R}}\leftrightarrow\forall
n[n=k_{99}\rightarrow\exists m[n=2m+1]]$, and we have no proof of: ‘$\forall
n[n=k_{99}\rightarrow\exists m[n=2m+1]]$’.

We thus see that, in general, given real numbers $x,y$, we have no means of
proving either one of the propositions ‘$x\leq_{\mathcal{R}}y$’,
‘$y\leq_{\mathcal{R}}x$’.

(4) Note: $\rho_{2}=_{\mathcal{R}}2\cdot\rho_{0}\leftrightarrow\forall
n[n=k_{99}\rightarrow\exists m[n=2m]]$ and
$\rho_{2}=_{\mathcal{R}}0_{\mathcal{R}}\leftrightarrow\forall
n[n=k_{99}\rightarrow\exists m[n=2m+1]]$. We have no means of proving either
one of the propositions ‘$\rho_{2}=_{\mathcal{R}}2\cdot\rho_{0}$’,
‘$\rho_{2}=_{\mathcal{R}}0_{\mathcal{R}}$’.
We will use use the number $\rho_{2}$ in Section 9.

$\rho_{0},\rho_{1},\rho_{2}$ are examples of real numbers oscillating around
$0_{\mathcal{R}}$.

$\rho_{0}$ oscillates above $0_{\mathcal{R}}$ and $\rho_{1}$ oscillates up and
down around $0_{\mathcal{R}}$.

$\rho_{2}=\rho_{0}+\rho_{1}$ oscillates between $0_{\mathcal{R}}$ and
$2\cdot\rho_{0}$.

##  8\. Rejecting $P\;\vee\;\neg P$

###  8.1. Mathematics and Logic

Brouwer describes mathematics as being developed by the mind having come to
awareness and playfully exploring its possibilities, see, for instance, [14].
Mathematics is not dependent on any evidence from the senses. All other
science is applied mathematics, as mathematics recognizes and enforces
patterns on the data acquired by observation.

Logic in particular is not a foundational science, prescribing the way one
should think, but an observational science. Mathematics is not reigned by
logic. Mathematics is a languageless activity of the mind. As we observed
already in Section 1, only when we want to communicate about mathematics,
language comes in. We communicate with other people, trying to induce them to
make mathematical constructions like the ones we ourselves are making, and we
communicate with ourselves, understanding the weakness of our memory, and
hoping to be able to remind ourselves tomorrow of what we did today. Observing
ourselves and others when we are busy communicating about mathematics, we take
notes of the sounds and signs that are used. We discover patterns and
regularities, and then promote such regularities to laws of logic. There is no
guarantee, however, that someone, even myself, who is making sounds or giving
other signs in accordance with these laws is actually succeeding in making
successful mathematical constructions. In this sense, the ‘laws of logic’ are
unreliable.

Learning logic is part of learning the language of mathematics. Learning the
meaning of the connectives ‘$\ldots$or$\ldots$’, ‘$\ldots$and $\ldots$’,
‘$\ldots$ if $\ldots$ ’, and ‘not :$\ldots$’, and the quantifiers ‘$\exists
x\in V[\ldots x\ldots]$’ and ‘$\forall x\in V[\dots x\ldots]$’, is like
learning the meaning of the expressions ‘infinite’ or ‘uncountable’ in the
case of Theorems 1 and 5.

A connective $\ast$ is a general method to obtain a new proposition, $P\ast
Q$, from any two given propositions, $P$ and $Q$. Understanding $P$ and $Q$
means having some idea about what counts as a proof of $P,Q$, respectively. If
we are able to point out in general terms what we should consider as a proof
of $P\ast Q$, given our understanding of proofs of $P,Q$, we will have
explained the meaning of the connective $\ast$.

###  8.2. Disjunction

Let us start with the case of disjunction, $\vee$.

If someone says to us: ‘I have a proof of $P\vee Q$, $P$ or $Q$’, we expect,
from our experience with earlier situations in which the word ‘or’ occurred,
that he will come up with a proof of $P$ or with a proof of $Q$. We therefore
adopt the rule that a proof of $P\vee Q$ must consist either in a proof of $P$
or in a proof of $Q$.

One might bring forward that disjunction is not always taken in this
constructively strong sense. There were other situations too! Some
mathematicians might even say: ‘When _I_ make a statement $P\vee Q$, I merely
want to remind my reader that $\neg P$ and $\neg Q$ are not both true’.

The intuitionistic mathematician then answers: ‘ Sometimes one uses the
stronger interpretation and at other times one uses the weaker one. Let us end
this confusion and make the first and stronger interpretation the canonical
one and always watch what we want to say.’

Our decision implies that the statement:

$\exists n[k_{99}\leq n]\;\vee\;\forall n[n<k_{99}]$, i.e. $\exists
n[k_{99}\leq n]\;\vee\;\neg\exists n[k_{99}\leq n]$.

is not a true statement.

Why?

Until now, we did not find a place in the decimal expansion of $\pi$ where
there is an uninterrupted sequence of $99$ digits 9: we have no proof of
‘$\exists n[k_{99}\leq n]$’.

Until now, we also did not find a clever argument showing that such an
uninterrupted sequence of $99$ digits $9$ never will be found: we have no
proof of ‘$\neg\exists n[k_{99}\leq n]$’.

Until now, therefore, we have no proof of ‘$\exists n[k_{99}\leq
n]\;\vee\;\neg\exists n[k_{99}\leq n]$’.

Note that there is an asymmetry in the two horns of the dilemma. The
(possible) truth of $\exists n[k_{99}\leq n]$ will become clear to anyone who
just patiently calculates the successive values of the decimal expansion of
$\pi$, but the discovery of the (possible) truth of $\forall n[n<k_{99}]$
requires mathematical ingenuity.

The example shows that the principle

If $\forall n[P(n)\;\vee\;\neg P(n)]$, then $\exists
n[P(n)]\;\vee\;\neg\exists n[P(n)]$

is unreliable.

How did we come to trust it?

We unthinkingly generalized our experience with handling finite sets and
bounded quantifiers. After all, the following holds, for any given $m$, even
for $m=10^{10^{10}}$:

If $\forall n\leq m[P(n)\;\vee\;\neg P(n)]$, then $\exists n\leq
m[P(n)]\;\vee\;\neg\exists n\leq m[P(n)]$,

because, at least in principle, we can check each of the numbers
$0,1,\ldots,m$ and find out if one of them has the property $P$.

The case $\\{0,1,\ldots,m\\}$ does not extend to the case $\\{0,1,2,\dots\\}$.
Checking each of the infinitely many numbers $0,1,2,\ldots$ is not feasible.
If we think we can do it we must imagine ourselves to be angels rather than
human beings.

###  8.3. ‘Reckless’ or ‘hardy’ statements

When in a playful mood, we call the statement:

$\exists n[k_{99}=n]\;\vee\;\forall n[n<k_{99}]$

a reckless or hardy statement. Actually, it is foul play. We call the
mathematician upholding the above statement as true ‘reckless’ because we take
him to read the statement constructively. Probably, he will protest.

For us, the terms ‘reckless’ and ‘hardy’ indicate that the statement called so
has no constructive proof, although the non-intuitionistic mathematician,
using his own reading, sees no objection.

Other examples of reckless statements are:

$\neg\forall n[n<k_{99}]\;\vee\;\forall n[n<k_{99}]$ $\exists
n[n=k_{88}]\rightarrow\exists n[n=k_{99}]$ $\forall n[2n\neq
k_{99}]\;\vee\;\forall n[2n+1\neq k_{99}]$ $\exists
n[n=k_{88}]\rightarrow(\forall n[2n\neq k_{99}]\;\vee\;\forall n[2n+1\neq
k_{99}])$

‘$n=k_{88}$’ here stands for: ‘$n$ is the least number $m$ such that at the
places $m,m+1,\ldots,m+87$ in the decimal expansion of $\pi$ we find the value
$8$’.

Theorems implying a reckless statement themselves will be considered reckless.

###  8.4. Brouwer’s example and the halting problem

The above example of an undecided proposition, ‘$\exists n[n=k_{99}]$’, is
simple and very important. A first such example was given by Brouwer in [10].

The example is related to the discovery, in 1936, of the ‘halting problem’ by
A.M. Turing (1912-1954). We briefly describe this problem using the approach
developed by S.C. Kleene (1909-1994), see [40, Chapter XI].

Natural numbers are used for coding algorithms for (partial) functions from
$\mathbb{N}$ to $\mathbb{N}$. There is a computable predicate on triples of
natural numbers called $T$. For all $e,n,z$, $T(e,n,z)$ if and only if $z$
codes a successful computation according to the algorithm coded by $e$ at the
argument $n$. The algorithm coded by $e$ halts at $n$ if and only if $\exists
z[T(e,n,z)]$. There is a function $U$ from $\mathbb{N}$ to $\mathbb{N}$ that
extracts from every $z$ coding a computation the outcome $U(z)$ of the
computation. A function $\alpha$ from $\mathbb{N}$ to $\mathbb{N}$ is
computable if and only if there exists $e$ such that
$\forall n\exists z[T(e,n,z)\;\wedge\;U(z)=\alpha(n)]$. A number $e$ with this
property is called an index of the function $\alpha$.

Every number $e$ determines a partial function $\varphi_{e}$ from $\mathbb{N}$
to $\mathbb{N}$:
for all $n$, $\varphi_{e}(n)=U(z)$, where $z$ is the least number $w$ such
that $T(e,n,w)$.
$\varphi_{e}$ is only defined at $n$ if $\exists w[T(e,n,w)]$.

The (self-)halting problem is the question if there exists a computable
function $\alpha$ from $\mathbb{N}$ to $\mathbb{N}$ such that, for each $e$,

$\alpha(e)\neq 0\leftrightarrow\exists
z[T(e,e,z)]\leftrightarrow\varphi_{e}\;\mathit{is\;defined\;at\;e}.$

Such a computable function $\alpha$ would be called a solution to the halting
problem.

Turing’s theorem is that there is no solution to the halting problem.

One may prove, without much difficulty, that there exists $e$ such that
$\exists n[k_{99}\leq n]\leftrightarrow\exists z[T(e,e,z)]$: the example we
considered is one of the problems in the scope of the halting problem.
Therefore, a solution to the halting problem would also solve the problem:
‘$\exists n[k_{99}\leq n]$’. This fact gives some apriori probability to
Turing’s result.

###  8.5. The other logical ‘constants’

The so-called proof-theoretical interpretation of the disjunction we sketched
in Subsection 8.2 is extended to the other logical ‘constants’ as follows.

A proof of ‘$P$ and $Q$’ is a proof of ‘$P$’ together with a proof of ‘$Q$’.

A proof of ‘if $P$, then Q’ is
a proof of ‘$Q$’ possibly using ‘$P$’ as an extra assumption.

A proof of ‘not $P$’ is a proof of ‘if $P$, then 0=1’.

For explaining the quantifiers, we need the notion of a propositional
function. Let $V$ be a set and let $v\mapsto P(v)$ a function that associates
to every $v$ in $V$ a proposition $P(v)$. We then may introduce propositions
$\exists x\in V[P(x)]$ and $\forall x\in V[P(x)]$ by stipulating:

A proof of ‘$\exists x\in V[P(x)]$’ consists of an element $v$ of $V$ together
with a proof of the proposition ‘$P(v)$’.

A proof of $\forall x\in V[P(x)]$ is a function $v\mapsto p(v)$ associating to
every $v$ in $V$ a proof $p(v)$ of the proposition ‘$P(v)$’.

These explanations are not to be considered as exact definitions. They only
indicate a provisional intention as to how we want to use our words.

##  9\. A test case: the Intermediate Value Theorem

###  9.1. The theorem

A function from $\mathcal{X}\subseteq\mathcal{R}$ to $\mathcal{R}$ is an
effective method $f$, that, given any input $x$ from $\mathcal{X}$, will
produce a well-defined outcome $f(x)$ in $\mathcal{R}$, of course respecting
the fundamental relation of real coincidence, i.e.

> for all $x,y$ in $\mathcal{X}$, if $x=_{\mathcal{R}}y$, then
> $f(x)=_{\mathcal{R}}f(y)$.

We take the notion of a function as a primitive notion, i.e. we do not explain
what a function is by using notions that have been introduced before.

######  Definition 6.

Let $f$ be a function from $\mathcal{X}\subseteq\mathcal{R}$ to $\mathcal{R}$
and let $x$ in $\mathcal{X}$ be given.
$f$ is _continuous at $x$_ if and only if $\forall p\exists m\forall
y\in\mathcal{X}[|y-x|<\frac{1}{2^{m}}\rightarrow|f(y)-f(x)|<\frac{1}{2^{p}}]$.
$f$ is _continuous_ if and only if $f$ is continuous at every $x$ in
$\mathcal{X}$.

The Intermediate Value Theorem states the following:

> Let $f$ be a continuous function from $[0,1]$ to $\mathcal{R}$.
> Then $\forall y\in\mathcal{R}[f(0)\leq y\leq f(1)\rightarrow\exists
> x\in[0,1][f(x)=y]]$.

The first version of this Theorem dates from 1817 and is due to B. Bolzano
(1781-1848), see [5].

Note that the intuitionistic mathematician reads the statement of the Theorem
differently from his non-intuitionistic colleague: he understands the logical
constants constructively, as sketched in Section 8.

###  9.2. The proof as we learnt it

One may use the fruitful method of successive bisection, as follows.

Let $y$ be given such that $f(0)\leq y\leq f(1)$.

Define $x$ in $[0,1]$, step by step, as follows.

Define $x(0):=(0,1)$.

Now let $n$ be given such that $x(n)$ has been defined already.

Consider $m:=\frac{x^{\prime}(n)+x^{\prime\prime}(n)}{2}$, the midpoint of the
rational interval $\bigl{(}x^{\prime}(n),x^{\prime\prime}(n)\bigr{)}$.

If $f(m)\leq y$, define $x(n+1)=\bigl{(}m,x^{\prime\prime}(n)\bigr{)}$.

If $y<f(m)$, define $x(n+1)=\bigl{(}x^{\prime}(n),m\bigr{)}$.

This completes the definition of $x$.

$x$ is a well-defined real number, and, as one verifies by induction,
for every $n$, $x^{\prime\prime}(n)-x^{\prime}(n)=\frac{1}{2^{n}}$ and
$f\bigl{(}x^{\prime}(n)\bigr{)}\leq y\leq
f\bigl{(}x^{\prime\prime}(n)\bigr{)}$.

We claim: $f(x)=y$, and we prove this claim as follows.

Assume $y<_{\mathcal{R}}f(x)$. Using the continuity of $f$ at $x$, find $r$
such that
$\forall z\in[0,1][|x-z|<\frac{1}{2^{r}}\rightarrow y<_{\mathcal{R}}f(z)]$.

Note: $|x-x^{\prime}(r+1)|<\frac{1}{2^{r}}$, and, therefore,
$y<_{\mathcal{R}}f\bigl{(}x^{\prime}(r+1)\bigr{)}]$, but also
$f\bigl{(}x^{\prime}(r+1)\bigr{)}<_{\mathcal{R}}y$.

Contradiction.

Conclude: $\neg\bigl{(}y<_{\mathcal{R}}f(x)\bigr{)}$, i.e.
$f(x)\leq_{\mathcal{R}}y$.

By a similar argument, conclude: $y\leq_{\mathcal{R}}f(x)$ and:
$f(x)=_{\mathcal{R}}y$.

###  9.3. An objection to the ‘proof’

The construction of the point $x$, in the above argument, can not be carried
out, as, in general, we are unable to decide:

$f(m)\leq_{\mathcal{R}}y$ or $\;y<_{\mathcal{R}}f(m)$.

###  9.4. Two counterexamples to the theorem

We give two examples showing that the statement of the theorem, if one reads
it constructively, sometimes fails to be true.

First example.

Let $\rho_{1}=(-\frac{1}{2})^{k_{99}}$ be the number oscillating up and down
around $0_{\mathcal{R}}$ introduced in Definition 5. Define a function $f_{0}$
from $[0,1]$ to $\mathcal{R}$ such that

  1. (i)

$f_{0}(0)=0$ and $f_{0}(1)=1$ and
$f_{0}(\frac{1}{3})=f_{0}(\frac{2}{3})=\frac{1}{2}+\rho_{1}$, and

  2. (ii)

$f_{0}$ is linear on the interval $[0,\frac{1}{3}]$, on the interval
$[\frac{1}{3},\frac{2}{3}]$ and on the interval $[\frac{2}{3},1]$.

Note: $0<\rho_{1}\leftrightarrow\forall
x\in[\frac{1}{3},1][f_{0}(x)>\frac{1}{2}]$ and
$\rho_{1}<0\leftrightarrow\forall x\in[0,\frac{2}{3}][f_{0}(x)<\frac{1}{2}]$.

Assume we find $x$ such that $f_{0}(x)=\frac{1}{2}$.

Find $p$ such that $x^{\prime\prime}(p)-x^{\prime}(p)<\frac{1}{3}$ and note:
either $\frac{1}{3}<x^{\prime}(p)$ or $x^{\prime\prime}(p)<\frac{2}{3}$.

If $\frac{1}{3}<x^{\prime}(p)$, then $\frac{1}{3}<x$ and $\neg(0<\rho_{1})$,
that is: $\rho_{1}\leq 0$, and,

if $x^{\prime\prime}(p)<_{\mathbb{Q}}\frac{2}{3}$, then $x<\frac{2}{3}$ and
$\neg(\rho_{1}<0)$, that is: $0\leq\rho_{1}$.

Conclude: either $0\leq\rho_{1}$ or $\rho_{1}\leq 0$.

This is a reckless or hardy conclusion.

Second example.

Let $\rho_{0}=(\frac{1}{2})^{k_{99}}$ the number oscillating above
$0_{\mathcal{R}}$ introduced in Definition 5 and let
$\rho_{2}=\rho_{0}+\rho_{1}=(\frac{1}{2})^{k_{99}}+(-\frac{1}{2})^{k_{99}}$ be
the number oscillating between $0_{\mathcal{R}}$ and $2\cdot\rho_{0}$, also
introduced in Definition 5.

Define a function $f_{1}$ from $[0,1]$ to $\mathcal{R}$ such that

  1. (i)

$f_{1}(0)=0$ and $f_{1}(\frac{1}{2})=\rho_{0}$ and $f_{1}(1)=\rho_{2}$, and

  2. (ii)

$f_{1}$ is linear on the interval $[0,\frac{1}{2}]$ and on the interval
$[\frac{1}{2},1]$.

Note: $f_{1}(0)\leq\frac{1}{2}\cdot\rho_{2}\leq f_{1}(1)$.

If $\exists n[2n=k_{99}]$,
then $0<\rho_{0}\;\wedge\;\rho_{2}=2\cdot\rho_{0}$ and $\forall
x\in[0,1][f_{1}(x)=\frac{1}{2}\cdot\rho_{2}\rightarrow x=\frac{1}{2}]$, and,
if $\exists n[2n+1=k_{99}]$,
then $0<\rho_{0}\;\wedge\;\rho_{2}=0$ and $\forall
x\in[0,1][f_{1}(x)=\frac{1}{2}\cdot\rho_{2}\rightarrow(x=0\;\vee\;x=1)]$.

Suppose we find $x$ in $[0,1]$ such that $f_{1}(x)=\frac{1}{2}\cdot\rho_{2}$.

Find $p$ such that $x^{\prime\prime}(p)-x^{\prime}(p)<\frac{1}{2}$ and note:
either $x^{\prime\prime}(p)<\frac{1}{2}$ or $\frac{1}{2}<x^{\prime}(p)$ or
$0<x^{\prime}(p)$ and $x^{\prime\prime}(p)<1$.

If $x^{\prime\prime}(p)<\frac{1}{2}$ or $\frac{1}{2}<x^{\prime}(p)$, then
$\neg\exists n[2n=k_{99}]$.

If $0<x^{\prime}(p)$ and $x^{\prime\prime}(p)<1$, then $\neg\exists
n[2n+1=k_{99}]$.

We thus see: $\neg\exists n[2n=k_{99}]$ or $\neg\exists n[2n+1=k_{99}]$.

This is a reckless or hardy conclusion.

Note that the above counterexamples pose a serious problem to the
mathematician. If the Intermediate Value Theorem does not stand a
straightforward constructive reading, what then is its meaning? The defender
of the theorem must mumble something like: ‘Well, I did not mean that you
really could find a point where $f$ assumes the intermediate value, but
$\ldots$’

Mathematical theorems without ‘numerical content’ are a shame and an
embarassment.

We should not, because of these examples, put aside the Intermediate Value
Theorem as nonsense, but, arguing carefully, try and find related statements
that are constructively true.

###  9.5. An approximate version

It helps to weaken the conclusion of the Intermediate Value Theorem by
requiring only that, for every given accuracy $\frac{1}{2^{p}}$, there exists
a point where the function assumes a value closer to the given intermediate
value than $\frac{1}{2^{p}}$.

Brouwer, who knew his own famous fixed-point theorem to be constructively
false, formulated and proved such an approximate fixed-point theorem, see [15]
111111The 1-dimensional case of Brouwer’s fixed-point theorem is closely
related to the Intermediate value Theorem.. Note that the proof of the new
theorem still is using the method of successive bisection.

######  Theorem 6 (The Approximate Intermediate Value Theorem).

Let $f$ be a continuous function from $[0,1]$ to $\mathcal{R}$.

Then $\forall p\forall y\in\mathcal{R}[f(0)\leq y\leq f(1)\rightarrow\exists
x\in[0,1][y-\frac{1}{2^{p}}<f(x)<y+\frac{1}{2^{p}}]$.

###### Proof.

Let $p$ be given and let $y$ be given such that $f(0)\leq y\leq f(1)$.

Define $x$ in $[0,1]$, step by step, as follows.

Define $x(0):=(0,1)$ and note:
$f\bigl{(}x^{\prime}(0)\bigr{)}-\frac{1}{2^{p+1}}<y<f\bigl{(}x^{\prime\prime}(0)\bigr{)}+\frac{1}{2^{p+1}}$.

Now let $n$ be given such that $x(n)$ has been defined already.

Consider $m:=\frac{x^{\prime}(n)+x^{\prime\prime}(n)}{2}$ and $z:=f(m)$.

Find $l$:= the least $k$ such that both
$z^{\prime\prime}(k)-z^{\prime}(k)<\frac{1}{2^{p+1}}$ and
$y^{\prime\prime}(k)-y^{\prime}(k)<\frac{1}{2^{p+1}}$ and define $s:=z(l)$.

1\. If $s^{\prime\prime}<y^{\prime}(l)+\frac{1}{2^{p+1}}$, define
$x(n+1)=(m,x^{\prime\prime}(n))$.
Then: $f(m)\leq s^{\prime\prime}<y^{\prime}(l)+\frac{1}{2^{p+1}}\leq
y+\frac{1}{2^{p+1}}$ and: $f(m)-\frac{1}{2^{p+1}}<y$.

2\. If not $s^{\prime\prime}<y^{\prime}(l)+\frac{1}{2^{p+1}}$, define
$x(n+1)=(x^{\prime}(n),m)$.
Then: $y^{\prime\prime}(l)<y^{\prime}(l)+\frac{1}{2^{p+1}}\leq
s^{\prime\prime}<s^{\prime}+\frac{1}{2^{p+1}}$ and:
$y<f(m)+\frac{1}{2^{p+1}}$.

This completes the definition of $x$.

$x$ is a well-defined real number, and,
for every $n$, $x^{\prime\prime}(n)-x^{\prime}(n)=\frac{1}{2^{n}}$ and
$f\bigl{(}x^{\prime}(n)\bigr{)}-\frac{1}{2^{p+1}}<y<f\bigl{(}x^{\prime\prime}(n)\bigr{)}+\frac{1}{2^{p+1}}$.

Using the fact that $f$ is continuous at $x$, find $r$ such that
$\forall z\in[0,1][x-\frac{1}{2^{r}}<z<x+\frac{1}{2^{r}}\rightarrow
f(x)-\frac{1}{2^{p+1}}<f(z)<f(x)+\frac{1}{2^{p+1}}]$.

1\. Note: $x-\frac{1}{2^{r}}<x^{\prime}(r+1)\leq x$, and:
$f(x)<f(x^{\prime}(r+1))+\frac{1}{2^{p+1}}<y+\frac{1}{2^{p+1}}+\frac{1}{2^{p+1}}=y+\frac{1}{2^{p}}$.

2\. Note: $x\leq x^{\prime\prime}(r+1)<x+\frac{1}{2^{r}}$, and:
$y<f\bigl{(}x^{\prime\prime}(r+1)\bigr{)}+\frac{1}{2^{p+1}}<f(x)+\frac{1}{2^{p+1}}+\frac{1}{2^{p+1}}=f(x)+\frac{1}{2^{p}}$.

Conclude: $y-\frac{1}{2^{p}}<f(x)<y+\frac{1}{2^{p}}$.∎

###  9.6. Locally non-constant functions

One may also try to restrict the class of functions to which the Intermediate
Value Theorem applies. Observe that the two functions mentioned as
counterexamples in Subsection 9.4 have the property that, over a whole
interval, one does not know if they change their value. Let us try to forbid
such behaviour. We require constructive evidence that, for every $y$, for
every interval $(p,q)$, the function does not have, on the interval $(p,q)$,
the constant value $y$.

######  Definition 7.

A function $f$ from $[0,1]$ to $\mathcal{R}$ is _locally non-constant_ if and
only if
$\forall y\in\mathcal{R}\forall p\in\mathbb{Q}\forall
q\in\mathbb{Q}[0<p<q<1\rightarrow\exists
x\in[0,1][p<x<q\;\wedge\;f(x)\;\\#_{\mathcal{R}}\;y]]$.

The following Lemma says that, if, for a given intermediate value $y$, the
function $f$ assumes, in any given interval, a value positively different from
$y$, then there is a point where $f$ assumes the value $y$.

######  Lemma 7.

Let $f$ be a continuous function from $[0,1]$ to $\mathcal{R}$.

Let $y$ be given such that $f(0)\leq y\leq f(1)$ and

$\forall p\in\mathbb{Q}\forall q\in\mathbb{Q}[0<p<q<1\rightarrow\exists
x\in[0,1][p<x<q\;\wedge\;f(x)\;\\#_{\mathcal{R}}\;y]]$.

Then $\exists x\in[0,1][f(x)=y]$.

###### Proof.

Let $y$ be given such that $f(0)\leq y\leq f(1)$.

Define $x$ in $[0,1]$, as follows, step by step.

Define $x(0):=(0,1)$.

Now let $n$ be given such that $s:=x(n)$ has been defined.

Using the continuity of $f$, find a rational number $q$ such that
$\frac{2}{3}s^{\prime}+_{\mathbb{Q}}\frac{1}{3}s^{\prime\prime}<q<\frac{1}{3}s^{\prime}+_{\mathbb{Q}}\frac{2}{3}s^{\prime\prime}$
and $f(q)\;\\#_{\mathcal{R}}\;y$.

If $f(q)<_{\mathcal{R}}y$, define $x(n+1):=\bigl{(}x^{\prime}(n),q\bigr{)}$,
and,
if $y<_{\mathcal{R}}f(q)$, define
$x(n+1):=\bigl{(}q,x^{\prime\prime}(n)\bigr{)}$.

This completes the definition of $x$.

$x$ is a well-defined real number, as, for each $n$,
$x^{\prime}(n)\leq x^{\prime}(n+1)\leq x^{\prime\prime}(n+1)\leq
x^{\prime\prime}(n)$ and
$x^{\prime\prime}(n+1)-x^{\prime}(n+1)\leq\frac{2}{3}\bigl{(}x^{\prime\prime}(n)-x^{\prime}(n)\bigr{)}$.

Moreover, for each $n$,
$f\bigl{(}x^{\prime}(n)\bigr{)}\leq_{\mathcal{R}}y\leq_{\mathcal{R}}f\bigl{(}x^{\prime\prime}(n)\bigr{)}$.

Assume: $f(x)<_{\mathcal{R}}y$.

Find $p$ such that $\frac{1}{2^{p}}<y-_{\mathcal{R}}f(x)$, and find $q$ such
that
$\forall
z\in[0,1][|z-x|<\frac{1}{2^{q}}\rightarrow|f(z)-f(x)|<_{\mathcal{R}}\frac{1}{2^{p}}]$.
Then $\forall z\in[0,1][|z-x|<\frac{1}{2^{q}}\rightarrow
f(z)<_{\mathcal{R}}y$. Find $r$ such that
$(\frac{2}{3})^{r}<\frac{1}{2})^{q}$.
Conclude: $f(x^{\prime\prime}(r))<_{\mathcal{R}}y$. Contradiction.

We thus see: $\neg(f(x)<_{\mathcal{R}}y)$, that is: $f(x)\geq_{\mathcal{R}}y$.

For similar reasons: $f(x)\leq_{\mathcal{R}}y$. Conclude:
$f(x)=_{\mathcal{R}}y$. ∎

######  Theorem 8 (The Intermediate Value Theorem for locally non-constant
functions).

Let $f$ be a continuous and locally non-constant function from $[0,1]$ to
$\mathcal{R}$. Then $\forall y[f(0)\leq y\leq f(1)\rightarrow\exists
x\in[0,1][f(x)=y]]$.

###### Proof.

Use Lemma 7. ∎

Many real functions may be proven to be locally non-constant and Theorem 8 is
widely applicable121212Theorems 6 and 8 may be found in [8, Theorem 2.5]..

From a constructive point of view, the next result, Theorem 9 is not a nice
result. The result nevertheless is instructive. The intuitionistic
mathematician may say: ‘Yes, this explains the classical mathematician’s
belief that the Intermediate Value Theorem is true. He means no more than that
it is impossible to have constructive evidence, for every point $x$ in the
domain of the function, that the value assumed at $x$ is apart from the given
intermediate value. Unfortunately, even if this impossible, it may also be
impossible to find a point where the intermediate value is assumed.’

######  Theorem 9 (The Negative Intermediate Value Theorem).

Let $f$ be a continuous function from $[0,1]$ to $\mathcal{R}$.

Then $\forall y[f(0)\leq y\leq f(1)\rightarrow\neg\forall
x\in[0,1][f(x)\;\\#_{\mathcal{R}}\;y]]$.

###### Proof.

Use Lemma 7. ∎

###  9.7. At most countably many exceptions

One may also observe that the Intermediate Value Theorem goes through for
‘most’ intermediate values.

######  Theorem 10 (The Intermediate Value Theorem holds with at most
countably many exceptions131313In [4], one finds various theorems ‘with
countably many exceptions’, for instance, Theorem 4.9: if
$f;[0,1]\rightarrow\mathcal{R}$ is uniformly continuous, then for all but
countably many $y\geq\inf(f)$ the set
$\\{x\in[0,1]\mid f(x)\leq y\\}$ is _(constructively)_ compact.).

Let $f$ be a continuous function from $[0,1]$ to $\mathcal{R}$.

There exists an infinite sequence $y_{0},y_{1},\ldots$ of elements of $[0,1]$
such that

$\forall y[\bigl{(}f(0)\leq y\leq f(1)\;\wedge\;\forall
n[y\;\\#_{\mathcal{R}}\;y_{n}]\bigr{)}\rightarrow\exists x\in[0,1][f(x)=y]].$

###### Proof.

Let $q_{0},q_{1},q_{2}\ldots$ be an enumeration of all rational numbers $q$ in
$[0,1]$. For each $n$, define $y_{n}:=f(q_{n})$.

Let $y$ in $[0,1]$ be given such that $\forall
n[y\;\\#_{\mathcal{R}}\;y_{n}]$.

Define $x$ in $[0,1]$, step by step.

Define $x(0):=(0,1)$ and note: $f(0)<_{\mathcal{R}}y<_{\mathcal{R}}f(1)$.

Now let $n$ be given such that $x(n)$ is defined and
$f\bigl{(}x^{\prime}(n)\bigr{)}<_{\mathcal{R}}y<_{\mathcal{R}}f\bigl{(}x^{\prime\prime}(n)\bigr{)}$.

Consider $m:=\frac{x^{\prime}(n)+x^{\prime\prime}(n)}{2}$. If
$f(m)<_{\mathcal{R}}y$, define: $x(n+1):=(m,x^{\prime\prime}(n))$, and, if
$y<_{\mathcal{R}}f(m)$, define: $x(n+1):=(x^{\prime}(n),m)$. Then
$f\bigl{(}x^{\prime}(n+1)\bigr{)}<_{\mathcal{R}}y<_{\mathcal{R}}f(\bigl{(}x^{\prime\prime}(n+1)\bigr{)}$.

This completes the definition of $x$.

Using the argument given in the last part of the proof of Lemma 7, one proves:
$f(x)=_{\mathcal{R}}y$. ∎

###  9.8. Perhaps, perhaps, perhaps,$\ldots$

Suppose we change the conclusion of the Intermediate Value Theorem into

$(\ast)$ $\exists x_{0}[f(x_{0})\;\\#_{\mathcal{R}}\;y\rightarrow\exists
x_{1}[f(x_{1})=_{\mathcal{R}}y]]$,

Perhaps141414A similar use of the expression ‘Perhaps’ is made in Section 20.,
$f$ assumes the value $y$.

One may think of $(\ast)$ as follows. You are offered $x_{0}$ where $f$ should
assume the value $y$. If you discover $x_{0}$ clearly does not work, you may
go back to the shop and ask for a better number and will be offered $x_{1}$
and $x_{1}$ certainly will work.

One may reconsider the two counterexamples given in Subsection 9.4, the
functions $f_{0}$ and $f_{1}$, in the light of this definition.

We have seen that the statement ‘$f_{0}$ assumes the value $\frac{1}{2}$’ is
reckless, but, if $f_{0}(\frac{1}{2})\;\\#_{\mathcal{R}}\;\frac{1}{2}$, then
$\rho_{1}\;\\#_{\mathcal{R}}\;0$ and: either $0<_{\mathcal{R}}\rho_{1}$ and
$f_{0}(\frac{1}{3}\cdot\frac{1}{1+2\cdot\rho_{1}})=\frac{1}{2}$, or
$\rho_{1}<_{\mathcal{R}}0$ and
$f_{0}(\frac{2}{3}-\frac{2\cdot\rho_{1}}{1-2\cdot\rho_{1}})=\frac{1}{2}$. We
thus see: perhaps, $f_{0}$ assumes the value $\frac{1}{2}$.

We also have seen that the statement ‘$f_{1}$ assumes the value
$\frac{1}{2}\cdot\rho_{2}$’ is reckless, but, if
$f_{1}(0)\;\\#_{\mathcal{R}}\;\frac{1}{2}\cdot\rho_{2}$, then
$\rho_{2}\;\\#_{\mathcal{R}}\;0_{\mathcal{R}}$ and
$\rho_{0}=_{\mathcal{R}}\rho_{1}$ and
$f_{1}(\frac{1}{2})=_{\mathcal{R}}\frac{1}{2}\cdot\rho_{2}$. We thus see:
perhaps, $f_{1}$ assumes the value $\frac{1}{2}\cdot\rho_{2}$.

The funny thing is that the operation Perhaps may be repeated. One may
consider the statement:

$\exists x_{0}[f(x_{0})\;\\#_{\mathcal{R}}\;y\rightarrow\exists
x_{1}[f(x_{1})\\#_{\mathcal{R}}\;y\rightarrow\exists
x_{2}[f(x_{2})=_{\mathcal{R}}y]]]$,

Perhaps, perhaps, $f$ assumes the value $y$.

We give an example showing that this statement indeed may be weaker than the
previous one, with only one ‘perhaps’.

Another example.

Consider $\rho_{1}=(-\frac{1}{2})^{k_{99}}$ but also
$\rho_{3}:=(-\frac{1}{2})^{k_{88}}$.
Define a function $f_{2}$ from $[0,1]$ to $\mathcal{R}$ such that

  1. (i)

$f_{2}(0)=0$ and $f_{2}(1)=1$ and
$f_{2}(\frac{1}{5})=f_{2}(\frac{2}{5})=\frac{1}{2}+\rho_{1}$, and
$f_{2}(\frac{3}{5})=f_{2}(\frac{4}{5})=\frac{1}{2}+\rho_{3}$, and,

  2. (ii)

for each $i\leq 4$, $f_{2}$ is linear on the interval
$[\frac{i}{5},\frac{i+1}{5}]$.

Let us first observe: if $f_{2}(\frac{1}{5})\;\\#_{\mathcal{R}}\;\frac{1}{2}$
and also $f_{2}(\frac{3}{5})\;\\#_{\mathcal{R}}\;\frac{1}{2}$, then
$\rho_{1}\;\\#_{\mathcal{R}}\;0$ and $\rho_{3}\;\\#_{\mathcal{R}}\;0$ and
$\exists x[f(x)=_{\mathcal{R}}\frac{1}{2}]$. Conclude:

> Perhaps, perhaps, $f_{2}$ assumes the value $\frac{1}{2}$.

Now assume: Perhaps, $f_{2}$ assumes the value $\frac{1}{2}$.
Find $x_{0}$ such that, if $f_{2}(x_{0})\;\\#_{\mathcal{R}}\;\frac{1}{2}$,
then $\exists x_{1}[f_{2}(x_{1})=_{\mathcal{R}}\frac{1}{2}]$.

Distinguish two cases.

Case (1). $x_{0}<_{\mathcal{R}}\frac{8}{15}$. Assume:
$\rho_{1}<_{\mathcal{R}}0$.
Define $x_{1}:=\sup(x_{0},\frac{2}{5})$ and note
$f(x_{1})=f(\frac{2}{5})+(x_{1}-\frac{2}{5})\cdot 5(\rho_{3}-\rho_{1})=\\\
\frac{1}{2}+\rho_{1}+(x_{1}-\frac{2}{5})\cdot
5(\rho_{3}-\rho_{1})\leq_{\mathcal{R}}\frac{1}{2}+\rho_{1}+(\frac{8}{15}-\frac{2}{5})\cdot
5(\rho_{3}-\rho_{1})=\\\ \frac{1}{2}+\frac{1}{3}\rho_{1}+\frac{2}{3}\rho_{3}$.
Conclude: $f(x_{0})\leq_{\mathcal{R}}f(x_{1})<_{\mathcal{R}}\frac{1}{2}$ or
$0<_{\mathcal{R}}\rho_{3}$.

In both cases, one may conclude:
$\exists x\in[0,1][f_{2}(x)=_{\mathcal{R}}\frac{1}{2}]$ and:
$0\leq_{\mathcal{R}}\rho_{3}\;\vee\;\rho_{3}\leq_{\mathcal{R}}0$.

We thus see: if $\rho_{1}<_{\mathcal{R}}0$, then
$0\leq_{\mathcal{R}}\rho_{3}\;\vee\;\rho_{3}\leq_{\mathcal{R}}0$, i.e.
if $\exists n[2n+1=k_{99}]$, then $\forall n[2n+1\neq k_{88}]\;\vee\;\forall
n[2n\neq k_{88}]$,
a reckless or hardy conclusion.

Case (2). $\frac{7}{15}<_{\mathcal{R}}x_{0}$. By a similar argumnet, we obtain
the result:
if $0<_{\mathcal{R}}\rho_{3}$, then
$0\leq_{\mathcal{R}}\rho_{1}\;\vee\;\rho_{1}\leq_{\mathcal{R}}0$, i.e.
if $\exists n[2n=k_{88}]$, then $\forall n[2n+1\neq k_{99}]\;\vee\;\forall
n[2n\neq k_{99}]$,
a reckless or hardy conclusion.

We thus see that the statement

> ‘Perhaps, $f_{2}$ assumes the value $\frac{1}{2}$’

has reckless consequences.

One now may define:

$Perhaps_{0}(f,y)$ if and only if $\exists x[f(x)=y]$

and, for each $n$,

$Perhaps_{n+1}(f,y)$ if and only if $\exists
x[f(x)\;\\#_{\mathcal{R}}\;y\rightarrow Perhaps_{n}(f,y)]$

and also

$Perhaps_{\omega}(f,y)$ if and only if $\exists n[Perhaps_{n}(f,y)]$,

and

$Perhaps_{\omega+1}(f,y)$ if and only if $\exists
x[f(x)\;\\#_{\mathcal{R}}\;y\rightarrow Perhaps_{\omega}(f,y)]$.

and prove that in general, alle these statements have different meanings.
Going this path further, increasing the number of ‘perhapses’ further into the
transfinite, one finds uncountably many intuitionistically different versions
of the notion: ‘$\exists x[f(x)=_{\mathcal{R}}y]$’, see [56].

##  10\. A function from $\mathcal{R}$ to $\mathcal{R}$ is nowhere positively
discontinuous

In the next three Sections we study the intuitionistic claim that every real
function is continuous. The first theorem, Theorem 15, is weak and negative.

###  10.1. No positive discontinuity

######  Definition 8.

Let $f$ be a function from $\mathcal{X}\subseteq\mathcal{R}$ to $\mathcal{R}$
and let $x$ in $\mathcal{X}$ be given.

$f$ is _positively discontinuous_ at $x$ if and only if
$\exists p\forall m\exists
y\in\mathcal{X}[|y-x|<\frac{1}{2^{m}}\;\wedge\;|f(y)-f(x)|\geq\frac{1}{2^{p}}].$

######  Theorem 11.

151515Cf. [17, Theorem 1].

Let $f$ be a function from $\mathcal{X}\subseteq\mathcal{R}$ to $\mathcal{R}$.
Assume there exists $x$ in $\mathcal{X}$ such that $f$ is positively
discontinuous at $x$. Then there exists $z$ in $\mathcal{R}$ such that we can
_not_ calculate $f(z)$, so $z$ can _not_ belong to $\mathcal{X}$.

###### Proof.

Let $\mathcal{X},f,x$ satisfy the conditions of the theorem.

Without loss of generality, we may assume: $x=0=f(0)$.

Find $p$ such that $\forall m\exists
y\in\mathcal{X}[|y|<\frac{1}{2^{m}}\;\wedge\;|f(y)|>\frac{1}{2^{p}}].$

Find an infinite sequence $y_{0},y_{1},\ldots$ of reals such that
$\forall m[|y_{m}|<\frac{1}{2^{m}}\;\wedge\;|f(y_{m})|>\frac{1}{2^{p}}].$

We give two arguments establishing the conclusion of the theorem.

First argument.

I start constructing a real number $z$ in an infinite sequence of steps,
defining successively $z(0),z(1),z(2),\ldots$.
I promise to take care that for each $n$, $z^{\prime}(n)\leq
z^{\prime}(n+1)\leq z^{\prime\prime}(n+1)\leq z^{\prime\prime}(n)$ and
$z^{\prime\prime}(n)-z^{\prime}(n)=\frac{1}{2^{n-1}}$. I am free, within these
bounds, to choose each $z(n)$ as I like it.

I have in mind to perhaps ‘freeze’ the free development of $z$, at some step
$n$, by making a decision that determines all values from that step $n$ on.

I define $z(0)=(-1,1)$ and do not freeze $z$ at step $0$. For each $n>0$, if
$z$ has not yet been frozen at one of the earlier steps, either I do not
freeze $z$ at this step and define $z(n)=(-\frac{1}{2^{n}},\frac{1}{2^{n}})$,
or I freeze $z$ by defining, for each $i$, $z(n+i)=y_{n-1}(q+i)$, where $q$ is
the least $k$ such that $-\frac{1}{2^{n-1}}<y^{\prime}_{n-1}(k)\leq
y^{\prime\prime}_{n-1}(k)<\frac{1}{2^{n-1}}$.

$z$ is a well-defined real number.

Note: if I never make use of my freedom to freeze $z$, then
$z=_{\mathcal{R}}0$ and $f(z)=_{\mathcal{R}}0$.

Note: if I do use this freedom at some step $n>0$, then
$z=_{\mathcal{R}}y_{n-1}$ and
$|f(z)|=_{\mathcal{R}}|f(y_{n-1})|>_{\mathcal{R}}\frac{1}{2^{p}}$.

But I am free and do not know myself if I ever will make use of the
possibility to freeze $z$ or not.

I thus am unable to find an approximation of $f(z)$ smaller than
$\frac{1}{2^{p}}$.

We must conclude: $f$ is not defined at the argument $z$ and $z$ does not
belong to the domain $\mathcal{X}$ of $f$.

Second argument.

Define $z$ such that, for each $n$,
if $n<k_{99}$, then $z(n)=(-\frac{1}{2^{n}},\frac{1}{2^{n}})$, and, if
$k_{99}\leq n$, then $z(n)=y_{k_{99}}(q+n)$,
where $q$ is the least $k$ such that
$-\frac{1}{2^{k_{99}}}<y^{\prime}_{k_{99}}(k)\leq
y^{\prime\prime}_{k_{99}}(k)<\frac{1}{2^{k_{99}}}$.

Note: if $\forall n[n<k_{99}]$, then
$f(z)=_{\mathcal{R}}f(0_{\mathcal{R}})=_{\mathcal{R}}0$, and,
if $\exists n[n=k_{99}]$, then
$|f(z)|=_{\mathcal{R}}|f(y_{k_{99}}|>_{\mathcal{R}}\frac{1}{2^{p}}$.

Assume we may calculate $f(z)$. By finding an approximation of $f(z)$ smaller
than $\frac{1}{2^{p}}$ we will be able to decide: $f(z)\;\\#_{\mathcal{R}}\;0$
or $|f(z)|<_{\mathcal{R}}\frac{1}{2^{p}}$.

Case (a). $f(z)\;\\#_{\mathcal{R}}\;0$, and, therefore: $\neg\forall
n[n<k_{99}]$.

Case (b). $|f(z)|<\frac{1}{2^{p}}$, and, therefore: $\forall n[n<k_{99}]$.

Conclude: $\neg\forall n[n<k_{99}]\;\vee\;\forall n[n<k_{99}]$.

This is a reckless conclusion.

We must admit that, at this point of time, $f$ is not defined at $z$ and $z$
does not belong to the domain $\mathcal{X}$ of $f$. ∎

Clearly, a function from $\mathcal{X}\subseteq\mathcal{R}$ with a positive
discontinuity can not be calculated at every point of $\mathcal{R}$. In
Brouwer’s terminology: such a function is not a full function.

##  11\. The meaning of ‘not’

###  11.1. A weak and a strong interpretation

May we conclude, from Theorem 15:

> A function $f$ from $\mathcal{R}$ to $\mathcal{R}$ is _not_ positively
> discontinuous at any point $x$ in $\mathcal{R}$?

We have to be careful. There is some ambiguity in the use of the word ‘not’.
When saying:

‘$\textit{not:}\;(\exists n[n=k_{99}]\;\vee\;\forall n[n<k_{99}])$’

we mean no more than:

‘As yet, we have no proof of ‘$\exists n[n=k_{99}\;\vee\;\forall
n[n<k_{99}]$’.

Most of the time, however, we take a proposition ‘not $P$’, $`\neg
P^{\prime}$, in the stronger sense indicated in Subsection 8.5: ‘Assuming $P$,
one is led to a contradiction’. This strong interpretation of ‘not’ is the
canonical one. It follows from reading ‘$not$-$P$’ as ‘$P\rightarrow 0=1$’ and
interpreting the implication ‘$P\rightarrow Q$’ as: ‘Assuming $P$, one may
prove $Q$’.

Following this strong and canonical interpretation, one may prove, for any
proposition $P$,

$\neg\neg(P\vee\neg P)$,

as follows: Assume: $\neg(P\vee\neg P)$, i.e. $P\vee\neg P$ leads to a
contradiction. Then both $P$ and $\neg P$ will lead to a contradiction. We
thus see: $\neg P$ and: $\neg P$ leads to a contradiction. We therefore have a
contradiction.

Conclude: $\neg(P\vee\neg P)$ leads to a contradiction, i.e.
$\neg\neg(P\vee\neg P)$.

In particular, we find:

$\neg\neg(\exists n[n=k_{99}]\;\vee\;\forall n[n<k_{99}])$.

###  11.2. Some useful remarks

Defining $Q:=\exists n[n=k_{99}]\;\vee\;\neg\exists n[n=k_{99}]$, we see that
there are propositions $Q$ such that $\neg\neg Q$ is true but $Q$ itself is
reckless or hardy. On the other hand, for every proposition $Q$, if $Q$, that
is: $Q$ has a proof, then $\neg Q$, (the statement that $Q$ leads to a
contradiction), leads indeed to a contradiction, i.e. if $Q$, then $\neg\neg
Q$.

Later in this paper, we need the following law of contraposition:
if $P\rightarrow Q$, then $\neg Q\rightarrow\neg P$, and its consequence: if
$P\rightarrow Q$, then $\neg\neg P\rightarrow\neg\neg Q$.

This law is easily seen to be valid for the proof-theoretical interpretation,

Using it, one sees that, as $Q\rightarrow\neg\neg Q$ is always true, also
$\neg\neg\neg Q\rightarrow\neg Q$ is always true. (The scheme $\neg\neg\neg
Q\rightarrow Q$ was discovered by Brouwer and may be called Brouwer’s first
law of logic).

Also note:
if $(P\;\vee\neg P)\rightarrow\neg Q$, then, as $\neg\neg(P\;\vee\;\neg P)$,
one has: $\neg\neg\neg Q$, and, therefore: $\neg Q$.

This fact may be useful in practice: if it is our aim to prove a negative
statement $\neg Q$ it does no harm to make an extra ssumption $P\vee\neg P$.

One should keep in mind: $\neg P$ means: $P$ is reducible to absurdity.
Therefore, the constructive mathematician has nothing to criticize if someone
proves $\neg P$ by reducing $P$ to absurdity. If one does so, one does what
one has to do.161616Hardy’s finest weapon is not bad in itself but can only be
used for proving negative statements. Constructively, negative statements are
not so useful. There are better statements and finer weapons. She feels
unhappy, however, if one proves $P$ itself by reducing $\neg P$ to absurdity.
The conclusion of the latter procedure is $\neg\neg P$ only, a statement that,
most of the time, is weaker than $P$.

###  11.3. More fugitive numbers

The following Definition extends Definition 4.

######  Definition 9 (The fugitive numbers $k_{\alpha}$).

Let an infinite sequence
$\alpha=\alpha(0),\alpha(1),\alpha(2),\ldots$ of natural numbers be given. For
each $n$ we define171717Note that we do not define a natural number
$k_{\alpha}$ bot only the meaning of an expression like ‘$k_{\alpha}\leq n$’.
:

$k_{\alpha}\leq n$ if and only if $\exists j\leq n[\alpha(j)\neq 0]$, and:

$n<k_{\alpha}$ if and only if $\forall j\leq n[\alpha(j)=0]$, and:

$n=k_{\alpha}$ if and only if $k_{\alpha}\leq n$ and $\forall
j<n[j<k_{\alpha}]$, i.e.
$n$ is the least $j$ such that $\alpha(j)\neq 0$.

$\mathbf{LPO}$, the limited principle of omniscience181818This statement got
its name from the American analyst E. Bishop, who, fifty years after Brouwer,
founded his own school of constructive analysis, see [8, page 3]. The name
comes from calling the Principle of the Excluded Third $P\;\vee\;\neg P$ the
_Principle of Omniscience_ , a perhaps infelicitous decision, as the name
suggests mathematics is a matter of ‘knowing facts’., is the statement

$\forall\alpha[\exists n[k_{\alpha}\leq n]\;\vee\;\forall n[n<k_{\alpha}]].$

$\mathbf{WLPO}$, the weak limited principle of omniscience is the statement

$\forall\alpha[\neg\forall n[n<k_{\alpha}]\;\vee\;\forall n[n<k_{\alpha}]].$

Using the second argument in the proof of Theorem 15 one may see:
If a real function from $\mathcal{R}$ to $\mathcal{R}$ has a positive
discontinuity, then $\mathbf{WLPO}$.

For an informal constructive mathematician like Brouwer, $\mathbf{LPO}$, and
also
$\mathbf{WLPO}$, represent the absurd, the contradiction, a statement one
feels sure never to be able to prove. For her, the argument for Theorem 15
establishes, for every ‘full’ function $f$ from $\mathcal{R}$ to
$\mathcal{R}$,

$\neg$(there exists $x$ in $\mathcal{R}$ such that $f$ is positively
discontinuous at $x$).

In Section 12, we introduce Brouwer’s Continuity Principle, an axiomatic
assumption one perhaps finds plausible after having seen and accepted the
first argument in the proof of Theorem 15. Brouwer’s Continuity Principle
proves: $\neg\mathbf{WLPO}$, see Theorem 12.

##  12\. The Continuity Principle

Let $f$ be a (‘full’) function from $\mathcal{R}$ to $\mathcal{R}$. The
statement that there is no point where $f$ is positively discontinuous is,
constructively, a weak statement and not a very useful one. The positive
result that $f$ is continuous at every point is obtained from an axiomatic
assumption first used by Brouwer.

###  12.1. Understanding Brouwer’s Continuity Principle

We first have to agree upon some notation.

In the following definition, we use $k,n_{0},n_{1},\ldots,s,t,u,\ldots$ as
variables over the set $\mathbb{N}$.

######  Definition 10 (Coding finite sequences of natural numbers by natural
numbers).

Let $p:\mathbb{N}\rightarrow\mathbb{N}$ be the function enumerating the
primes: $p(0)=2,p(1)=3,p(2)=5,\ldots$.

For each $k$, for all $n_{0},n_{1},\ldots,n_{k-1}$, $\langle
n_{0},n_{1},\ldots,n_{k-1}\rangle:=p(k-1)\cdot\prod_{i<k}p(i)^{n_{i}}-1$.

We also define: $\langle\;\rangle:=0.$

For all $s$, for each $k$, for all $n_{0},n_{1},\ldots,n_{k-1}$, if $s=\langle
n_{0},n_{1},\ldots,n_{k-1}\rangle$, then $length(s)=k$ and, for all
$i<length(s)$, $s(i):=n_{i}$.

For all $k$, $\omega^{k}:=\\{s\mid length(s)=k\\}$.

For all $k,l$, for all $s$ in $\omega^{k}$, for all $t$ in $\omega^{l}$,
$s\ast t$ is the element of $\omega^{k+l}$ satisfying $\forall i<k[s\ast
t(i)=s(i)]$ and $\forall j<l[s\ast t(k+j)=t(j)]$.

For all $s,t$, $s\sqsubseteq t\leftrightarrow\exists u[s\ast u=t]$ and
$s\sqsubset t\leftrightarrow(s\sqsubseteq t\;\wedge\;s\neq t)$.

For all $s,t$, $s\perp t\leftrightarrow\neg(s\sqsubseteq t\;\vee\;t\sqsubseteq
s)$.

######  Definition 11.

$\mathcal{N}:=\omega^{\omega}$ is the set of all infinite sequences
$\alpha=\alpha(0),\alpha(1),\alpha(2),\ldots$ of non-negative integers. We use
$\alpha,\beta,\ldots\varphi,\psi,\ldots$ as variables over $\mathcal{N}$.

$\mathcal{N}$ is sometimes called _Baire space_.

For each $\alpha$, for each $m$,
$\overline{\alpha}m:=\langle\alpha(0),\alpha(1),\ldots,\alpha(m-1)\rangle.$

For all $s$, for all $\alpha$, $s\sqsubset\alpha\leftrightarrow\exists
n[\overline{\alpha}n=s]$ and
$s\perp\alpha\leftrightarrow\neg(s\sqsubset\alpha)$.

For each $n$, we let $\underline{n}$ be the infinite sequence with the
constant value $n$, that is, for all $i$, $\underline{n}(i)=n$.

######  Axiom 1 (Brouwer’s Continuity Principle, $\mathbf{BCP}$).

For every $R\subseteq\mathcal{N}\times\mathbb{N}$,

if $\forall\alpha\in\mathcal{N}\exists n[\alpha Rn]$, then
$\forall\alpha\in\mathcal{N}\exists m\exists
n\forall\beta\in\mathcal{N}[\overline{\alpha}m\sqsubset\beta\rightarrow\beta
Rn]$.

How may we convince each other that thia axiom is ‘reasonable’ and that we
should accept it as a rule for our common mathematical game?

We should ask what we mean by the ‘set’ $\mathcal{N}$ of all infinite
sequences of natural numbers. This ‘set’ is a kind of framework in which all
kinds of infinite sequences will grow, although only a very few of them have
been realized up to now.

Cantor’s suggestion that a set is the result of taking together its (earlier
constructed?) elements is a notion that does not make sense to us.

An infinite sequence $\alpha$ may be given by a finite description or an
algorithm that enables us to find, one by one, the successive values
$\alpha(0),\alpha(1),\ldots$ of $\alpha$. Brouwer calls such infinite
sequences lawlike sequences.

As we saw in the first argument in the proof of Theorem 15, there are also
infinite sequences $\alpha$ that are not governed by a law. The successive
values $\alpha(0),\alpha(1),\alpha(2),\ldots$ of $\alpha$ then are freely
chosen, step by step. At any given moment, only a finite initial part
$\bigl{(}\alpha(0),\alpha(1),\ldots,\alpha(n-1)\bigr{)}$ of $\alpha$ is known.
One may ask for further values, but, having received the answers, one still
only knows a finite initial part of $\alpha$, albeit a longer one.

There are intermediate possibilities. Having begun with choosing freely, step
by step, $\alpha(0),\alpha(1),\ldots\alpha(n-1)$ one may decide, to ‘freeze’
$\alpha$ and to determine the remaining values by means of some rule or
algorithm.

There is even a possibility I make $\alpha$ dependent on my future
mathematical experience, by saying, for instance, $\alpha(n)=0$ if at the
moments $0,1,\ldots,n$, I did not find a proof of the $abc$-conjecture, and
$\alpha(n)=1$, if I did.

If we think of the set $\mathcal{N}$ as a framework making room for lawlike
sequences as well as for free-choice-sequences and sequences that are of some
intermediate kind, we are thinking of, what Brouwer calls, the full continuum.

Now assume $R\subseteq\mathcal{N}\times\mathbb{N}$ is given such that
$\forall\alpha\exists n[\alpha Rn]$. Every infinite sequence $\alpha$, also a
lawlike sequence $\alpha$, may be thought of as being produced, step by step,
by a black box. At the moment we produce a number $n$ such that $\alpha Rn$,
only finitely many values of $\alpha$, say
$\alpha(0),\alpha(1),\ldots,\alpha(m-1)$, will have become known. Clearly, for
any infinite sequence such that $\beta(0)=\alpha(0)$,
$\beta(1)=\alpha(1),\ldots$ and $\beta(m-1)=\alpha(m-1)$, one may conclude:
$\beta Rn$.

Adopting Axiom 1 as a starting point for our further mathematical discourse,
we lay down a canonical meaning for expressions of the form
‘$\forall\alpha\exists n[\alpha Rn]$’. Earlier, we did so for expressions of
the form ‘infinite’, ‘uncountable’ and ‘or’.

######  Theorem 12.

$\mathbf{BCP}\Rightarrow\neg\mathbf{WLPO}$.

###### Proof.

Assume $\mathbf{WLPO}$ i.e. $\forall\alpha[\neg\forall
n[n<k_{\alpha}]\;\vee\;\forall n[n<k_{\alpha}]]$, i.e.
$\forall\alpha[\neg\forall n[\alpha(n)=0]\;\vee\;\forall n[\alpha(n)=0]]$.
Consider $\alpha=\underline{0}$ and, applying $\mathbf{BCP}$, find $m$ such
that
either
$\forall\beta[\overline{\underline{0}}m\sqsubset\beta\rightarrow\neg\forall
n[\beta(n)=0]]$ or
$\forall\beta[\overline{\underline{0}}m\sqsubset\beta\rightarrow\forall
n[\beta(n)=0]]$.
The first of these two statements is not true, consider:
$\beta=\underline{0}$, and the second one also fails, consider:
$\beta=\underline{\overline{0}}m\ast\underline{1}$.

We thus obtain a contradiction.∎

###  12.2. The (pointwise) continuity of functions from $\mathcal{R}$ to
$\mathcal{R}$

In the next Definition, we introduce a function $\alpha\mapsto u_{\alpha}$
associating to every $\alpha$ in $\mathcal{N}$ a real number $u_{\alpha}$.

######  Definition 12.

We let
$(r_{0}^{\prime},r_{0}^{\prime\prime}),\;(r_{1}^{\prime},r_{1}^{\prime\prime}),\;(r_{2}^{\prime},r_{2}^{\prime\prime}),\;\ldots$
be a fixed enumeration of all pairs of rationals.

We define a mapping associating to each $s\neq 0$ a pair
$(u_{s}^{\prime},u_{s}^{\prime\prime})$ of rationals, as follows.

For each $n$, _if_ $0<r_{n}^{\prime\prime}-r_{n}^{\prime}\leq 1$, then
$(u^{\prime}_{\langle n\rangle},u^{\prime\prime}_{\langle
n\rangle})=(r_{n}^{\prime},r_{n}^{\prime\prime})$, and,
_if not_ , then $(u^{\prime}_{\langle n\rangle},u^{\prime\prime}_{\langle
n\rangle})=(0,1)$.

For each $s\neq 0$, for each $n$, _if_
$u^{\prime}_{s}<r^{\prime}_{n}<r^{\prime\prime}_{n}<u^{\prime\prime}_{s}$ and
$0<r_{n}^{\prime\prime}-r_{n}^{\prime}\leq\frac{1}{2}(u^{\prime\prime}_{s}-u^{\prime}_{s})$,
then $(u^{\prime}_{s\ast\langle n\rangle},u^{\prime\prime}_{s\ast\langle
n\rangle})=(r_{n}^{\prime},r_{n}^{\prime\prime})$, and,
_if not_ , then $(u^{\prime}_{s\ast\langle
n\rangle},u^{\prime\prime}_{s\ast\langle
n\rangle})=(\frac{2}{3}u^{\prime}_{s}+\frac{1}{3}u^{\prime\prime}_{s},\frac{1}{3}u^{\prime}_{s}+\frac{2}{3}u^{\prime\prime}_{s})$.

For each $\alpha$ in $\mathcal{N}$ we let $u_{\alpha}$ be the infinite
sequence of pairs of rationals such that,
for all $n$,
$u_{\alpha}(n)=(u_{\overline{\alpha}(n+1)}^{\prime},u_{\overline{\alpha}(n+1)}^{\prime\prime})$.

######  Theorem 13.

191919See [48], [52, §2] and [65, §4].

  1. (i)

For every $\alpha$, $u_{\alpha}$ is a real number.

  2. (ii)

For every real number $x$, there exists $\alpha$ such that
$x=_{\mathcal{R}}u_{\alpha}$.

  3. (iii)

$\mathbf{BCP}\Rightarrow$ Every function from $\mathcal{R}$ to $\mathcal{R}$
is continuous at every point $x$.

###### Proof.

The proof of (i) and (ii) is left to the reader.

(iii) Let $f$ be a real function and let a real $x$ be given. We shall prove
that $f$ is continuous at $x$.

Let $p$ be given. We have to find $m$ such that, for every real $y$, if
$|y-x|<\frac{1}{2^{m}}$, then $|f(y)-f(x)|<\frac{1}{2^{p}}$.

Note: $\forall\alpha\exists
n[r^{\prime}_{n}<f(u_{\alpha})<r_{n}^{\prime\prime}]$ and find $\alpha$ such
that $x=_{\mathcal{R}}u_{\alpha}$.

Applying $\mathbf{BCP}$, find $q,n$ such that
$\forall\beta[\overline{\alpha}q\sqsubset\beta\rightarrow
r^{\prime}_{n}<f(u_{\beta})<r_{n}^{\prime\prime}]$.

Find $i,j$ such that $u_{\alpha}(n-1)=(r_{i}^{\prime},r_{i}^{\prime\prime})$
and $u_{\alpha}(n)=(r_{j}^{\prime},r_{j}^{\prime\prime})$.

Note:
$r_{i}^{\prime}<_{\mathbb{Q}}r_{j}^{\prime}<_{\mathbb{Q}}r_{j}^{\prime\prime}<_{\mathbb{Q}}r_{i}^{\prime\prime}$.

Find $m$ such that
$\frac{1}{2^{m}}<\min_{\mathbb{Q}}(r_{j}^{\prime}-_{\mathbb{Q}}r_{i}^{\prime},r_{i}^{\prime\prime}-_{\mathbb{Q}}r_{j}^{\prime\prime})$.

Note: for every real $y$, if $|y-x|<\frac{1}{2^{m}}$, then
$r_{i}^{\prime}<y<r_{i}^{\prime\prime}$ and there exists $\beta$ such that
$\overline{\alpha}n\sqsubset\beta$ and $y=_{\mathcal{R}}u_{\beta}$ and,
therefore: $r_{n}^{\prime}<f(u_{\beta})<r_{n}^{\prime\prime}$ and
$r_{n}^{\prime}<f(y)<r_{n}^{\prime\prime}$.

Conclude: for every real $y$, if $|y-x|<\frac{1}{2^{m}}$ then
$|f(y)-f(x)|<r_{n}^{\prime\prime}-r_{n}^{\prime}<\frac{1}{2^{p}}$. ∎

##  13\. The Fan Theorem

###  13.1. Proving the Fan Theorem

The intuitionistic mathematician holds not only that every function from
$[0,1]$ tot $\mathcal{R}$, like every function from $\mathcal{R}$ to
$\mathcal{R}$, see Theorem 19(iii) is continuous at every point, but also that
every function from $[0,1]$ to $\mathcal{R}$ is continuous uniformly on
$[0,1]$. In order to obtain this result, she first proves the Fan Theorem.

We need some definitions in order to formulate the Fan Theorem.

######  Definition 13.

Let $\mathcal{X}\subseteq\mathcal{N}$ and $B\subseteq\mathbb{N}$.

$B$ _is a bar in_ $\mathcal{X}$, notation: $Bar_{\mathcal{X}}(B)$, if and only
if: $\forall\alpha\in\mathcal{X}\exists s\in B[s\sqsubset\alpha]$.

$\mathcal{C}:=2^{\omega}:=\\{\alpha\mid\forall n[\alpha(n)<2]\\}$.

$\mathcal{C}$ is sometimes called _Cantor space_.

$Bin:=2^{<\omega}:=\\{s\mid\forall i<length(s)[s(i)<2]\\}$.

For each $n$, $Bin_{n}:=\\{s\in Bin\mid
length(s)=n\\}=\\{s\in\omega^{n}\mid\forall j<n[s(j)<2]\\}$.

######  Definition 14.

For each $\mathcal{X}\subseteq\mathcal{N}$, for each $s$, we define:
$\mathcal{X}\cap s:=\\{\alpha\in\mathcal{X}|s\sqsubset\alpha\\}.$

The Fan Theorem is the statement that every bar in $\mathcal{C}$ has a finite
subbar. Brouwer actually proved the more general but equivalent statement that
every bar in a so-called fan has a finite subbar. Here, $B\subseteq\mathbb{N}$
is called finite if and only if $\exists u\forall s[s\in
B\leftrightarrow\exists i<length(u)[s=u(i)]]$.

We avoid defining the notion of a fan. For understanding the name of the
Theorem, it suffices to know every fan is a subset of $\mathcal{N}$ and that
$\mathcal{C}$ is the prime example of a fan.

The proof of the Fan Theorem turns on a philosophical claim.

######  Theorem 14 (Brouwer’s Fan Theorem).

For every $B\subseteq\mathbb{N}$, if $Bar_{\mathcal{C}}(B)$, then there exists
$u$ such that $\forall i<length(u)[u(i)\in B]$ and
$\forall\alpha\in\mathcal{C}\exists i<length(u)[u(i)\sqsubset\alpha].$

###### Proof.

202020In [12] and [16], the Fan Theorem is obtained as a corollary of the ‘Bar
Theorem’, in this paper Theorem 19. We give an argument for the Fan Theorem
inspired by Brouwer’s proof of the Bar Theorem, like A. Heyting did in [36,
§3.4.2].

Let $B\subseteq\mathbb{N}$ be given such that $Bar_{\mathcal{C}}(B)$.

Define, for every $s$ in $2^{<\omega}$, $s$ is $B$-safe, or simply: safe, if
and only if $Bar_{\mathcal{C}\cap s}(B)$.

As $Bar_{\mathcal{C}}(B)$, $\langle\;\rangle$ is safe.

We now ask the probably somewhat surprising question: ‘How is it possible we
know this?’ and, after some reflection, we come forward with the claim: there
must be a canonical proof of the fact: ‘$\langle\;\rangle$ is safe.’

What do we mean by: ‘a canonical proof’?

The canonical proof is an arrangement of statements of the form: ‘$s$ is
safe’. The conclusion of the canonical proof is the statement:
‘$\langle\;\rangle$ is safe.’

The starting points of the canonical proof have the form:

$s\in 2^{<\omega}$ and $s\in B$.

Therefore: $s$ is safe.

There are only two kinds of reasoning steps: forward reasoning steps and
backward reasoning steps.

A forward reasoning step has the form:

$s\in 2^{<\omega}$, and $s\ast\langle 0\rangle$ is safe, and $s\ast\langle
1\rangle$ is safe.

Therefore: $s$ is safe.

A backward reasoning step either has the form:

$s\in 2^{<\omega}$ and $s$ is safe.

Therefore: $s\ast\langle 0\rangle$ is safe.

or it has the form

$s\in 2^{<\omega}$ and $s$ is safe.

Therefore: $s\ast\langle 1\rangle$ is safe.

Clearly, the canonical proof may be visualized as a finite tree, with the
statement ‘$\langle\;\rangle$ is safe’ at its bottom node and statements
‘$s\in B$’ at its top nodes. Each node that is not a top node has either one
or two upstairs neighbours.

One easily sees that all resoning steps are sound and that a canonical proof
of ‘$\langle\;\rangle$ is safe’ is indeed a proof of ‘$\langle\;\rangle$ is
safe’.

Our claim gives expression to the feeling that, if we know:
‘$Bar_{\mathcal{C}}(B)$’, this knowledge must be based upon an orderly
organization of elementary pieces of information of the form: ‘$s\in B$’.

Now, trusting our claim, let us take a canonical proof of: ‘$\langle\;\rangle$
is safe.’ We are going to use it in order to build another proof.

Define, for every $s$ in $2^{<\omega}$, $s$ is supersafe if and only if there
exists $u$ such that $\forall i<\mathit{length}(u)[u(i)\in B]$ and
$\forall\alpha\in\mathcal{C}\cap s\exists i<length(u)[u(i)\sqsubset\alpha]$.

Note that the conclusion we are after is: ‘$\langle\;\rangle$ is supersafe.’

Replace, in the canonical proof of ‘$\langle\;\rangle$ is safe’, every
statement ‘$s$ is safe’ by the statement ‘$s$ is supersafe’.

The result will be another valid proof.

Why?

First, the new starting points are sound: if $s\in 2^{<\omega}$ and $s\in B$,
define: $u:=\langle s\rangle$ and note: $u(0)\in B$ and
$\forall\alpha\in\mathcal{C}\cap s[u(0)\sqsubset\alpha]$.

Then, the new forward reasoning steps are sound.

For assume: $s\in 2^{<\omega}$ and both $s\ast\langle 0\rangle$ and
$s\ast\langle 1\rangle$ are supersafe.

Find $u_{0},u_{1}$ such that: for each $j<2$, $\forall
i\leq\mathit{length}(u_{j})[u_{j}(i)\in B]$ and
$\forall\alpha\in\mathcal{C}\cap s\ast\langle j\rangle\exists
i<\mathit{length}(u_{j})[u_{j}(i)\sqsubset\alpha].$

Define $u:=u_{0}\ast u_{1}$ and note
$\forall i<\mathit{length}(u)[u(i)\in B]$ and $\forall\alpha\in\mathcal{F}\cap
s\exists i<\mathit{length}(u)[u(i)\sqsubset\alpha],$
that is: $s$ is supersafe.

Also, the new backward reasoning steps are sound.

For assume: $s\in 2^{<\omega}$ and $s$ is supersafe.

Find $u$ such that

$\forall i<\mathit{length}(u)[u(i)\in B]$ and $\forall\alpha\in\mathcal{C}\cap
s\exists i<\mathit{length}(u)[u(i)\sqsubset\alpha].$

Note: for both $j<2$, $\mathcal{C}\cap s\ast\langle
j\rangle\subseteq\mathcal{C}\cap s$ and $s\ast\langle j\rangle$ is supersafe.

Conclude: our new proof is sound and its conclusion is true, i.e.
$\langle\;\rangle$ is supersafe. ∎

Generalizing the proof of Theorem 14 we obtain the following conclusion:

######  Theorem 15 (Bar Induction in $\mathcal{C}$).

Let $B\subseteq\mathbb{N}$ be a bar in $\mathcal{C}$.

  1. (i)

Assume $B\subseteq C\subseteq 2^{<\omega}$ and, for all $s$ in $2^{<\omega}$,
$s\in C$ if and only if $\forall j<2[s\ast\langle j\rangle\in C]$. Then
$\langle\;\rangle\in C$.

  2. (ii)

Assume $B\subseteq C\subseteq 2^{<\omega}$ and, for all $s$ in $2^{<\omega}$,
if $\forall j<2[s\ast\langle j\rangle\in C]$, then $s\in C$. Then
$\langle\;\rangle\in C$.

###### Proof.

(i) Define, for each $s$ in $2^{<\omega}$, $s$ is safe if and only if
$Bar_{\mathcal{C}\cap s}(B)$. In the canonical proof of: ‘$\langle\;\rangle$
is safe’, replace every statement ‘$s$ is safe’ by ‘$s\in C$’. The result will
be a proof of: ‘$\langle\;\rangle\in C$’.

(ii) Define $C^{\ast}:=\\{s\in 2^{<\omega}[\exists t\sqsubseteq s[t\in C]\\}$.

Note: for all $s$ in $2^{<\omega}$, if $s\in C^{\ast}$, then $\forall
j<2[s\ast\langle j\rangle\in C^{\ast}]$.

Now assume: $s\in 2^{<\omega}$ and $\forall j<2[s\ast\langle j\rangle\in
C^{\ast}]$. We may distinguish two cases.

Case 1. $\forall j<2[s\ast\langle j\rangle\in C]$. Then $s\in C\subseteq
C^{\ast}$.

Case 2. $\exists t\sqsubseteq s[t\in C]$. Then $s\in C^{\ast}$.

We thus see: for all $s$ in $2^{<\omega}$, $s\in C^{\ast}$ if and only if
$\forall j<2[\sigma(s\ast\langle j\rangle\in C^{\ast}]$.

Applying (i), we conclude: $\langle\;\rangle\in C^{\ast}$, and:
$\langle\;\rangle\in C$. ∎

Theorem 15(ii) shows that, in the canonical proof of $Bar_{\mathcal{C}}(B)$,
introduced in the proof of Theorem 14, the backward steps might have been left
out. They may not be left out in the canonical proof of the Bar Theorem, the
infinitary analog of the Fan Theorem, see Subsection 15.2.

###  13.2. Every function from $[0,1]$ to $\mathcal{R}$ is uniformly
continuous

Brouwer’s Continuity Principle implies that every function from $[0,1]$ to
$\mathcal{R}$, like every function from $\mathcal{R}$ to $\mathcal{R}$, see
Theorem 19(iii), is continuous at every point. Using the Fan Theorem, we now
prove that every function from $[0,1]$ to $\mathcal{R}$ is even continuous
uniformly on $[0,1]$. This is historically the first application of the Fan
Theorem, see [12].

In the next Definition, we introduce a function $\alpha\mapsto c_{\alpha}$
associating to every $\alpha$ in $\mathcal{C}$ a real number $c_{\alpha}$ in
$[0,1]$.

######  Definition 15.

We define a mapping associating to every $s$ in $2^{<\omega}$ a pair
$(a_{s},b_{s})$ of rationals such that
$(a_{\langle\;\rangle},b_{\langle\;\rangle})=(0,1)$ and for each $s$ in
$2^{<\omega}$,
$(a_{s\ast\langle 0\rangle},b_{s\ast\langle
0\rangle})=(a_{s},\frac{1}{3}a_{s}+\frac{2}{3}b_{s})$ and $(a_{s\ast\langle
1\rangle},b_{s\ast\langle
1\rangle})=(\frac{2}{3}a_{s}+\frac{1}{3}b_{s},b_{s})$.

For each $\alpha$ in $\mathcal{C}$ we let $c_{\alpha}$ be the real $x$ such
that, for each $n$, $x(n)=(a_{\overline{\alpha}n},b_{\overline{\alpha}n})$.

######  Theorem 16 (Uniform-Continuity Theorem).

Every function $f$ from $[0,1]$ to $\mathcal{R}$ is continuous _uniformly on
$[0,1]$_, i.e.

$\forall p\in\mathbb{N}\exists m\in\mathbb{N}\forall x\in[0,1]\forall
y\in[0,1][|x-y|<\frac{1}{2^{m}}\rightarrow|f(x)-f(y|<\frac{1}{2^{p}}].$

###### Proof.

Let $f$ be a function from $[0,1]$ to $\mathcal{R}$ and let $p$ be given. We
want to find $m$ such that $\forall x\in[0,1]\forall
y\in[0,1][|x-y|<\frac{1}{2^{m}}\rightarrow|f(x)-f(y|<\frac{1}{2^{p}}].$

Let $B$ be the set of all $s$ in $2^{<\omega}$ such that, for all $x,y$ in
$[a_{s},b_{s}]$, $|f(x)-f(y)|<\frac{1}{2^{p}}$.

We first prove that $B$ is a bar in $\mathcal{C}$, i.e.
$Bar_{\mathcal{C}}(B)$.

Let $\alpha$ in $\mathcal{C}$ be given. As $f$ is continuous at $c_{\alpha}$,
see Theorem 19(iii), find $m$ such that $\forall
y\in[0,1][|c_{\alpha}-y|<\frac{1}{2^{m}}\rightarrow|f(c_{\alpha})-f(y|<\frac{1}{2^{p+1}}]$.
Find $n$ such that
$b_{\overline{\alpha}n}-a_{\overline{\alpha}n}<\frac{1}{2^{m}}$ and note:
$\overline{\alpha}n\in B$.

We thus see that every $\alpha$ in $\mathcal{C}$ has an initial part in $B$.

Now let $C$ be the set of all $s$ in $2^{<\omega}$ such that, for some $m$,
for all $x,y$ in $[a_{s},b_{s}]$, if $|x-y|<\frac{1}{2^{m}}$, then
$|f(x)-f(y)|<\frac{1}{2^{p}}$.

Note: $B\subseteq C$.

Let $s$ in $2^{<\omega}$ be given such that $\forall i<2[s\ast\langle
i\rangle\in C]$. We are going to prove: $s\in C$.

First find $m_{0}$ such that, for all $x,y$ in $(a_{s\ast\langle
0\rangle},b_{s\ast\langle
0\rangle})=(a_{s},\frac{1}{3}a_{s}+\frac{2}{3}b_{s})$, if
$|x-y|<\frac{1}{2^{m_{0}}}$, then $|f(x)-f(y)|<\frac{1}{2^{p}}$. Then find
$m_{1}$ such that, for all $x,y$ in $(a_{s\ast\langle
1\rangle},b_{s\ast\langle
1\rangle})=(\frac{2}{3}a_{s}+\frac{1}{3}b_{s},b_{s})$, if
$|x-y|<\frac{1}{2^{m_{1}}}$, then $|f(x)-f(y)|<\frac{1}{2^{p}}$.

Now find $n:=length(s)$.

Note: $b_{s}-a_{s}=(\frac{2}{3})^{n}$, and, for all $x,y$ in $[a_{s},b_{s}]$,
if $|x-y|<\frac{1}{3}(\frac{2}{3})^{n}$, then either $x,y$ both are in
$[a_{s},\frac{1}{3}a_{s}+\frac{2}{3}b_{s}]$ or $x,y$ both are in
$[\frac{2}{3}a_{s}+\frac{1}{3}b_{s},b_{s}]$.

Find $m$ such that $m\geq m_{0}$ and $m\geq m_{1}$ and
$\frac{1}{2^{m}}<\frac{1}{3}(\frac{2}{3})^{n}$ and note: for all $x,y$ in
$[a_{s},b_{s}]$, if $|x-y|<\frac{1}{2^{m}}$, then
$|f(x)-f(y)|<\frac{1}{2^{p}}$. We thus see: $s\in C$.

Clearly, for all $s$ in $Bin$, if $\forall i<2[s\ast\langle i\rangle\in C]$,
then $s\in C$.

Using Theorem 15(ii), conclude: $\langle\;\rangle\in C$, that is:

$\exists m\forall x\in[0,1]\forall
y\in[0,1][|x-y|<\frac{1}{2^{m}}\rightarrow|f(x)-f(y)|<\frac{1}{2^{n}}].$ ∎

###  13.3. The failure of the Fan Theorem in computable analysis

In the next Theorem, we use some notations introduced in Subsection 8.4.

######  Theorem 17 (Kleene’s Alternative212121Kleene discovered this theorem
in 1950, see [39] and [41, Lemma 9.8].).

There exists $B^{\ast}\subseteq\mathbb{N}$ such that

  1. (i)

Every _computable_ $\alpha$ in $\mathcal{C}$ has an initial part in $B$, i.e.
$\exists s\in B^{\ast}[s\sqsubset\alpha]$.

  2. (ii)

Every finite subset of $B$ positively fails to be a bar in the set
$\\{\alpha\in\mathcal{C}\mid\alpha\;is\;computable\\}$, i.e.
for all $u,p$, if $length(u)=p>0$ and $\forall i<p[u(i)\in B^{\ast}]$,
then there exists a computable $\alpha$ in $\mathcal{C}$ such that $\forall
i<p[u(i)\perp\alpha]$.

  3. (iii)

$B^{\ast}$ is an algorithmically decidable subset of $\mathbb{N}$.

###### Proof.

First, let $B$ be the set of all $s$ in $Bin$ such that, for some $e$,
$length(s)=e+1$ and $\forall i\leq e\exists z[T(e,i,z)\;\wedge\;U(z)=s(i)].$

$\langle\;\rangle\notin B$ and, for every $e$, there is at most one $s$ in $B$
such that $length(s)=e+1$.

Let $\alpha$ be a computable element of $\mathcal{C}$. Find $e$ such that
$\alpha=\varphi_{e}$.
Note: $\overline{\alpha}(e+1)=\overline{\varphi_{e}}(e+1)\in B$.

Let $u,p$ be given such that $length(u)=p>0$ and $\forall n<p[u(n)\in B]$.
We may assume:
$0<length\bigl{(}u(0)\bigr{)}<length\bigl{(}u(1)\bigr{)}<\ldots<length\bigl{(}u(p-1)\bigr{)}$
and, therefore, $\forall n<p[\mathit{length}\bigl{(}u(n)\bigr{)}>n]$. Define
$\alpha$ such that, for each $n<p$, $\alpha(n)=1-\bigl{(}u(n)\bigr{)}(n)$,
and, for each $n\geq p$, $\alpha(n)=0$. Note: $\alpha$ is computable and
$\forall n<p[u(n)\perp\alpha]$.

Unfortunately, $B$ is not an algorithmically decidable subset of $\mathbb{N}$.

We therefore introduce another subset of $\mathbb{N}$.

Let $B^{\ast}$ be the set of all $s$ in $Bin$ such that, for some
$e<\mathit{length}(s)$,
$\forall i\leq e\exists z<\mathit{length}(s)[T(e,i,z)\;\wedge\;U(j)=s(i)]$,
and, therefore, $\overline{s}(e+1)\in B$.

Note that $B^{\ast}$ is an algorithmically decidable subset of $\mathbb{N}$.

Let $\alpha$ be a computable element of $\mathcal{C}$. Find $e$ such that
$\alpha=\varphi_{e}$. Find $n>e$ such that $\forall i\leq e\exists
z<n[T(e,i,z)\;\wedge\;U(z)=s(i)]$ and conclude: $\overline{\alpha}n\in
B^{\ast}$.

We thus see that every computable $\alpha$ in $\mathcal{C}$ has an initial
part in $B^{\ast}$.

Let $u,p$ be given such that $length(u)=p>0$ and $\forall n<p[u(n)\in
B^{\ast}]$. Find $v$ such that $length(v)=p$ and $\forall n<p[v(n)\sqsubseteq
u(n)\;\wedge\;v(n)\in B]$. Find a computable $\alpha$ in $\mathcal{C}$ such
that $\forall n<p[v(n)\perp\alpha]$ and conclude $\forall
n<p[u(n)\perp\alpha]$.

We thus see that every finite subset of $B^{\ast}$ positively fails to be a
bar in
$\\{\alpha\in\mathcal{C}\mid\alpha\;is\;computable\\}$. ∎

The subject of computable analysis starts from the assumption that every
$\alpha$ in $\mathcal{N}$ is given by an algorithm, i.e., if one uses Church’s
Thesis, by a Turing-algorithm. One may study this subject from an
intuitionistic point of view. As appears from Theorem 17, computable analysis
is dramatically different from intuitionistic analysis. For instance, there
exists a real function from $[0,1]$ to $\mathcal{R}$ that is everywhere
continuous but positively unbounded. Many more such results may be found in
[60].

##  14\. The Determinacy Theorem as an equivalent of the Fan Theorem

The Uniform-Continuity Theorem, Theorem 16, is the first application of the
Fan Theorem, and may be called the goal for which it was devised. In this
Section we want to introduce to the reader to a second and more recent
application, an application in the theory of games.

In the first two Subsections we consider two kinds of two-move-games for
Players $I,II$ and define when such games are constructively determinate from
the viewpoint of Player $I$. Games from the first Subsection may fail to have
this property but we will see that the Fan Theorem proves that the games from
the second Subsection always have it. In the third Subsection we prove that,
conversely, this result implies an important case of the Fan Theorem. In the
fourth Subsection we introduce the intuitionistic Determinacy Theorem.

###  14.1. Games in $2\times\omega$

For every $C\subseteq 2\times\omega$, we introduce a game
$\mathcal{G}_{2\times\omega}(C)$.
There are two players, Player $I$ and Player $II$. Every play goes a follows.
Player $I$ chooses $i$ in $\\{0,1\\}$, thereafter Player $II$ chooses $n$ in
$\omega$ and the play is finished. Player $I$ wins the play if and only if
$\langle i,n\rangle\in C$. Player $II$ tries to prevent that Player $I$ wins
the play.
Clearly, Player $I$ has a winning first move if and only if $\exists i\forall
n[\langle i,n\rangle\in C]$. A strategy for Player $II$, on the other hand, is
a pair of numbers $\langle p_{0},p_{1}\rangle$, and the strategy is winning if
$\forall i<2[\langle i,p_{i}\rangle\notin C]$.

The game $\mathcal{G}_{2\times\omega}(C)$ is called determinate if and only if
either Player $I$ has a winning first move or Player $II$ has a winning
strategy. As one may conjecture, it may happen that this decision can not be
taken in a constructive way. We will see this in a moment.

We now define: the game $\mathcal{G}_{2\times\omega}(C)$ is determinate from
the viewpoint of Player $I$ if and only if:

> If Player $II$ does not have a winning strategy in the constructively strong
> sense: $\forall p_{0}\forall p_{1}[\langle 0,p_{0}\rangle\in
> C\;\vee\;\langle 1,p_{1}\rangle\in C]$, then Player $I$ has a winning first
> move, i.e. $\exists i<2\forall n[\langle i,n\rangle\in C]$

and ask ourselves the question: is the game $\mathcal{G}_{\omega\times 2}(C)$
always determinate from the viewpoint of Player $I$?

The following example shows that, sometimes, it is not.
Define $C:=\\{\langle i,n\rangle\mid k_{99}\leq n\rightarrow\exists
l[k_{99}=2l+i]\\}$.
Let $p_{0},p_{1}$ be given. If $k_{99}\leq p_{0}$, one may find $i<2$ and $l$
such that $k_{99}=2l+i$ and $\langle i,p_{i}\rangle\in C$. If $p_{0}<k_{99}$,
then $\langle 0,p_{0}\rangle\in C$. We thus see Player $I$ has an answer to
any given strategy of Player $II$.
On the other hand, if Player $I$ has a winning first move, then $\exists
i<2\forall n[\langle i,n\rangle\in C]$ and $\exists i<2[\exists
j[j=k_{99}]\rightarrow\exists n[2n+i=k_{99}]]$, i.e. $\neg\exists
n[2n=k_{99}]\;\vee\;\neg\exists n[2n+1=k_{99}]$, a reckless or hardy
statement.

Note that the statement: ‘the game $\mathcal{G}_{2\times\omega}(C)$ is
determinate’ is also reckless, as, for every $C\subseteq 2\times\omega$, if
$\mathcal{G}_{2\times\omega}(C)$ is determinate, then
$\mathcal{G}_{2\times\omega}(C)$ is determinate from the viewpoint of Player
$II$.

###  14.2. Games in $\omega\times 2$

222222See [49, §4].

For every $C\subseteq\omega\times 2$, we introduce a game
$\mathcal{G}_{\omega\times 2}(C)$.
There are again two players, Player $I$ and Player $II$. Every play goes a
follows. Player $I$ chooses $n$ in $\omega$, thereafter Player $II$ chooses
$i$ in $\\{0,1\\}$ and the play is finished. Player $I$ wins the play if and
only if $\langle n,i\rangle\in C$. Player $II$ tries to prevent that Player
$I$ wins the play. Clearly, Player $I$ has a winning first move if and only if
$\exists n\forall i<2[\langle n,i\rangle\in C]$. A strategy for Player $II$ is
an element $\tau$ of $\mathcal{C}$ and the strategy $\tau$ is winning if and
only if $\forall n[\langle n,\tau(n)\rangle\notin C]$.

The game $\mathcal{G}_{\omega\times 2}(C)$ is called determinate if and only
if either Player $I$ has a winning first move or Player $II$ has a winning
strategy.

Considering the example $C:=\\{\langle n,i\rangle\in\omega\times 2\mid
n=k_{99}]$, we see that it may happen that the statement:
‘$\mathcal{G}_{\omega\times 2}(C)$ is determinate’ is a reckless one.

We now define: the game $\mathcal{G}_{\omega\times 2}(C)$ is determinate from
the viewpoint of Player $I$ if and only if

> If Player $II$ does not have a winning strategy in the strong sense:
> $\forall\tau\in\mathcal{C}\exists n[\langle n,\tau(n)\rangle\in C]$, then
> Player $I$ has a winning first move, i.e. $\exists n\forall i<2[\langle
> n,i\rangle\in C]$.

The Fan Theorem proves that, for every $C\subseteq\omega\times 2$, the game
$\mathcal{G}_{\omega\times 2}(C)$ is determinate from the viewpoint of Player
$I$.

For assume $\forall\tau\in\mathcal{C}\exists n[\langle n,\tau(n)\rangle\in
C]$.
Define $B:=\bigcup_{m}\\{t\in Bin_{m}\mid\exists n<m)[\langle n,t(n)\rangle\in
C]\\}$ and note: $B$ is a bar in $\mathcal{C}$. Applying the Fan Theorem, find
$u$ such that $\forall i<length(u)[u(i)\in B]$ and
$\forall\tau\in\mathcal{C}\exists i<length(u)[u(i)\sqsubset\tau]$. Find $m$
such that $\forall i<m[length(u(i))<m]$ and conclude: $\forall t\in
Bin_{m}\exists n<m[\langle n,t(n)\rangle\in C]$.
We now prove, by backwards induction:
for each $j\leq m$, either $\forall t\in Bin_{j}\exists n<j[\langle
n,t(n)\rangle\in C]$ or $\exists n\forall i<2[\langle n,i\rangle\in C]$.
This clearly holds if $j=m$.
Now assume $j+1\leq m$ and $\forall t\in Bin_{j+1}\exists n<j+1[\langle
n,t(n)\rangle\in C]$. For every $t$ in $Bin_{j}$, one may consider
$t\ast\langle 0\rangle$ and conclude: $\exists n<j[\langle n,t(n)\rangle\in
C]$ or $\langle j,0\rangle\in C$. Therefore: either $\langle j,0\rangle\in C$
or $\forall t\in Bin_{j}\exists n<j[\langle n,t(n)\rangle\in C]$. For similar
reasons, either $\langle j,1\rangle\in C$ or $\forall t\in Bin_{j}\exists
n<j[\langle n,t(n)\rangle\in C]$. Conclude: either: $\forall i<2[\langle
j,i\rangle\in C]$ and $\exists n\forall i<2[\langle n,i\rangle\in C]$ or:
$\forall t\in Bin_{j}\exists n<j[\langle n,t(n)\rangle\in C]$. Repeating this
step $m$ times we find the conclusion: $\exists n\forall i<2[\langle
n,i\rangle\in C]$.

###  14.3. Recovering the Fan Theorem

Let us consider the result of the last subsection:

> $(\\#)$ For every $C\subseteq\omega\times 2$,
> if $\forall\tau\in\mathcal{C}\exists n[\langle n,\tau(n)\rangle\in C]$, then
> $\exists n[\langle n,0\rangle\in C\;\wedge\;\langle n,1\rangle\in C]$.

We prove that this statement implies an important case of the Fan Theorem. The
Fan Theorem is the statement that every $B\subseteq\mathbb{N}$ that is a bar
in $\mathcal{C}$ has a finite subset that is a bar in $\mathcal{C}$. We prove
that $\\#$ implies this statement for the case that $B$ is a decidable subset
of $\mathbb{N}$.

Assume $(\\#)$ and let $B\subseteq\mathbb{N}$ be given such that
$Bar_{\mathcal{C}}(B)$ and one may decide, for each $n$, $n\in B$ or $n\notin
B$. For all $n$, we define: $B_{n}:=\\{s\in B\mid s<n\\}$.
We want to prove the statement $QED:=\exists
n[Bar_{\mathcal{C}}(B_{n})]$232323We read $QED$ not in its usual sense: ‘quod
erat demonstrandum, what had to be proven’ but as: ‘quod est demonstrandum,
what has to be proven’..
We let $C$ be the set of all pairs $\langle s,i\rangle$ such that either:
$QED$ or: $Bar_{\mathcal{C}\cap s\ast\langle i\rangle}(B_{n})$ and not
$Bar_{\mathcal{C}\cap s\ast\langle 1-i\rangle}(B_{n})$. Note that, for each
$s$ in $Bin$, if both $s\ast\langle 0\rangle$ and $s\ast\langle 1\rangle$ are
in $C$, then $QED$. Also note that $C$, like $B$, is a decidable subset of
$\mathbb{N}$.
Let $\tau$ in $\mathcal{C}$ be given. Find $\alpha$ in $\mathcal{C}$ such that
$\forall i[\alpha(i)=\tau(\overline{\alpha}i)]$. Find $n$ such that
$\overline{\alpha}n\in B$ and define $m:=\overline{\alpha}n+1$. Note:
$Bar_{C\cap\overline{\alpha}n}(B_{m})$.
Note that, for each $i$, if $i+1\leq n$ and
$Bar_{\mathcal{C}\cap\overline{\alpha}(i+1)}(B_{m})$, then either:
$Bar_{\mathcal{C}\cap\overline{\alpha}(i)}(B_{m})$ or: $\neg
Bar_{\mathcal{C}\cap\overline{\alpha}(i)\ast\langle
1-\alpha(i)\rangle}(B_{m})$ and $\langle\overline{\alpha}i,\alpha(i)\rangle\in
C$. Using backwards induction,
starting from the fact: $Bar_{\mathcal{C}\cap\overline{\alpha}n}(B_{m})$, we
prove:
for each $i\leq n$, either $Bar_{\mathcal{C}\cap\overline{\alpha}i}(B_{m})$ or
$\exists j<n[\langle\overline{\alpha}j,\alpha(j)\rangle\in C]$.
Taking $i=0$, we find: either $Bar_{\mathcal{C}}(B_{m})$ or $\exists
j[\langle\overline{\alpha}j,\alpha(j)\rangle\in C]$, i.e. either $QED$ or
$\exists j[\langle\overline{\alpha}j,\tau(\overline{\alpha}j)\rangle\in C]$.
In both cases, one may conclude: $\exists s[\langle s,\tau(s)\rangle\in C]$.

We thus see: $\forall\tau\in\mathcal{C}\exists s[\langle s,\tau(s)\rangle\in
C]$. Using $(\\#)$, we conclude:
$\exists s[s\ast\langle 0\rangle\in C\;\wedge\;s\ast\langle 1\rangle\in C]$,
and, therefore: $QED$, i.e. $\exists n[Bar_{\mathcal{C}}(B_{n})]$.

This shows that every decidable subset $B$ of $\mathbb{N}$ that is a bar in
$\mathcal{C}$ has a finite subset that is a bar in $\mathcal{C}$.

###  14.4. The Intuitionistic Determinacy Theorem

We now study games with infinitely many moves rather than two moves only.

######  Definition 16.

$(\omega\times 2)^{\omega}:=\\{\alpha\mid\forall n[\alpha(2n+1)<2]\\}$.

For each $\sigma$, for each $\alpha\in(\omega\times 2)^{\omega}$,
$\alpha\in_{I}\sigma:=\forall
n[\alpha(2n)=\sigma\bigl{(}\overline{\alpha}(2n)\bigr{)}]$

For each $\tau$ in $\mathcal{C}$, for each $\alpha$ in $(\omega\times
2)^{\omega}$, $\alpha\in_{II}\tau:=\forall
n[\alpha(2n+1)=\tau\bigl{(}\overline{\alpha}(2n+1)\bigr{)}]$.

For every $\mathcal{X}\subseteq(\omega\times 2)^{\omega}$, we introduce a game
$\mathcal{G}_{(\omega\times 2)^{\omega}}(\mathcal{X})$. There are two players,
Player $I$ and Player $II$. Every play takes infinitely many moves and goes as
follows. Player $I$ chooses $n_{0}$ in $\omega$, thereafter Player $II$
chooses $i_{0}$ in $2=\\{0,1\\}$, then Player $I$ chooses $n_{1}$ in $\omega$
and, thereafter, Player $II$ chooses $i_{1}$ in $2$, and so on. Player $I$
wins the play if the infinite sequence $n_{0},i_{0},n_{1},i_{1},\ldots$ is in
$\mathcal{X}$. Player $II$ tries to prevent that Player $I$ wins the game.

######  Theorem 18 (Intuitionistic Determinacy Theorem).

For all $\mathcal{X}\subseteq(\omega\times 2)^{\omega}$, if
$\forall\tau\in\mathcal{C}\exists\alpha\in(\omega\times
2)^{\omega}[\alpha\in_{II}\tau\;\wedge\;\alpha\in\mathcal{X}]$, then
$\exists\sigma\forall\alpha\in(\omega\times
2)^{\omega}[\alpha\in_{I}\sigma\rightarrow\alpha\in\mathcal{X}]$.

The Theorem is good news for Player $I$. Suppose
$\mathcal{X}\subseteq\mathcal{(}\omega\times 2)^{\omega}$ is such that Player
$I$ is able, once Player $II$ has told her the strategy $\tau$ she intends to
follow, to find a play following $\tau$ that is in $\mathcal{X}$. She then may
devise a strategy $\sigma$, such that every play following $\sigma$ is in
$\mathcal{X}$. Using $\sigma$, Player $I$ can do without information about the
strategy followed by Player $II$.

We will not give the proof of Theorem 18242424See [47, Chapter 16], [59] and
[61, Section 9].. As in Subsection 14.2, the Fan Theorem plays a key rôle in
the argument. From Subsection 14.1, one may see it is crucial for Theorem 18
that, in $(\omega\times 2)^{\omega}$, Player $II$ has, at each one of her
moves, only 2 choices. The theorem extends to the case that Player $II$ has,
at each one of her moves, finitely many choices.

##  15\. Brouwer’s Thesis

###  15.1. The Principle of Bar Induction

The key point in the proof of the next Theorem is a philosophical
assumption252525The theorem better might be called an axiom. one might call
Brouwer’s Thesis (on bars in $\mathcal{N}$)262626For a discussion, see [57]..

######  Theorem 19 (Bar Induction).

Let $B\subseteq\mathbb{N}$ be given such that $Bar_{\mathcal{N}}(B)$. Let
$C\subseteq\mathbb{N}$ be given such that $B\subseteq C$ and, for all $s$,
$s\in C$ if and only if $\forall n[s\ast\langle n\rangle\in C]$. Then
$\langle\;\rangle\in C$.

###### Proof.

Let $B\subseteq\mathbb{N}$ be given such that $Bar_{\mathcal{N}}(B)$.

Define, for every $s$, $s$ is B-safe, or simply: safe, if and only if
$Bar_{\mathcal{N}\cap s}(B)$.

Note: $\langle\;\rangle$ is safe.

There must exist a canonical proof of the fact:

$\langle\;\rangle$ is safe.

The conclusion of the canonical proof is: ‘$\langle\;\rangle$ is safe.’

The starting points of the canonical proof have the form:

$s\in B$.

Therefore: $s$ is safe.

There are two kinds of reasoning steps, forward steps and backward steps.

A forward reasoning step has infinitely many premises and is of the following
form:

$s\ast\langle 0\rangle$ is safe, $s\ast\langle 1\rangle$ is safe,
$s\ast\langle 2\rangle$ is safe, $\ldots$

Therefore: $s$ is safe.

A backward reasoning step has the form:

$s$ is safe.

Therefore: $s\ast\langle n\rangle$ is safe.

The canonical proof is not a finite tree but an infinite one. The canonical
proof can not be written out explicitly as a finite text.

Let $C\subseteq\mathbb{N}$ be given such that $B\subseteq C$ and, for all $s$,
$s\in C$ if and only if $\forall n[s\ast\langle n\rangle\in C]$.

Now replace in the canonical proof every statement ‘$s$ is safe’ by the
statement ‘$s\in C$’. The result will be another valid proof.

Why?

As $B\subseteq C$, the new starting points are sound.

As, for every $s$, if $\forall n[s\ast\langle n\rangle\in C]$, then $s\in
C$272727$C\subseteq\mathbb{N}$ with this property is called inductive., the
new forward reasoning steps are sound.

As, for every $s$, for every $n$, if $s\in C$, then $s\ast\langle n\rangle\in
C$282828$C\subseteq\mathbb{N}$ with this property is called monotone., the new
backward reasoning steps are sound.

We must conclude: the new conclusion is true, that is: $\langle\;\rangle\in
C$. ∎

###  15.2. One needs backward steps

######  Theorem 20 (Kleene’s example292929See [41, §7.14].).

There exist $B\subseteq C\subseteq\mathbb{N}$ such that $Bar_{\mathcal{N}}(B)$
and, for all $s$, if $\forall n[s\ast\langle n\rangle\in C]$, then $s\in C$,
while the statement ‘$\langle\;\rangle\in C$’ is a reckless one.

###### Proof.

Let $B$ consist of all $s$ such that
either $\exists n<k_{99}[s=\langle n\rangle]$ or $s=\langle\;\rangle$ and
$\exists n[n=k_{99}]\vee\forall n[n<k_{99}]$.

Let $\alpha$ be given. Either $\alpha(0)<k_{99}$ and $\overline{\alpha}1\in
B$, or $\alpha(0)\geq k_{99}$ and $\langle\;\rangle=\overline{\alpha}0\in B$.
We thus see: $Bar_{\mathcal{N}}(B)$.

Let $C$ coincide with $B$.

For all $s$, if, for all $n$, $s\ast\langle n\rangle\in C$, then
$s=\langle\;\rangle$ and $\forall n[n<k_{99}]$ and $\langle\;\rangle\in C$.

The statement ‘$\langle\;\rangle\in C$’ is equivalent to ‘$\exists
n[n=k_{99}]\vee\forall n[n<k_{99}]$’, and is reckless. ∎

Consider the set $B$ mentioned in the proof of Theorem 20. Note that every
canonical proof of ‘$\langle\;\rangle$ is (B-)safe’ must use backward steps.
The last step in a canonical proof of ‘$\langle\;\rangle$ is (B-)safe’ must be
a forward step: $\langle\;\rangle$ is safe because: $\langle 0\rangle$ is
safe, $\langle 1\rangle$ is safe, $\langle 2\rangle$ is safe, $\ldots$. For
each $n<k_{99}$ the conclusion: $\langle n\rangle$ is safe follows by a basic
step from: $\langle n\rangle\in B$. For each $n\geq k_{99}$ the conclusion:
$\langle n\rangle$ is safe follows by a backward step from: $\langle\;\rangle$
is safe and that follows in its turn by a basic step from:
$\langle\;\rangle\in B$ (as $n\geq k_{99}$).

We thus see that, in this particular case, the backward steps can not be
missed. In the case of the Fan Theorem, Theorem 14, as we learned from Theorem
15, one might have claimed there is a canonical proof using only forward
reasoning steps.

##  16\. Open Induction in $[0,1]$

Brouwer’s main application of the Principle of Bar Induction, Theorem 19, is
the Fan Theorem. We now give an example of a stronger consequence of the
Principle.

######  Definition 17.

We let
$(r_{0}^{\prime},r_{0}^{\prime\prime}),\;(r_{1}^{\prime},r_{1}^{\prime\prime}),\;(r_{2}^{\prime},r_{2}^{\prime\prime}),\;\ldots$
be a fixed enumeration of all pairs of rationals.

For each $\alpha$, $\mathcal{G}_{\alpha}:=\\{x\in\mathcal{R}|\exists
n[r_{\alpha(n)}^{\prime}<x<r_{\alpha(n)}^{\prime\prime}]\\}.$

For each $a$, $\mathcal{G}_{a}:=\\{x\in\mathcal{R}\mid\exists
n<length(a)[r^{\prime}_{a(n)}<x<r^{\prime\prime}_{a(n)}]\\}$.

$\mathcal{G}\subseteq\mathcal{R}$ is _open_ if and only if, for some $\alpha$,
$\mathcal{G}=\mathcal{G}_{\alpha}$.

For all $x,y$ in $\mathcal{R}$ such that $x<y$, we define
$[x,y):=\\{z\in\mathcal{R}\mid x\leq_{\mathcal{R}}z<_{\mathcal{R}}y\\}$.

$\mathcal{G}\subseteq\mathcal{R}$ is _progressive in $[0,1]$_ if and only if
$\forall x\in[0,1][[0,x)\subseteq\mathcal{G}\rightarrow x\in\mathcal{G}]$.

######  Theorem 21 (Principle of Open Induction in ${[}0,1{]}$).

For every open $\mathcal{G}\subseteq\mathcal{R}$, if $\mathcal{G}$ is
progressive in $[0,1]$, then $[0,1]\subseteq\mathcal{G}$.

Although the theorem may be new to the reader, É. Borel in fact introduced and
used it when he proved, in 1895, see [6], what is now called the Heine-Borel
Theorem:

for each $\alpha$, if $[0,1]\subseteq\mathcal{G}_{\alpha}$, then $\exists
n[[0,1]\subseteq\mathcal{G}_{\overline{\alpha}n}]$.

Borel’s argument may be described as follows. Let $\alpha$ be given such that
$[0,1]\subseteq\mathcal{G}_{\alpha}$. Define
$\mathcal{H}:=\\{y\in\mathcal{R}\mid\exists
n[[0,y]\subseteq\mathcal{G}_{\overline{\alpha}n}]\\}$. Note that $\mathcal{H}$
is open and progressive in $[0,1]$. Applying the principle of Open Induction
on $[0,1]$, conclude: $1\in\mathcal{H}$ and $\exists
n[[0,1]\subseteq\mathcal{G}_{\overline{\alpha}n}]$.

How does the classical mathematician convince herself of the validity of the
Principle of Open Induction in $[0,1]$?

Given an open $\mathcal{G}\subseteq\mathcal{R}$ that is progressive in
$[0,1]$, she starts defining an infinite sequence $x_{0},x_{1},\ldots$ of
reals. She defines $x_{0}:=0$ and notes $x_{0}\in\mathcal{G}$. She then finds
$x_{1}>x_{0}$ such that $[0,x_{1})\subseteq\mathcal{G}$. If $x_{1}\geq 1$, she
is done and defines, for each $n\geq 1$, $x_{n}=1$. If not, she observes:
$x_{1}\in\mathcal{G}$ and finds $x_{2}>x_{1}$ such that
$[0,x_{2})\subseteq\mathcal{G}$. If $x_{2}\geq 1$ she is done and defines, for
each $n\geq 2$, $x_{n}=1$. If not, she observes: $x_{2}\in\mathcal{G}$ and
finds $x_{3}>x_{2}$ such that $[0,x_{3})\subseteq\mathcal{G}$. And so on. She
thus finds an infinite sequence $0\leq x_{0}\leq x_{1}\leq x_{2}\leq\ldots$ of
reals such that, for each $n$, $[0,x_{n})\subseteq\mathcal{G}$ and:
$x_{n+1}=x_{n}$ if and only if $x_{n}=1$. The infinite non-decreasing sequence
$x_{0},x_{1},\ldots$ is bounded by $1$ and thus converges, to, say,
$x_{\omega+0}=x_{\omega}$. Then: $x_{\omega}\in\mathcal{G}$ as
$[x,x_{\omega})\subseteq\mathcal{G}$. If $x_{\omega}\geq 1$, she is done and
defines, for each $n\geq 0$, $x_{\omega+n}=1$. If not, she starts again and
finds suitable $x_{\omega+1},x_{\omega+2},\ldots$ such that, for each $n$,
$[0,x_{\omega+n})\subseteq\mathcal{G}$ and $x_{\omega+n}\leq x_{\omega+n+1}$
and: $x_{\omega+n+1}=x_{\omega+n}$ if and only if $x_{\omega+n}\geq 1$. She
then considers $x_{\omega\cdot 2}=x_{\omega+\omega}:=\lim_{n}x_{\omega+n}$.
She has inexhaustible energy and, if needed, finds $x_{\omega\cdot 3}$
$x_{\omega\cdot 4},\ldots x_{\omega\cdot\omega},\ldots$. She thus continues
her infinite sequence through the countable ordinals.

She believes this procedure will come to an end, that is: there must exist a
countable ordinal $\beta$ such that $x_{\beta}=1$. She argues a follows. For
each $k>0$ there can be only $k$ countable ordinals $\alpha$ such that
$x_{\alpha}+\frac{1}{k}<x_{\alpha+1}$. Therefore, there are only countably
many countable ordinals such that $x_{\alpha}<x_{\alpha+1}$. Find a countable
ordinal $\beta$ that lies beyond every countable ordinal $\alpha$ such that
$x_{\alpha}<x_{\alpha+1}$. Then $x_{\beta}=x_{\beta+1}$ and: $x_{\beta}=1$.

Borel argued in this way, proudly using the countable ordinals introduced by
Cantor some 20 years earlier, see [34].

This argument, from a constructive point of view, is quite fantastic. We
parted company with the classical mathematician already at the point where she
believed to find $x_{\omega}$. It is not true, constructively, that every non-
decreasing bounded infinite sequence of reals has a limit: consider the
sequence defined by: $x_{n}=0$ if $n<k_{99}$ and $x_{n}=1$ if $k_{99}\leq n$.
303030Assume $c:=\lim_{n}x_{n}$ exists. If $c>0$, then $\exists n[n=k_{99}]$
and, if $c<1$, then $\forall n[n<k_{99}]$.

The classical mathematician may propose a second line of thought. She might
use a classical mathematician’s finest weapon313131See Section 4., as follows.
Assume $\mathcal{G}\neq[0,1]$. Consider $y:=\inf([0,1]\setminus\mathcal{G})$.
As $\mathcal{G}$ is open, $y\notin\mathcal{G}$, but also
$[0,y)\subseteq\mathcal{G}$. Contradiction.

Again, we can not partake in her joy. It is not clear that we may construct
$y$. And, of course, it is not clear that, having proved: $\neg\exists
x\in[0,1][x\notin\mathcal{G}]$, we might conclude: $\forall
x\in[0,1][x\in\mathcal{G}]$.

In order to make the problem more pictorial, let us define: Achilles323232See
[52, p. 338]. arrives at $x$ if and only if $[0,x)\subseteq\mathcal{G}$.

How might we, constructive mathematicians, convince ourselves that Achilles
arrives at $1$? We should first prove that Achilles will arrive at
$\frac{1}{2}$, but it does not seem easier to prove that Achilles will arrive
at $\frac{1}{2}$ than to prove that he will arrive at $1$.

###### Proof.

333333The theorem was found and proven by Thierry Coquand, in 1997. We were
discussing then the problem if positive contrapositions of the minimal bad
sequence arguments used in [43] might be intuitionistically true, see [54,
§11].

Let $\mathcal{G}\subseteq\mathcal{R}$ be open and progressive in $[0,1]$. Find
$\alpha$ such that $\mathcal{G}=\mathcal{G}_{\alpha}$. We define a mapping
$s\mapsto(c_{s},d_{s})$ that associates to every $s$ in $\mathbb{N}$ a pair of
rationals. The elements $s$ of $\mathbb{N}$ are thought of as coding finite
sequences of natural numbers, see Subsection 12.1, Definition 10.

  1. (i)

$(c_{\langle\;\rangle},d_{\langle\;\rangle}):=(0,1)$.

  2. (ii)

For each $s$, for each $n$, find out if $\forall
x\in[0,\frac{c(s)+d(s)}{2}]\exists
i<n[r^{\prime}_{\alpha(i)}<x<r^{\prime\prime}_{\alpha(i)}]$.343434Note that
this a decidable proposition.
If so, define $(c_{s\ast\langle n\rangle},d_{s\ast\langle
n\rangle})=(\frac{c_{s}+d_{s}}{2},d_{s})$, and