1 Introduction
1.1 Bishop’s disagreement with Brouwer
E. Bishop, who founded constructive analysis, has an ambivalent attitude towards L. E. J. Brouwer, who, a generation earlier, began intuitionistic mathematics.Footnote 1
On the one hand, Bishop recognizes that Brouwer was the first to raise his voice against the disturbing fact that many mathematical theorems lack constructive content. He also judges that Brouwer made a good beginning with the necessary reconstruction of parts of mathematics. He agrees with him that disjunction and the existential quantifier should be interpreted constructively and that, as a consequence, the principle of the excluded third
$X\;\vee \;\neg X$
should be rejected.
On the other hand, he thinks Brouwer went the wrong way by introducing ‘semi-mystical elements’ into mathematics in order to prove the theorem that every (effectively total) function from the closed real interval
$[0,1]$
to the set
$\mathcal {R}$
of the real numbers is uniformly continuous.
This theorem may be split up into two statements:
-
1. Every function from
$[0,1]$
to
$\mathcal {R}$
is pointwise continuous. -
2. Every pointwise continuous function from
$[0,1]$
to
$\mathcal {R}$
is uniformly continuous.
The first statement is a consequence of Brouwer’s Continuity Principle and the second one follows from his Fan Theorem.
Bishop rejects Brouwer’s argument for the first conclusion and argues even that its conclusion is not useful. He says that a set like ‘the set of all functions from
$[0,1]$
to
$\mathcal {R}$
’ has little practical interest, [Reference Bishop and Bridges1, p. 67], meaning probably, that one can do without general statements about “all functions from
$[0,1]$
to
$\mathcal {R}$
” like the statement 1.
He also decides not to use the notion of a pointwise continuous function, see [Reference Bishop and Bridges1, p. 6]. He defines a function from
$\mathcal {R}$
to
$\mathcal {R}$
to be continuous if and only if the function is uniformly continuous on every closed interval
$[a,b]$
, see [Reference Bishop and Bridges1, Chapter 2, Definition 4.5].Footnote
2
The statement 2 then becomes a tautology.
The Continuity Principle and the Fan Theorem together imply that every sequence
$f_0, f_1, \ldots $
of continuous functions from
$[0,1]$
to
$\mathcal {R}$
that converges pointwise to a continuous function f from
$[0,1]$
to
$\mathcal {R}$
will converge uniformly to f. Bishop avoids the notion of pointwise convergence, and defines the sequence
$f_0, f_1, \ldots $
to converge on [
$0,1]$
if it does so uniformly, see [Reference Bishop and Bridges1, Chapter 2, Definition 4.9].
Brouwer derived his Fan Theorem from a much stronger statement, the Bar Theorem. Bishop never discussed this stronger statement.
1.2 Going back to Brouwer’s basic assumptions
Brouwer’s arguments for the statements 1 and 2 in Section 1.1 are philosophical rather than mathematical. One should not put them aside as non-mathematical and, therefore, not worth a mathematician’s attention. Moreover, these arguments may have consequences that go further than the statements 1 and 2 and are important for the further development of constructive mathematics.
Brouwer is trying to redefine the game of mathematics and make it a better game than it has been up to now. This game is our common undertaking. The starting points of the game have to be agreed upon, and are a topic of ongoing discussion. They should be called axioms, although Brouwer avoids this expression. Brouwer, somewhat misleadingly, presents his axioms and the arguments that should convince us to accept them as being beyond doubt and speaking for themselves. He does not distinguish such ‘philosophical’ arguments from his more mathematical arguments.
1.3 The three varieties
Constructive mathematics is often described as having three varieties, BISH, i.e., Bishop style constructive mathematics, INT, i.e., intuitionistic mathematics and RUSS, i.e., Russian style constructive mathematics, where the notion of a computable function from the set
$\omega $
of the natural numbers to
$\omega $
sets the scene, see [Reference Bridges and Richman4]. This division is problematic.
It is difficult to make sense of the slogan:
In essence, BISH is simply mathematics with intuitionistic logic
explained and defended in [Reference Bridges and Vîţă5, Section 1.3].
The slogan suggests that, for a classical mathematician who decides to join the constructive enterprise, mathematical objects remain the same in spite of the fact that he is changing the language he uses for describing them. This suggestion is wrong. It sounds as if the objects are and remain there, like animals in a zoo, while we, the visitors, start babbling about them in a foreign tongue.
More fundamentally, it does not make sense to say:
‘We may prove statement X classically as well as intuitionistically’
as the statement X does not mean the same intuitionistically as it does classically. Classical and intuitionistic mathematicians do not speak the same language. They may use the same expressions and the same formulas but they give them their own interpretation.
Of course, if we formalize mathematics we may prove combinatorial facts of the form:
Formula
$\varphi $
is provable in the classical as well as in the intuitionistic system.
But the meaning of the formula would change with the user of the formalisms.
One sometimes says:
BISH is part of INT.
One might accept this statement if one explains it as follows:
An intuitionistic result is reckoned to belong to BISH if it can be proven without making use of either the Continuity Principle, the Fan Theorem or the Bar Theorem.
The third variety, RUSS, arises from BISH by adding the assumption that every real is given by an algorithm in the Church–Turing sense. The study of computable number-theoretic functions, however, if it is done properly, i.e., intuitionistically, is part of intuitionistic mathematics, in fact a part of intuitionistic number theory, and not an alternative for intuitionistic mathematics, see [Reference Veldman36]. Unfortunately, the theory of computable functions, up to now, is mostly done from a classical point of view, and, in Russian style constructive mathematics, where one uses intuitionistic logic, one also uses Markov’s PrincipleFootnote
3
, a principle for which there is no good intuitionistic reason. Let RUSS
$_{int}$
denote the collection of results from RUSS that are obtained without using Markov’s Principle.
So, we propose the following picture:
$$ \begin{align*} \textit{RUSS}_{int} \;\subseteq\; \textit{BISH}\;\subseteq\; \textit{INT} \end{align*} $$
where each of the three RUSS, BISH, and INT is considered as a body of proven intuitionistically meaningful results.Footnote 4
CLASS, the collection of results obtained classically, does not occur in the picture. The constructive mathematician has no immediate understanding of results in CLASS. The inclusion BISH
$\;\subseteq \;$
CLASS makes no sense.
In [Reference Bridges and Richman4, Chapter 6] we find the statement:
BISH is widely accepted as the common core of INT, RUSS and any genuinely constructive development of mathematics other than a strictly finitistic one.
Again, the only way to make sense of this statement requires that one consider INT, RUSS and ‘other constructive developments of mathematics’ as sets of formulas proven in some suitable formal system. This thus presupposes a formalist view of mathematics. Both Brouwer and Bishop dissociated themselves from such a view.
1.4 The need for axioms
The constructive rebuilding of mathematics forces one to rethink radically the meaning of mathematical statements. One should keep in mind that the meaning of a mathematical statement is ultimately given by its proof. The proof should be seen as an explication or unfolding of the meaning of the statement. The proof is a mental construction and should be distinguished from its always imperfect description by a formal deduction.
In the proof we may refer to constructions we did earlier but, sometimes, we come to invoke ‘axioms’. An axiom might be seen as a stipulation on the meaning of some of the expressions we are using in our language. As such, axioms come very close to ‘definitions’.
Axioms arise from situations we want to consider as canonical, as setting an example.
For instance, once we have seen Euclid’s proof that there exist infinitely many primes, we see how we want to prove such a thing, and we define: ‘
$X\subseteq \omega $
is infinite if one is able to indicate an algorithm providing, given any finite list
$(n_0, n_1, \ldots , n_{k-1})$
of natural numbers, an element of X not occurring in the list’.
Or, observing our own use of the disjunction, we may decide to lay down: ‘a proof of
$X \vee Y$
should consist either in a proof of X or in a proof of Y’.
Setting up our common mathematical discourse, we have to discuss carefully the question which principles deserve the status of a canonical starting point for our arguments, i.e., the status of an axiom.
An axiom is not a truth solid as a rock that is beyond doubt and discussion. On the contrary, it is a proposal that invites and shapes discussion. It might be compared to an hypothesis or a thought experiment. Like Gödel suggested in the context of axiomatic set theory, an axiom may prove its value when we decide to follow its lead and try to see what we find when using it.
It is an illusion however that one can do without axioms, and it is wrong to condemn arguments defending them as philosophical and unmathematical and therefore not relevant.
Brouwer’s Continuity Principle, the Fan Theorem, and the Bar Theorem, to be discussed later in this paper, may be seen as agreements on the meaning of certain statements of the form
$\forall x \exists y[xRy]$
.
1.5 The aim and contents of the paper
In this paper, we want to make clear how constructive mathematics develops if one does not, like Bishop, abandon the path shown by Brouwer. We introduce three main axioms of intuitionistic mathematics not accepted by Bishop: the Continuity Principle, the Fan Theorem, and the Thesis on Bars in
$\omega ^{\omega }$
. We discuss their plausibility and go into some of their applications.
Apart from this introductory Section, the paper contains eight Sections.
In Section 2, we explain Brouwer’s Continuity Principle. We see how it leads to its most famous consequence: the pointwise continuity of real functions. We also introduce axioms of countable and continuous choice.
In Section 3, we give a more sophisticated application of Brouwer’s Continuity Principle: the proof of an intuitionistic version of the Borel Hierarchy Theorem, see [Reference Veldman25, Chapter 9] and [Reference Veldman33, Section 7]. The classical proof of this theorem hinges on the duality of classical logic and can not be used. There are other points in the development of intuitionistic descriptive set theory where the Continuity Principle plays a key role. It is crucial for proving the fine structure of the hierarchy, see [Reference Veldman35], and a strong formulation of the PrincipleFootnote 5 leads to the collapse of the projective hierarchy, see [Reference Veldman25, Chapter 14] and [Reference Veldman40, Section 7]. We do not go into these further applications.
In Section 4, we explain the Fan Theorem. Brouwer himself called it a theorem and not an axiom, but the argument he uses for this ‘theorem’ and that we paraphrase, should be called philosophical, and the statement itself is better called an axiom. We give the first and most famous application of the Fan Theorem: functions with domain
$[0,1]$
that are pointwise continuous are also uniformly continuous.
In Section 5 we sketch the intuitionistic development of the theory of measure and integration, as begun by Brouwer and developed further by some students of Heyting, see [Reference Heyting16, Chapter VI]. Bishop, see [Reference Bishop and Bridges1, Chapter 6] decided not to follow Brouwer’s lead in this field, probably out of fear of the Fan Theorem.
In Section 6, we explain Brouwer’s Thesis on bars in the set
$\omega ^{\omega }$
of all infinite sequences of natural numbers. This Thesis is an axiom stronger than the Fan Theorem. We paraphrase Brouwer’s argument for the Thesis. Brouwer introduced it for proving the Fan Theorem but it has stronger consequences than that, although Brouwer himself did not use the Thesis for other purposes than the Fan theorem. As an example of a different application, we prove the equivalence of two definitions of the class of enumerable and well-founded subsets of the set of the rationals.
In Section 7, the longest Section of the paper, we explain the Almost-Fan Theorem. Like the Fan Theorem itself, the Almost-Fan Theorem follows from the Bar Theorem. For a classical spectator, who has an opaque view of things, the Almost-Fan Theorem is difficult to distinguish from the Fan Theorem itself. The Almost-Fan Theorem implies the Fan Theorem but it is a stronger statement and we will see it has other important consequences too: the so-called Principle of Open Induction on
$[0,1]$
, a version of what we call Dedekind’s Theorem, a version of the Infinite Ramsey Theorem, a version of the Bolzano–Weierstrass Theorem and the Paris–Harrington–Ramsey Theorem. In [Reference Veldman37] these results are studied within the framework of Intuitionistic Reverse Mathematics.
In Section 8, we explain our notations. This Section may be used by the reader as a reference.
2 Axioms of Continuity and Choice
Brouwer’s Continuity Principle is an axiom that revolutionizes constructive mathematics, see [Reference Veldman, Berger, Osswald and Schuster29]. We explain the axiom and show that it leads to the theorem that every real function is pointwise continuous. We introduce spreads, a special kind of subsets of
$\omega ^{\omega }$
. We show that the Continuity Principle generalizes to spreads. We then consider two Axioms of Countable Choice and their plausibility. Finally, we introduce two Axioms of Continuous Choice that are strengthenings of the Continuity Principle.
2.1 The Continuity Principle
Axiom 1 (Brouwer’s Continuity Principle).
For every relation
${R\kern1.4pt{\subseteq}\kern1.4pt \omega ^{\omega }\kern1.4pt{\times}\kern1.4pt \omega} $
,
if
$\forall \alpha \exists n[\alpha Rn]$
, then
$\forall \alpha \exists m\exists n \forall \beta [\overline \alpha m \sqsubset \beta \rightarrow \beta Rn]$
.
The principleFootnote
6
came on the scene in 1918. In [Reference Brouwer7, p. 13], Brouwer explains that there can not exist an injective function from
$\omega ^{\omega }$
to the set
$\omega $
of the natural numbers. Brouwer argues as follows. If we are given a function f from
$\omega ^{\omega }$
to
$\omega $
and an element
$\alpha $
of
$\omega $
, then
$f(\alpha )$
, the value of f at
$\alpha $
, will have to be decided upon at a point of time at which only finitely many values of
$\alpha $
, say,
$ \alpha (0), \alpha (1), \ldots , \alpha (m-1),$
have become known. So all infinite sequences
$\beta $
that take the same values as
$\alpha $
at the arguments
$0,1, \ldots , m-1$
would be allotted the same value by f as
$\alpha $
, and f would be non-injective.
The principle Brouwer is using here, for the first time, is what we now call his Continuity Principle. In our formulation of the principle, the starting point seems to be a little bit more general: ‘
$\forall \alpha \exists n[\alpha R n]$
’, but we interpret this as: ‘we have a method to assign to any given
$\alpha $
a suitable n, i.e., there exists a function f from
$\omega ^{\omega }$
to
$\omega $
such that
$\forall \alpha [\alpha R f(\alpha )]$
’.
Brouwer is imagining that the sequence
$$\begin{align*}\alpha=\alpha(0), \alpha(1), \ldots \end{align*}$$
is given to us only step by step. We learn its values one by one and have no information on the development of the sequence as a whole.
The first and foremost example of an infinite sequence is the sequence
$$\begin{align*}\alpha(0)=0, \alpha(1)=1, \alpha(2)=2,\ldots \end{align*}$$
of the natural numbers themselves. Even this infinite sequence is growing step by step and never fully realized. Its construction is a job that we started to carry out and always will work on without ever finishing it. As one sometimes says, it is a project rather than an object.
Another infinite sequence that grows step by step is the sequence
$$\begin{align*}\alpha(0)= 1, \alpha(1)= 4, \alpha(2) =1, \ldots \end{align*}$$
of the decimals of
$\pi $
.
These two examples do not give us a complete picture. Although we construct the natural numbers one by one and also calculate the decimals of
$\pi $
one by one, we have, in both cases, a key for finding all future values that precludes surprises. Brouwer calls such algorithmic infinite sequences lawlike sequences.
We make room for other infinite sequences too. We admit the possibility that the values of
$\alpha $
are disclosed to us, or chosen by us, one by one, and that we do not know any finite algorithm that determines the values of
$\alpha $
.
Every individual member of the set
$\omega ^{\omega }$
of the infinite sequences of natural numbers may be imagined to be always under construction and never completed.
Brouwer thus saw that ‘sets’ like
$\omega ^{\omega }$
deserve careful treatment.
Cantor’s idea that a set is the result of collecting certain already existing objects, to be called its elements, into a new whole, is wrong. In this picture, the elements of the set are ‘earlier there’ than the set itself. The intuitionistic mathematician proposes to view a set like
$\omega ^{\omega }$
as a realm of possibilities. A set is like a musical instrument, on which many tunes will be played in the future.
One should keep in mind that it does not make sense, intuitionistically, that something is the case without our knowing so. The meaning of a statement
$$ \begin{align*} \forall \alpha\exists n[\alpha Rn] \end{align*} $$
must be that I see that I am able to effectively find a suitable n to any possible
$\alpha $
.
$\alpha $
may be given to me, or created by myself making free choices, value by value, without, at any point of time, any further information on the whole of its course, and, what is very important, even if
$\alpha $
is not given in this way but, somehow, at one stroke,
$\alpha $
might have been given to me in this way.
In this way, we defend the claim that, if
$\forall \alpha \exists n[\alpha Rn]$
, then, given any
$\alpha $
, one must be able to come up with a suitable n for
$\alpha $
knowing only finitely many values of
$\alpha $
.
Note that an infinite sequence that I am creating freely, value by value, may turn out, in the end, to be a ‘simple’ one that admits of a finite description. The decimal expansion of
$\pi $
, for instance, like the infinite sequence
$\underline 0$
that has the constant value
$0$
, may be the result of an infinite sequence of free choices.
2.2 A first application
Theorem 1. For every relation
$R\subseteq \mathcal {R}\times \omega $
, if
$\forall x \exists n[x Rn]$
, then
$\forall x\exists m \exists n \forall y[|x-y|<\frac {1}{2^m}\rightarrow yRn]$
.
Proof Assume
$\forall x\in \mathcal {R}\exists n[x Rn]$
. We prove the promised conclusion for the case
$x=0$
, i.e.,
$\exists m \exists n[\forall y[|y|<\frac {1}{2^m}\rightarrow yRn]$
. The general case is proven similarly.
We first define a function
$\varphi $
from
$\omega ^{\omega }$
to
$\omega ^{\omega }$
.
Let
$q_0:=0, q_1, q_2, \ldots $
be an enumeration of the rationals. Let
$\alpha $
be given. We construct the infinite sequence
$\varphi |\alpha = (\varphi |\alpha )(0), (\varphi |\alpha )(1), \ldots $
as follows. We define
$(\varphi |\alpha )(0)=0$
, and, for each n, if
$|q_{\alpha (n+1)}-q_{(\varphi |\alpha )(n)}|\le \frac {1}{2^n}$
, we define
$(\varphi |\alpha )(n+1)= \alpha (n+1)$
, and, if not, we define
$(\varphi |\alpha )(n+1)=(\varphi |\alpha )(n)$
.
Note that, for each
$\alpha $
, the sequence
$q_{(\varphi |\alpha )(0)}, q_{(\varphi |\alpha )(1)}, \ldots $
converges. Also note that, if, for all n,
$|q_{\alpha (n+1)}-q_{\alpha (n)}|\le \frac {1}{2^n}$
, then
$\varphi |\alpha =\alpha $
. We define, for each
$\alpha $
,
$x_\alpha :=\lim _{n\rightarrow \infty } q_{(\varphi |\alpha )(n)}$
.
Note that
$\forall \alpha \exists n[x_\alpha Rn]$
. Apply the Continuity Principle and find
$m,n$
such that
$\forall \alpha [\underline {\overline 0}m \sqsubset \alpha \rightarrow x_\alpha Rn]$
. Note that, for each x in
$[-\frac {1}{2^m}, \frac {1}{2^m}]$
there exists
$\alpha $
such that
$\overline {\underline 0}m\sqsubset \alpha $
and
$x=x_\alpha $
. Conclude that
$\forall x \in [-\frac {1}{2^m}, \frac {1}{2^m}][ x R n]$
.
Corollary 2. Every function from
$\mathcal {R}$
to
$\mathcal {R}$
is pointwise continuous.
Proof Let a function f from
$\mathcal {R}$
to
$\mathcal {R}$
be given.
Let
$q_0, q_1, \ldots $
be an enumeration of the rationals. Let p be given. Note that
$\forall x \in \mathcal {R}\exists n[|f(x) - q_n| < \frac {1}{2^{p+1}}]$
. Let x in
$\mathcal {R}$
be given. Applying Theorem 1, find m, n such that
$\forall y \in \mathcal {R}[|x-y|<\frac {1}{2^m} \rightarrow |f(x) - q_n|< \frac {1}{2^{p+1}}]$
. Conclude that
$\forall y \in \mathcal {R}[|x-y|< \frac {1}{2^m}\rightarrow |f(x)-f(y)|<\frac {1}{2^p}]$
. We thus see that
$\forall p\exists m\forall y \in \mathcal {R}[|x-y|< \frac {1}{2^m}\rightarrow |f(x)-f(y)|<\frac {1}{2^p}]$
, i.e., f is continuous at x.
We thus see that Corollary 2 follows from the Continuity Principle alone. Brouwer seems to have thought the Fan Theorem is needed for this result, see [Reference Brouwer8], [Reference Veldman26] and [Reference Veldman, Berger, Osswald and Schuster29].Footnote 7
2.3 Spreads
The ‘set’
$\omega ^{\omega }$
is an example of a kind of sets that are called spreads.
A spread is given by a spread-law
$\beta $
. The elements of the spread will be certain elements of
$\omega ^{\omega }$
that, as we saw, in general, are unfinished and are created step-by-step. The spread-law is there to regulate the process of defining elements of the spread. It informs me, whenever I have completed a finite initial part
$$\begin{align*}\alpha(0), \alpha(1), \ldots, \alpha(n-1) \end{align*}$$
of an element
$\alpha $
of the spread, what are the numbers I may choose for the next value,
$\alpha (n)$
.
The spread-law
$\beta $
itself is an element of
$\omega ^{\omega }$
. For every s, the informal meaning of ‘
$\beta (s)=0$
’ is: ‘the finite sequence coded by s is admitted by
$\beta $
’. The spread-law
$\beta $
has to satisfy the following condition:
$$\begin{align*}\forall s[\beta(s)=0\leftrightarrow \exists n[\beta(s\ast\langle n \rangle)=0]] \end{align*}$$
The ‘set’ consisting of all
$\alpha $
such that
$\forall n[\beta (\overline \alpha n)=0]$
will be called
$\mathcal {F}_\beta $
.
$\mathcal {F}_\beta $
is the spread determined by the spread-law
$\beta $
.
The condition just imposed on the spread-law
$\beta $
guarantees that, when I am creating an element
$\alpha $
of
$\mathcal {F}_\beta $
, then, at every stage n, having chosen
$\alpha (0), \alpha (1), \ldots , \alpha (n-1)$
, I am able to decide, for each m, if I may define
$\alpha (n):=m$
, and there will be at least one such m, i.e., I never will get ‘stuck’.
Theorem 3 (Brouwer’s Continuity Principle, extended to spreads).
Let
$\beta $
be a spread-law. For every relation
$R\subseteq \mathcal {F}_\beta \times \omega $
, if
$\forall \alpha \in \mathcal {F}_\beta \exists n[\alpha Rn]$
, then
$\forall \alpha \in \mathcal {F}_\beta \exists m\exists n \forall \gamma \in \mathcal {F}_\beta [\overline \alpha m \sqsubset \gamma \rightarrow \gamma Rn]$
.
Proof One might defend this theorem like Axiom 1 itself, as a more general formulation of the same principle. One may also derive the Theorem from the Axiom, as follows.
Let a spread-law
$\beta $
be given. Define
$\rho :\omega ^{\omega }\rightarrow \omega ^{\omega }$
such that, for each
$\alpha $
, for each n, if
$\beta \big (\overline \alpha (n+1)\big )=0$
, then
$(\rho |\alpha )(n)=\alpha (n)$
, and, if not, then
$(\rho |\alpha )(n)=\mu k[\beta \big (\overline {\rho |\alpha }n\ast \langle k \rangle \big )=0]$
. Then
$\forall \alpha [\rho |\alpha \in \mathcal {F}_\beta ]$
and
$\forall \alpha \in \mathcal {F}_\beta [\rho |\alpha =\alpha ]$
. The function
$\rho $
is called a retraction of
$\omega ^{\omega }$
onto
$\mathcal {F}_\beta $
.
Now assume
$\forall \alpha \in \mathcal {F}_\beta \exists n[\alpha R n]$
. Then
$\forall \alpha \exists n[(\rho |\alpha )Rn]$
. By Axiom 1, for any given
$\alpha $
in
$\mathcal {F}_\beta $
, one may find
$m,n$
such that
$\forall \gamma [\overline \alpha m\sqsubset \gamma \rightarrow (\rho |\gamma )Rn]$
and, therefore,
$\forall \gamma \in \mathcal {F}_\beta [\overline \alpha m \sqsubset \gamma \rightarrow \gamma R n]$
. Conclude that
$\forall \alpha \in \mathcal {F}_\beta \exists m\exists n \forall \gamma \in \mathcal {F}_\beta [\overline \alpha m \sqsubset \gamma \rightarrow \gamma Rn]$
.
2.4 Axioms of Countable Choice
Axiom 2 (First Axiom of Countable Choice).
For every relation
$R\subseteq \omega \times \omega $
, if
$\forall m \exists n [mRn]$
, then
$\exists \alpha \forall m[m R\alpha (m)]$
.
ThisFootnote
8
seems to be a good proposal as we decided to allow the possibility that an infinite sequence
$\alpha $
is created step by step. If
$\forall m\exists n[mRn]$
, we first find n, such that
$0Rn$
and define
$\alpha (0)=n$
, we then find n such that
$1Rn$
and define
$\alpha (1)=n$
, and so on. The axiom is not so plausible if we should require that an infinite sequence
$\alpha $
is given by means of an algorithm. The classical mathematician would suggest to define
$\alpha $
: for each m,
$\alpha (m)$
should be the least n such that
$mRn$
. This suggestion does not work in a constructive context, except for the case that one may decide, for all
$m, n$
, if
$mRn$
or not
$mRn$
.
Axiom 3 (Second Axiom of Countable Choice).
For every relation
$R\subseteq \omega \times \omega ^{\omega }$
, if
$\forall m \exists \alpha [mRn]$
, then
$\exists \alpha \forall m[m R\alpha ^m]$
.
This axiomFootnote
9
also seems to be a good proposal as, in general, we think it is possible to start a project for an infinite sequence, do some work on it, then start a second project for an infinite sequence, and do some work on it, then return to the first project and do some further work on it, and so on. Assume
$\forall n\exists \alpha [nR\alpha ]$
. Start a project for an infinite sequence suitable for
$0$
, calling it
$\alpha ^0$
and find
$\alpha ^0(0)$
. Start a project for an infinite sequence suitable for
$1$
, calling it
$\alpha ^1$
, and find
$\alpha ^1(0)$
and
$\alpha ^0(1)$
. Start a project for an infinite sequence suitable for
$2$
, calling it
$\alpha ^2$
and calculate
$\alpha ^2(0)$
,
$\alpha ^1(1)$
and
$\alpha ^0(2)$
. And so on.
2.5 Sharpened versions of the Continuity Principle
For some of the notations we are going to use, one may consult Section 8.3.
For every
$\varphi $
in
$\omega ^{\omega }$
, we define:
$\varphi :\omega ^{\omega }\rightarrow \omega $
if and only if
$\forall \alpha \in \omega ^{\omega }\exists n[\varphi (\overline \alpha n)\neq 0]$
.
If
$\varphi :\omega ^{\omega }\rightarrow \omega $
, then, for all
$\alpha $
,
$\varphi (\alpha )$
is the number p satisfying
$\exists n[\varphi (\overline \alpha n)=p+1 \;\wedge \;\forall i<n[\varphi (\overline \alpha i)=0]]$
.
Axiom 4 (First Axiom of Continuous Choice).
For every relation
$R\subseteq \omega ^{\omega }\times \omega $
, if
$\forall \alpha \exists n[\alpha R n]$
, then there exists
$\varphi :\omega ^{\omega }\rightarrow \omega $
such that
$\forall \alpha [\alpha R \varphi (\alpha )]$
.
One may argue for the axiomFootnote 10 as follows.
Assume
$\forall \alpha \exists n[\alpha R n]$
. We find the promised
$\varphi $
recursively, as follows. Given any s, we first ask if
$\exists t\sqsubset s[\varphi (t)\neq 0]$
. If so, we define
$\varphi (s)=0$
. If not, we imagine the finite sequence (coded by) s as the beginning of an infinite sequence
$\alpha $
that is created step by step, and we ask ourselves: ‘do we judge that s contains sufficient information for finding n such that
$\alpha R n$
?’Footnote
11
If so, we choose such n and define
$\varphi (s)=n+1$
, and, if not, we define
$\varphi (s) =0$
.
For every
$\varphi $
in
$\omega ^{\omega }$
, we define:
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
if and only if
$\forall n[\varphi ^n: \omega ^{\omega } \rightarrow \omega ]$
.
If
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
, then, for all
$\alpha $
,
$\varphi |\alpha $
is the element
$\beta $
of
$\omega ^{\omega }$
satisfying
$\forall n[\beta (n) = \varphi ^n(\alpha )]$
.
Axiom 5 (Second Axiom of Continuous Choice).
For every relation
$R\subseteq \omega ^{\omega }\times \omega ^{\omega }$
, if
$\forall \alpha \exists \beta [\alpha R \beta ]$
, then there exists
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
such that
$\forall \alpha [\alpha R (\varphi |\alpha )]$
.
One may argue for the axiomFootnote
12
as follows. Assume
$\forall \alpha \exists \beta [\alpha R \beta ]$
. We find the promised
$\varphi $
recursively, as follows. Given any s, we find the largest p such that
$\forall i<p\exists t\sqsubset s[\varphi ^i (t)\neq 0]$
. We imagine the finite sequence (coded by) s as the beginning of an infinite sequence
$\alpha $
that is created step by step. Clearly, we convinced ourselves that s contains sufficient information for finding the first p values of a sequence
$\beta $
satisfying
$\alpha R \beta $
. We now ask ourselves: ‘do we judge that s contains sufficient information for finding the next value of the sequence
$\beta $
such that
$\alpha R\beta $
, i.e., for finding n such that
$n =\beta (p)$
?’ If so, we choose such n and define
$\varphi ^p(s)=n+1$
, and, if not, we define
$\varphi ^p(s) =0$
.
3 The Borel Hierarchy Theorem
Borel subsets of
$\omega ^{\omega }$
are obtained by the operations of countable union and countable intersection from open and closed subsets of
$\omega ^{\omega }$
. Borel classes of subsets of
$\omega ^{\omega }$
are obtained as follows. The class of the open subsets of
$\omega ^{\omega }$
and the class of the closed subsets of
$\omega ^{\omega }$
are Borel classes, and, given a sequence
$\mathcal {K}_0$
,
$\mathcal {K}_1, \ldots $
of Borel classes, one may form two new classes, the class consisting of all countable unions of sets from
$\bigcup _n\mathcal {K}_n$
and the class consisting of all countable intersections of sets from
$\bigcup _n\mathcal {K}_n$
. Every Borel set belongs to some Borel class. The Borel Hierarchy Theorem is the statement that no Borel class exhausts the collection of all Borel sets.
Although the early descriptive set theorist had their doubts about some of Cantor’s assumptions, they never questioned the use of classical logic. The symmetry of classical logic is heavily used in the classical proof of the Borel Hierarchy Theorem. It is not so easy to formulate and prove a satisfying similar result in a constructive context. Brouwer’s Continuity Principle comes to the rescue, and the resulting theorem may be considered a significant and surprising application of the principle.
3.1 Introducing stumps
Generalized inductive definitions like the following Definition 1 are acceptable intuitionistically, see [Reference Troelstra and Dalen24, vol. I, Section 8.3], where they are introduced in a formal theory called
$\mathbf {IDB}_1$
. They do not occur in [Reference Kleene and Vesley19].
Definition 1.
$\mathbf {Stp}$
, a collection of subsets of
$\omega $
, is defined as follows. The elements of
$\mathbf {Stp}$
are called stumps.
-
(i)
$\emptyset \in \mathbf {Stp}$
. This is the basic element of the set
$\mathbf {Stp}$
. -
(ii) For every infinite sequence
$S_0, S_1, \ldots $
of elements of
$\mathbf {Stp}$
, the set
$S:= \{\langle \;\rangle \}\cup \bigcup \limits _{n \in \omega }\langle n \rangle \ast S_n$
is again an element of
$\mathbf {Stp}$
.This is the construction step of the set
$\mathbf {Stp}$
. -
(iii) Nothing more: every element of
$\mathbf {Stp}$
is obtained by starting from
$\emptyset $
and applying the operation mentioned in (ii) repeatedly.
We shall call
$\mathbf {Stp}$
a class or a set, although it is a totality of a different kind than
$\omega ^{\omega }$
or
$\omega $
. We have a general idea how its members are created but only a very few of these elements have been realized until now.
Stumps take the rôle fulfilled by countable ordinals in classical analysis.
Definition 2. For every non-empty stump S, for every n,
$S\upharpoonright \langle n \rangle = \{s\mid \langle n \rangle \ast s \in S\}$
is called the n-th immediate substump of S.
As we accept Definition 1, we feel entitled to use the following axiom.Footnote 13
Axiom 6 (Induction on
$\mathbf {Stp}$
).
Let
$P\subseteq \mathbf {Stp}$
be given. If
-
(i)
$\emptyset \in P$
and, -
(ii) for every nonempty stump S, if, for all n,
$S\upharpoonright \langle n \rangle \in P$
, then
$S\in P$
,
then
$\mathbf {Stp}=P$
.
Definition 3. We define binary relations
$<, \le $
on the set
$\mathbf {Stp}$
by induction, as follows.
-
(i) For all T in
$\mathbf {Stp}$
,
$\emptyset \le T$
. -
(ii) For all
$S,T$
in
$\mathbf {Stp}$
,
$S<T$
if and only if
$T\neq \emptyset $
and
$\exists n [S \le T\upharpoonright \langle n \rangle ]$
. -
(iii) For all S in
$\mathbf {Stp}$
, if
$S\neq \emptyset $
, then
$S\le T$
if and only if
$\forall m [S\upharpoonright \langle m \rangle < T]$
.
Lemma 4 (Transfinite induction on
$(\mathbf {Stp}, <)$
).
Let
$P\subseteq \mathbf {Stp}$
be given.
If
$\forall T \in \mathbf {Stp}[\forall S\in \mathbf {Stp}[S< T\rightarrow S\in P]\rightarrow T \in P]$
, then
$\mathbf {Stp}=P$
.
Proof Define
$Q:=\{T\in \mathbf {Stp}\mid \forall S\in \mathbf {Stp}[S\le T\rightarrow S\in P]\}$
and prove, using Axiom 6, that
$\mathbf {Stp} =Q$
.
Definition 4. For every stump S we define
$S':=\{s\mid s\notin S \;\wedge \;\forall t[t\sqsubset s\rightarrow t \in S]\}$
. The set
$S'$
is called the border of the stump S.
The border
$S'$
of S consists of those (code numbers of) finite sequences of natural numbers that are just outside S.
The following definition introduces a subclass of the class of stumps, useful for the treatment of Borel sets.
Definition 5.
$\mathbf {Hrs}$
, a collection of subsets of
$\omega $
is defined as follows. The elements of
$\mathbf {Hrs}$
are called hereditarily repetitive nonzero stumps
-
(i)
$\{\langle \;\rangle \} \in \mathbf {Hrs}$
, and -
(ii) for every infinite sequence
$S_0, S_1, \ldots $
of elements of
$\mathbf {Hrs}$
, the set
$S:= \{\langle \;\rangle \}\cup \bigcup \limits _{m, n } \langle (m, n)\rangle \ast S_n$
is again an element of
$\mathbf {Hrs}$
, and -
(iii) nothing more: every element of
$\mathbf {Hrs}$
is obtained by starting from
$\{\langle \;\rangle \}$
and applying the operation mentioned in (ii) repeatedly.
$1^\ast :=\{\langle \;\rangle \}$
is called the basic element of
$\mathbf {Hrs}$
. Note that, for every S in
$\mathbf {Hrs}$
,
$S=1^\ast $
if and only if
$\langle 0 \rangle \notin S$
, so one may decide if
$S=1^\ast $
or not.
For every S in
$\mathbf {Hrs}$
, for every s, s is called an endpoint of S if and only if
$s\in S$
and
$s\ast \langle 0 \rangle \notin S$
. Note that
$\langle \;\rangle $
is an endpoint of
$1^\ast $
and that, for every
$S\ne 1^\ast $
in
$\mathbf {Hrs}$
, for every s, s is and endpoint of S if and only if there exist
$n,t$
such that
$s=\langle n \rangle \ast t$
and t is an endpoint of
$S\upharpoonright \langle n \rangle $
.
Note that, for every S in
$\mathbf {Hrs}$
, for each s, s is an endpoint of S if and only if, for each n,
$s\ast \langle n \rangle $
is en element of the border
$S'$
of S.
Note:
$(1^\ast )' = \{\langle n \rangle \mid n \in \omega \}$
.
3.2 (Positively) Borel sets
The class of the (positively) Borel subsets of
$\omega ^{\omega }$
is the least class of subsets of
$\omega ^{\omega }$
containing the open subsets of
$\omega ^{\omega }$
and the closed subsets of
$\omega ^{\omega }$
that is closed under the operations of countable union and countable intersection. We define this class using hereditarily repetitive nonzero stumps as indices. The constructive mathematician avoids negationFootnote
14
and the operation of taking the complement
$X\setminus Y$
of a given set
$Y\subseteq X$
as much as possible. It is not true, intuitionistically, that the complement
$\omega ^{\omega }\setminus Y$
of a of a given positively Borel set
$Y\subseteq \omega ^{\omega }$
is again positively Borel, see [Reference Veldman33, Section 9.2].
Definition 6 (Borel sets and Borel classes).
For every S in
$\mathbf {Hrs}$
, for every
$\beta $
, we define subsets
$\mathcal {G}^S_\beta $
and
$\mathcal {F}^S_\beta $
of
$\omega ^{\omega }$
, by induction, as follows.
-
(i)
$\mathcal {G}^{1^\ast }_\beta =\{\alpha \mid \exists n[\beta (\overline \alpha n) \neq 0]\}$
and
$\mathcal {F}^{1^\ast }_\beta =\{\alpha \mid \forall n[\beta (\overline \alpha n) = 0]\}$
. -
(ii) For every
$S\neq 1^\ast $
,
$\mathcal {G}^S_\beta = \bigcup _n \mathcal {F}^{S\upharpoonright \langle n \rangle }_{\beta \upharpoonright \langle n \rangle }$
and
$\mathcal {F}^S_\beta = \bigcap _n \mathcal {G}^{S\upharpoonright \langle n \rangle }_{\beta \upharpoonright \langle n \rangle }$
.
For every S in
$\mathbf {Hrs}$
, we define classes
$\mathbf {\Sigma }^0_S$
and
$\mathbf {\Pi }^0_S$
of subsets of
$\omega ^{\omega }$
as follows.
For every
$\mathcal {X}\subseteq \omega ^{\omega }$
,
$\mathcal {X}$
is
$\mathbf {\Sigma }^0_S$
if and only if
$\exists \beta [\mathcal {X}=\mathcal {G}^S_\beta ]$
and
$\mathcal {X}$
is
$\mathbf {\Pi }^0_S$
if and only if
$\exists \beta [\mathcal {X}=\mathcal {F}^S_\beta ]$
.
$\mathcal {X}\subseteq \omega ^{\omega }$
is open if and only if
$\mathcal {X}$
is
$\mathbf {\Sigma }^0_{1^\ast }$
and closed if and only if
$\mathcal {X}$
is
$\mathbf {\Pi }^0_{1^\ast }$
.
$\mathcal {X}\subseteq \omega ^{\omega }$
is
$\mathfrak {Borel}$
if and only if, for some S in
$\mathbf {Hrs}$
,
$\mathcal {X}$
is
$\mathbf {\Sigma }^0_S$
.
In each Borel class, we single out a special element that will turn out to be an element of the class of maximal complexity.
Definition 7 (The leading sets of the hierarchy).
For every S in
$\mathbf {Hrs}$
we define subsets
$\mathcal {E}_S$
and
$\mathcal {A}_S$
of
$\omega ^{\omega }$
as follows.
-
(i)
$\mathcal {E}_{1^\ast }:=\mathcal {G}^{1^\ast }_{Id}:=\{\alpha \mid \exists n[\alpha (\langle n \rangle )\neq 0]\}$
and
$\mathcal {A}_{1^\ast }:=\mathcal {F}^{1^\ast }_{Id}:=\{\alpha \mid \forall n[\alpha (\langle n \rangle )= 0]\}$
. -
(ii) for each hereditarily repetitive nonzero stump S, if
$S\neq 1^\ast $
, then
$\mathcal {E}_S:= \mathcal {G}^S_{Id}=\{\alpha \mid \exists n [\alpha \upharpoonright \langle n \rangle \in \mathcal {A}_{S\upharpoonright \langle n \rangle }]\}$
and
$\mathcal {A}_S:=\mathcal {F}^S_{Id}= \{\alpha \mid \forall n[\alpha \upharpoonright \langle n \rangle \in \mathcal {E}_{S\upharpoonright \langle n \rangle }]\}$
.
It will become clear in Theorem 7 why these sets are called the leading sets of the Borel hierarchy.
Remark 1. One may prove, by induction on
$\mathbf {Hrs}$
, that, for each S in
$\mathbf {Hrs}$
, for all
$\alpha , \beta $
, if
$\alpha \in \mathcal {A}_S$
and
$\beta \in \mathcal {E}_S$
, then
$\alpha \:\#\;\beta $
.
3.3 Games
It is very useful to think of the leading sets of the Borel hierarchy in a game theoretic way, as follows.
Definition 8 (Introducing games and strategies).
Let a hereditarily repetitive nonzero stump S be given, and let also
$\alpha $
in
$\omega ^{\omega }$
be given. We introduce
$\mathbb {G}_S(\alpha )$
, the game in S for
$\alpha $
.
A play in
$\mathbb {G}_S(\alpha )$
goes as follows. Players
$I,II$
start constructing an infinite sequence
$\gamma $
in
$\omega ^{\omega }$
.
I chooses
$\gamma (0)$
,
$II$
chooses
$\gamma (1)$
, I chooses
$\gamma (2)$
,
$\ldots $
The play ends as soon as a position
$\overline \gamma n= \langle \gamma (0), \gamma (1), \ldots , \gamma (n-1)\rangle $
in the border
$S'$
of S is reached. If n is even, then Player I wins the play if and only if
$\alpha (\overline \gamma n)=0$
and, if n is odd, then Player I wins the play if and only if
$\alpha (\overline \gamma n)\neq 0$
. Player
$II$
wins the play if and only if Player I does not win the play.
For all
$\sigma , \tau $
, for all s, we define:
$s\in _I\sigma $
, ‘s is played by Player I according to the strategy
$\sigma $
’, if and only if
$\forall n[2n<length(s)\rightarrow s(2n)=\sigma \big (\overline s(2n)\big )]$
, and
$s\in _{II}\tau $
, ‘s is played by Player
$II$
according to the strategy
$\tau $
’, if and only if
$\forall n[2n+1<length(s)\rightarrow s(2n+1)=\tau \big (\overline s(2n+1)\big )]$
.
For each S in
$\mathbf {Hrs}$
, for each
$\alpha $
, for all
$\sigma ,\tau $
, we define:
$\mathcal {W}^I_S(\sigma , \alpha )$
,
$\sigma $
is a winning strategy for Player I in
$\mathbb {G}_S(\alpha )$
, if and only if
$\forall i\forall s\in S'[s\in _I\sigma \rightarrow \big ( (s\in \omega ^{2i} \rightarrow \alpha (s)= 0)\;\wedge \; (s\in \omega ^{2i+1} \rightarrow \alpha (s)\neq 0)\big )]$
, and:
$\mathcal {W}^{II}_S(\tau , \alpha )$
,
$\tau $
is a winning strategy for Player
$II$
in
$\mathbb {G}_S(\alpha )$
, if and only if
$\forall i\forall s\in S'[s\in _{II}\tau \rightarrow \big ( (s\in \omega ^{2i} \rightarrow \alpha (s)\neq 0)\;\wedge \; (s\in \omega ^{2i+1} \rightarrow \alpha (s)= 0)\big )]$
.
Theorem 5. For every S in
$\mathbf {Hrs}$
,
-
(i) for every
$\alpha $
, for every
$\sigma $
, if
$\mathcal {W}^I(\sigma , \alpha )$
, then
$\alpha \in \mathcal {E}_S$
and -
(ii) for every
$\alpha $
, for every
$\tau $
, if
$\mathcal {W}^{II}_S(\tau , \alpha )$
, then
$\alpha \in \mathcal {A}_S$
. -
(iii) for every
$\alpha $
, if
$ \alpha \in \mathcal {E}_S$
, then, for some
$\sigma $
,
$\mathcal {W}^I_{S}(\sigma , \alpha )$
, and -
(iv) for every
$\alpha $
, if
$ \alpha \in \mathcal {A}_S$
, then, for some
$\tau $
,
$\mathcal {W}^{II}_S(\tau , \alpha )$
.
Proof (i) and (ii). The proof is by induction on
$\mathbf {Hrs}$
.
The case
$S=1^\ast $
is easy and left to the reader.
Now let S be given such that
$S\neq 1^\ast $
and, for each n, for each
$\alpha $
, if
$\exists \sigma [\mathcal {W}_{S\upharpoonright \langle n \rangle }^I(\sigma , \alpha )]$
, then
$\alpha \in \mathcal {E}_{S\upharpoonright \langle n \rangle }$
, and, if
$\exists \tau [\mathcal {W}_{S\upharpoonright \langle n \rangle }^{II}(\tau , \alpha )]$
, then
$\alpha \in \mathcal {A}_{S\upharpoonright \langle n \rangle }$
.
Let
$\sigma , \alpha $
be given such that
$\mathcal {W}^I_S(\sigma , \alpha )$
. Define
$n_0:=\sigma (\langle \;\rangle )$
. Define
$\tau :=\sigma \upharpoonright \langle n_0\rangle $
and note that
$\mathcal {W}^{II}_{S\upharpoonright \langle n_0\rangle }(\tau , \alpha \upharpoonright \langle n_o\rangle )$
. Conclude that
$\alpha \upharpoonright \langle n_0\rangle \in \mathcal {A}_{S\upharpoonright \langle n_0\rangle }$
and
$\alpha \in \mathcal {E}_S$
.
Let
$\tau , \alpha $
be given such that
$\mathcal {W}_S^{II}(\tau , \alpha )$
. Then, for each n,
$\mathcal {W}_{S\upharpoonright \langle n \rangle }^I(\tau \upharpoonright \langle n \rangle , \alpha \upharpoonright \langle n \rangle )$
. Conclude that, for each n,
$\alpha \upharpoonright \langle n \rangle \in \mathcal {E}_{S\upharpoonright \langle n \rangle }$
and
$\alpha \in \mathcal {A}_S$
.
(iii) and (iv). The proof is by induction on
$\mathbf {Hrs}$
.
The case
$S=1^\ast $
is easy and left to the reader.
Now let S be given such that
$S\neq 1^\ast $
and, for each n, for each
$\alpha $
, if
$ \alpha \in \mathcal {E}_{S\upharpoonright \langle n \rangle } $
, then, for some
$\sigma $
,
$\alpha \in \mathcal {W}^I_{S\upharpoonright \langle n \rangle }(\sigma , \alpha )$
, and, if
$ \alpha \in \mathcal {A}_{S\upharpoonright \langle n \rangle } $
, then for some
$\tau $
,
$\alpha \in \mathcal {W}^{II}_{S\upharpoonright \langle n \rangle }(\tau , \alpha )$
,
Let
$\alpha $
be given such that
$\alpha \in \mathcal {E}_S$
. Find n such that
$\alpha \upharpoonright \langle n \rangle \in \mathcal {A}_{S\upharpoonright \langle n \rangle }$
. Find
$\tau $
such that
$\mathcal {W}^{II}_{S\upharpoonright \langle n \rangle } (\tau , \alpha \upharpoonright \langle n \rangle )$
. Define
$\sigma $
such that
$\sigma (\langle \;\rangle )=n$
and
$\sigma \upharpoonright \langle n \rangle =\tau $
and note that
$\mathcal {W}^I_S(\sigma , \alpha )$
.
Let
$\alpha $
be given such that
$\alpha \in \mathcal {A}_S$
. Then
$\forall n[\alpha \upharpoonright \langle n \rangle \in \mathcal {E}_{S\upharpoonright \langle n \rangle }]$
and
$\forall n\exists \sigma [\mathcal {W}^I_{S\upharpoonright \langle n \rangle }(\sigma , \alpha \upharpoonright \langle n \rangle )]$
. Using the Second Axiom of Countable Choice, Axiom 3, find
$\tau $
such that
$\forall n[\mathcal {W}^I_{S\upharpoonright \langle n\rangle }(\tau \upharpoonright \langle n \rangle , \alpha \upharpoonright \langle n \rangle )]$
and note that
$\mathcal {W}^{II}_S(\tau , \alpha )$
.
Definition 9. For every S in
$\mathbf {Hrs}$
, for every
$\tau $
, for every
$\alpha $
, we let
$\tau \Join _S^{II}\alpha $
, ‘
$\alpha $
-as-corrected by the strategy
$\tau $
for Player
$II$
in
$\mathbb {G}_S(\alpha )$
’, be the element of
$\omega ^{\omega } $
such that, for all s in the border
$S'$
of S,
-
(i) if
$length(s)$
is even, then
$(\tau \Join _S^{II}\alpha )(s) =\max \big (1, \alpha (s)\big )$
, and, -
(ii) if
$length(s)$
is odd, then
$(\tau \Join _S^{II}\alpha )(s) =0,$
and, for all s, if s is not in the border
$S'$
of S, then
$(\tau \Join _S^{II}\alpha )(s)=\alpha (s)$
.
Remark 2. Note that, for every S in
$\mathbf {Hrs}$
, for every
$\alpha $
,
$\alpha \in \mathcal {A}_S$
if and only if, for some
$\tau $
,
$\alpha = \tau \Join ^{II}_S\alpha $
.
The following Lemma will be a crucial tool in the proof of the Hierarchy Theorem.
Lemma 6 (A consequence of Brouwer’s Continuity Principle).
For every S in
$\mathbf {Hrs}$
, for every relation
$R\subseteq \omega ^{\omega }\times \omega $
, if
$\forall \alpha \in \mathcal {A}_S\exists n[\alpha R n]$
, then
$\forall \alpha \in \mathcal {A}_S\exists p\exists q\forall \beta \in \mathcal {A}_S[\big (\beta (0)=\alpha (0) \;\wedge \;\forall n<p[\beta \upharpoonright \langle n\rangle =\alpha \upharpoonright \langle n\rangle ]\big )\rightarrow \beta Rq]$
.
Proof Assume that
$\forall \alpha \in \mathcal {A}_S\exists n[\alpha Rn]$
. Conclude that
$\forall \alpha \forall \tau \exists n[(\tau \Join ^{II}_S\alpha )Rn]$
. Let
$\alpha $
in
$\mathcal {A}_S$
be given. Using Theorem 5(iv), find
$\tau $
such that
$\alpha = \tau \Join _S^{II}\alpha $
. Using Brouwer’s Continuity Principle, Axiom 1, find
$m,q$
such that
$\forall \beta \forall \sigma [(\overline \alpha m\sqsubset \beta \;\wedge \; \overline \tau m\sqsubset \sigma )\rightarrow (\sigma \Join ^{II}_S \beta )Rq]$
. Find p such that, for all s, if
$s\le m$
, then
$s(0)< p$
. Note that, for all
$\beta $
in
$\mathcal {A}_S$
, if
$\beta (0)=\alpha (0)$
and
$\forall n<p[\beta \upharpoonright \langle n \rangle =\alpha \upharpoonright \langle n \rangle ]$
, then
$\overline \alpha m \sqsubset \beta $
and, for some
$\sigma $
,
$\overline \tau m\sqsubset \sigma $
and
$\beta =\sigma \Join ^{II}_S\beta $
, and, therefore,
$\beta Rq$
.
3.4 (Wadge-)reducibility
The following notion of reducibility is very important. In classical descriptive set theory this notion is called Wadge-reducibility. Its analog in computability theory is many-one-reducibility.
Definition 10 (Reducibility).
For all
$\mathcal {X}, \mathcal {Y}\subseteq \omega ^{\omega }$
, for all
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
we define:
$\varphi $
reduces
$\mathcal {X}$
to
$\mathcal {Y}$
if and only if, for every
$\alpha $
,
$\alpha \in \mathcal {X} \leftrightarrow \varphi |\alpha \in \mathcal {Y}$
.
For all
$\mathcal {X}, \mathcal {Y}\subseteq \omega ^{\omega }$
, we define:
$\mathcal {X}\preceq \mathcal {Y}$
,
$\mathcal {X}$
reduces to
$\mathcal {Y}$
, if and only if there exists
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
reducing
$\mathcal {X}$
to
$\mathcal {Y}$
.
Theorem 7 (
$\mathcal {E}_S$
,
$\mathcal {A}_S$
are complete elements of
$\mathbf {\Sigma }^0_S$
,
$\mathbf {\Pi }^0_S$
, respectively).
For each S in
$\mathbf {Hrs}$
, for every
$\mathcal {X}\subseteq \omega ^{\omega }$
,
$\mathcal {X}\subseteq \omega ^{\omega }$
is
$\mathbf {\Sigma }^0_S$
if and only if
$\mathcal {X}\preceq \mathcal {E}_S$
, and
$\mathcal {X}\subseteq \omega ^{\omega }$
is
$\mathbf {\Pi }^0_S$
if and only if
$\mathcal {X}\preceq \mathcal {A}_S$
.
Proof The proof that, for each S in
$\mathbf {Hrs}$
,
$\mathcal {E}_S$
is
$\mathbf {\Sigma }^0_S$
and
$\mathcal {A}_S$
is
$\mathbf {\Pi }^0_S$
is left to the reader. Also the proof that, for each S in
$\mathbf {Hrs}$
, for all
$\mathcal {X}, \mathcal {Y}\subseteq \omega ^{\omega }$
, if
$\mathcal {X}\preceq \mathcal {Y}$
, then, if
$\mathcal {Y}$
is
$\mathbf {\Sigma }^0_S$
, then
$\mathcal {X}$
is
$\mathbf {\Sigma }^0_S$
and, if
$\mathcal {Y}$
is
$\mathbf {\Pi }^0_S$
, then
$\mathcal {X}$
is
$\mathbf {\Pi }^0_S$
, is left to the reader.
We now prove that, for each S in
$\mathbf {Hrs}$
, for each
$\beta $
, there exists
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
reducing both
$\mathcal {G}^S_\beta $
to
$\mathcal {E}_S$
and
$\mathcal {F}^S_\beta $
to
$\mathcal {A}_S$
and we do so by induction on
$\mathbf {Hrs}$
.
We first consider the case that
$S=\{\langle \;\rangle \}=1^\ast $
is the basic element of
$\mathbf {Hrs}$
. Let
$\beta $
be given. Define
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
such that, for each
$\alpha $
, for each n,
$(\varphi |\alpha )(\langle n\rangle )=\beta (\overline \alpha n)$
, and note that
$\varphi $
reduces
$\mathcal {G}^{1^\ast }_\beta $
to
$\mathcal {E}_{1^\ast }$
and
$\mathcal {F}^{1^\ast }_\beta $
to
$\mathcal {A}_{1^\ast }$
.
Now let S be a non-basic element of
$\mathbf {Hrs}$
. Let
$\beta $
be given. Using the induction hypothesis and the Second Axiom of Countable ChoiceFootnote
15
, find
$\varphi $
such that, for each n,
$\varphi ^n:\omega ^{\omega }\rightarrow \omega ^{\omega }$
reduces
$\mathcal {G}^{S\upharpoonright \langle n \rangle }_{\beta \upharpoonright \langle n \rangle }$
to
$\mathcal {E}_{S\upharpoonright \langle n \rangle }$
and
$\mathcal {F}^{S\upharpoonright \langle n \rangle }_{\beta \upharpoonright \langle n \rangle }$
to
$\mathcal {A}_{S\upharpoonright \langle n \rangle }$
. Define
$\psi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
such that, for each
$\alpha $
, for each n,
$(\psi |\alpha )\upharpoonright \langle n \rangle = \varphi ^n|(\alpha \upharpoonright \langle n\rangle )$
and note that
$\psi $
reduces
$\mathcal {G}^S_\beta $
to
$\mathcal {E}_S$
and
$\mathcal {F}^S_\beta $
to
$\mathcal {A}_S$
.
Corollary 8.
-
(i) For all
$S, T$
in
$\mathbf {Hrs}$
, if
$S\le T$
, then
$\mathbf {\Pi }^0_S \subseteq \mathbf {\Pi }^0_T$
and
$\mathbf {\Sigma }^0_S \subseteq \mathbf {\Sigma }^0_T$
. -
(ii) For all
$S, T$
in
$\mathbf {Hrs}$
, if
$S< T$
, then
$\mathbf {\Pi }^0_S \subseteq \mathbf {\Sigma }^0_T$
and
$\mathbf {\Sigma }^0_S \subseteq \mathbf {\Pi }^0_T$
.
Proof (i) One may prove this by showing that, for all
$T,S$
in
$\mathbf {Hrs}$
, if
$S\le T$
, then
$\mathcal {A}_S\preceq \mathcal {A}_T$
and
$\mathcal {E}_S\preceq \mathcal {E}_T$
. One does so by induction on
$\mathbf {Hrs}$
.
(ii) Note that, for each
$S\neq 1^\ast $
in
$\mathbf {Hrs}$
, for each n,
$\mathcal {E}_{S\upharpoonright \langle n \rangle } \preceq \mathcal {A}_S$
and
$\mathcal {A}_{S\upharpoonright \langle n \rangle } \preceq \mathcal {E}_S$
. Also, for all
$S,T$
in
$\mathbf {Hrs}$
,
$S<T$
if and only
$\exists n[S\le T\upharpoonright \langle n \rangle ]$
. Using the just given proof of (i), one easily obtains the desired conclusion.
Definition 11. For each S in
$\mathbf {Hrs}$
, we define canonical elements
$\varepsilon ^{\ast }_S$
,
$\alpha ^{\ast }_S$
, of the sets
$\mathcal {E}_S$
,
$\mathcal {A}_S$
, respectively, as follows.
-
(i)
$\forall s[(s\notin S' \rightarrow \varepsilon ^\ast _S(s)=0]$
and -
(ii)
$\forall i \forall s\in S'[ \big (s\in \omega ^{2i} \rightarrow \varepsilon ^\ast _S(s)=0\big )\;\wedge \; \big (s\in \omega ^{2i+1} \rightarrow \varepsilon ^\ast _S(s)=1\big )]$
, and -
(iii)
$\forall s[(s\notin S' \rightarrow \alpha ^\ast _S(s)=0]$
and -
(iv)
$\forall i \forall s\in S'[ \big (s\in \omega ^{2i} \rightarrow \alpha ^\ast _S(s)=1\big )\;\wedge \; \big (s\in \omega ^{2i+1} \rightarrow \alpha ^\ast _S(s)=0\big )]$
.
Remark 3. Note that, for every S in
$\mathbf {Hrs}$
, for every
$\sigma $
,
$\mathcal {W}^I_S(\sigma , \varepsilon ^\ast _S)]$
, and, for every
$\tau $
,
$\mathcal {W}^{II}_S(\tau , \alpha _S^\ast )]$
.
3.5 The Hierarchy Theorem
We would like to prove the statement that, for each S in
$\mathbf {Hrs}$
,
$\mathbf {\Pi }^0_S$
is not a subclass of
$\mathbf {\Sigma }^0_S$
and, conversely,
$\mathbf {\Sigma }^0_S$
is not a subclass of
$\mathbf {\Pi }^0_S$
. We are going to prove a stronger and more positive statement. We shall make use of the following technical notion.
Definition 12 (Freedom in spreads).
Let
$\beta $
be a spread-law and let
${\mathcal {F}=\mathcal {F}_\beta }$
be the corresponding spread. Let t be given.
We define: t is free in
$\mathcal {F}$
if and only if, for all
$s=\langle s(0), s(1), \ldots , s(t-1)\rangle $
in
$\omega ^t$
, if
$\beta (s)=0$
, then, for all m,
$\beta (s\ast \langle m \rangle )=0$
.
We define: t is completely free in
$\mathcal {F}$
if and only if, for all u such that
$t\sqsubseteq u$
, u is free in
$\mathcal {F}$
.
Remark 4. If t is free in
$\mathcal {F}=\mathcal {F}_\beta $
, then, when building, step-by-step, an element
$\alpha $
of
$\mathcal {F}$
, and having defined
$\alpha (0), \ldots , \alpha (t-1)$
, we may choose any number m as a value of
$\alpha (t)$
. The spread-law
$\beta $
does not impose any restriction on our freedom of choice at t.
We shall prove that, for each S in
$\mathbf {Hrs}$
,
$\mathbf {\Pi }^0_S$
is not a subclass of
$\mathbf {\Sigma }^0_S$
by showing that every
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
mapping
$\mathcal {A}_S$
into
$\mathcal {E}_S$
positively fails to reduce
$\mathcal {A}_S$
to
$\mathcal {E}_S$
, and, similarly, we prove that, for each S in
$\mathbf {Hrs}$
,
$\mathbf {\Sigma }^0_S$
is not a subclass of
$\mathbf {\Pi }^0_S$
by showing that every
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
mapping
$\mathcal {E}_S$
into
$\mathcal {A}_S$
positively fails to reduce
$\mathcal {E}_S$
to
$\mathcal {A}_S$
, i.e.,
Theorem 9 (Borel Hierarchy Theorem).
-
(i) For every S in
$\mathbf {Hrs}$
, for every
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
, if
$\forall \alpha [\alpha \in \mathcal {A}_S\rightarrow \varphi |\alpha \in \mathcal {E}_S]$
, then
$\exists \alpha [\alpha \in \mathcal {E}_S \;\wedge \; \varphi |\alpha \in \mathcal {E}_S]$
. -
(ii) For every S in
$\mathbf {Hrs}$
, for every
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
, if
$\forall \alpha [\alpha \in \mathcal {E}_S\rightarrow \varphi |\alpha \in \mathcal {A}_S]$
, then
$\exists \alpha [\alpha \in \mathcal {A}_S \;\wedge \; \varphi |\alpha \in \mathcal {A}_S]$
.
Proof (i) Let S in
$\mathbf {Hrs}$
be given. Let
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
be given such that
$\forall \alpha [\alpha \in \mathcal {A}_S\rightarrow \varphi |\alpha \in \mathcal {E}_S]$
. We are going to construct
$\alpha , \sigma , \tau $
such that
$\mathcal {W}^{I}_S(\sigma , \alpha )$
and
$\mathcal {W}^{I}_S(\tau , \varphi |\alpha )$
, and, therefore, both
$\alpha $
and
$\varphi |\alpha $
are in
$\mathcal {E}_S$
.
We do so by building an infinite sequence
$\mathcal {F}_0, \mathcal {F}_1, \mathcal {F}_2, \ldots $
of spreads such that
-
a.
$\mathcal {F}_0 = \omega ^{\omega }$
and for each t,
$\mathcal {F}_{t+1}\subseteq \mathcal {F}_t$
, and, for each s, if
$length(s)<length(t)$
, then s is admitted by the spread-law defining
$\mathcal {F}_t$
if and only if s is admitted by the spread-law defining
$\mathcal {F}_{t+1}$
. -
b. for all
$i,t, u$
, if
$t,u\in \omega ^{2i}$
and
$t \in S$
and
$t\in _I \sigma $
and
$u\in _I\tau $
and
$t_{II}=u_{II}$
, then-
b1. t is completely free in
$\mathcal {F}_t$
, and -
b2.
$u\in S$
and
$S\upharpoonright t=S\upharpoonright u$
, and -
b3.
$\forall \alpha \in \mathcal {F}_t[\alpha \upharpoonright t \in \mathcal {A}_{S\upharpoonright t} \rightarrow (\varphi |\alpha )\upharpoonright u \in \mathcal {E}_{S\upharpoonright u}]$
, and, -
b4. if t is an endpoint of S, then u is an endpoint of S and
$\forall \alpha \in \mathcal {F}_{t+1}[ \alpha (t\ast \langle \sigma (t)\rangle )=(\varphi |\alpha )(u\ast \langle \delta (u)\rangle ) =1 ]$
, and, -
b5. if
$t\ast \langle \sigma (t)\rangle $
is an endpoint of S, then
$u\ast \langle \tau (u)\rangle $
is an endpoint of S and
$\forall \alpha \in \mathcal {F}_{t+1}\forall n[ \alpha (t\ast \langle \sigma (s), n\rangle )=(\varphi |\alpha )(u\ast \langle \delta (u), n\rangle = 0]$
.
-
Note that, as
$\mathcal {F}_0=\omega ^{\omega }$
, conditions b1, b2 and b3 are satisfied for
$i=0$
.
Now let t be given. We want to define
$\mathcal {F}_{t+1}$
and distinguish two cases.
Case (i)
$t\notin S$
, or
$\exists i[t\in \omega ^{2i+1}]$
, or
$t\notin _I\sigma $
. We define
$\mathcal {F}_{t+1}=\mathcal {F}_t$
.
Case (ii).
$t\in S$
, and
$\exists i[t\in \omega ^{2i}]$
, and
$t\in _I\sigma $
. We now determine u such that
$length(u)=length(t)$
and
$u\in _I\tau $
and
$t_{II}=u_{II}$
. We then know
$S\upharpoonright t=S\upharpoonright u$
and t is completely free in
$\mathcal {F}_t$
and
$\forall \alpha \in \mathcal {F}_t[\alpha \upharpoonright t \in \mathcal {A}_{S\upharpoonright t} \rightarrow (\varphi |\alpha )\upharpoonright u \in \mathcal {E}_{S\upharpoonright u}]$
. We have to define
$\mathcal {F}_{t+1}$
but also
$\sigma (t)$
and
$\tau (u)$
.
We again distinguish two cases.
Case (ii)(I).
$S\upharpoonright t= S\upharpoonright u =1^\ast =\{\langle \;\rangle \}$
, i.e.,
$t,u$
are endpoints of S. Note that
$\forall \alpha \in \mathcal {F}_t[\alpha \upharpoonright t \in \mathcal {A}_{1^\ast }\rightarrow (\varphi |\alpha )\upharpoonright u \in \mathcal {E}_{1^\ast }]$
. Find
$\eta $
in
$\mathcal {F}_t$
such that
$\forall n[\eta (t\ast \langle n \rangle )=0]$
, i.e.,
$ \eta \upharpoonright t \in \mathcal {A}_{1^\ast }$
. Note that
$(\varphi |\eta )\upharpoonright u \in \mathcal {E}_{1^\ast }$
, and find q such that
$(\varphi |\eta )(u\ast \langle q\rangle )\neq 0$
. Define
$\tau (u):=q$
. Find p such that
$\overline {\varphi |\eta }(u\ast \langle \tau (u) \rangle +1)\sqsubseteq \varphi |(\overline \eta p)$
. Find r such that
$t\ast \langle r\rangle \ge p$
. Note that
$t\ast \langle r\rangle $
is free in
$\mathcal {F}_t$
. Define
$\sigma (t):=r$
. Find c such that
$\overline \eta \tau (u)\sqsubset c$
and
$c(t\ast \langle \sigma (t) \rangle ) =1$
and c is admitted by
$\mathcal {F}_t$
. Define
$\mathcal {F}_{t+1}= \mathcal {F}_t \cap c$
.
Note that, for every
$\alpha $
in
$\mathcal {F}_{t+1}$
,
$\alpha (t\ast \langle \sigma (t)\rangle ) =1$
and
$(\varphi |\alpha )(u\ast \langle \tau (u)\rangle )=1$
, i.e., both
$\alpha \upharpoonright t$
and
$(\varphi |\alpha )\upharpoonright u$
are in
$\mathcal {E}_{1^\ast }$
. Also note that for all
$v\perp t$
, if v is (completely) free in
$\mathcal {F}_t$
, then v is (completely) free in
$\mathcal {F}_{t+1}$
.
Case (ii)(II).
$S\upharpoonright t= S\upharpoonright u \neq 1^\ast $
, i.e.,
$t,u$
are no endpoints of S. Find
$\eta $
in
$\mathcal {F}_t$
such that
$\eta \upharpoonright t =\alpha ^\ast _{S\upharpoonright t}\in \mathcal {A}_{S\upharpoonright t}$
. We define
$\psi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
such that, for each
$\beta $
,
-
(1)
$\forall u[\neg (t\sqsubseteq u)\rightarrow (\psi |\beta )(u)=\eta (u)]$
, and -
(2)
$(\varphi |\beta )\upharpoonright t=\beta $
.
Note that, for all
$\beta $
, if
$\beta \in \mathcal {A}_{S\upharpoonright t}$
, then
$(\psi |\beta )\upharpoonright t \in \mathcal {A}_{S \upharpoonright t}$
and
$\big (\varphi |(\psi |\beta )\big )\upharpoonright u \in \mathcal {E}_{S\upharpoonright u}$
. In particular, this is true for
$\beta = \alpha ^\ast _{S\upharpoonright t}$
. Note that
$\psi |(\alpha ^\ast _{S\upharpoonright t})=\;\eta $
. Using Lemma 6, find
$p, q$
such that, for each
$\beta $
, if
$\beta \in \mathcal {A}_{S\upharpoonright t}$
and
$\beta (0)=\alpha ^\ast _{S\upharpoonright t}(0)$
and
$\forall n <p[\beta \upharpoonright \langle n \rangle = \alpha ^\ast _{S\upharpoonright t}\upharpoonright \langle n \rangle ]$
, then
$\big (\varphi |(\psi |\beta )\big )\upharpoonright u\ast \langle q\rangle \in \mathcal {A}_{S\upharpoonright u\ast \langle q \rangle }$
. Define
$\tau (u)=q$
. Find
$r>p$
such that
$S\upharpoonright t\ast \langle r \rangle = S\upharpoonright u\ast \langle q \rangle = S\upharpoonright u \ast \langle \tau (u)\rangle $
and define
$\sigma (t)=r$
. Define
$\mathcal {F}= \{\alpha \in \mathcal {F}_t \mid \forall u [(t\sqsubset u \;\wedge \;u\perp t\ast \langle \sigma (t)\rangle )\rightarrow \alpha (u)=\eta (u)]\}$
. Note that
$t\ast \langle \sigma (t)\rangle $
is completely free in
$\mathcal {F}$
. Also note that, for each v, if
$v \perp t$
and v is completely free in
$\mathcal {F}_t$
, then v is completely free in
$\mathcal {F}$
. Note that
$\forall \alpha \in \mathcal {F}[\alpha \upharpoonright t\ast \langle \gamma (t)\rangle \in \mathcal {E}_{S\upharpoonright t\ast \langle \gamma (t)\rangle }\rightarrow (\varphi |\alpha )\upharpoonright u\ast \langle \delta (u)\rangle \in \mathcal {A}_{S\upharpoonright u\ast \langle \delta (u)\rangle }]$
.
We distinguish two subcases of Case (ii)(II).
Case (ii)(II)a.
$t\ast \langle \sigma (t)\rangle $
and
$u\ast \langle \tau (u)\rangle $
are endpoints of S. Define
$\mathcal {F}_{t+1}= \{\alpha \in \mathcal {F} \mid \forall n[\alpha (t\ast \langle \sigma (t), n \rangle )=0]\}$
. We claim that
$\forall \alpha \in \mathcal {F}_{t+1} \forall n[(\varphi |\alpha )(u\ast \langle \tau (u), n\rangle )=0]$
. We prove this claim as follows. Assume we find
$\alpha $
in
$\mathcal {F}_{t+1}$
and n such that
$(\varphi |\alpha )(u\ast \langle \tau (u), n\rangle )\neq 0$
. Find m such that
$\overline {\varphi |\alpha }(u\ast \langle \tau (u),n\rangle +1)\sqsubseteq \varphi |\overline \alpha m$
. Find
$\alpha ^\diamond $
in
$\mathcal {F}_{t+1}$
such that
$\overline \alpha m \sqsubset \alpha ^\diamond $
and, for some p,
$\alpha ^\diamond (t\ast \langle \sigma (t), p\rangle )\neq 0$
. Note that both
$\alpha ^\diamond \upharpoonright t\ast \langle \sigma (t)\rangle $
and
$(\varphi |\alpha ^\diamond )\upharpoonright u\ast \langle \tau (u)\rangle $
are in
$\mathcal {E}_{1^\ast }$
. Contradiction. We have to conclude that
$\forall \alpha \in \mathcal {F}_{t+1} \forall n[(\varphi |\alpha )(u\ast \langle \tau (u), n\rangle )=0]$
.
Case (ii)(II)b.
$t\ast \langle \sigma (t)\rangle $
and
$u\ast \langle \tau (u)\rangle $
are no endpoints of S. Define
$\mathcal {F}_{t+1} =\mathcal {F}$
. Note that
$\forall \varepsilon \in \mathcal {F}_{t+1}[\varepsilon \upharpoonright t\ast \langle \sigma (t)\rangle \in \mathcal {E}_{S\upharpoonright t\ast \langle \sigma (t)\rangle }\rightarrow (\varphi |\varepsilon )\upharpoonright u\ast \langle \tau (u)\rangle \in \mathcal {A}_{S\upharpoonright u\ast \langle \delta (u)\rangle }]$
. Conclude that
$\forall \alpha \in \mathcal {F}_{t+1}\forall n[\alpha \upharpoonright t\ast \langle \sigma (t),n\rangle \in \mathcal {A}_{S\upharpoonright t\ast \langle \gamma (t),n\rangle }\rightarrow (\varphi |\alpha )\upharpoonright u\ast \langle \tau (u), n\rangle \in \mathcal {E}_{S\upharpoonright u\ast \langle \delta (u),n\rangle }]$
. Also note that, for each n,
$t\ast \langle \sigma (t), n\rangle $
is completely free in
$\mathcal {F}_{t+1}$
.
This concludes the definition of the sequence
$\mathcal {F}_0, \mathcal {F}_1, \ldots $
.
Using the fact that condition a is satisfied, find
$\alpha $
such that for each t,
$\alpha \in \mathcal {F}_t$
.
Conclude from the fact that conditions b4 and b5 are satisfied that, for all t in the border
$S'$
of S such that
$t\in _I\sigma $
, if
$length(t)$
is even, then
$\alpha (t)=0$
and, if
$length(t)$
is odd, then
$\alpha (t)=1$
, and that, for all u in the border
$S'$
of S such that
$u\in _I\tau $
, if
$length(u)$
is even, then
$(\varphi |\alpha )(u)=0$
and, if
$length(u)$
is odd, then
$(\varphi |\alpha )(u)=1$
.
Conclude
$\mathcal {W}^{I}_S(\sigma , \alpha )$
and
$\mathcal {W}^{I}_S(\tau , \varphi |\alpha )$
and: both
$\alpha $
and
$\varphi |\alpha $
are in
$\mathcal {E}_S$
.
(ii) Let S in
$\mathbf {Hrs}$
and
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
be given such that
$\forall \alpha [\alpha \in \mathcal {E}_S \rightarrow \varphi |\alpha \in \mathcal {A}_S]$
. Find T in
$\mathbf {Hrs}$
such that
$\forall n[T\upharpoonright \langle n \rangle = S]$
.Footnote
16
Define
$\psi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
such that
$\forall \alpha \forall n[(\psi |\alpha )\upharpoonright \langle n \rangle = \varphi |(\alpha \upharpoonright \langle n \rangle )]$
. Note that
$\forall \alpha [\alpha \in \mathcal {A}_T\rightarrow \forall n[(\psi |\alpha )\upharpoonright \langle n \rangle \in \mathcal {A}_S]$
. Find
$\rho :\omega ^{\omega }\rightarrow \omega ^{\omega }$
such that
$\forall \beta [\forall n[\beta \upharpoonright \langle n \rangle \in \mathcal {A}_S] \leftrightarrow \rho |\beta \in \mathcal {A}_S]$
.Footnote
17
Define
$\zeta :\omega ^{\omega }\rightarrow \omega ^{\omega }$
such that, for all
$\alpha $
, for all n,
$(\zeta |\alpha )\upharpoonright \langle n \rangle = \rho |(\psi |\alpha )$
. Note that, for every
$\alpha $
, if
$\alpha \in \mathcal {A}_T$
, then
$\zeta |\alpha \in \mathcal {E}_T$
. Using (i), find
$\alpha $
in
$\mathcal {E}_T$
such that
$\zeta |\alpha \in \mathcal {E}_T$
. Find n such that
$\alpha \upharpoonright \langle n \rangle \in \mathcal {A}_{T\upharpoonright \langle n \rangle }=\mathcal {A}_S$
. Find m such that
$(\zeta |\alpha )\upharpoonright \langle m \rangle \in \mathcal {A}_{T\upharpoonright \langle m \rangle }=\mathcal {A}_S$
. Note that
$(\zeta |\alpha )\upharpoonright \langle m \rangle = \rho |(\psi |\alpha ) \in \mathcal {A}_S$
and conclude that
$(\psi |\alpha )\upharpoonright \langle n \rangle =\varphi |(\alpha \upharpoonright \langle n \rangle ) \in \mathcal {A}_S$
. Defining
$\beta :=\alpha \upharpoonright \langle n \rangle $
, we thus see that both
$\beta $
and
$\varphi |\beta $
are in
$\mathcal {A}_S$
.
4 The Fan Theorem
The Fan Theorem was presented by Brouwer as a theorem but the argument he gave for the Theorem is philosophical rather than mathematical, and it is perhaps better to call the Theorem an axiom and the so-called ‘proof’ a plausibility argument. In fact, Brouwer ‘proved’ a more general statement that we will treat in Section 6. We have narrowed down Brouwer’s argument for the more general statement to an argument for its special case, the Fan Theorem. We also see how one uses the Fan Theorem in order to obtain the Uniform-Continuity Theorem. We conclude with an observation on Bishop’s attempt to avoid the Fan Theorem.
4.1 Finitary spreads
Definition 13. A spread-law
$\beta $
will be called finitary if it satisfies the following condition:
$$\begin{align*}\forall s[\beta(s)=0\rightarrow \exists m\forall n[\beta(s\ast\langle n \rangle)=0\rightarrow n\le m]]. \end{align*}$$
If the spread-law
$\beta $
is finitary, the corresponding spread
$\mathcal {F}_\beta $
will be called a finitary spread or a fan.
When I am creating an element
$\alpha $
of a fan
$\mathcal {F}_\beta $
, then, at each stage n, having completed an initial part
$\alpha (0), \alpha (1), \ldots , \alpha (n-1)$
of
$\alpha $
, I only have finitely many choices for the next value,
$\alpha (n)$
.
An important example of a fan is Cantor space
$2^{\omega }:=\mathcal {C}:=\{\alpha \mid \forall n[\alpha (n) \le 1]\}$
.
Definition 14. For all
$\mathcal {X}\subseteq \omega ^{\omega }$
, for all
$B\subseteq \omega $
, we define: B is a bar in
$\mathcal {X}$
,
$Bar_{\mathcal {X}}(B)$
, if and only if
$\forall \alpha \in \mathcal {X}\exists n[\overline \alpha n \in B]$
.
Theorem 10 (Fan Theorem).
Let
$\beta $
be a finitary spread-law. If
$B\subseteq \omega $
is a bar in
$\mathcal {F}_\beta $
, some finite
$B'\subseteq B$
is bar in
$\mathcal {F}_\beta $
.
Proof One may argue for the Fan Theorem as follows.Footnote 18
Assume
$\beta $
is a finitary spread-law and let
$B\subseteq \omega $
be a bar in
$\mathcal {F}_\beta $
.
I now ask the philosophical question: ‘How may I have convinced myself that B is indeed a bar in
$\mathcal {F}_\beta $
?’ (Under what circumstances shall we say that this conclusion is justified? Some agreement here is, intuitionistically, the only way to make sense of the statement).
We introduce the following notion in order to discuss this question. For each s such that
$\beta (s)=0$
, we will say that B bars s in
$\mathcal {F}_\beta $
if and only if
$Bar_{\mathcal {F}_\beta \cap s}(B)$
, i.e.,
$\forall \alpha \in \mathcal {F}_\beta [ s\sqsubset \alpha \rightarrow \exists n[\overline \alpha n \in B]]$
. Observe the following:
-
(i) For each s, if
$\beta (s) =0$
and
$s\in B$
, then B bars s in
$\mathcal {F}_\beta $
. -
(ii) For each s, if
$\beta (s)=0$
and, for every n such that
$\beta (s\ast \langle n \rangle )=0$
, B bars
$s\ast \langle n \rangle $
in
$\mathcal {F}_\beta $
, then B bars s in
$\mathcal {F}_\beta $
. -
(iii) For each s, if
$\beta (s)=\beta (s\ast \langle n \rangle )=0$
and B bars s in
$\mathcal {F}_\beta $
, then B bars
$s\ast \langle n \rangle $
in
$\mathcal {F}_\beta $
.
Note that one may prove a statement of the form ‘B bars s in
$\mathcal {F}_\beta $
’ by starting from observations of the form (i) and using observations of the form (ii) and (iii) as reasoning steps. Such a proof will be called a canonical proof
Footnote
19
. Let us now agree to consider the statement ‘B bars s in
$\mathcal {F}_\beta $
’ as established or true if and only if we are able to provide a canonical proof of ‘B bars s’.
This agreement marks an important point in the development of our intuitionistic mathematics. We are introducing an axiomatic assumption.
We now may argue as follows.
Assume
$Bar_{\mathcal {F}_\beta }(B)$
, i.e., B bars
$\langle \; \rangle $
in
$\mathcal {F}_\beta $
. Find a canonical proof of this statement. Now replace in this canonical proof every statement ‘B bars s in
$\mathcal {F}_\beta $
’ by ‘B finitely bars s in
$\mathcal {F}_\beta $
’ where the latter means: ‘some finite
$B'\subseteq B$
bars s in
$\mathcal {F}_\beta $
’. Under this replacement our canonical proof changes into another valid proof. In order to see this, we have to use the fact that a finite union of finite sets of integers is itself a finite set of integers. The conclusion of the new proof will be: ‘some finite
$B'\subseteq B$
bars
$\langle \;\rangle $
in
$\mathcal {F}_\beta $
’ and that is what we wanted to establish.
4.2 The Uniform-Continuity Theorem
The following result is the first application of the Fan Theorem.
Theorem 11. Every pointwise continuous function from
$[0,1]$
to
$\mathcal {R}$
is uniformly continuous on
$[0,1]$
.
Proof Let f be a pointwise continuous function from
$[0,1]$
to
$\mathcal {R}$
. We define
$\rho $
such that, for each s in
$2^{<\omega }$
,
$\rho (s)=\big (\rho '(s), \rho "(s)\big )$
is a pair of rationals. We do so by induction on the length of the argument.
$\rho (\langle \;\rangle ):= (0,1)$
and, for each s in
$2^{<\omega }$
,
$\rho (s\ast \langle 0 \rangle )):= \big (\rho '(s), \frac {1}{3}\rho '(s) + \frac {2}{3}\rho "(s)\big )$
and
$\rho (s\ast \langle 1 \rangle ):=\big (\frac {2}{3}\rho '(s) +\frac {1}{3}\rho "(s), \rho "(s)\big )$
.
Let m be given. We have to prove
$\exists n \forall x \in [0,1]\forall y \in [0,1][|x-y|<\frac {1}{2^n}\rightarrow |f(x)-f(y)|<\frac {1}{2^m}]$
. We define, for all rationals
$p,q$
such that
$0\le p < q\le 1$
,
$[p,q]$
is fine if and only if
$\exists n \forall x \in [p,q]\forall y \in [p,q][|x-y|<\frac {1}{2^n}\rightarrow |f(x)-f(y)|<\frac {1}{2^m}]$
. Our aim is to prove that
$[0,1]$
is fine.
Let B be the set of all s in
$2^{<\omega }$
such that
$[\rho '(s), \rho "(s)]$
is fine. We show that B is a bar in Cantor space
$2^{\omega }$
. Let
$\alpha $
in
$2^{\omega }$
be given. Find a real x such that, for all n,
$\rho '(\overline \alpha n)\le x \le \rho "(\overline \alpha n)$
. As f is continuous at x, find l such that
$\forall y \in [0,1][|x-y|<\frac {1}{2^l} \rightarrow |f(x)-f(y)|<\frac {1}{2^{m+1}}]$
. Note that
$\rho "\big (\overline \alpha (2l)\big )-\rho '\big (\overline \alpha (2l)\big )= (\frac {2}{3})^{2l}<(\frac {1}{2})^l$
. Conclude that
$\overline \alpha (2l)\in B$
. We thus see that
$\forall \alpha \in 2^{\omega } \exists n[\overline \alpha n \in B]$
, i.e., B is a bar in
$2^{\omega }$
. Find a canonical proof of ‘B bars
$\langle \;\rangle $
in
$2^{\omega }$
’. Note that, for all s in
$2^{<\omega }$
,
$s\in B$
if and only if both
$s\ast \langle 0\rangle \in B$
and
$s\ast \langle 1 \rangle \in B$
. Replace, in the canonical proof, every statement: ‘B bars s in
$2^{\omega }$
’ by ‘
$s \in B$
’. The result will be a valid proof, and the conclusion of the proof is: ‘
$\langle \;\rangle \in B$
’, i.e., ‘
$[0,1]$
is fine’.
We thus see that
$\forall m \exists n\forall x \in [0,1]\forall y \in [o,1][|x-y|<\frac {1}{2^n}\rightarrow |f(x)-f(y)|<\frac {1}{2^m}]$
, i.e., f is uniformly continuous on
$[0,1]$
.
4.3 Avoiding the Fan Theorem
Bishop rejected Brouwer’s ‘proof’ of the Fan Theorem and tried to develop constructive mathematics without using it. This is not an easy task. Bishop adapted, for instance, the definition of ‘a continuous function from
$\mathcal {R}$
to
$\mathcal {R}$
’. Let us call a function from
$\mathcal {R}$
to
$\mathcal {R}$
Bishop-continuous if and only if, for each
$M>0$
, f is uniformly continuous on
$[{-}M, +M]$
. Franka Waaldijk has shown that, if the composition
$f\circ g$
of Bishop-continuous functions
$f,g$
from
$\mathcal {R}$
to
$\mathcal {R}$
is always Bishop-continuous itself, then the Fan Theorem holds, see [Reference Waaldijk43] and [Reference Veldman36, Corollary 9.10].
4.4 Many equivalents
In [Reference Veldman36] and [Reference Veldman41], one may find a host of statements that are, in a weak formal context, equivalent to the Fan Theorem.
5 Measure and Integration
Brouwer worked on the theory of measure and integration, following the lead of H. Lebesgue, see [Reference Heyting16, Chapter VI]. Bishop chose for an approach inspired by P. J. Daniell see [Reference Bishop and Bridges1, Chapter 6]. We here return to Brouwer’s approach. Bishop developed his theory of profiles in order to prove the existence of sufficiently many integrable sets, see [Reference Bishop and Bridges1, Chapter 6, Theorem 4.11]. We will see how, in our intuitionistic context, this theory is avoided. On the other hand, we make essential use of the Fan Theorem.
We proved Theorems 1 and 11 without using a precise definition of the notion of a real number. It is now useful to introduce such a definition.
5.1 A note on real numbers
A real number is an infinite sequence
$x=x(0), x(1), \ldots $
of pairs
$x(n)=\big (x'(n), x"(n)\big )$
of rationals such that
-
(1) x is shrinking, i.e., for all n,
$x'(n)\le x'(n+1)\le x"(n+1)\le x"(n)$
, and -
(2) x is dwindling, i.e., for every m, there exists n such that
$x"(n)-x'(n)<\frac {1}{2^m}$
.
$\mathcal {R}$
denotes the set of the real numbers. For all
$x,y$
in
$\mathcal {R}$
, one defines
-
(1)
$x<_{\mathcal {R}} y$
if and only if, for some n,
$x"(n)<y'(n)$
, and -
(2)
$x\le _{\mathcal {R}} y$
if and only if, for all n,
$x'(n)\le y"(n)$
, and -
(3)
$x=_{\mathcal {R}}y$
(x really-coincides with y, x is (really) equal to y), if and only if
$x\le _{\mathcal {R}} y$
and
$y\le _{\mathcal {R}} x$
.
If confusion seems unlikely, we omit the subscript ‘
$\mathcal {R}$
’.
One may prove Cantor’s Intersection Theorem:
Given an infinite sequence
$(x_0, y_0), (x_1, y_1), \ldots $
of pairs of reals that is shrinking, i.e., for all n,
$x_n\le x_{n+1}\le y_{n+1}\le y_n$
, and dwindling, i.e., for all m there exists n such that
$y_n-x_n < \frac {1}{2^m}$
, then there exists a real z such that, for all n,
$x_n\le z \le y_n$
, and, for each real t, if, for all n,
$x_n\le _{\mathcal {R}} t \le _{\mathcal {R}} y_n$
, then
$t=_{\mathcal {R}} z$
.
$[0,1]:= \{x\in \mathcal {R}\mid 0\le x \le 1\}$
.
We will treat rationals and also pairs of rationals as if they were natural numbers. This approach may be made precise by suitable coding functions, see [Reference Veldman36, Section 8].
5.2 Measurable open sets
Definition 15. Let
$(q_0, r_0), (q_1, r_1), \ldots $
be an enumeration of all pairs
$(q,r)$
of rationals such that
$q\le r$
.
For all n, for all a in
$\omega ^n$
, we define
$\mathcal {H}_a :=\{x\in \mathcal {R}\mid \exists j < n[ q_{a(j)}< x<r_{a(j)}]\}.$
For all
$\alpha $
in
$\omega ^{\omega }$
, we define
$\mathcal {H}_\alpha :=\{x\in \mathcal {R}\mid \exists j[q_{\alpha (j)}<x<r_{\alpha (j)}]\}=\bigcup _n \mathcal {H}_{\overline \alpha n}$
.
$\mathcal {X}\subseteq [0,1]$
is called open if and only if there exists
$\alpha $
such that
$\mathcal {X}=\mathcal {H}_\alpha \cap [0,1]$
.
Definition 16. For each n, for each b in
$\omega ^n$
, b is neatly increasing if and only if
$\forall j<n[q_{b(j)}< r_{b(j)}]$
and
$\forall j<n-1[r_{b(j)}\le q_{b(j+1)}]$
.
Remark 5. For each a, there exists exactly one b such that b is neatly increasing and
$\mathcal {H}_a=\mathcal {H}_b$
.
The proof of this fact is left to the reader.
Definition 17. For each a, we define
$\mu (a) := \sum _{j<length(b)} r_{b(j)}-_{\mathbb {Q}} q_{b(j)}$
, where b is neatly increasing and satisfies
$\mathcal {H}_a =\mathcal {H}_b$
.
$\alpha $
is called measurable if and only if
$\mu (\alpha ):=\lim _{n\rightarrow \infty } \mu ( \overline \alpha n)$
exists, i.e.,
$\exists \zeta \in [\omega ]^{\omega }\forall n[\mu \big (\overline \alpha (\zeta (n+1))\big )-\mu \big (\overline \alpha (\zeta ( n))\big ) < \frac {1}{2^n}]$
.
It is not true, constructively, that every
$\alpha $
such that
$\mathcal {H}_\alpha $
is a bounded subset of
$\mathcal {R}$
is measurable. Consider, for instance, the infinite sequence
$\alpha $
such that, for each n, if n is the least k such that
$\forall i<99[d(n+i)=9]$
, then
$(q_{\alpha (n)}, r_{\alpha (n)})=(0,1)$
and, if not, then
$(q_{\alpha (n)}, r_{\alpha (n)})=(0,0)$
. Here,
$d:\omega \rightarrow \{0,1,\ldots 9\}$
is the decimal expansion of
$\pi $
. If
$\mu (\alpha )$
should exist, then either
$\mu (\alpha )>0$
and
$\exists k\forall i<99[d(n+1)=9]$
or
$\mu (\alpha )<1$
and
$\neg \exists k\forall i<99[d(n+1)=9]$
. This is a reckless conclusion.
Definition 18. For all rationals
$q,r,s,t$
such that
$q\le r$
and
$s\le t$
we define a pair of rationals called
$(q,r)\cap (s,t)$
as follows. If
$r<s$
or
$t<q$
, we define
$(q,r)\cap (s,t):= (0,0)$
, and, if
$s\le r$
and
$q\le t$
we define
$(q,r)\cap (s,t):=\big (\max (q,s), \min (r,t)\big )$
.
Definition 19. Let
$\alpha $
be measurable and let rationals
$q,r$
be given such that
$q< r$
. Find
$\beta $
such that, for each j,
$(q_{\beta (j)}, r_{\beta (j)})=(q_{\alpha (j)}, r_{\alpha (j)})\cap (q,r)$
. Note that
$\beta $
is measurable. We define
$\mu \upharpoonright [q,r](\alpha ):= \mu (\beta )$
.
For each n, we define:
$\alpha $
covers
$(q,r)$
for more than
$1-\frac {1}{n}$
if and only if
$\mu \upharpoonright [q,r](\alpha )> (1-\frac {1}{n})(r-q)$
.
We also define:
$\alpha $
never covers
$(q,r)$
if and only if
$\mu \upharpoonright [q,r](\alpha ) <r-q$
.
Lemma 12. Let
$\alpha $
be measurable and let rationals
$p,q,r$
be given such that
$q<p<r$
.
-
(i) For each n, either
$\alpha $
covers
$(q,r)$
for more than
$1-\frac {1}{n}$
, or
$\alpha $
never covers
$(q,r)$
. -
(ii)
$\mu \upharpoonright [q,r](\alpha )=\mu \upharpoonright [q,p](\alpha )+\mu \upharpoonright [p,r](\alpha )$
. -
(iii) For all n, if
$\alpha $
covers both
$(q,p)$
and
$(p,r)$
for more than
$1-\frac {1}{n}$
, then
$\alpha $
covers
$(q,r)$
for more than
$1-\frac {1}{n}$
. -
(iv) If
$\alpha $
never covers
$(q,r)$
, then either
$\alpha $
never covers
$(q,p)$
or
$\alpha $
never covers
$(p,r)$
.
Proof The proof of these statements is left to the reader.
Lemma 13. Let
$\alpha , \beta $
be given such that both
$\alpha , \beta $
are measurable.
-
(i) If
$\mu (\alpha )<\mu (\beta )$
and
$\mathcal {H}_\alpha \subseteq \mathcal {H}_\beta $
, then one may find an element of
$\mathcal {H}_\beta \setminus \mathcal {H}_\alpha $
. -
(ii) if
$\mathcal {H}_\beta \subseteq \mathcal {H}_\alpha $
, then
$\mu (\beta )\le \mu (\alpha )$
, and, if
$\mathcal {H}_\beta = \mathcal {H}_\alpha $
, then
$\mu (\beta )=\mu (\alpha )$
.
Proof (i) Find n such that
$\mu (\overline \beta n)>\mu (\alpha )$
. Find b such that b is neatly increasing and
$\mathcal {H}_b = \mathcal {H}_{\overline \beta n}$
. Find
$j<length(b)$
such that
$\alpha $
never covers
$ (q_{b(j)}, r_{b(j)})$
. Using Lemma 12, define a real x such that
$x(0)= (q_{b(j)}, r_{b(j)})$
and, for each n,
$x'(n)<x'(n+1)<x"(n+1)<x"(n)$
and
$\alpha $
never covers
$x(n)$
. Note that
$x\in \mathcal {H}_\beta \setminus \mathcal {H}_\alpha $
.
(ii) This easily follows from (i).
Note that, in the proof of Lemma 13(ii), we did not use the Fan Theorem, whereas the Fan Theorem is used for proving this result in [Reference Heyting16, Section 6.1.2, Theorem 2].
5.3 On the complement of a measurable open set
Definition 20. We construct
$\rho $
such that, for each s,
$\rho (s)=\big (\rho '(s), \rho "(s)\big )$
is a pair of rationals and
$0\le \rho '(s)\le \rho "(s)\le 1$
. The definition is by induction on
$length(s)$
.
-
(i)
$\rho (\langle \;\rangle ):= (0,1)$
and, -
(ii) for each s in
$2^{<\omega }$
,
$\rho (s\ast \langle 0 \rangle )):= \big (\rho '(s), \frac {\rho '(s) +\rho "(s)}{2}\big )$
and
$\rho (s\ast \langle 1\rangle ) :=\big (\frac {\rho '(s) +\rho "(s)}{2}, \rho "(s)\big )$
, and, -
(iii) for each s, if
$s\notin 2^{<\omega }$
, then
$\rho (s)=0$
.
We also define a function
$\varphi _{bin}$
from Cantor space
$2^{\omega }$
to
$[0,1]$
, by the following.
For each
$\gamma $
in
$2^{\omega }$
, for each n,
$(\varphi _{bin}|\gamma )(n) =\rho (\overline \gamma n)$
.
Note that, for all
$\gamma $
in
$2^{\omega }$
,
$\varphi _{bin}|\gamma =_{\mathcal {R}} \sum _{n=0}^\infty \gamma (n)\cdot 2^{-n-1}$
.
Note that, constructively,
$\varphi _{bin}$
is not a surjective mapping of Cantor space
$\mathcal {C}$
onto
$[0,1]$
. The set
$\varphi _{bin}|2^{\omega }$
consists of all x in
$[0,1]$
that admit of a binary expansion, i.e., for all m, for all
$i<2^m$
, one may decide:
$x\le \frac {i}{2^m}$
or
$\frac {i}{2^m} \le x$
.
The following Lemma shows that, within the complement of a ‘small’ measurable open subset of
$[0,1]$
, one may construct ‘large’, ‘compact’ sets.
Lemma 14. Let
$n>0$
and
$ \alpha $
be given such that
$\alpha $
is measurable and
$\mu (\alpha )<\frac {1}{2^{n+2}}$
. There exists a fan-law
$\beta $
in
$2^{\omega }$
such that
-
(1) for all a, if
$\beta (a)=0$
, then
$a \in 2^{<\omega }$
, and
$\alpha $
never covers
$\rho (a)$
, -
(2) for all a in
$2^{<\omega }$
, for all
$i<2$
, if
$\beta (a)= 0$
and
$\beta (a\ast \langle i \rangle )=1$
, then
$\alpha $
covers
$\rho (a\ast \langle i \rangle )$
for more than
$\frac {1}{2}$
, and -
(3) there exists a measurable
$\alpha ^+$
such that
$\mathcal {H}_\alpha \subseteq \mathcal {H}_{\alpha ^+}$
and
$\mu (\alpha ^+)<\frac {1}{2^n}$
and, for all x in
$[0,1]$
, if
$x\notin \mathcal {H}_{\alpha ^+}$
, then
$\exists \gamma \in \mathcal {F}_\beta [\varphi _{bin}|\gamma = x]$
.
Proof Let
$n>0$
and
$ \alpha $
be given such that
$\alpha $
is measurable and
$\mu (\alpha )<\frac {1}{2^{n+2}}$
. We define the promised fan-law
$\beta $
as follows. For each a, if
$a\notin 2^{<\omega }$
, then
$\beta (a)= 1$
. For a in
$2^{<\omega }$
,
$\beta (a)$
is defined by induction on
$length(a)$
. We will take care that, for each a in
$2^{<\omega }$
, if
$\beta (a) =0$
, then
$\alpha $
never covers
$\rho (a)$
. Define
$\beta (\langle \;\rangle )=0$
and note that
$\alpha $
never covers
$\rho (\langle \;\rangle )$
. Now assume that
$a\in 2^{<\omega }$
, and
$\beta (a)$
has been defined and
$\alpha $
never covers
$\rho (a)$
. If
$\beta (a)=1$
, define
$\beta (a\ast \langle 0\rangle )= \beta (a\ast \langle 1 \rangle )=1$
. If
$\beta (a) = 0$
, find
$i<2$
such that
$\alpha $
never covers
$\rho (a\ast \langle i \rangle )$
and define
$\beta (a\ast \langle i \rangle )=0$
. Then consider
$a\ast \langle 1-i\rangle $
and note that either
$\alpha $
never covers
$\rho (a\ast \langle 1-i\rangle )$
or
$\alpha $
covers
$\rho (a\ast \langle 1-i\rangle )$
for more than
$\frac {1}{2}$
. Define
$\beta (a\ast \langle 1-i\rangle )$
such that, if
$\beta (a\ast \langle 1-i\rangle )=0$
, then
$\alpha $
never covers
$\rho (a\ast \langle 1 -i\rangle )$
, and, if
$\beta (a\ast \langle 1 -i\rangle ) =1$
, then
$\alpha $
covers
$\rho (a\ast \langle 1 - i\rangle )$
for more than
$\frac {1}{2}$
. Note that we have some freedom in carrying out this step as the conditions ‘a never covers
$\rho (a\ast \langle 1-i\rangle )$
’ and ‘a covers
$\rho (a\ast \langle 1-i\rangle )$
for more than
$\frac {1}{2}$
’ do not exclude each other.
Define
$\gamma $
such that, for each s, if there exists
$a,i$
such that
$a\in 2^{<\omega }$
and
$i<2$
and
$s= a\ast \langle i \rangle $
and
$ \beta (a)= 0$
and
$\beta (a\ast \langle i\rangle = 1$
, then
$(q_{\gamma (s)}, r_{\gamma (s)})= \rho (a\ast \langle i \rangle )$
, and if not, then
$(q_{\gamma (s)}, r_{\gamma (s)})=(0,0)$
.
We now prove that
$\gamma $
is measurable. Let k be given. Find p such that
$\mu (\alpha )-\mu (\overline \alpha p) < \frac {1}{2^{k+2}}$
. Define
$\delta $
such that, for each m, for each a, if
$a\in 2^{<\omega } $
and
$length(a)=m$
and
$\big (\rho '(a), \rho "(a)\big )\subseteq \mathcal {H}_{\overline \alpha p}$
, then
$(q_{\delta ^m(a)}, r_{\delta ^m(a)})= \rho (a)$
, and if not, then
$\big (q_{\delta ^m(a)}, r_{\delta ^m(a)}\big )=(0,0)$
. Note that
$\mathcal {H}_{\delta ^m}\subseteq \mathcal {H}_{\overline \alpha p}$
.Footnote
20
Now find m such that
$\mu (\delta ^m)>\mu (\overline \alpha p)-\frac {1}{2^{k+2}}$
. Finally, find q such that
$\mathcal {H}_{\delta ^m}\subseteq \mathcal {H}_{\overline \gamma q}$
. Note that, for all
$r>q$
,
$\mu (\overline {\gamma }r) - \mu (\overline \gamma q)\le 2\big (\mu (\alpha )-\mu (\delta ^m)\big )\le 2\big (\mu (\alpha ) -\mu (\overline \alpha p)+\frac {1}{2^{k+2}}\big ) < \frac {1}{2^k}$
. Conclude that
$\forall k\exists q\forall r>q[\mu (\overline \gamma r)-\mu (\overline \gamma q)<\frac {1}{2^k}]$
. We thus see that
$\mu (\gamma )=\lim _{r\rightarrow \infty }\mu (\overline {\gamma }r)$
exists, i.e.,
$\gamma $
is measurable. Note that
$\mu (\alpha )<\frac {1}{2^{n+2}}$
and that
$\mu (\gamma )\le 2\mu (\alpha )< \frac {1}{2^{n+1}}$
. Finally, note that, for each
$\varepsilon $
in
$\mathcal {F}_\beta $
, for each r,
$\alpha $
does not cover
$(\varphi _{bin}|\varepsilon )(r)= \rho (\overline \varepsilon r)$
, and conclude that
$\varphi _{bin}|\varepsilon \notin \mathcal {H}_\alpha $
.
Now define
$\alpha ^+$
such that, for each a,
$\alpha ^+(2a)= \gamma (a)$
, and
$\alpha (2a+1)=(q_a-\frac {1}{2^{n+a+3}}, q_a+\frac {1}{2^{n+a+3}})$
. Note that
$\mathcal {H}_\gamma \subseteq \mathcal {H}_{\alpha ^+}$
and that
$\alpha ^+$
is measurable and
$\mu (\alpha ^+)\le \mu (\gamma ) + \frac {1}{2^{n+2}}<\frac {1}{2^n}$
. Assume
$x\in [0,1]$
and
$x \notin \mathcal {H}_{\alpha ^+}$
. Then
$\forall q \in \mathbb {Q}[q \;\#\; x]$
. We thus may find
$\varepsilon $
in
$2^{\omega }$
such that
$\varphi _{bin}|\varepsilon = x$
. Note that
$x\notin \mathcal {H}_{\gamma }$
and thus, for each r,
$\beta (\overline \varepsilon r)=0$
and
$\varepsilon \in \mathcal {F}_\beta $
. Conclude that
$\forall x \in [0,1][x \notin \mathcal {H}_{\alpha ^+}\rightarrow \exists \varepsilon \in \mathcal {F}_\beta [\varphi _{bin}|\varepsilon = x]]$
.
5.4 Almost-full subsets of
$[0,1]$
and almost-full functions from
$[0,1]$
to
$[{-}1,1]$
Definition 21.
$\mathcal {X}\subseteq [0,1]$
will be called almost-full if and only if, for each n, there exists a measurable
$\alpha $
such that
$\mu (\alpha )<\frac {1}{2^n}$
and
$\forall x \in [0,1][x\notin \mathcal {H}_\alpha \rightarrow x \in \mathcal {X}]$
.
A partial function f from
$[0,1]$
to
$[{-}1,1]$
will be called almost-full if and only if its domain
$Dom(f) = \{x\in [0,1]\mid \; f(x)\; is \; defined \}$
is almost-full.
Definition 22. Let f be an almost-full function from
$[0,1]$
to
$[{-}1,1]$
.
f is called measurable if and only if, for each n, one may find m and rationals
$u_0, u_1, \ldots , u_{2^m-1}$
such that for each
$i<2^m$
,
$-1\le u_i\le 1$
, and a measurable
$\alpha $
such that
$\mu (\alpha )<\frac {1}{2^{n+2}}$
and, for each x in
$Dom(f)$
, for each
$i<2^m$
, if
$x\notin \mathcal {H}_\alpha $
and
$\frac {i}{2^m}< x <\frac {i+1}{2^m}$
, then
$|f(x)-u_i|<\frac {1}{2^{n+1}}$
.
The number
$\sum _{i<2^{m}} u_i\cdot \frac {1}{2^{m}}$
will be called an estimate of the integral of f of accuracy
$\frac {1}{2^{n}}$
.
Theorem 15. Let f be an almost-full and measurable function from
$[0,1]$
to
$[{-}1,1]$
.
-
(i) For all rationals
$q,r$
, if
$q,r$
are estimates of the integral of f of accuracy
$\frac {1}{2^m}$
,
$\frac {1}{2^n}$
, respectively, then
$|q-r| \le \frac {1}{2^m} + \frac {1}{2^n}$
. -
(ii) There exists a real x such that, for all n, for all estimates q of the integral of f of accuracy
$\frac {1}{2^n}$
,
$|x-q|\le \frac {1}{2^n}$
.
Proof The proof of this Theorem is left to the reader.
The number intended in Theorem 15(ii) is unique up to the relation of real coincidence and will be called:
$\int _0^1f$
, the integral of f on
$[0,1]$
.
For the next result, see [Reference Rootselaar22, p. 7] and [Reference Heyting16, Section 6.2.2, Theorem 1].
Theorem 16 (van RootselaarFootnote 21 ).
Every almost-full function from
$[0,1]$
to
$[{-}1,1]$
is measurable.
Proof Let f be an almost-full function from
$[0,1]$
to
$[{-}1,1]$
. Let n be given. Find a measurable
$\alpha $
such that
$\mu (\alpha )<\frac {1}{2^{n+4}}$
and
$\forall x \in [0,1][x\notin \mathcal {H}_\alpha \rightarrow x \in Dom(f)]$
. Using Lemma 14, find a fan-law
$\beta $
in
$2^{\omega }$
such that
-
(1) for all a, if
$\beta (a)=0$
, then
$a \in 2^{<\omega }$
, and
$\alpha $
never covers
$\rho (a)$
, -
(2) for all a in
$2^{<\omega }$
, for all
$i<2$
, if
$\beta (a)= 0$
and
$\beta (a\ast \langle i \rangle )=1$
, then
$\alpha $
covers
$\rho (a\ast \langle i \rangle )$
for more than
$\frac {1}{2}$
, and -
(3) there exists a measurable
$\alpha ^+$
such that
$\mathcal {H}_\alpha \subseteq \mathcal {H}_{\alpha ^+}$
and
$\mu (\alpha ^+)<\frac {1}{2^{n+2}}$
and, for all x in
$[0,1]$
, if
$x\notin \mathcal {H}_{\alpha ^+}$
, then
$\exists \gamma \in \mathcal {F}_\beta [\varphi _{bin}|\gamma = x]$
.
Conclude that
$\forall \gamma \in \mathcal {F}_\beta [\varphi _{bin}|\gamma \in Dom(f)]$
and
$\forall \gamma \in \mathcal {F}_\beta \exists u \in \mathbb {Q}[|u-f(\varphi _{bin}|\gamma )|<\frac {1}{2^{n+1}}]$
. Using the extension of Brouwer’s Continuity Principle to spreads, Theorem 3, conclude that
$\forall \gamma \in \mathcal {F}_\beta \exists m\exists u \in \mathbb {Q}\forall \delta \in \mathcal {F}_\beta [ \overline \gamma m \sqsubset \delta \rightarrow [|u-f(\varphi _{bin}|\delta )|<\frac {1}{2^{n+1}}]$
. Using the Fan Theorem, Theorem 10, find m such that
$\forall \gamma \in \mathcal {F}_\beta \exists u \in \mathbb {Q}\forall \delta \in \mathcal {F}_\beta [ \overline \gamma m \sqsubset \delta \rightarrow |u-f(\varphi _{bin}|\delta )|<\frac {1}{2^{n+1}}]$
, i.e.,
$\forall a \in 2^{<\omega }[\big (length(a)=m \;\wedge \;\beta (a)=0\big )\rightarrow \exists u \in \mathbb {Q}\forall \delta \in \mathcal {F}_\beta [ a \sqsubset \delta \rightarrow |u-f(\varphi _{bin}|\delta )|<\frac {1}{2^{n+1}}]]$
.
Now find rationals
$u_0, u_1, \ldots , u_{2^m-1}$
such that, for all
$i<2^m-1$
, for all
$a\in 2^{<\omega }$
such that
$length(a)=m$
, if
$\rho (a) = (\frac {i}{2^m}, \frac {i+1}{2^m})$
, then,
-
(1) if
$\beta (a)=0$
, then
$\forall \delta \in \mathcal {F}_\beta [ a\sqsubset \delta \rightarrow |u_i-f(\varphi _{bin}|\delta )|<\frac {1}{2^{n+1}}]$
, and, -
(2) if
$\beta (a)=1$
, then
$u_i=0$
.
Note that, for all x in
$Dom(f)$
, for all
$i<2^m$
, if
$x \notin \mathcal {H}_{\alpha ^+}$
and
$\frac {i}{2^m}<x<\frac {i+1}{2^m}$
, then
$|f(x)-u_i|<\frac {1}{2^{n+1}}$
.
Thus, for each m, we can make an estimate of the integral of f of accuracy
$\frac {1}{2^n}$
, i.e., f is measurable.
Definition 23.
$\mathcal {Y}\subseteq [0,1]$
is measurable if and only if its characteristic function
$$\begin{align*}\chi_{\mathcal{Y}} :=\{(x,i)\in [0,1]\times\{0,1\}\mid (x \in \mathcal{Y} \wedge i=1)\vee (x \notin \mathcal{Y} \wedge i=0)\} \end{align*}$$
is measurable. If
$\mathcal {Y}\subseteq [0,1]$
is measurable, we define
$\mu (\mathcal {Y}) := \int _0^1\chi _{_{\mathcal {Y}}}$
.
$\mu (\mathcal {Y})$
is called the measure of
$\mathcal {Y}$
.
Corollary 17.
$\mathcal {Y}\subseteq [0,1]$
is measurable if and only if
$\mathcal {Y}\cup ([0,1]\setminus \mathcal {Y})$
is almost-full.
5.5 Many integrable sets
We want to prove an important result overlooked by Brouwer and Heyting:
for every almost-full and therefore measurable function f from
$[0,1]$
to
$[{-}1,1]$
, for all but countably many y in
$[{-}1,1]$
, the set
$\{x\in [0,1] \mid x\in Dom(f)\;\wedge \;f(x) <y\}$
is measurable.
We avoid the theory of profiles developed by E. Bishop for the purpose of proving this theorem, see [Reference Bishop and Bridges1, Chapter 6, Section 4, and Theorem 4.11]. Our approach is the one followed in [Reference Driessen14].
Lemma 18. Let f be a measurable function from
$[0,1]$
to
$[{-}1,1]$
. Let rationals
$q,r$
be given such that
$-1\le q < r\le 1$
. Let n be given.
One may find rationals
$s,t$
such that
$q\le s<t\le r$
and a measurable
$\alpha $
such that
$\mu (\alpha )<\frac {1}{2^n}$
and
$\forall x\in Dom(f)[x\notin \mathcal {H}_\alpha \rightarrow \big (f(x)<s \;\vee \; t<f(x)\big )]$
.
Proof Let f be a measurable function from
$[0,1]$
to
$[{-}1,1]$
. Let rationals
$q,r$
be given such that
$-1\le q < r\le 1$
. Let n be given.
Find l such that
$\frac {1}{2^l}<\frac {r-q}{2^{n+1}}$
. Note that
$r-q\le 2$
and
$l> n$
. Using Definition 22, find m and rationals
$u_0, u_1, \ldots , u_{2^m-1}$
such that, for each
$i<2^m$
,
$-1\le u_i\le 1$
, and a measurable
$\alpha $
such that
$\mu (\alpha )<\frac {1}{2^{l+2}}$
and, for each x in
$Dom(f)$
, for each
$i<2^m$
, if
$x\notin \mathcal {H}_\alpha $
and
$\frac {i}{2^m}< x < \frac {i+1}{2^m}$
, then
$|f(x)-u_i|<\frac {1}{2^{l+2}}$
.
Define
$j_0:=\mu j[r<q+\frac {j+1}{2^l}]$
. Note that
$2^{n+1}\cdot \frac {1}{2^l}< r-q$
, so
$2^{n+1}\le j_0$
. For each
$j< j_0$
, consider the set
$A_j:=\{i<2^m\mid q+\frac {j}{2^l}\le u_i < q+\frac {j+1}{2^l}\}$
. Note that for all
$j<k< j_0$
,
$A_j\cap A_k = \emptyset $
. Find
$j_1\le j_0$
such that, for all
$j\le j_0$
,
$Card(A_{j_1})\le Card(A_j)$
. Note that
$Card(A_{j_1})\le \frac {2^m}{j_0}\le \frac {2^m}{2^{n+1}}=2^{m-n-1}$
.
Define
$s:= q+\frac {j_1}{2^l}+\frac {1}{2^{l+2}}$
and
$t:=q+\frac {j_1+1}{2^l}-\frac {1}{2^{l+2}}$
and note that
$q<s<t<r$
. Note that, for each
$i<2^m$
, if
$i\notin A_{j_1}$
, then either
$u_i<q+\frac {j_1}{2^l}$
and, for all x in
$Dom(f)\cap (\frac {i}{2^m}, \frac {i+1}{2^m})$
, if
$x\notin \mathcal {H}_\alpha $
, then
$f(x)< q+\frac {j_1}{2^l}+\frac {1}{2^{l+2}} = s$
, or
$q+\frac {j_1+1}{2^l}\le u_i$
and, for all x in
$Dom(f)\cap (\frac {i}{2^m}, \frac {i+1}{2^m})$
, if
$x \notin \mathcal {H}_\alpha $
, then
$t= q+\frac {j_1+1}{2^l}-\frac {1}{2^{l+2}}< f(x) $
.
One now may define
$\alpha ^+$
such that
$\alpha ^+$
is measurable and
$\mathcal {H}_\alpha \subseteq \mathcal {H}_{\alpha ^+}$
and, for each i in
$A_{j_1}$
,
$(\frac {i}{2^m}, \frac {i+1}{2^m})\subseteq \mathcal {H}_{\alpha ^+}$
and, for each
$i\le 2^m$
,
$\frac {i}{2^m}\in \mathcal {H}_{\alpha ^+}$
and
$\mu (\alpha ^+)<\mu (\alpha ) + \sum _{i\in A_{j_1}} \frac {1}{2^m}<\frac {1}{2^{l+2}} + \frac {1}{2^{n+1}}< \frac {1}{2^n}$
. Note that
$\mu (\alpha ^+)<\frac {1}{2^n}$
, and, for all x in
$Dom(f)$
, if
$x\notin \mathcal {H}_{\alpha ^+}$
, then either
$f(x)<s$
or
$t<f(x)$
.
Theorem 19. Let f be a measurable function from
$[0,1]$
to
$[{-}1,1]$
. Let rationals
$u,v$
be given such that
$-1\le u<v\le 1$
.
There exists y in
$(u,v)$
such that, for almost all x in
$[0,1]$
,
$x\in Dom(f)$
and
$f(x) <y$
or
$y<f(x)$
.
Proof Applying Lemma 18, we find an infinite sequence
$(u_0, v_0), (u_1, v_1), \ldots $
of pairs of rationals, and an infinite sequence
$\alpha _0, \alpha _1, \ldots $
of measurable elements of
$\omega ^{\omega }$
such that
-
(1)
$(u_0, v_0)= (u, v)$
, -
(2) for each n,
$u_n < u_{n+1} < v_{n+1} < v_n$
, and
$v_{n+1} - u_{n+1}<\frac {1}{2^n}$
, -
(3) for each n,
$\mu (\alpha _n) < \frac {1}{2^n}$
and
$\forall x \in Dom(f)\setminus \mathcal {H}_{\alpha _n}[f(x) < u_n \;\vee \;v_n < f(x)]$
.
Find y such that, for each n,
$u_n \le y \le v_n$
and note that y satisfies the requirements.
Corollary 20. Let f be a measurable function from
$[0,1]$
to
$[{-}1.1]$
. The set
$\{y\in [{-}1,1]\mid \{x\in [0,1]\mid f(x) <y\}\;is\;measurable\}$
is dense in
$[{-}1,1]$
.
Lemma 21. Let h be a partial function from
$[{-}1,1]$
to
$[0, 1]$
such that
$ Dom(h)$
is dense in
$[{-}1,1]$
and h is non-decreasing, i.e.,
$\forall x \in Dom(h)\forall y \in Dom(h)[x<y\rightarrow h(x) \le h(y)]$
. Let
$x,y$
in
$Dom(h)$
be given such that
$x<y$
and
$h(x) < h(y)$
.
There exists z in
$[x, y]$
such that, for all u in
$Dom(h)$
, if
$u\;\#\; z$
, then
$\exists t\in Dom(h)\exists w\in Dom(h)[t<u<w \;\wedge \; h(w)-h(t) < \frac {2}{3}\big (h(y)-h(x)\big )]$
.
Proof Define
$\varepsilon := h(y)-h(x)$
. A point u in
$[x,y]$
will be called neat if and only if
$$\begin{align*}\exists t\in Dom(h)\exists w\in Dom(h)[t<u<w \;\wedge\; h(w)-h(t) < \frac{2}{3}\varepsilon]. \end{align*}$$
We now construct an infinite sequence
$(x_0, y_0), (x_1, y_1), \ldots $
of pairs of elements of
$Dom(h)$
, such that, for all n,
$x\le x_n\le x_{n+1}\le y_{n+1}\le y_n\le y$
and
$y_n-x_n\le (\frac {2}{3})^n(y-x)$
and every u in
$[x,x_n)\cup (y_n, y]$
is neat.
We define
$(x_0, y_0):= (x,y)$
.
Now let n be given such that
$(x_n, y_n)$
has been defined already such that
$x_n< y_n$
. Determine a in
$Dom(h)$
such that
$\frac {2}{3}x_n + \frac {1}{3}y_n < a < \frac {1}{3}x_n + \frac {2}{3} y_n$
. Note that
$a-x_n<\frac {2}{3}(y_n-x_n)$
and
$y_n-a<\frac {2}{3}(y_n-x_n)$
. Note that
$h(x)\le h(a) \le h(y)$
.
Either
$\frac {1}{2}\varepsilon <h(a)-h(x)$
or
$h(a) -h(x) <\frac {2}{3}\varepsilon $
, and either
$\frac {1}{2}\varepsilon <h(y)-h(a)$
or
$h(y) -h(a) <\frac {2}{3}\varepsilon $
, but not both
$\frac {1}{2}\varepsilon <h(a)-h(x)$
and
$\frac {1}{2}\varepsilon <h(y)-h(a)$
.
Note that, if
$h(a)-h(x)<\frac {2}{3}\varepsilon $
, then every u in
$[x,a)$
will be neat, and, if
$h(y)-h(a)<\frac {2}{3}\varepsilon $
, then every u in
$(a, y]$
will be neat.
We define
$(x_{n+1}, y_{n+1})$
in such a way that either
$(x_{n+1}, y_{n+1})=(x_n, a)$
and
$h(y)-h(a) < \frac {2}{3}\varepsilon $
, or
$(x_{n+1}, y_{n+1})=(a, y_n)$
and
$h(a)-h(x) < \frac {2}{3}\varepsilon $
.
Then every u in
$[x,x_{n+1})\cup (y_{n+1}, y]$
will be neat.
Clearly, the infinite sequence
$(x_0, y_0), (x_1, y_1), \ldots $
satisfies our requirements.
Using Cantor’s Intersection Theorem, find z such that, for all n,
$x_n\le z \le y_n$
and note that, for all u in
$[0,1]$
, if
$u\;\#\;z$
, then, for some n,
$u<x_n$
or
$y_n<u$
and, therefore, u is neat.
Definition 24. Let h be a partial function from
$[{-}1,1]$
to
$[0,1]$
such that
$Dom(h)$
is dense in
$[{-}1,1]$
and h is non-decreasing. Let u in
$[{-}1,1]$
be given. u is a point of continuity for h if and only if
$\forall n \exists t \in Dom(h)\exists w\in Dom(h)[t<u<w \;\wedge \; h(w)-h(t) <\frac {1}{2^n}]$
.
Remark 6. If u is a point of continuity for h, there exists y in
$[0,1]$
such that
$\forall n\exists m \forall t\in Dom(h)[u-\frac {1}{2^m}<t<u+\frac {1}{2^m} \rightarrow |h(t)-y|<\frac {1}{2^n}]$
. y is unique up to the relation of real coincidence and will be called the value of h at u. One may extend the partial function h to the partial function
$g\subseteq [{-}1,1]\times [0,1]$
consisting of all pairs
$(u,y)$
such that either
$(u,y)\in h$
or u is a point of continuity for h and y is the value of h at u.
Theorem 22. Let h be a partial function from
$[{-}1,1]$
to
$[0,1]$
such that
$Dom(h)$
is dense in
$[{-}1,1]$
and h is non-decreasing. All but countably many elements of
$[{-}1,1]$
are points of continuity for h.
Proof Find an infinite sequence
$x_0, x_1, \ldots $
of elements of
$Dom(h)$
such that
$\forall p \in \mathbb {Q} \forall q\in \mathbb {Q}[0\le p <q\le 1\rightarrow \exists n[p\le x_n\le q]]$
.
Define, for all
$m,n$
such that
$x_m<x_n$
and
$h(x_m)<h(x_n)$
, for all z in
$[0,1]$
,
$$\begin{align*}z\ \textit{resolves } (x_m, x_n) \end{align*}$$
if and only if
$x_m\le z \le x_n$
and, for all u in
$[x_m, x_n]$
, if
$u\;\#\;z$
, then
$\exists t \in Dom(h)\exists w \in Dom(h)[t<u<w \;\wedge \; h(w)-h(t) < \frac {2}{3}\big (h(x_n)-h(x_m)\big )]$
.
Using Lemma 21, define an infinite sequence
$z_0, z_1, \ldots $
of elements of
$[0,1]$
such that
$z_0=0$
and
$z_1=1$
and, for each n, if
$\big (x_{n(0)})"\big (n(2)\big )<\big (x_{n(1)})'\big (n(2)\big )$
and
$(h\big (x_{n(0)}))"\big ((n(3)\big ) <(h\big (x_{n(1)}))'\big (n(3)\big )$
, then
$z_{n+2}$
resolves
$(x_{n(0)}, x_{n(1)})$
.
Let u be given such that, for each n,
$u\;\#\; z_n$
. We prove that u is a point of continuity for h, by showing, inductively:
For each n, there exist
$t,w$
in
$Dom(h)$
such that
$t<u<w$
and
$h(w)-h(t)<(\frac {2}{3})^n\cdot 3$
The case
$n=0$
obviously holds: find
$t,w$
in
$Dom(h)$
such that
$t<u<w$
and note:
$h(w) -h(t)\le |h(w)|+|h(t)| \le 2<3$
.
Now let
$n, t,w$
be given such that
$t,w$
in
$Dom(h)$
and
$t<u<w$
and
$h(w) - h(t)<(\frac {2}{3})^n\cdot 3$
. Find
$m,p$
such that
$t<x_m<u<x_p<w$
and note
$h(x_p) - h(x_m)<(\frac {2}{3})^n\cdot 3$
. Now distinguish two cases.
Case (1).
$h(x_p) - h(x_m)<(\frac {2}{3})^{n+1}\cdot 3$
and we are done, or
Case (2).
$0<h(x_p)-h(x_m)$
.
In the latter case, find
$q,r$
such that
$x_m"(q)<x_p'(q)$
and
$\big (h(x_m)\big )"(r) < \big (h(x_p)\big )'(r)$
.
Then find s such that
$s(0) = m, \;s(1)= p, \;s(2) =q$
and
$s(3)=r$
.
As
$y_{s+2}$
resolves
$(x_m, x_p)$
and
$u\;\#\; y_{s+2}$
, find
$t,w$
in
$Dom(h)$
such that
$t<u<w$
and
$h(w)-h(t)<\frac {2}{3}\big (h(x_p)-h(x_m)\big )< (\frac {2}{3})^{n+1}\cdot 3$
.
We thus see that u is indeed a point of continuity for h.
Remark 7. Using Remark 6 and Theorem 22, observe that a non-decreasing partial function h from
$[{-}1,1]$
to
$[0, 1]$
such that
$Dom(h)$
is dense in
$[{-}1,1]$
may be extended to a non-decreasing partial function g from
$[{-}1,1]$
to
$[0,1]$
such that
$Dom(g)$
is co-enumerable, i.e., there exists an infinite sequence
$z_0, z_1, \ldots $
of elements of
$[{-}1,1]$
such that, for every u in
$[0,1]$
, if
$\forall n[ u \;\#\;z_n]$
, then
$u\in Dom(g)$
.
Theorem 23. Let f be a measurable function f from
$[0,1]$
to
$[{-}1,1]$
. The domain of the partial function
$$\begin{align*}D(f):=\{(y, m)\in [{-}1,1]\times [0,1]\mid m= \mu(\{x\in [0,1]\mid f(x)<y\})\} \end{align*}$$
is a co-enumerable subset of
$[{-}1,1]$
.
6 The Bar Theorem
Brouwer, when first proving the Fan Theorem, obtained the Fan Theorem as a Corollary of a more general result, see [Reference Brouwer8] and [Reference Brouwer9]. Like the Fan Theorem, this more general result, the Bar Theorem, should be called an axiom. We describe how Brouwer convinced himself of its truth by an argument that is philosophical rather than mathematical.
Brouwer’s only application of this more general axiom is the Fan Theorem. We will see how the Fan Theorem follows from the Bar Theorem. As an example of a different application, we show that the Bar Theorem enables us to characterize enumerable and well-founded subsets of
$\mathbb {Q}$
.
The Bar Theorem is also called Brouwer’s Thesis on Bars (in
$\omega ^{\omega }$
) and we will see that it may be formulated as a Principle of Bar Induction, as in [Reference Kleene and Vesley19,
${}^x26$
].
We give a second proof of our characterization of enumerable and well-founded subsets of
$\omega $
that uses the Principle of Bar Induction rather than the Bar Theorem itself.
6.1 Brouwer’s argument
Stumps have been introduced in Section 3.1.
$B\subseteq \omega $
is a bar in
$\omega ^{\omega }$
if and only if
$\forall \alpha \in \omega ^{\omega }\exists n[\overline \alpha n \in B]$
.
Theorem 24 (Bar Theorem).
Footnote
22
If
$B\subseteq \omega $
be a bar in
$\omega ^{\omega }$
, there exists a stump S such that
$ S\cap B$
is a bar in
$\omega ^{\omega }$
.
Proof Let us define, for each
$B\subseteq \omega $
, for each s, B bars s if and only if
$Bar_{\omega ^{\omega }\cap s}(B)$
, i.e.,
$\forall \alpha [s\sqsubset \alpha \rightarrow \exists n[\overline \alpha n \in B]]$
.
Note that
$Bar_{\omega ^{\omega }}(B)$
if and only if B bars
$\langle \;\rangle $
.
The following three observations are important.
-
(i) For all s, if
$s\in B$
, then B bars s. -
(ii) For all s, if B bars
$s\ast \langle 0\rangle $
and B bars
$s\ast \langle 1\rangle $
and B bars
$s\ast \langle 2\rangle $
and
$\ldots $
, then B bars s. -
(iii) For all s, for all n, if B bars s, then B bars
$s\ast \langle n \rangle $
.
Note that one may prove a statement of the form ‘B bars s’ by starting from observations of the form (i) and using observations of the form (ii) and (iii) as reasoning steps. Such a proof will be called a canonical proof. Note that the reasoning steps corresponding to the observation (ii) have infinitely many premises. Therefore, a canonical proof is no longer a finite ‘tree’, like in the case of the Fan Theorem, but an infinitary one. The structure of a canonical proof is comparable to the structure of a stump.
Let us now agree to consider a statement ‘B bars s’ as established or true if and only if we are able to provide such a canonical proof. We thus introduce an axiomatic assumption.
Let us now prove the theorem.
Assume
$Bar_{\omega ^{\omega }}(B)$
.
Take a canonical proof of ‘B bars
$\langle \;\rangle $
’. We use this canonical proof in order to build another proof, as follows.
In the canonical proof, replace every statement: ‘B bars s’ by the statement: ‘there exists a stump S such that
$(s\ast S )\cap B$
bars s’.
We now verify that the new ‘proof’ is indeed a valid proof.
(i) If
$s\in B$
we can take
$S=\{\langle \;\rangle \}$
.
(ii) Let s be given such that, for each n, there exists a stump S such that
$(s\ast \langle n \rangle \ast S)\cap B$
bars
$s\ast \langle n \rangle $
. Using the Second Axiom of Countable ChoiceFootnote
23
, Axiom 3, we build, step by step, a stump S such that, for each n,
$(s\ast \langle n \rangle \ast (S\upharpoonright n))\cap B$
bars
$s\ast \langle n \rangle $
. Note that
$(s\ast S)\cap B$
bars s.
(iii) Let
$s, n$
be given. Let S be a stump such that
$(s\ast \langle n\rangle \ast S))\cap B$
bars s. Now distinguish two cases.
Case (1).
$S\upharpoonright \langle n \rangle =\emptyset $
. Conclude:
$\exists t \sqsubseteq s[t \in B]$
. Define
$T:=\{\langle \;\rangle \}$
and note:
$(s\ast \langle n \rangle \ast T)\cap B$
bars
$s\ast \langle n \rangle $
.
Case (2).
$\langle \; \rangle \in S\upharpoonright \langle n \rangle $
. Then
$(s\ast \langle n \rangle \ast S\upharpoonright \langle n \rangle )\cap B$
bars
$s\ast \langle n \rangle $
.
We thus see that our new ‘proof’ is a valid proof indeed. We may affirm its conclusion: ‘there exists a stump S such that
$S\cap B$
bars
$\langle \;\rangle $
, i.e.,
$Bar_{\omega ^{\omega }}(S\cap B)$
.’
6.2 The Fan Theorem follows from the Bar Theorem
Theorem 25 (Fan Theorem, Theorem 10).
Let
$\beta $
be a finitary spread-law. If
$B\subseteq \omega $
is a bar in
$\mathcal {F}_\beta $
, some finite
$B'\subseteq B$
is bar in
$\mathcal {F}_\beta $
.
Proof
Footnote
24
Let
$\beta $
be a finitary spread-law and let
$B\subseteq \{s\mid \beta (s)=0\}$
be a bar in
$\mathcal {F}_\beta $
. Let
$\rho :\omega ^{\omega }\rightarrow \mathcal {F}_\beta $
be a retractionFootnote
25
of
$\omega ^{\omega }$
onto
$\mathcal {F}_\beta $
. Define
$B^+:= B\cup \{s\mid \beta (s)\neq 0\}$
. Let
$\alpha $
be given. Find n such that
$\overline {(\rho |\alpha )}n \in B$
. If
$\overline {(\rho |\alpha )}n\neq \overline \alpha n$
, then
$\beta (\overline \alpha n)\neq 0$
and
$\overline \alpha n \in B^+$
. Conclude that, in any case,
$\overline \alpha n\in B^+$
. We thus see that
$B^+$
is a bar in
$\omega ^{\omega }$
. Using Theorem 24, find a stump S such that
$S\cap B^+$
is a bar in
$\omega ^{\omega }$
. Note that
$S\cap B$
is a bar in
$\mathcal {F}_\beta $
.
Finally, observe that, for every stump T, for every finitary spread-law
$\gamma $
the set
$\{s \mid \gamma (s)=0\}\cap T$
is finite. This observation is proven by the principle of induction on the set
$\mathbf {Stp}$
of stumps, Axiom 6 in Section 3.1. One needs two facts.
-
(i) For every finitary spread-law
$\gamma $
, for every n,
$\gamma ^n$
is also a finitary spread-law. -
(ii) The union of finitely many finite subsets of
$\omega $
is finite.
It follows that
$B':=S\cap B\subseteq B$
is finite and a bar in
$\mathcal {F}_\beta $
.
6.3 Well-ordered enumerable subsets of
$\mathbb {Q}$
Definition 25. For all
$A,B\subseteq \mathbb {Q}$
, we define:
$A<B$
if and only if
$\forall q \in A\forall r \in B[q<r]$
.
We define a collection
$\mathcal {WO}$
of subsets of
$\mathbb {Q}$
by the following inductive definition. The elements of
$\mathcal {WO}$
are called the inductively well-ordered subsets of
$\mathbb {Q}$
.
-
(i)
$\emptyset \in \mathcal {WO}$
, and, for each q in
$\mathbb {Q}$
,
$\{q\}\in \mathcal {WO}$
.These are the basic elements of
$\mathcal {WO}$
. -
(ii) For every sequence
$A_0, A_1, \ldots $
of elements of
$\mathcal {WO}$
such that, for each n,
$A_n<A_{n+1}$
, also
$\bigcup _n A_n \in \mathcal {WO}$
.This is the construction step of the set
$\mathcal {WO}$
. -
(iii) Every element of
$\mathcal {WO}$
is obtained from basic elements of
$\mathcal {WO}$
by applying the construction step repeatedly.
We let
$q_0, q_1, \ldots $
be some canonical enumeration of
$\mathbb {Q}$
.
$A\subseteq \mathbb {Q}$
is a decidable subset of
$\mathbb {Q}$
if and only if
$\exists \alpha \forall n[q_n \in A \leftrightarrow \alpha (n)\neq 0]$
.
Let
$A\subseteq \mathbb {Q}$
and
$\alpha $
be given.
$\alpha $
is called an enumeration of A if and only if
$\forall n [q_n\in A \leftrightarrow \exists m[ \alpha (m)=n+1]]$
.
$A\subseteq \mathbb {Q}$
is enumerable if and only if there exists an enumeration of A.
$A\subseteq \mathbb {Q}$
is (explicitly) well-founded if and only if
$\forall \gamma [\forall n[q_{\gamma (n)} \in A]\rightarrow \exists n[q_{\gamma (n)}\le q_{\gamma (n+1)}]]$
.
Lemma 26. Let
$\alpha $
be an enumeration of
$A\subseteq \mathbb {Q}$
. A is (explicitly) well-founded if and only if
$\forall \gamma \exists n[ \forall i\le n+1[\alpha \circ \gamma (i)>0]\rightarrow q_{\alpha \circ \gamma (n)-1}\le q_{\alpha \circ \gamma (n+1)-1}]$
.
Proof Let
$\alpha $
be an enumeration of
$A\subseteq \mathbb {Q}$
, i.e.,
$\forall n [q_n\in A \leftrightarrow \exists m[ \alpha (m)=n+1]]$
.
First assume A is well-founded. Let
$\gamma $
be given. Distinguish two cases.
Case (a).
$\alpha \circ \gamma (0)=0$
. Then
$\forall i\le 2[\alpha \circ \gamma (i)>0]\rightarrow q_{\alpha \circ \gamma (0)-1}\le q_{\alpha \circ \gamma (1)-1}$
.
Case (b).
$\alpha \circ \gamma (0)>0$
. Now define
$\beta $
such that, for each n, if
$\alpha (n)>0$
, then
$\beta (n) =\alpha (n)$
, and, if
$\alpha (n)=0$
, then
$\beta (n)=\alpha \circ \gamma (0)$
. Note that
$\forall n[\beta (n)>0 \;\wedge \; q_{\beta (n)-1} \in A]$
. Find n such that
$q_{\beta (n)-1} \le q_{\beta (n+1)-1}$
. Note that, if
$\forall i\le n+1[\alpha (i)>0]$
, then
$\alpha (n)=\beta (n)$
and
$\alpha (n+1)=\beta (n+1)$
and
$q_{\alpha (n)-1} \le q_{\alpha (n+1)-1}$
. Conclude that
$\forall \gamma \exists n[ \forall i\le n+1[\alpha \circ \gamma (i)>0]\rightarrow q_{\alpha \circ \gamma (n)-1}\le q_{\alpha \circ \gamma (n+1)-1}]$
.
Now assume
$\forall \gamma \exists n[ \forall i\le n+1[\alpha \circ \gamma (i)>0]\rightarrow q_{\alpha \circ \gamma (n)-1}\le q_{\alpha \circ \gamma (n+1)-1}]$
. Let
$\gamma $
be given such that
$\forall n[q_{\gamma (n)}\in A]$
. Find
$\delta $
such that, for each n,
$\alpha \circ \delta (n)>0$
and
$q_{\alpha \circ \delta (n)-1}=q_{\gamma (n)}$
. Find n such that
$q_{\alpha \circ \delta (n)-1}\le q_{\alpha \circ \delta (n+1)-1}$
and conclude that
$q_{\gamma (n)}\le q_{\gamma (n+1)}$
. Conclude that
$\forall \gamma [\forall n [q_{\gamma (n)}\in A]\rightarrow \exists n[q_{\gamma (n)}\le q_{\gamma (n+1)}]]$
, i.e., A is well-founded.
Lemma 27.
-
(i) Every A in
$\mathcal {WO}$
is enumerable and (explicitly) well-founded. -
(ii) For all A in
$\mathcal {WO}$
, for all
$q,t$
in
$ A$
, the set
$\{r\in A\mid q< r \le t\}$
belongs to
$\mathcal {WO}$
. -
(iii) For every enumerable subset A of
$\mathbb {Q}$
, if, for all q in A, the set
$\{r\in A\mid r\le q\}$
belongs to
$\mathcal {WO}$
, then
$A \in \mathcal {WO}$
.
Proof The proof of (i) and (ii) is by straightforward induction on
$\mathcal {WO}$
and left to the reader.
(iii) Let
$\alpha $
be an enumeration of A.
Define an infinite sequence
$A_0, A_1, A_2, \ldots $
of subsets of A, such that, for each n, if
$\alpha (n)>0$
, then
$A_n:=\{r \in A \mid \forall i<n[\alpha (i)>0\rightarrow r> q_{\alpha (i)-1}]\;\wedge \;r\le q_{\alpha (n)-1}\}$
, and, if
$\alpha (n)=0$
, then
$A_{n}=\emptyset $
. Using (ii), note that, for all n,
$A_n \in \mathcal {WO}$
. Then note that, for all n,
$A_n <A_{n+1}$
and
$A:=\bigcup _n A_n$
and conclude that
$A\in \mathcal {WO}$
.
The next result may be compared to results in [Reference Howard and Kreisel17, Section 5].
Theorem 28.
Footnote
26
For every enumerable subset A of
$\mathbb {Q}$
, if A is (explicitly) well-founded, then
$A\in \mathcal {WO}$
.
Proof For every
$\alpha $
we define
$A_\alpha :=\{q_n\mid \exists m[\alpha (m)=n+1]\}$
. Note that
$A\subseteq \mathbb {Q}$
is enumerable if and only if
$\exists \alpha [A=A_\alpha ]$
.
For every
$\alpha $
, define
$B_\alpha :=\bigcup _n \{s\in \omega ^{n+1} \mid \exists i<n+1[\alpha \circ s(i)=0]\} \cup \bigcup _n\{s\in \omega ^{n+2}\mid \forall i<n+2[\alpha \circ s(i)>0]\;\wedge \; q_{\alpha \circ s(n)-1}\le q_{\alpha \circ s(n+1)-1}\}$
.
Note that, by Lemma 26, for each
$\alpha $
,
$A_\alpha $
is well-founded if and only if
$\forall \gamma \exists n[\overline \gamma n \in B_\alpha ]$
, i.e.,
$B_\alpha $
is bar in
$\omega ^{\omega }$
. Note that, by Theorem 24, for each
$\alpha $
,
$A_\alpha $
is well-founded if and only if there exists a stump S such that
$S\cap B_\alpha $
is a bar in
$\omega ^{\omega }$
.
We will say say that a stump S has the property
$(\ast )$
if and only if
$$ \begin{align*} (\ast) \textit{for every } \alpha\textit{, if } S\cap B_\alpha \text{ is a bar in } \omega^{\omega}\textit{, then } A_\alpha\in \mathcal{WO}. \end{align*} $$
We now prove that every stump has the property
$(\ast )$
, by induction on the set
$\mathbf {Stp}$
of stumps. Let a stump S be given such that every immediate substump of S has the property
$(\ast )$
. Let
$\alpha $
be given such that
$S\cap B_\alpha $
is a bar in
$\omega ^{\omega }$
. We want to prove that
$A_\alpha \in \mathcal {WO}$
, and, by Lemma 27, it suffices to prove that, for all q in
$\mathbb {Q}$
, if
$q \in A_\alpha $
, then
$\{r\in A_\alpha \mid r\le q\}\in \mathcal {WO}$
. Let q in
$A_\alpha $
be given. Find m such that
$\alpha (m)>0$
and
$q_{\alpha (m)-1}=q$
. Define
$\beta $
such that, for all p, if
$\alpha (p)>0$
and
$q_{\alpha (p)-1}<q$
, then
$\beta (p)=\alpha (p)$
, and, if not, then
$\beta (p)= 0$
. Note that
$A_\beta = \{r\in A_\alpha \mid r<q\}$
. Let
$\delta $
be given. Find p such that
$\langle m \rangle \ast \overline \delta p \in S\cap B_\alpha $
. Note that
$\alpha (m)>0$
and, therefore,
$p>0$
. Now distinguish two cases.
Case (a).
$\alpha \circ \delta (p-1) =0$
. Then also
$\beta \circ \delta (p-1)=0$
and
$\overline \delta p \in B_\beta $
.
Case (b).
$\alpha \circ \delta (p-1)>0$
. We distinguish two subcases.
Case (bi).
$p=1$
and
$q=q_{\alpha (m)-1}\le q_{\alpha \circ \delta (0)-1}$
. Then
$\beta \circ \delta (0) =0$
and
$\overline \delta 1= \overline \delta p \in B_\beta $
.
Case (bii).
$p>1$
and
$\forall i <p[\alpha \circ \delta (i)>0]$
and
$q_{\alpha \circ \delta (p-2)-1}\le q_{\alpha \circ \delta (p-1)-1}$
. Now either
$\beta \circ \delta (p-2)=\alpha \circ \delta (p-2)$
and
$\beta \circ \delta (p-1)=\alpha \circ \delta (p-1)$
and
$\overline \delta p \in B_\beta $
, or
$\exists i<p[\beta \circ \delta (i) = 0]$
and, again,
$\overline \delta p \in B_\beta $
.
Conclude that
$\forall \delta \exists p[\langle m \rangle \ast \overline \delta p \in S \;\wedge \; \overline \delta p \in B_\beta ]$
. We thus see that
$(S\upharpoonright \langle m \rangle )\cap B_\beta $
is a bar in
$\omega ^{\omega }$
. As
$S\upharpoonright \langle m \rangle $
has the property
$(\ast )$
, conclude that
$A_\beta =\{r\in A_\alpha \mid r<q\} \in \mathcal {WO}$
and that also
$\{r\in A_\alpha \mid r\le q\} \in \mathcal {WO}$
. We thus see that, for all q in
$\mathbb {Q}$
, if
$q\in A_\alpha $
, then
$\{r\in A_\alpha \mid r\le q\} \in \mathcal {WO}$
. Conclude that
$A_\alpha =\bigcup _n A_n \in \mathcal {WO}$
.
We may conclude that every stump has the property
$(\ast )$
and that every enumerable and well-founded subset of
$\mathbb {Q}$
belongs to
$\mathcal {WO}$
.
6.4 Bar Induction
Theorem 29 (Principle of Bar Induction).
Let
$B,C\subseteq \omega $
be given such that
$Bar_{\omega ^{\omega }}(B)$
and
$B\subseteq C$
and
$\forall s[s\in C\leftrightarrow \forall n[s\ast \langle n \rangle \in C]]$
. Then
$\langle \;\rangle \in C$
.
Proof
Footnote
27
Assume
$Bar_{\omega ^{\omega }}(B)$
, i.e., B bars
$\langle \;\rangle $
. Find a canonical proof of: ‘B bars
$\langle \;\rangle $
’. Assume also that
$B\subseteq C$
and
$\forall s[s\in C\leftrightarrow \forall n[s\ast \langle n \rangle \in C]]$
. In the canonical proof, replace every statement: ‘B bars s’ by the statement ‘
$s \in C$
’. Note that the result is another valid proof, with conclusion:
$`\langle \;\rangle \in C$
’.
Note that, conversely, our ‘proof’ of Theorem 24, the Bar Theorem, actually is an application the Principle of Bar Induction.
6.5 Using Bar Induction rather than the Bar Theorem itself
We may give a second proof of Theorem 28.
Proof Let
$\alpha $
be given such that
$A_\alpha =\{q_n\mid \exists m[\alpha (m)=n+1\}$
is well-founded. We then may conclude that
$B_\alpha :=\bigcup _n \{s\in \omega ^{n+1} \mid \exists i < n+1 [\alpha \circ s (i)=0]\} \cup \bigcup _n\{s\in \omega ^{n+2}\mid \forall i<n+2[\alpha \circ s(i)>0] \;\wedge \; q_{\alpha \circ s(n)-1}\le q_{\alpha \circ s(n+1)-1}\}$
is a bar in
$\omega ^{\omega }$
. Let
$C_\alpha $
be the set of all s such that either
$\exists t\sqsubseteq s[t \in B_\alpha ]$
or
$s=\langle \;\rangle $
and
$A_\alpha \in \mathcal {WO}$
, or
$n:=length(s)>0$
and
$\alpha \circ s(n-1)>0$
and
$\{r\in A_\alpha \mid r \le q_{\alpha \circ s(n-1)-1}\}\in \mathcal {WO}$
. Note that
$B_\alpha \subseteq C_\alpha $
. Also note that, for all s, if
$s\in C_\alpha $
, then
$\forall n[s\ast \langle n \rangle \in C_\alpha ]$
. Finally, let s be given such that
$\forall n[s\ast \langle n \rangle \in C_\alpha ]$
. We want to prove that
$s\in C_\alpha $
. If
$\exists t\sqsubseteq s[t\in B_\alpha ]$
, we are done. Define
$p:= length(s)$
. We may assume that
$\forall i<p[\alpha \circ s(i)>0]$
and
$\forall i[i+1<p\rightarrow q_{\alpha \circ s(p-2)-1}< q_{\alpha \circ s(p-1)-1}]$
.
Case (1).
$s=\langle \;\rangle $
. For all m, such that
$\alpha (m)>0$
, we note that
$\langle m \rangle $
belongs to
$C_\alpha $
, and conclude that
$\{r\in A_\alpha \mid r \le q_{\alpha (m)-1}\} \in \mathcal {WO}$
. It follows that, for each q in
$A_\alpha $
, the set
$\{r\in A_\alpha \mid r\le q\}$
belongs to
$\mathcal {WO}$
. By Lemma 27,
$A\in \mathcal {WO}$
and
$\langle \;\rangle \in C$
.
Case (2).
$p:=length(s)>0$
. For all m, such that
$\alpha (m)>0$
and
$q_{\alpha (m)-1}< q_{s(p-1)-1} $
we note that
$s\ast \langle m \rangle $
belongs to
$C_\alpha $
, and conclude that
$\{r\in A_\alpha \mid r \le q_{\alpha (m)-1}\} \in \mathcal {WO}$
. It follows that, for each q in
$A_\alpha $
, if
$q<q_{\alpha \circ s(p-1)-1}$
, then
$\{r\in A_\alpha \mid r \le q\} \in \mathcal {WO}$
. By Lemma 27,
$\{r \in A_\alpha \mid r\le q_{\alpha \circ s(p-1)-1}\}\in \mathcal {WO}$
and
$s \in C_\alpha $
.
Using Theorem 29, we conclude that
$\langle \;\rangle \in C$
and
$A\in \mathcal {WO}$
.
7 The Almost-Fan Theorem
We want to show that Brouwer’s Thesis on bars in
$\omega ^{\omega }$
has many more applications than the applications mentioned in the previous Section. In Section 7.1 we introduce the notion of an almost-finite subset of
$\omega $
and in Section 7.2 we introduce almost-finitary spreads. i.e., almost-fans, and we formulate the Almost-Fan Theorem. We will see that, like the Fan Theorem, the Almost-Fan Theorem follows from the Bar Theorem and that the Almost-Fan Theorem implies the Fan theorem. In the remaining five Subsections we consider some consequences of the Almost-Fan Theorem. In Section 7.3 we formulate the Principle of Open Induction on
$[0,1]$
and show that it follows from the Almost-Fan Theorem. In Section 7.4 we see that the Principle of Open Induction on
$[0,1]$
implies a version of ‘Dedekind’s Theorem’, i.e., the theorem that every bounded and non-decreasing sequence of rationals has a limit. In Section 7.5 we prove that the Almost-Fan Theorem also implies an intuitionistic version of the Infinite Ramsey Theorem. In Section 7.6 we use this Ramsey Theorem together with Dedekind’s Theorem in order to prove an intuitionistic version of the Bolzano–Weierstrass Theorem. In Section 7.7 we show that the Infinite Ramsey Theorem implies the Paris–Harrington–Ramsey Theorem.
One may compare the results of this Section with results in classical Reverse Mathematics, see [Reference Simpson23, Chapter III]. One there proves, among other things, the equivalence over
$\mathrm {RCA}_0$
of König’s Lemma, the Bolzano–Weierstrass Theorem and Ramsey’s Theorem. These three statements are wrong, if read constructively. The Almost-Fan Theorem may be seen as a (proposal for a) constructive substitute for König’s Lemma. The Almost-Fan Theorem is a kind of contraposition of König’s Lemma.Footnote
28
Similarly, the Intuitionistic Bolzano–Weierstrass Theorem and the Intuitionistic Ramsey Theorem are contrapositions of their classical counterparts.
In this paper, we do not follow a strictly formal approach and we refrain from proving formal equivalences, but we do so in [Reference Veldman36] and [Reference Veldman37].
7.1 Almost-finite subsets of
$\omega $
One may formulate many notions of finiteness, even for decidable subsets of
$\omega $
, see [Reference Veldman, de Swart and Bergmans27], [Reference Veldman and Cantini28] and [Reference Veldman31, Section 3]. We need three of them.
Definition 26.
$B\subseteq \omega $
is a decidable subset of
$\omega $
if and only if
$\exists \alpha \forall n[n\in B\leftrightarrow \alpha (n)\neq 0]$
. A decidable subset B of
$\omega $
is
-
(1) finite if and only if
$\exists n\forall m>n[m\notin B]$
, -
(2) bounded-in-number if and only if
$\exists k\forall s \in [\omega ]^{k+1}\exists i\le k[s(i)\notin B]$
, and -
(3) almost-finite if and only if
$\forall \zeta \in [\omega ]^{\omega }\exists i[\zeta (i)\notin B]$
.
Theorem 30.
-
(i) For every decidable
$B\subseteq \omega $
, if B is finite, then B is bounded-in-number, but not conversely. -
(ii) For every decidable
$B\subseteq \omega $
, if B is bounded-in-number, then B is almost-finite, but not conversely.
Proof (i) Let
$B\subseteq \omega $
be decidable and finite. Find n be such that
$\forall m>n[m \notin B]$
. Clearly, for all s in
$[\omega ]^{n+2}$
,
$s(n+1)>n$
and
$s(n+1)\notin B$
. We thus see that B is bounded-in-number.
As to the converse, we give a counterexample in Brouwer’s style. Let
$d:\omega \rightarrow \{0,1,\ldots ,9\}$
be the decimal expansion of
$\pi $
. Define
$B:=\{k_{99}\}:=\{n \mid n=\mu k \forall i<99[d(k+i)=9]\}$
. B is a decidable subset of
$\omega $
and B has at most one member, but we are unable to find n such that
$\forall m>n[m\notin B]$
.
(ii) Let
$B\subseteq \omega $
be decidable and bounded-in-number. Find k such that
$\forall s \in [\omega ]^{k+1}\exists i\le k[s(i) \notin B]$
. Conclude that
$\forall \zeta \in [\omega ]^{\omega } \exists i\le k[\zeta (i)\notin B]$
and B is almost-finite.
As to the converse, we give a counterexample in Brouwer’s style. Define
$B:=\{n\mid k_{99} \le n \le 2\cdot k_{99}\}:= \{ n\mid \mu k \forall i<99[d(k+i)=9\}]\le n \le 2\cdot \mu k \forall i<99[d(k+i)=9]\}$
. Let
$\zeta $
in
$[\omega ]^{\omega }$
be given. Either
$\zeta (0)< k_{99}$
and
$\zeta (0)\notin B$
, or
$\zeta (0)\ge k_{99}$
and
$\zeta (2\cdot k_{99} +1)\notin B$
. We thus see that B is almost-finite. We are unable, however, to find n such that B has at most n members.
We now prove that the union of two almost-finite subsets of
$\omega $
is almost-finite, and that a decidable subset of
$\omega $
that is the union of almost-finitely many almost-finite subsets of
$\omega $
, is itself almost-finite.
Lemma 31.
-
(i) For all decidable subsets
$B,C$
of
$\omega $
, if
$B,C$
are almost-finite, then
$B\cup C$
is almost-finite. -
(ii) For every decidable subset B of
$\omega $
, if there exists an infinite sequence
$B_0, B_1, B_2, \ldots $
of decidable and almost-finite subsets of
$\omega $
such that
$B=\bigcup _n B_n$
and
$\forall \zeta \in [\omega ]^{\omega }\exists i[B_{\zeta (i)}=\emptyset ]$
, then B itself is almost-finite.
Proof (i) Let
$\zeta $
in
$[\omega ]^{\omega }$
be given. Find
$\eta $
in
$[\omega ]^{\omega }$
such that, for each n,
$\eta (n)=\mu p[\forall i<n[p>\eta (i)]\;\wedge \;\zeta (p) \notin B]$
. Note that
$\forall p[\zeta \circ \eta (p)\notin B]$
. Find p such that
$\zeta \circ \eta (p)\notin C$
. Define
$m:=\eta (p)$
and note:
$\zeta (m) \notin B\cup C$
. We thus see:
$\forall \zeta \in [\omega ]^{\omega }\exists m[\zeta (m)\notin B\cup C]$
.
(ii) Let
$\zeta $
in
$[\omega ]^{\omega }$
be given. We want to prove
$QED:=\exists p[\zeta (p)\notin \bigcup _n B_n]$
.Footnote
29
Find
$\alpha $
such that, for all p, if
$\zeta (p)\in B=\bigcup _n B_n$
, then
$\alpha (p)=\mu n[\zeta (p)\in B_n]$
. We claim that
$\forall p \exists q>p[\alpha (q)>p \;\vee \; QED]$
and we prove this claim as follows. Let p be given. Using (i), observe that
$\bigcup _{i\le p}B_i$
is almost-finite. Find
$q>p$
such that
$\zeta (q) \notin \bigcup _{i \le p}B_i$
. If
$\zeta (q) \in \bigcup _n B_n$
, then
$\alpha (q)>p$
. If
$\zeta (q) \notin \bigcup _n B_n$
, then
$QED$
. Now find
$\eta $
in
$[\omega ]^{\omega }$
such that
$\eta (0)=0$
and
$\forall p[\alpha \circ \eta (p+1)> \alpha \circ \eta (p) \;\vee \; QED]$
. Find p such that
$B_{\alpha \circ \eta (p)}=\emptyset $
and conclude that either
$QED$
, or
$\zeta \circ \eta (p)\notin \bigcup _nB_n$
and, again,
$QED$
.
7.2 Almost-finitary spreads
Definition 27. A spread-law
$\beta $
will be called almost-finitary if it satisfies the following condition:
$$\begin{align*}\forall s[\beta(s)=0\rightarrow \forall \zeta\in[\omega]^{\omega}\exists n[\beta(s\ast\langle \zeta(n) \rangle)\neq 0]]. \end{align*}$$
If the spread-law
$\beta $
is almost-finitary, the corresponding spread
$\mathcal {F}_\beta $
will be called an almost-finitary spread or an almost-fan.
If
$\beta $
is an almost-finitary spread-law and s is admitted by
$\beta $
, there are only almost-finitely many immediate successors
$s\ast \langle n \rangle $
of s that are admitted by
$\beta $
.
The following theorem appears in [Reference Veldman, Berger, Osswald and Schuster29] and [Reference Veldman37, Section 7.2].
Theorem 32 (Almost-Fan Theorem).
Let
$\beta $
be an almost-finitary spread-law and let
$B\subseteq \omega $
be a bar in
$\mathcal {F}_\beta $
. There exists
$B'\subseteq B$
such that
$B'$
is a bar in
$\mathcal {F}_\beta $
and
$B'$
is a decidable and almost-finite subset of
$\omega $
.
Proof Let
$\beta $
be an almost-finitary-spread-law and let
$B\subseteq \omega $
be a bar in
$\mathcal {F}_\beta $
. Define
$B^+:= B \cup \{s\mid \beta (s)\neq 0\}$
. Then
$B^+$
is a bar in
$\omega ^{\omega }$
Footnote
30
.
Let C be the set of all s such that either
$\beta (s)\neq 0$
or
$\beta (s)=0$
and there exists
$B'\subseteq B$
such that
$Bar_{\mathcal {F}_\beta \cap s}(B')$
and
$B'$
is a decidable and almost-finite subset of
$\omega $
. Note that
$B^+\subseteq C$
. Also note that, for all s, if
$s\in C$
, then for all n,
$s\ast \langle n \rangle \in C$
. We now prove that, for all s, if
$\forall n[s\ast \langle n \rangle \in C]$
, then
$s\in C$
. Let s be given such that
$\forall n[s\ast \langle n \rangle \in C]$
. Find, using Axiom 3, an infinite sequence
$B_0, B_1, \ldots $
of subsets of B such that, for each n, if
$\beta (s\ast \langle n \rangle )\neq 0$
, then
$B_n=\emptyset $
and, if
$\beta (s\ast \langle n \rangle )=0$
, then
$B_n$
is a decidable and almost-finite subset of
$\omega $
and
$B_n$
is a bar in
$\mathcal {F}_\beta \cap s\ast \langle n\rangle $
. Define
$E:=\bigcup _n B_n$
and note that E is a decidable subset of
$\omega $
and
$\forall \zeta \in [\omega ]^{\omega }\exists n[B_{\zeta (n)}=\emptyset ]$
and E is a bar in
$\mathcal {F}_\beta \cap s$
and
$E\subseteq B$
. According to Lemma 31, E is almost-finite. One may conclude that
$s \in C$
. We thus see that, indeed, if
$\forall n[s\ast \langle n \rangle \in C]$
, then
$s\in C$
.
Using Theorem 29, conclude that
$\langle \;\rangle \in C$
, i.e., there exists
$B'\subseteq B$
such that
$B'$
is bar in
$\mathcal {F}_\beta $
and
$B'$
is a decidable and almost-finite subset of
$\omega $
.
Corollary 33. Let
$\beta $
be an almost-finitary spread-law and let B be a decidable subset of
$\omega $
that is a bar in
$\mathcal {F}_\beta $
. The set
$Below(B):=\{s \mid \beta (s)=0 \;\wedge \; \forall t\sqsubseteq s[t\notin B]\}$
is a decidable and almost-finite subset of
$\omega $
.
Proof Using Theorem 32 find a decidable and almost-finite subset
$B'$
of
$\omega $
such that
$B'\subseteq B$
and
$Bar_{\mathcal {F}_\beta }(B')$
. Note that
$Below(B) \subseteq Below(B')= \bigcup _{s\in B'}\{t\mid t\sqsubset s\}$
. Using Lemma 31(ii), conclude that
$Below(B)$
is almost-finite.
The Fan Theorem may be derived from the Almost-Fan Theorem, as follows.
Corollary 34 (Fan Theorem).
Let
$\beta $
be a finitary spread-law. If
$B\subseteq \omega $
is a a decidable subset of
$\omega $
and a bar in
$\mathcal {F}_\beta $
, some finite subset of B is a bar in
$\mathcal {F}_\beta $
.
Proof Let
$\beta $
be a finitary spread-law and let
$B\subseteq \omega $
be a decidable subset of
$\omega $
and a bar in
$\mathcal {F}_\beta $
. Applying the Almost-Fan Theorem, Theorem 32, find
$B'\subseteq B$
such that
$B'$
is a bar in
$\mathcal {F}_\beta $
and
$B'$
is a decidable and almost-finite subset of
$\omega $
. Note that
$\mathcal {F}_\beta $
is a fan. Therefore, for all n, for all s in
$\omega ^n$
, either
$\forall \alpha \in \mathcal {F}_\beta \exists i<n[s(i)\sqsubset \alpha ]$
, i.e., the set
$\{s(0), s(1), \ldots , s(n-1)\}$
is a bar in
$\mathcal {F}_\beta $
, or
$\exists \alpha \in \mathcal {F}_\beta \forall i <n[s(i)\perp \alpha ]$
. Now define
$\eta $
such that, for all n, if
$\exists \alpha \in \mathcal {F}_\beta \forall i<n[\alpha \perp \eta (i)]$
, then
$\eta (n) = \mu t \in B'\forall i<n[t\perp \eta (i)]$
, and, if
$\forall \alpha \in \mathcal {F}_\beta \exists i<n[\ \eta (i)\sqsubset \alpha ]$
, then
$\eta (n)=\mu p[\beta (p)\neq 0 \;\wedge \;\forall i<n[\eta (i)<p]]$
. Note that
$\eta \in [\omega ]^{\omega }$
. Define
$k:=\mu n[\eta (n)\notin B']$
and conclude that
$\{\eta (0), \eta (1), \ldots \eta (k-1)\}$
is a finite subset of B and a bar in
$\mathcal {F}_\beta $
.
7.3 Open Induction in
$[0,1]$
Definition 28. Let
$(q_0, r_0), (q_1, r_1), \ldots $
be an enumeration of all pairs
$(q,r)$
of rationals such that
$q\le r$
. Note that
$q_0, q_1, \ldots $
then is an enumeration of all rationals.
RecallFootnote
31
that, for every n for every a in
$\omega ^n$
,
$\mathcal {H}_a= \bigcup _{i<n}(q_{a(i)}, r_{a(i)})$
. We now define
$\chi $
such that, for each a,
$\chi (a)$
is the largest rational c such that
$[0,c)\subseteq \mathcal {H}_a$
. One may define
$\chi (a)$
by induction on
$length(a)$
, as follows.
-
(i)
$\chi (\langle \;\rangle ) =0$
, and -
(ii) for all a, for all p, if
$q_{p}<q_{\chi (a)}<r_{p}\}$
, then
$\chi (a\ast \langle p\rangle )=r_p$
, and, if not, then
$\chi (a\ast \langle p \rangle )=\chi (a)$
.
Definition 29.
$\mathcal {X}\subseteq [0,1]$
is called progressive in
$[0,1]$
if and only if, for every x in
$[0,1]$
, if
$[0,x)\subseteq \mathcal {X}$
, then
$x\in \mathcal {X}$
.
The following principle was used by É. Borel in the proof of what is now called the Heine–Borel Theorem, see [Reference Borel2] and [Reference Veldman37, Section 4.3]. Its first proof in an intuitionistic context is due to Th. Coquand, see [Reference Coquand12] and [Reference Veldman37, Theorem 4.1].
Theorem 35 (Principle of Open Induction in
${[} 0, 1{]} $
).
If
$\mathcal {H}\subseteq \mathcal {R}$
is open and progressive in
$[0,1]$
, then
$[0,1]\subseteq \mathcal {H}$
.
Proof We first construct
$\rho $
such that, for each s,
$\rho (s)=\big (\rho '(s), \rho "(s)\big )$
is a pair of rationals and
$0\le \rho '(s)\le \rho "(s)\le 1$
. The definition is by induction on
$length(s)$
.
-
(i)
$\rho (\langle \;\rangle ):= (0,1)$
and, -
(ii) for each s,
$\rho (s\ast \langle 0 \rangle )):=\big (\rho '(s), \frac {\rho '(s) +\rho "(s)}{2}\big )$
and, -
(iii) for each s, for each
$n>0$
,
$\rho (s\ast \langle n\rangle ) := \big (\frac {\rho '(s) +\rho "(s)}{2}, \rho "(s)\big )$
.
This is almost the same definition as in Definition 20, but the function we defined here behaves differently on
$\omega \setminus 2^{<\omega }$
than the function defined in Definition 20.
Now let
$\mathcal {H}\subseteq \mathcal {R}$
be given such that
$\mathcal {H}$
is open and progressive in
$[0,1]$
. Find
$\alpha $
be such that
$\mathcal {H}=\mathcal {H}_\alpha $
. Note that
$\mathcal {H}_\alpha =\bigcup _n \mathcal {H}_{\overline \alpha n}$
and that
$\forall n[\chi (\overline \alpha n)\le \chi \big (\overline \alpha (n+1)\big )]$
.
Define
$\beta $
such that
$\beta (\langle \;\rangle )=0$
and, for all s,
-
(1) if
$\beta (s)=0$
, then
$\beta (s\ast \langle 0 \rangle )=0$
and, -
(2) for all
$ n$
,
$\beta (s\ast \langle n+1 \rangle ) =0$
if and only if n is the least p such that
$\chi (\overline \alpha p)\ge \frac {\rho '(s)+\rho "(s)}{2}$
.
Note that, if
$\beta (s\ast \langle n+1\rangle ) =0$
, then
$\rho '(s\ast \langle n+1\rangle )=\frac {\rho '(s)+\rho "(s)}{2}$
and
$[0, \rho '(s\ast \langle n+1\rangle )]\subseteq \mathcal {H}_{\overline \alpha n}$
. One may prove that, for each s, if
$\beta (s)=0$
, then
$[0, \rho '(s)]\subseteq \mathcal {H}$
. The proof goes by induction on
$length(s)$
.
Note that
$\beta $
is a spread-law, and that, for each s, if
$\beta (s)=0$
, there are at most two numbers n such that
$\beta (s\ast \langle n \rangle )=0$
, so
$\beta $
is an almost-finitary spread-law.
We let B be the set of all s such that
$\beta (s)=0$
and, for some
$n<length(s)$
,
$q_{\alpha (n)} < \rho '(s) <\rho "(s) < r_{\alpha (n)}$
. We now prove that B is a bar in
$\mathcal {F}_\beta $
. Let
$\gamma $
in
$\mathcal {F}_\beta $
be given. Note that, for each n,
$[0, \rho '(\overline \gamma n)]\subseteq \mathcal {H}$
. Let x be the real number such that, for each n,
$x(n)=\rho (\overline \gamma n )$
. Note that
$[0,x)\subseteq \mathcal {H}$
, and, therefore,
$x\in \mathcal {H}$
. Find n such that
$q_{\alpha (n)}<x<r_{\alpha (n)}$
. Find
$m>n$
such that
$q_{\alpha (n)}<\rho '(\overline \gamma m)<\rho "(\overline \gamma m)<r_{\alpha (n)}$
and note that
$\overline \gamma m \in B$
. Conclude that
$\forall \gamma \in \mathcal {F}_\beta \exists m[\overline \gamma m \in B]$
.
We now apply Theorem 32 and find
$B'\subseteq B$
such that
$B'$
is a bar in
$\mathcal {F}_\beta $
and a decidable and almost-finite subset of
$\omega $
. Recall, from Definition 28, that, for each a,
$\chi (a)$
is the largest rational c such that
$[0,c)\subseteq \mathcal {H}_a$
. Define
$\zeta $
in
$\omega ^{\omega }$
as follows, by induction. For each n, we distinguish two cases.
Case (1).
$\chi (\overline \zeta n) <1$
. Note that
$[0, \chi (\overline \zeta n)\big )\subseteq \mathcal {H}_\alpha $
and, therefore,
$\chi (\overline \zeta n) \in \mathcal {H}_\alpha $
. Let
$\zeta (n)$
be the least s in
$B'$
such that
$\rho '(s)<\chi (\overline \zeta n) < \rho "(s)$
.
Case (2).
$\chi (\overline \zeta n) \ge 1$
. Let
$\zeta (n)$
be the least s such that
$s\notin B'$
and
$\forall i\le n[ \zeta (i)<s]$
. Observe that
$\chi (\overline \zeta n)< \chi \big ( \overline \zeta (n+1)\big )$
.
Note that
$\forall i\forall j[i<j\rightarrow \zeta (i)\neq \ \zeta (j)]$
. Find
$\eta $
in
$[\omega ]^{\omega }$
such that
$\zeta \circ \eta \in [\omega ]^{\omega }$
Use the fact that
$B'$
is almost-finite and conclude that
$\exists n[\zeta \circ \eta (n)\notin B']$
. Let p be the least n such that
$\zeta (n+1)\notin B'$
and note that
$\chi (\overline \zeta p)\ge 1$
, and
$[0,1]\subseteq \mathcal {H}$
.
7.4 Dedekind’s Theorem
The following Theorem shows that a nondecreasing sequence of reals that positively fails to converge grows beyond all bounds. This is a counterpart in intuitionistic analysis to ‘Dedekind’s Theorem’:
‘A non-decreasing infinite sequence of reals that is bounded from above must have a limit’.
R. Dedekind’s aim in writing [Reference Dedekind13] was to give a rigorous proof of this statement.Footnote 32
Theorem 36 (Dedekind’s Theorem).
For all
$\gamma $
, if
$\forall n[q_{\gamma (n)}\le q_{ \gamma (n+1)}]$
and
$\forall \zeta \in [\omega ]^{\omega }\exists n [ q_{\gamma \circ \zeta (n)} + \frac {1}{2^n}< q_{\gamma \circ \zeta (n+1)}]$
, then
$\exists n[ 1 <q_{ \gamma (n)}]$
.
Note that the condition: ‘
$\forall \zeta \in [\omega ]^{\omega }\exists n [ q_{\gamma \circ \zeta (n)} + \frac {1}{2^n}< q_{\gamma \circ \zeta (n+1)}]$
’ says: ‘The sequence
$q_{\gamma (0)}, q_{\gamma (1)}, \ldots $
positively fails to be convergent’.
Also note that, once one sees how to obtain the conclusion ‘
$\exists n[ 1 <q_{ \gamma (n)}]$
’, one will also see how to obtain the conclusion: ‘
$\forall M\in \mathbb {Q}\exists n[ M<r_{\gamma (n)}]$
’, i.e., ‘The sequence
$q_{\gamma (0)}, q_{\gamma (1)}, \ldots $
grows beyond all bounds’.
Proof Define
$\mathcal {H}:=\{x\in \mathcal {R}\mid \exists n[x<q_{\gamma (n)}]\}$
. Note that
$\mathcal {H}$
is an open subset of
$\mathcal {R}$
. We now prove that
$\mathcal {H}$
is progressive in
$[0,1]$
. Let x in
$[0,1]$
be given such that
$[0,x)\subseteq \mathcal {H}$
. Then, in particular, for each n,
$x-\frac {1}{2^n} \in \mathcal {H}$
. Find
$\zeta $
in
$[\omega ]^{\omega }$
such that, for each n,
$x-\frac {1}{2^n} < q_{\gamma \circ \zeta (n)}$
, i.e.,
$x<q_{\gamma \circ \zeta (n)}+\frac {1}{2^n}$
. Find n such that
$q_{\gamma \circ \zeta (n)} +\frac {1}{2^n}<q_{\gamma \circ \zeta (n+1)}$
and conclude that
$x<q_{\gamma \circ \zeta (n+1)}$
, and that
$x\in \mathcal {H}$
. Conclude that
$\forall x \in [0,1][[0,x)\subseteq \mathcal {H}\rightarrow x \in \mathcal {H}]$
, i.e.,
$\mathcal {H}$
is progressive in
$[0,1]$
. Using Theorem 35, conclude that
$1\in \mathcal {H}$
, i.e.,
$\exists n[1<q_{\gamma (n)}]$
.
One may also prove the Principle of Open Induction on
$[0,1]$
from Dedekind’s Theorem, see [Reference Veldman37, Corollary 5.7].
7.5 Ramsey’s Theorem
The usual formulation of (the two-dimensional case of) the Infinite Ramsey Theorem is the following.
Given
$R\subseteq [\omega ]^2$
, there exists an infinite subset Z of
$\omega $
such that either
$[Z]^2 \subseteq R$
or
$[Z]^2\subseteq [\omega ]^2\setminus R$
.
Usually, given any
$X\subseteq \omega $
,
$[X]^2$
denotes the collection of the 2-element-subsets of X. We prefer to define
$[X]^2$
as the collection of strictly increasing sequences of elements of X of length 2. We also prefer the set
$[\omega ]^{\omega }$
of the infinite strictly increasing sequences of natural numbers above the the collection of the infinite subsets of
$\omega $
. We now reformulate Ramsey’s theorem:
Given
$R\subseteq [\omega ]^2$
, there exists
$\zeta $
in
$[\omega ]^{\omega }$
such that
either
$\forall s \in [\omega ]^2[\zeta \circ s \in R]$
or
$\forall s \in [\omega ]^2[\zeta \circ s \notin R]$
.
As finite sequences of natural numbers are coded by natural numbers, we may further simplify this to:
Given
$R\subseteq \omega $
, there exists
$\zeta $
in
$[\omega ]^{\omega }$
such that
either
$\forall s \in [\omega ]^2[\zeta \circ s \in R]$
or
$\forall s \in [\omega ]^2[\zeta \circ s \in \omega \setminus R]$
.
If we consider this statement from a constructive point of view, we soon discover, thinking of the constructive interpretation of ‘or’, that it can not be true. A counterexample in Brouwer’s style is given by the setFootnote 33
$$ \begin{align*} R:=\{s\in [\omega]^2 \mid s(0)<k_{99} \;\wedge\; s(1) < k_{99}\}. \end{align*} $$
(Note that, for every
$\zeta $
in
$[\omega ]^{\omega }$
, if
$\forall s \in [\omega ]^2[\zeta \circ s \in R]$
, then
$\forall n[n< k_{99}]$
, and, if
$\forall s \in [\omega ]^2[\zeta \circ s \notin R]$
, then
$\exists n\le \zeta (0)[n=k_{99}]$
.)
One might hope however, that the following holds:
Given
$R\subseteq \omega $
, a contradiction follows from the assumption
$\neg \exists \zeta \kern1.5pt{\in}\kern1.5pt [\omega ]^{\omega }\forall s \kern1.5pt{\in}\kern1.5pt [\omega ]^2[\zeta \circ s \kern1.5pt{\in} R]$
and
$\neg \exists \zeta \kern1.5pt{\in}\kern1.5pt [\omega ]^{\omega }\forall s \kern1.5pt{\in}\kern1.5pt [\omega ]^2[\zeta \circ s \kern1.5pt{\in}\kern1.5pt \omega \kern1.5pt{\setminus}\kern1.5pt R]$
.
This turns out to be difficult. One may replace the assumption by a more positive one and cherish some hopes about:
Given
$R\subseteq \omega $
, a contradiction follows from the assumption
$\forall \zeta \kern1.6pt{\in}\kern1.6pt [\omega ]^{\omega }\exists s \kern1.6pt{\in}\kern1.6pt [\omega ]^2[\zeta \circ s \kern1.6pt{\in}\kern1.6pt \omega \setminus R]$
and
$\forall \zeta \kern1.5pt{\in}\kern1.5pt [\omega ]^{\omega }\exists s \kern1.5pt{\in}\kern1.6pt [\omega ]^2[\zeta \circ s \kern1.6pt{\in}\kern1.6pt R]$
.
Indeed, this may be proven intuitionistically. One obtains this conclusion as a corollary of a stronger, more positive statement:
Given
$R, T\subseteq \omega $
, if
$\forall \zeta \in [\omega ]^{\omega }\exists s \in [\omega ]^2[\zeta \circ s \in R]$
and also
$\forall \zeta \in [\omega ]^{\omega }\exists s \in [\omega ]^2[\zeta \circ s \in T]$
, then
$\forall \zeta \in [\omega ]^{\omega }\exists s \in [\omega ]^2[\zeta \circ s \in R\cap T]$
.
We will prove Ramsey’s Theorem and its extension to higher dimensions in the above form. The proof uses the Almost-Fan Theorem and a version of the ‘Erdös-Rado compactness argument’.
Definition 30. For each
$\alpha $
,
$D_\alpha :=\{n\mid \alpha (n)\neq 0\}$
.
$D_\alpha $
is called the subset of
$\omega $
decided by
$\alpha $
. For each
$k>0$
, for each
$\alpha $
,
$D_\alpha $
is k-almost-full if and only if
$\forall \zeta \in [\omega ]^{\omega }\exists s \in [\omega ]^k[\zeta \circ s \in D_\alpha ]$
.
For all
$n,k$
such that
$k\le n$
, for all s in
$[\omega ]^n$
, for all
$\alpha $
,
-
(1) s is
$(\alpha , k)$
-monochromatic if and only if
$\forall t \in [n]^k\forall u \in [n]^k[\alpha (s\circ t)=\alpha (s\circ u)]$
, and -
(2) s is
$(\alpha , k+1)$
-pre-monochromatic if and only if
$\forall t \kern1.8pt{\in}\kern1.8pt [n]^k\forall p \forall q[(t\ast \langle p \rangle \in [n]^{k+1} \wedge t\ast \langle q \rangle \kern1.7pt{\in}\kern1.7pt [n]^{k+1})\rightarrow \alpha (t\ast \langle p \rangle )\kern1.7pt{=} \alpha (t\ast \langle q \rangle )]$
.
Note that, if
$D_\alpha $
is k-almost-full, then
$\neg \exists \zeta \kern1.4pt{\in}\kern1.4pt [\omega ]^{\omega }\forall s \kern1.4pt{\in}\kern1.4pt [\omega ]^k[\zeta \circ s \kern1.4pt{\in}\kern1.4pt \omega \setminus D_\alpha ]$
.
Theorem 37 (Ramsey’s Theorem, the infinite case).
For all
$k>0$
, for all
$\alpha , \beta $
, if
$D_\alpha $
,
$D_\beta $
are k-almost-full, then
$D_\alpha \cap D_\beta $
is k-almost-full.
Proof We use induction, and start with the case
$k=1$
.
Let
$\alpha , \beta $
be given such that
$D_\alpha , D_\beta $
are
$1$
-almost-full. Let
$\zeta $
in
$[\omega ]^{\omega }$
be given. Find
$\eta $
in
$[\omega ]^{\omega }$
such that
$\forall n \in \omega [\langle \zeta \circ \eta (n)\rangle \in D_\alpha ]$
. Find p such that
$\langle \zeta \circ \eta (p)\rangle \in D_\beta $
. Define
$q:=\eta (p)$
and note that
$\langle \zeta (q)\rangle \in D_\alpha \cap D_\beta $
. We thus see that
$\forall \zeta \in [\omega ]^{\omega }\exists q[\langle \zeta (q)\rangle \in D_\alpha \cap D_\beta $
, i.e.,
$D_\alpha \cap D_\beta $
is
$1$
-almost-full.
Now assume
$k>0$
is given such that for all
$\alpha , \beta $
, if
$D_\alpha $
,
$D_\beta $
are k-almost-full, then
$D_\alpha \cap D_\beta $
is k-almost-full. Let
$\alpha , \beta $
be given such that
$D_\alpha $
,
$D_\beta $
are
$k+1$
-almost-full. We want to prove that
$D_\alpha \cap D_\beta $
is
$k+1$
-almost-full. Let
$\zeta $
in
$[\omega ]^{\omega }$
be given. We want to prove
$QED:=\exists s\in [\omega ]^{k+1}[\zeta \circ s \in D_\alpha \cap D_\beta ]$
.Footnote
34
We define 
and 
. Define
$\varphi $
such that
$\varphi (0) = \langle \; \rangle $
, and, for each n,
$\varphi (n+1) = \varphi (j) \ast \langle n\rangle $
where j is the largest
$i\le n$
such that
$\varphi (i) \ast \langle n \rangle $
is both 
-pre-monochromatic and 
-pre-monochromatic. Note that
$\varphi (n+1)$
is well-defined, as
$\varphi (0) \ast \langle n \rangle $
is both 
-pre-monochromatic and 
-pre-monochromatic. Define
$\delta $
such that
$\delta (\langle \;\rangle )\neq 0$
and
$\forall t\forall n[\delta (t\ast \langle n\rangle ) \neq 0\leftrightarrow \varphi (n)=t\ast \langle n \rangle ]$
. Note that
$\forall s[\delta (s)\neq 0\leftrightarrow \exists n[\varphi (n)=s]]$
. The set
$D_\delta $
has the property that, for all
$s,n$
, if
$s\ast \langle n \rangle \in D_\delta $
, then
$s \in D_\delta $
, and for this reason,
$D_\delta $
is called a tree. We call
$D_\delta $
the 
-Erdös-Rado-tree. Note that
$D_\delta \subseteq [\omega ]^{<\omega }$
. Note that, for each n, there exists exactly one s such that
$s\ast \langle n \rangle \in D_\delta $
. Note that, for each n, for each s in
$D_\delta \cap \omega ^n$
, there are at most
$4^{\binom {n}{k}}$
numbers i such that
$s\ast \langle i \rangle \in D_\delta $
. This is because, for each n, the set
$[n]^k$
has
$\binom {n}{k}$
elements, and for each t in
$[n]^k$
, for each i,
$(s\circ t)\ast \langle i \rangle $
belongs to one of the four sets 
, 
, 
and 
. Define
$\varepsilon $
such that
$\forall s[\varepsilon (s) = 0\leftrightarrow \exists t\exists n[t \in D_\delta \;\wedge \;s = t\ast \overline {\underline 0}n]]$
. Note that
$\varepsilon $
is an almost-finitary spread-law and that the set
$\mathcal {F}_\varepsilon $
is an almost-finitary spread.
Define 
. We now prove that B is a bar in the almost-finitary spread
$\mathcal {F}_\varepsilon $
. Assume
$\gamma \in \mathcal {F}_\varepsilon $
. Define
$\gamma ^\ast $
such that, for each n, if
$\overline {\gamma }(n+1) \in D_\delta $
then
$\overline {\gamma ^\ast }(n+1) = \overline \gamma (n+1)$
, and, if not, then
$\overline {\gamma ^\ast }(n+1)\in [\omega ]^{n+1}\setminus D_\delta $
. Note that
$\gamma ^\ast \in [\omega ]^{\omega }$
and
$\forall n[\overline \gamma n \neq \overline {\gamma ^*}n\rightarrow \overline \gamma n \notin D_\delta ]$
. Recall that
$k>0$
. For each t in
$[\omega ]^k$
, we let
$t^+$
be the element of
$[\omega ]^{k+1}$
satisfying
$t\sqsubset t^+$
and
$t^+(k)=t(k-1)+1$
. Define
$\alpha ^\ast $
and
$\beta ^\ast $
such that, for each t in
$[\omega ]^k$
, 
and 
.
We now prove that
$\forall \eta \in [\omega ]^{\omega } \exists t\in [\omega ]^k [\eta \circ t \in D_{\alpha ^\ast } \;\vee \;\exists n[\overline {\gamma ^\ast }n\notin D_\delta ]].$
Let
$\eta \in [\omega ]^{\omega }$
be given. Find s in
$[\omega ]^{k+1}$
such that 
. Define
$n:=(\eta \circ s)(k) +1$
. Define
$t:= \overline s k$
and
$i:= s(k)$
. Note that 
, i.e., 
. Conclude that either 
. and, therefore,
$\eta \circ t \in D_{\alpha ^\ast }$
, or
$(\eta \circ t)^+ \neq \eta \circ s$
and
$\overline {\gamma ^\ast }n$
is not 
-pre-monochromatic, and, therefore,
$\overline {\gamma ^\ast } n \notin D_\delta $
.
One may prove by a similar argument that
$\forall \eta \in [\omega ]^{\omega }\exists t\in [\omega ]^k [\eta \circ t \in D_{\beta ^\ast }\;\vee \;\exists n[\overline {\gamma ^\ast }n\notin D_\delta ]]$
.
Define
$\alpha ^{\ast \ast },\beta ^{\ast \ast }$
such that
$\forall s[\alpha ^{\ast \ast }(s)\neq 0 \leftrightarrow \big (\alpha ^\ast (s)\neq 0\;\vee \;\exists n\le s[\delta (\overline {\gamma ^\ast }n)=0]\big )]$
and
$\forall s[\beta ^{\ast \ast }(s)\neq 0 \leftrightarrow \big (\beta ^\ast (s)\neq 0\;\vee \;\exists n\le s[\overline {\gamma ^\ast }n\notin D_\delta ]\big )]$
. Conclude that
$\forall \eta \in [\omega ]^{\omega } \exists t \in [\omega ]^k[\eta \circ t \in D_{\alpha ^{\ast \ast }}] \;\wedge \; \forall \eta \in [\omega ]^{\omega } \exists t \in [\omega ]^k[\eta \circ t \in D_{\beta ^{\ast \ast }}] $
.
Using the induction hypothesis, we conclude that
$\forall \eta \in [\omega ]^{\omega } \exists t \in [\omega ]^k[\eta \circ t \in D_{\alpha ^{\ast \ast }}\cap D_{\beta ^{\ast \ast }}]$
. Find t in
$[\omega ]^k$
such that
$t \in D_{\alpha ^{\ast \ast }} \cap D_{\beta ^{\ast \ast }}$
. Either
$t \in D_{\alpha ^\ast } \cap D_ {\beta ^\ast }$
or
$\exists n[\delta (\overline {\gamma ^\ast }n) = 0]$
, that is, either 
, where
$j = t(k-1) + 1$
, or
$\exists n[\delta (\overline {\gamma ^\ast } n) = 0]$
. In both cases, we find n such that
$\overline {\gamma ^\ast } n \in B$
. Either
$\overline \gamma n = \overline {\gamma ^\ast } n$
or
$\overline \gamma n \notin D_\delta $
. In both cases:
$\overline \gamma n \in B$
. We thus see that
$\forall \gamma \in \mathcal {F}_\varepsilon \exists n[\overline \gamma n \in B]$
, i.e.,
$Bar_{\mathcal {F}_\varepsilon }(B)$
.
We now use Corollary 33. Find
$\eta $
in
$[\omega ]^{\omega }$
such that
$D_\delta =\{\eta (n)\mid n\in \omega \}$
. Then find
$n,m$
such that
$\overline {\eta (n)}m \in B$
. Conclude that 
, i.e.,
$\exists t \in [\omega ]^{k+1}[ \zeta \circ t \in D_\alpha \cap D_\beta ]$
.
We thus see that
$\forall \zeta \in [\omega ]^{\omega }\exists t \in [\omega ]^{k+1}[ \zeta \circ t \in D_\alpha \cap D_\beta ]$
, i.e.,
$D_\alpha \cap D_\beta $
is
$(k+1)$
-almost-full.
This completes the proof of the induction step and, thereby, the proof of the Theorem.
In [Reference Veldman39, Section 18.3] one finds a proof of the so-called (Intuitionistic) Clopen Ramsey Theorem, an important extension of Theorem 37.
7.6 The Bolzano–Weierstrass Theorem
The Bolzano–Weierstrass Theorem:
‘An infinite sequence of reals bounded both from above and from below must have a convergent subsequence’.
is a strengthening of Dedekind’s Theorem, see Section 7.4. As Dedekind’s Theorem, in its usual formulation, already fails to be true constructively, the case of the usual formulation of the Bolzano–Weierstrass Theorem is also hopeless.
Theorem 38 (Bolzano–Weierstrass-Theorem).
For all
$\gamma $
,
if
$\forall \zeta \in [\omega ]^{\omega }\exists n [ \frac {1}{2^n}<|q_{\gamma \circ \zeta (n} -q_{\gamma \circ \zeta (n+1)}|]$
, then
$\exists n[ 1<|q_{\gamma (n)}|]$
.
Note that the condition: ‘
$\forall \zeta \in [\omega ]^{\omega }\exists n [ \frac {1}{2^n}<|q_{\gamma \circ \zeta (n} -q_{\gamma \circ \zeta (n+1)}|]$
’ says: ‘every subsequence of the sequence
$q_{\gamma (0)}, q_{\gamma (1)}, \ldots $
positively fails to be convergent.’
Also note that, once one sees how to obtain the conclusion ‘
$\exists n[ 1 <|q_{ \gamma (n)}|]$
’, one will also see how to obtain the conclusion: ‘
$\forall M\in \mathbb {Q}\exists n[ M<|r_{\gamma (n)}|]$
’, i.e., the sequence
$q_{\gamma (0)}, q_{\gamma (1)}, \ldots $
grows beyond all bounds.
Our proof uses both Dedekind’s Theorem and Ramsey’s Theorem.
Proof Let
$\gamma $
be given such that
$\forall \zeta \in [\omega ]^{\omega }\exists n [ \frac {1}{2^n}<|q_{\gamma \circ \zeta (n+1)} -q_{\gamma \circ \zeta (n)}|]$
.
We first prove that
$$ \begin{align*}(\ast) \ \forall \zeta \in [\omega]^{\omega}\exists n[q_{\gamma\circ\zeta(n+1)}< q_{\gamma\circ\zeta(n)} \;\vee \; 1<q_{\gamma(n)}]. \end{align*} $$
Let
$\zeta $
in
$[\omega ]^{\omega }$
be given. Define
$\delta =\gamma \circ \zeta $
. Define
$\delta ^\ast $
such that
$\delta ^\ast (0)=\delta (0)$
and, for each n, if
$\forall i \le n[q_{\delta (i)}\le q_{ \delta (i+1)}]$
, then
$\delta ^\ast (n+1)=\delta (n+1)$
and, if not, then
$q_{\delta ^\ast (n+1)}= q_{\delta ^\ast (n)}+1$
. Note that
$\forall n[q_{\delta ^\ast (n)}\le q_{\delta ^\ast (n+1)}]$
. We now prove that
$\forall \eta \in [\omega ]^{\omega } \exists n[q_{\delta ^\ast \circ \eta (n)}+\frac {1}{2^n} < q_{\delta ^\ast \circ \eta (n+1)}]$
. Let
$\eta $
in
$[\omega ]^{\omega }$
be given. Find n such that
$\frac {1}{2^n}<|q_{\gamma \circ \zeta \circ \eta (n+1)}-q_{\gamma \circ \zeta \circ \eta (n)}|$
. Either
$q_{\delta ^\ast \circ \eta (n)}=q_{\gamma \circ \zeta \circ \eta (n)}$
and
$q_{\delta ^\ast \circ \eta (n+1)}=q_{\gamma \circ \zeta \circ \eta (n+1)}$
and
$q_{\delta ^\ast \circ \eta (n)}+\frac {1}{2^n} < q_{\delta ^\ast \circ \eta (n+1)}$
, or
$\exists m<\zeta \circ \eta (n+1)[q_{\delta (m+1)}< q_{\delta (m)}]$
. In the latter case, for all sufficiently large i,
$q_{\delta ^\ast \circ \eta (i)} + 1\le q_{\delta ^\ast \circ \eta (i+1)}$
. Using Theorem 36, we find n such that
$1<q_{\delta ^\ast (n)}$
. If
$q_{\delta ^\ast (n)} = q_{\delta (n)}$
, we conclude that
$\exists m[1<q_{\gamma (m)}]$
, and if not, we conclude that
$\exists i\le n[q_{\delta (i+1)}<q_{\delta (i)}]$
, i.e.,
$\exists i\le n[q_{\gamma \circ \zeta (i+1)}<q_{\gamma \circ \zeta (i)}]$
. This concludes our proof of
$(\ast )$
.
One may also prove that
$$ \begin{align*}(\ast\ast) \ \forall \zeta \in [\omega]^{\omega}\exists n[q_{\gamma\circ\zeta(n)}< q_{\gamma\circ\zeta(n+1)} \;\vee \; q_{\gamma(n)}<-1].\end{align*} $$
(Find
$\gamma ^\ast $
such that
$\forall n[q_{\gamma ^\ast (n)}=-q_{\gamma (n)}]$
and use
$(\ast )$
, but now for
$\gamma ^\ast $
rather than for
$\gamma $
itself.)
Using both
$(\ast )$
and
$(\ast \ast )$
and Theorem 37, conclude that
$$ \begin{align*}\exists n[q_{\gamma(n)}<-1\;\vee\; 1<q_{\gamma(n)}], \text{ i.e., } \exists n[1<|q_{\gamma(n)}|].\end{align*} $$
7.7 The Paris–Harrington–Ramsey Theorem
F.P. Ramsey proved the Infinite Ramsey Theorem, in [Reference Ramsey21], in order to make his reader gain experience before attacking the Finite Ramsey Theorem. Later, it turned out that one may prove the Finite Ramsey Theorem from the Infinite Ramsey Theorem by a so-called ‘compactness argument’, see [Reference de Bruijn and Erdös11]. Paris and Harrington then saw that one may prove also certain strengthenings of the Finite Ramsey Theorem from the Infinite Ramsey Theorem, see [Reference Graham, Rothschild and Spencer15, Sections 1.5 and 6.3]. One such statement turned out to be expressible in the language of first-order arithmetic but unprovable from Peano’s axioms. We want to show that the ‘compactness argument’ works also intuitionistically, thanks to the intuitionistic version of the Infinite Ramsey Theorem proven in Section 7.5 and the Fan Theorem.
We need some terminology in order to introduce the Finite Ramsey Theorems.
Definition 31. For all
$r>0$
,
$r^{<\omega }:=\{c\mid \forall i<length(c)[c(i)<r]\}$
.
For all positive integers
$m,k$
,
$[m]^k:=\{s\in [\omega ]^k\mid \forall i<k[s(i) < m]\}$
.
One may consider elements of
$[m]^k$
as k-element subsets of
$m=\{0,1,\ldots , m-1\}$
.
For all positive integers
$c,m,k,r$
,
$c:[m]^k\rightarrow r$
if and only if
$c\in r^{<\omega }$
and
$\forall s \in [m]^k[s <\mathit {length}(c)]$
.
One may consider
$c:[m]^k\rightarrow r$
as an r-colouring of the k-element subsets of m.
For all positive integers
$c,k,m,r,t,n$
, if
$c:[m]^k\rightarrow r$
and
$n\le m$
and
${t\in [m]^n}$
, then t is
$c,k$
-monochromatic if and only if
$\exists j<r\forall u \in [n]^k[c(t\circ u)=j]$
.
For all positive integers
$k,r,n,M$
,
$M\rightarrow (n)^k_r$
if and only if, for every
$c:[M]^k\rightarrow r$
, there exists t in
$[M]^n$
such that t is
$c,k$
-monochromatic.
If
$M\rightarrow (n)^k_r$
, then, for every r-colouring c of the k-element subsets of
${M=\{0,1, \ldots , M-1\}}$
there exists an n-element subset
$A=\{t(0), t(1), \ldots , t(n-1)\}$
of M such that all k-element subsets of A obtain, from c, one and the same colour.
$t\in \bigcup _n[\omega ]^n$
is relatively large if and only if
$n>0$
and
$length(t)\ge t(0)$
.
The expression relatively large is used in [Reference Paris, Harrington and Barwise20]. A finite subset A of
$\omega $
is relatively large if the number of elements of A is at least as big as the smallest member of A.
For all positive integers
$k,r,n,M$
,
$M\rightarrow _{\ast } (n)^k_r$
if and only if, for every
$c:[M]^k\rightarrow r$
, there exist t in
$[M]^{<\omega }$
such that
$length(t)\ge n$
and t is relatively large and
$c,k$
-monochromatic.
We want to call a collection A of finite subsets of
$\omega $
omnipresent if and only if every infinite subset of
$\omega $
has a subset in A. With our terminology, the definition takes the following form.
Definition 32.
$A\subseteq [\omega ]^{<\omega }$
is called omnipresent if and only if
$\forall \zeta \in [\omega ]^{\omega }\exists s \in [\omega ]^{<\omega }[\zeta \circ s \in A]$
.
For every positive integer r,
$r^{\omega }:=\{\chi \mid \forall i[\chi (i)<r]\}$
.
Note that
$r^{\omega }$
is a fan.
One may consider an element
$\chi $
of
$r^{\omega }$
as an r-colouring of
$\omega $
.
Theorem 39. Let
$A\subseteq [\omega ]^{<\omega }$
be a decidable subset of
$\omega $
and omnipresent.
-
(i) For all positive integers
$k,r$
, for all
$\chi $
in
$r^{\omega }$
, the set
$B=B(A, k,r, \chi ):=\{s\in A\mid s \;is\; (\chi , k)\textit {-monochromatic}\}$
is omnipresent. -
(ii) For all positive integers
$k,r$
, the set
$C:= C(A,k,r):= \{s \in [\omega ]^{<\omega }\mid \forall \chi \in r^{\omega }\exists t\in [\omega ]^{<\omega }[s\circ t \in A \;\wedge \;s\circ t\;is \;(\chi ,k)\textit {-monochromatic}]\}$
is a bar in
$[\omega ]^{\omega }$
.
Proof (i) Let
$A\subseteq [\omega ]^{<\omega }$
be a decidable subset of
$\omega $
and omnipresent. Let
$k>0, r>0$
and
$\chi $
in
$r^{\omega }$
be given. We are going to prove that
$B:=\{s\in A\mid s \;is\; (\chi , k)$
-
$monochromatic\}$
is omnipresent.
Let
$\zeta \in [\omega ]^{\omega }$
be given. We want to prove
$QED:= \exists s[\zeta \circ s \in A\;\wedge \;\zeta \circ s \;is\; (\chi ,k)$
-
$monochromatic]$
. Let
$j<c$
and
$\eta $
in
$[\omega ]^{\omega }$
be given. Find s such that
$\zeta \circ \eta \circ s \in A$
. Note that either
$\zeta \circ \eta \circ s \;is\; (\chi ,k)$
-
$monochromatic$
or
$\exists t \in [\omega ]^k[\chi (\zeta \circ \eta \circ s\circ t)\neq j]$
. Define
$\chi ^\ast :\omega \rightarrow r+1$
such that, for all u in
$[\omega ]^k$
, if
$\exists s\le u[\zeta \circ s \in A\;\wedge \; \zeta \circ s \; is\; (\chi ,k)$
-
$monochromatic]$
, then
$\chi ^\ast (u)=r$
and, if not, then
$\chi ^\ast (u)=\chi (u)$
. Note that
$\forall j<r\forall \eta \in [\omega ]^{\omega } \exists u \in [\omega ]^k[\chi ^\ast (u)= r \;\vee \; \chi ^\ast (u) \neq j]$
. Ramsey’s Theorem, the infinite case, (Theorem 37), implies that the intersection of r decidable subsets of
$\omega $
each of which is k-almost-full, is k-almost-full itself. Conclude that
$\forall \eta \in [\omega ]^{\omega } \exists u \in [\omega ]^k\forall j<r[\chi ^\ast (u)= r \;\vee \; \chi ^\ast (u) \neq j]$
. Conclude that
$\exists u \in [\omega ]^k[\chi ^\ast (u)=r]$
and
$QED$
.
We thus see that the set
$B=B(A,k,r,\chi )$
is omnipresent.
(ii) Let positive integers
$k,r$
and
$\zeta $
in
$[\omega ]^{\omega }$
be given. By (i), for each
$\chi $
in
$r^{\omega }$
, one may find n such that
$\exists t \in [n]^{<n+1}[\overline \zeta n \circ t \in A \;\wedge \; \overline \zeta n \circ t \;is\;(\chi , k)$
-
$monochromatic]$
. Conclude that, for each
$\chi $
in
$r^{\omega }$
, one may find m such that, for some
$n<m$
,
$\exists t \in [n]^{<n+1}[\overline \zeta n \circ t \in A \;\wedge \; \overline \zeta n \circ t \;is\;(\overline \chi m, k)$
-
$monochromatic]$
. Applying the Fan Theorem, one may find m such that for each
$\chi $
in
$r^{\omega }$
, for some
$n<m$
,
$\exists t \in [n]^{<n+1}[\overline \zeta n \circ t \in A \;\wedge \; \overline \zeta n \circ t \;is\;(\overline \chi m, k)$
-
$monochromatic]$
. Clearly,
$\overline \zeta m \in C(A,k,r)$
.
We thus see that the set
$C=C(A,k,r)$
is a bar in
$[\omega ]^{\omega }$
.
Corollary 40.
-
(i) The Finite Ramsey Theorem:
$\forall k \forall r \forall n \exists M[M\rightarrow (n)^k_r]$
. -
(ii) The Paris–Harrington–Ramsey Theorem:
$\forall k \forall r \forall n \exists M[M\rightarrow _\ast (n)^k_r]$
.
Proof (i) Define
$A:=[\omega ]^n$
. Note that A is omnipresent. Let positive integers
$k,r$
be given. Using Theorem 39, conclude that the set
$C=\{s\in \omega ]^{<\omega }\mid \forall \chi \in r^{\omega }\exists t\in [\omega ]^{<\omega }[s\circ t \in A\;\wedge \; s\circ t\; is\; (\chi $
-
$k)$
-
$monochromatic]\}$
is a bar in
$[\omega ]^{\omega }$
. Consider
$Id_{\omega }$
, the element of
$[\omega ]^{\omega }$
such that
$\forall n[Id_{\omega }(n)=n]$
. Find M such that
$\overline {Id_{\omega }}M \in C$
and note:
$M\rightarrow (n)^k_r$
.
(ii) Start with
$A:=\bigcup _n \{s\in [\omega ]^{n+1}\mid s(0) \le n\}$
. Note that A is omnipresent and repeat the argument given for (i).
Note that we obtained Corollary 40(ii), a number-theoretic result not provable in Peano arithmetic
$\mathrm {PA}$
or in Heyting arithmetic
$\mathrm {HA}$
, by using Brouwer’s Thesis on Bars in
$\omega ^{\omega }$
.
8 Notation and conventions
8.1
$\omega $
denotes the set of the natural numbers
$0,1,2,\ldots $
.
We use
$a, b, \ldots m,n, \ldots p,q,r,s, \ldots $
as variables over
$\omega $
.
We assume a bijective function
$J:\omega \times \omega \rightarrow \omega $
has been defined with inverse functions
$K,L:\omega \rightarrow \omega $
such that
$\forall n[J\big (K(n), L(n)\big )=n]$
.
$\forall m\forall n[(m,n):=J(m,n)]$
and
$\forall n[n':=K(n)]$
and
$\forall n[n":=L(n)]$
.
We assume a function
$<\;>:\bigcup _k \omega ^k \rightarrow \omega $
has been defined that is a bijection.
If
$\langle m_0, m_1, \ldots ,m_{k-1}\rangle =s$
then
$length(s) =k$
, and for each
$i<k$
,
$s(i)=m_i$
.
$\omega ^k:=\{s\mid length(s) = k\}$
.
$\omega ^{<\omega }:=\bigcup _k \omega ^k$
. Note that
$\omega ^{<\omega }=\omega $
.
For all
$k,l$
, for all s in
$\omega ^k$
, for all t in
$\omega ^l$
,
$s\ast t$
is the element u of
$\omega ^{k+l}$
satisfying
$\forall i<k[u(i)=s(i)]$
and
$\forall j<l[u(k+j)=t(j)]$
.
For every s in
$\omega $
, for every
$A\subseteq \omega $
,
$s\ast A := \{s\ast t \mid t \in A\}.$
For all
$s,t$
such that
$\forall n<length(t)[t(n)<length(s)]$
,
$s\circ t$
is the number u satisfying
$length(u)=length(t)$
and
$\forall n<length(u)[u(n)=s\big (t(n)\big )]$
.
$\langle \;\rangle $
denotes the empty sequence, that is, the unique s such that
$length(s)\,{=}\,0$
.
$s\sqsubseteq t\leftrightarrow \exists u[t=s\ast u]$
.
$s\sqsubset t\leftrightarrow (s\sqsubseteq t \;\wedge \; s\neq t)$
.
$s\perp t\leftrightarrow \neg (s\sqsubseteq t \;\vee \; t\sqsubseteq s)$
.
For all s, for all
$n\le length(s)$
,
$\overline s n$
is the unique u in
$\omega ^n$
such that
$u\sqsubseteq s$
.
For all s, n,
$s^n$
is the largest u such that
$\forall m<length(u)[\langle n \rangle \ast m<length(s) \;\wedge \; u(m)=s(\langle n \rangle \ast m)]$
.
$2^{<\omega }:=\{s\mid \forall n<length(s)[s(i)<2]\}$
.
$[\omega ]^k:=\{s\in \omega ^k\mid \forall n<k-1[s(n)<s(n+1)]\}$
.
$[\omega ]^{<\omega }:=\bigcup _k [\omega ]^k$
.
smallskip
$\mu n[P(n)]=k\;\;\leftrightarrow \;\;\big (P(k)\;\wedge \;\forall n<k[\neg P(n)]\big )$
.
8.2
$\omega ^{\omega }=\mathcal {N}$
is the set of all functions from
$\omega $
to
$\omega $
.
We use
$\alpha , \beta , \ldots , \zeta , \eta , \ldots , \varphi , \psi , \ldots $
as variables over
$\omega ^{\omega }$
.
$Id:=Id_{\omega }$
is the element of
$\omega ^{\omega }$
satisfying
$\forall n[Id_{\omega }(n)=n]$
.
$\mathcal {C}=2^{\omega }$
is the set of all
$\alpha $
in
$\omega ^{\omega }$
such that
$\forall n[\alpha (n)<2]$
.
For each n,
$\underline n$
is the element
$\beta $
of
$\omega ^{\omega }$
such that
$\forall m[\beta (m)=n]$
.
$\alpha \;\#\:\beta \leftrightarrow \alpha \perp \beta \leftrightarrow \exists n[\alpha (n)\neq \beta (n)]$
.
$\overline \alpha k:=\langle \alpha (0), \alpha (1), \ldots \alpha (k-1)\rangle $
.
$s\sqsubset \alpha \leftrightarrow \overline \alpha \big (length(s)\big )= s$
.
For all
$\mathcal {X}\subseteq \omega ^{\omega }$
, for all s,
$\mathcal {X}\cap s:=\{\alpha \in \mathcal {X}\mid s\sqsubset \alpha \}$
.
$s\perp \alpha \leftrightarrow \alpha \perp s\leftrightarrow \neg (s\sqsubset \alpha )$
.
$(\alpha \upharpoonright s)(t):=\alpha (s\ast t)$
.
$(\alpha \upharpoonright \langle n \rangle )(m) :=\alpha ^n(m) :=\alpha (\langle n \rangle \ast m)$
.
For every
$X\subseteq \omega $
, for every s,
$X\upharpoonright s:=\{t\mid s\ast t \in X\}$
.
$[\omega ]^{\omega }$
is the set of all
$\alpha $
in
$\omega ^{\omega }$
such that
$\forall n[\alpha (n)<\alpha (n+1)]$
.
8.3
$\mathcal {F}\subseteq \omega ^{\omega }$
is a spread if and only if
$\exists \beta [\forall s[\beta (s)=0\leftrightarrow \exists n[\beta (s\ast \langle n \rangle )=0]]\;\wedge \;\forall \alpha [\alpha \in \mathcal {F}\leftrightarrow \forall n[\beta (\overline \alpha n)=0]]]$
.
Let
$\mathcal {F}\subseteq \omega ^{\omega }$
be a spread.
$\varphi :\mathcal {F}\rightarrow \omega \;\;\leftrightarrow \;\; \forall \alpha \in \mathcal {F}\exists n[\varphi (\overline \alpha n)\neq 0]$
.
If
$\varphi :\mathcal {F}\rightarrow \omega $
then, for each
$\alpha $
in
$\mathcal {F}$
,
$\varphi (\alpha )$
is the number p such that
$\exists n[\varphi (\overline \alpha n)=p+1\;\wedge \;\forall i<n[\varphi (\overline \alpha i)=0]]$
.
$\varphi :\mathcal {F}\rightarrow \omega ^{\omega }\;\;\leftrightarrow \;\;\forall n[\varphi ^n:\mathcal {F}\rightarrow \omega ]$
.
If
$\varphi :\mathcal {F}\rightarrow \omega ^{\omega }$
, then, for each
$\alpha $
in
$\mathcal {F}$
,
$\varphi |\alpha $
is the element
$\beta $
of
$\omega ^{\omega }$
such that
$\forall n[\beta (n)=\varphi ^n(\beta )]$
.
If
$\varphi :\mathcal {F}\rightarrow \omega ^{\omega }$
, then, for each s such that
$\exists \delta \in \mathcal {F}[a\sqsubset \delta ]$
,
$\varphi |s$
is the greatest number
$t\le s$
such that
$\forall i<length(t)\exists n<length(s) [\varphi ^i(\overline s n) =t(i)+1\;\wedge \;\forall j<n[\varphi ^i(\overline s j)=0]]$
.
Note that, if
$\varphi :\mathcal {F}\rightarrow \omega ^{\omega }$
, then, for all
$\alpha $
in
$\mathcal {F}$
, for all
$ \beta $
,
$\varphi |\alpha =\beta \;\;\leftrightarrow \;\;\forall n \exists m[\overline \beta n\sqsubseteq \varphi |\overline \alpha m]$
.
For all
$\varphi :\omega ^{\omega }\rightarrow \omega ^{\omega }$
, for all
$\mathcal {X}\subseteq \omega ^{\omega }$
,
$\varphi |\mathcal {X}:=\{\varphi |\alpha \mid \alpha \in \mathcal {X}\}$
.
For each
$V\subseteq \omega ^{\omega }$
,
$\varphi :\mathcal {F}\hookrightarrow V$
if and only if
$\varphi :\mathcal {F}\rightarrow \omega ^{\omega }$
and
$\forall \alpha \in \mathcal {F}\forall \beta \in \mathcal {F}[\alpha \;\#\;\beta \rightarrow \varphi |\alpha \;\#\;\varphi |\beta ]$
and
$\forall \alpha \in \mathcal {F}[\varphi |\alpha \in V]$
.
For each
$\mathcal {X}\subseteq \omega ^{\omega }$
,
$\mathcal {X}^\neg :=\{\alpha \mid \alpha \notin \mathcal {X}\}$
.
$\mathcal {R}$
, the set of the real numbers, may be defined as a subset of
$\omega ^{\omega }$
.
For
$x,y$
in
$\mathcal {R}$
,
$x\;\#_{\mathcal {R}}\;y\leftrightarrow \exists n[|x-y|>_{\mathcal {R}} \frac {1}{2^n}$
.
