toig‘ar >eg’w toi, xe ine, m’al> >atrek’ews >agore’uswWell then, let me you, stranger, precisely explain these mattersOd. \(\alpha \) 214
1 Introduction
1.1 Topology and Foundations
We want to introduce the reader to the intuitionistic view of mathematics proposed, developed and defended by the Dutch mathematician L.E.J. Brouwer (1881-1966).1
Advertisement
Brouwer obtained his fame as a mathematician by a number of very important results in topology such as the Dimension Theorem:
and the closely related Brouwer Fixed-point Theorem:For all positive integers \(m,n\),if there is a homeomorphism from \([0,1]^{m}\) to \([0,1]^{n}\), then \(m=n\),
For each positive integer \(n\), for every continuous function \(f\) from \([0,1]^{n}\) to \([0,1]^{n}\), there exists \(p\) in \([0,1]^{n}\) such that \(f(p)=p\).
These results were obtained in 1911.
1.2 Against the Formalists
In his inaugural lecture at the University of Amsterdam in 1912, entitled: ‘Intuitionism and Formalism’, see [11], Brouwer declares himself an opponent of the formalists. The formalists, in Brouwer’s words, explain the exactness and precision of the statements of mathematics by describing mathematics as a game with meaningless strings of symbols according to very strict and precise rules. The game may turn out to be useful for certain purposes, and then may give ‘a vague sensation of delight’, but these other purposes are not the concern of the mathematician. In the formalist’s ‘game’, there is no place for truth, only for correctness.
Advertisement
Brouwer most emphatically did not want to explain away the meaningfulness of mathematical statements and the experience of truth. In his intuitionistic view, the source of mathematical exactness is not to be found ‘on paper’ but ‘in the human intellect’.
1.3 I. Kant
Brouwer was inspired by the philosopher I. Kant (1724-1804) who described the simple theorem ‘\(7+5=12\)’ as the result of a construction in ‘pure intuition’.
Pure intuition has to be distinguished from observation by the senses. In Kant’s terms, it is the ‘form’ of all observations by the senses, and, as such, independent of all individual observations by the senses, i.e. a priori.
It is very important that one has to do something in order to come to the insight of the truth of ‘\(7+5=12\)’: counting 1, 2, 3, \(\dots , 7\) and then, continuing, putting 1 below 8, 2 below 9, 3 below 10, 4 below 11, and, finally, 5 below 12. This is why Kant holds the mathematical judgment ‘\(7+5=12\)’ is not analytic, i.e. a matter of logic, but synthetic, see [37, §2c], i.e., going beyond logic, and, one might perhaps say, a product of some activity by the judging subject.
1.4 Languageless Constructions
For the intuitionistic mathematician, every mathematical theorem is, like ‘\(7+5=12\)’, the result of a construction in pure intuition. The successful completion of this construction, the proof of the theorem, gives joy and a sense of beauty, and one wants to tell one’s friends.
A construction in pure intuition is languageless. Language comes in if I want to preserve the memory of the construction for myself, or if I want to make an attempt to explain to my fellow mathematician what I did, in the hope she will be able to do something similar. Language is not trustworthy: it always may fail to do what one expects it to do, as we all know from our experience as unsuccessful teachers and forgetful researchers.
There is no such thing as an exact linguistic description of a mathematical construction. The linguistic description only is the accompaniment of an act of understanding, either between me and one of my former selves, or between me and a fellow mathematician.
Nevertheless, it is our task to study the language of mathematics carefully and to find out where it perhaps may be improved. Although it is impossible we express ourselves in a perfect way, we always have to try to do better than we did until now.
1.5 Intuitionistic Mathematics Is Constructive Mathematics
Intuitionistic mathematics is not a new, alternative kind of mathematics. Mathematics is intuitionistic mathematics. Brouwer’s revolution is a call for reflection. A sharpened awareness of what it is we do when doing mathematics makes us more careful and more precise and, thereby, hopefully, better mathematicians.
Intuitionistic mathematics is constructive mathematics. The reason is that mathematics itself essentially is constructive although this fact has been obscured by our mistaken trust in (classical) logic.
Thinking of Brouwer’s ability in topology one may reflect that a continuous function \(f\) from \([0,1]^{m}\) to \([0,1]^{n}\) has the property that, for each \(p\) in \([0,1]^{m}\), one may effectively find approximations of the function value \(f(p)\) from approximations of the argument \(p\). Continuous functions are constructive functions: there is a deep connection between Brouwer’s foundational interests and his topological concerns.
1.6 The Contents of the Paper
The paper is divided into 21 Sections. Section 2 treats the basic intuition giving rise to the nonnegative integers. Section 3 is a short reflection on theorems and their proofs. In Sects. 4-6, we consider three famous results, that usually are taken to be negative statements although they are not negative at all. In Sect. 4, we have a look at Euclid’s theorem that there are infinitely many primes. In Sect. 5, we consider the theorem that \(\sqrt{2}\) is irrational. In Sect. 6, we introduce the reals and Cantor’s theorem that there are uncountably many of them. In Sect. 7, we introduce reals oscillating around 0: if \(x\) is such a number, one is unable to make out if \(x<0\), \(x=0\) or \(x>0\). Section 8 explains the reasons for interpreting the logical constants constructively and rejecting the principle of the excluded third \(X\vee \neg X\). In Sect. 9 we study a basic result of real analysis: the Intermediate Value Theorem. The theorem is an existential statement that fails when taken at its constructive face value, but, if suitably reformulated and adapted, leads to several true and useful results. Finding such reconstructions of a constructively invalid result is part of the intuitionistic program.
Intuitionistic mathematicians hold that every real function is (pointwise) continuous. In Sect. 10, we treat the preliminary observation that a real function can not have a positive discontinuity. In Sect. 11, we go into the intuitionistic meaning of negation. In Sect. 12, we introduce the Continuity Principle, an axiom used by Brouwer and we show that this axiom leads to the positive result that real functions are (pointwise) continuous.
In Sect. 13, we introduce the Fan Theorem, a theorem that perhaps, like the Continuity Principle, should be called an axiom: we discover Brouwer’s ‘proof’: most of us would call it a philosophical argument. One should note, however, that, as long as we do not organize our mathematical results in a formal way, it is difficult to distinguish axioms from theorems. As we shall see, the Fan Theorem implies that a real function from \([0,1]\) to ℛ is not only pointwise but even uniformly continuous. As an aside, we prove that the Fan Theorem fails to be true in computable analysis. In Sect. 14, we go into the rôle of the Fan Theorem in game theory.
In Sect. 15, we consider Brouwer’s Thesis on Bars in \(\mathcal{N}=\omega ^{\omega }\), formulated as a Principle of Bar Induction. The Thesis on Bars in \(\mathcal{N}\) implies the Fan Theorem but is a far stronger statement. We show how the argument for the Fan Theorem extends to the Thesis on Bars in \(\mathcal{N}\). As an application we prove, in Sect. 16, the Principle of Open Induction in \([0,1]\). In Sect. 17 we give a second formulation of Brouwer’s Thesis. This second formulation uses stumps: inductively generated sets of finite sequences of natural numbers, whose rôle may be compared to the rôle of countable ordinals in classical, non-intuitionistic analysis. As an application we give, in Sect. 18, an intuitionistic formulation and proof of the Clopen Ramsey Theorem, itself an impressive extension of Ramsey’s result from 1928. The proof of this intuitionistic theorem has not been published before. In Sect. 19 we study Borel sets. Because of the failure of De Morgan’s Law \(\neg \forall n [\neg P(n)]\rightarrow \exists n[ P(n)]\), the subject of descriptive set theory needs a complete reconstruction. In Sect. 20 we reflect on the notion of a finite subset of the set ℕ of the non-negative integers. This mathematical notion may be made intuitionistically precise in uncountably many ways. It is a perfect illustration of the subtlety and expressivity the language of mathematics has obtained from Brouwer’s intervention.
In Sect. 21, we briefly describe how E. Bishop, who founded his own school of constructive analysis in the 1960’s, treated Brouwer’s legacy, and how also P. Martin-Löf’s view on constructive mathematics was influenced by Brouwer.
Many Sections may be read independently from other Sections.
2 The Basic Intuition
2.1 If You Don’t Become Like Little Children …2
Mathematics is a child’s game and each of us, from his tender days, is familiar with the infinite sequence:
$$ 0,\;1, \;2, \;3,\dots $$
The sequence of these natural numbers or non-negative integers has no end.
No end? Can we always go on? Yes, yes, we can always go on!
We never die, or get tired of the game. Please, do not plague us with such silly objections.
We courageously stick to the fascinating perspective of the never finished infinite.
2.2 Induction and Recursion
The function \(\mathsf{S}\) produces, given any non-negative integer \(n\), the next one, \(\mathsf{S}(n)\): Let \(P\) be a property of non-negative integers such that one has a proof of \(P(0)\), and, for each \(n\), a proof of \(P\bigl (\mathsf{S}(n)\bigr )\) from \(P(n)\), i.e. a proof of \(P(1)\) from \(P(0)\), a proof of \(P(2)\) from \(P(1)\), a proof of \(P(3)\) from \(P(2)\), and so on. One then proves, step by step, first \(P(1)\), then \(P(2)\), then \(P(3)\), and so on, that is, one proves, for each \(n\), \(P(n)\). We see this happening although the process is never finished.
$$ \mathsf{S}(0)=1, \;\mathsf{S}(1) =2, \;\mathsf{S}(2)=3, \ldots $$
The principle of complete induction on the non-negative integers thus is obvious.
Suppose one defines: for each \(m\), \(m+0=m\) and for each \(n\), \(m+\mathsf{S}(n)=\mathsf{S}(m+n)\). One then calculates, first \(m+1= m+\mathsf{S}(0)\), then \(m+2= m+\mathsf{S}(1)\), then
\(m+3=m+\mathsf{S}(2)\), and so on, and, in this way, one finds, for each \(n\), the meaning of \(m+n\).
This also is obvious.
2.3 The ‘Logicist’ Attempt to ‘Prove’ Induction
In the nineteenth century, G. Frege and R. Dedekind tried to define the non-negative integers, logically or set-theoretically, and then to prove the principle of complete induction and the possibility of defining functions by recursion.
Brouwer considered such attempts futile and misleading.
2.4 Awakening Consciousness
Brouwer spent a lot of thought on finding the origin of the idea of the non-negative integers, see for instance [14].
A first thing, then a next thing, then another thing, and again another thing …
Mark the beginning: a first thing, then a next thing. Brouwer called it the basic intuition of two-ity. He saw it happening in an awakening of slumbering consciousness, a shift of attention, a moment’s reflection, or a move of time: here I am, and now I see: ‘here I am’, and that is two things. Iterating this shift of attention, I obtain three things, four things, and so on.
One is reminded of R. Dedekind’s proof of [23, Theorem 66]: There exist infinite sets, for instance, the ‘world of my thoughts, meine Gedankenwelt’. Dedekind invokes a function \(s\mapsto s'\) that associates to every thought \(s\) of mine the thought \(s'\): ‘I am thinking of \(s\)’ and concludes, from the fact that this function should be one-to-one and non-surjective, the latter because ‘I myself, mein eigenes Ich’ am a thought of mine not of the form \(s'\), that I have infinitely many thoughts.
As we mentioned already, Brouwer refers to Kant. Kant held that the concepts of ‘time’ and ‘space’, the ‘forms’ of ‘inner sense’ and ‘outer sense’, respectively, are apriori concepts, that is, independent from every observation by the senses. These apriori concepts are studied by mathematics, in its two divisions: ‘arithmetic’ and ‘geometry’. Brouwer wants to maintain Kant’s conviction about the apriori character of ‘time’ but rejects the apriori character of ‘space’. This is partly because Kant believed space to be Euclidean, and, after Kant, one had the non-euclidean revolution. Also, geometry may be ‘arithmetized’ and be robbed of its status as an independent discipline.
2.5 The ‘Set’ ℕ
We use ℕ to denote the set of the nonnegative integers. This ‘set’ is a well-understood totality but an ongoing project, in no sense finished or complete. We use \(m,n, \ldots , s, t, \ldots \) as variables over ℕ.
3 Theorems and Their Proofs
3.1 Mere Announcements
One does not understand a mathematical theorem immediately upon hearing its statement. The statement of the theorem is only a preliminary announcement, a partial communication, a promise. Its full meaning will unfold itself in the proof, and understanding this full meaning is reserved for someone who takes the trouble to go through the proof and to reconstruct it for herself.
3.2 No to ‘Platonism’
The statement of a theorem tells us that some mental construction has been successfully completed. It is not reporting a fact one might ‘observe’ in a mathematical reality lying outside us.
The latter view has been strongly defended by Plato (427-347 B.C.). He believed that the contemplation of the timeless mathematical reality, that one approaches with the mind and not with the senses and that one should not touch with one’s fingers,3 would prepare us for the contemplation of what is the true interest of the philosopher: the timeless reality of the ‘Ideas’.
The intuitionistic mathematician rejects this view. In the ancient debate between Speusippus (405-338 B.C.) and Menaechmus (380-320 B.C.) as reported by Proclus (410-485), she would definitely have sided with Menaechmus. Speusippus held that every ‘problem’ essentially is a ‘theorem’, i.e. a truth to behold, whereas Menaechmus defended the view that every ‘theorem’ essentially is a ‘problem’, i.e. a construction to find and carry out.4 Proclus, in his wisdom, judged that both views contain some truth,5 and, indeed, one might say, both views try to explain a part of our mathematical experience.
In our days, many mathematicians still feel they are discovering hard facts not of their own making. They prefer a so-called realistic view, reminiscent of Plato’s, while admitting it is difficult to give a convincing account of the mathematical reality see [35, p. 123].
As to Brouwer’s formalist adversaries, some of them develop their formalisms with an eye to ‘reality’ while others, like Brouwer himself, keep far from it. A famous defender of the realistic point of view is K. Gödel (1906-1972). The formula \(\mathsf{CH}\) in the language of set theory that is taken to represent Cantor’s famous continuum hypothesis6 has been shown, by Gödel himself in 1938, and by P. Cohen in 1963, respectively, not to be refuted and not to be proven by the rules of first-order predicate logic from the formulas accepted as representing ‘the’ axioms of set theory, provided the latter do not give a contradiction. Gödel observed, even before Cohen proved his result, that this fact does not solve the problem: we still have to find out if \(\mathsf{CH}\) holds in the mathematical universe, see [30].7
The intuitionistic mathematician discards the realistic view: he believes it is wrong and harmful for the practice of mathematics.
3.3 Propositions (as Yet) Without Proof
From our intuitionistic perspective, it seems impossible to fully understand a proposition that has (as yet) no proof. We like to say, however, that we also ‘understand’ the proposition ‘\(0=1\)’, in the sense that we see this proposition never will have a proof.
Besides, propositions that are only partially understood in the sense that we have as yet no proof and also do not see that we never will have one, have an important part to play in mathematics. Let us consider an example.
Studying Euclid’s proof that there are infinitely many primes,8 one comes to understand the statement: ‘there are infinitely many primes’ and to enjoy its beauty and depth. One now may ask: ‘Are there also infinitely many twin primes, i.e. prime numbers \(p\) such that also \(p+2\) is prime?’. By analogy, we have some understanding of the latter proposition. We can imagine what a proof of this proposition might be and, in this sense, catch its meaning, although, up to now, no proof or refutation has been found.
By his exemplary proof, Euclid suggests us how to (partially) understand other propositions of the form ‘there are infinitely many numbers \(n\) such that \(P(n)\)’.
3.4 Negative Theorems
There is a large supply of theorems whose statement is negative. Such theorems report us that a construction of a kind we hoped for is impossible. We obtain such conclusions imagining ourselves possessed of a construction of the required kind and seeing that we then could prove \(0=1\). We hastily retreat, admitting we were imagining the impossible.
Indeed, when constructing proofs, we often use our imagination. We make temporary extra assumptions for the sake of the argument, that later perhaps will have to be given up. G. Gentzen (1909-1945), the inventor of ‘Natural Deduction’, put great emphasis on this fact. Gentzen was inspired by Brouwer, see [27, Section II, \(\S 3\)].
In a sense, propositions with a negative conclusion are second-rank. They tell us about a lost hope, a failure. Fortunately, many mathematical theorems are unnecessarily negative. Their negative formulation is caused by laziness or lack of attention. The intuitionistic mathematician likes to find the positive content of seemingly negative statements.
4 Infinitely Many Prime Numbers
The following theorem is due to Euclid, see [25, Book IX, Proposition 20]. It is important and rewarding to study the proof in the original.
Theorem 1
The prime numbers are more than every quantity of prime numbers given beforehand.
Proof
Let the prime numbers given beforehand be \(A, B, C\). I say that there are more prime numbers than \(A, B, C\). Let the least number measured by9\(A,B, C\) be taken, and let it be \(DE\), and let the unit \(DF\) be added to it; we thus obtain \(EF\). \(EF\) is prime or \(EF\) is not prime.10 First, let it be prime. Then the prime numbers \(A, B, C, EF\) are more than \(A, B, C\). Next, let \(EF\) be not prime. Then there is a prime number that measures \(EF\). Let it be \(G\). I say \(G\) is not the same with any of \(A, B, C\). For, if possible, let it be so. Now \(A, B, C\) measure \(DE\) and thus also \(G\) measures \(DE\). But the number \(G\) also measures \(EF\) and thus the number \(G\) measures the remainder \(DF\) which is a unit, and that is absurd. So \(G\) is not the same with any of \(A, B, C\). Thus prime numbers \(A,B,C,G\) are found which are more than the quantity of prime numbers \(A,B,C\) given beforehand. □
We now paraphrase Euclid’s proof in contemporary terms. Euclid explains us, how, given any finite list \(q_{0}, q_{1}, \ldots , q_{n-1}\) of prime numbers, one produces a prime number \(q\) that is not on the list: consider \(c:=\) the least common multiple of \(q_{0},q_{1}, \ldots , q_{n-1}\). If \(c\) is prime, take \(q := c\). If \(c\) is not prime, determine the least number \(q>1\) that divides \(c\). Then \(q\) is prime, and, for every \(i< n\), \(q \neq q_{i}\).
One may seriously wonder if this paraphrase is better than the original.
Note that Euclid only treats the case: \(n=3\). He of course expects the reader to pick up the general idea from this exemplary case. The reader must be willing to understand him. This is a conditio sine qua non for every written proof.
Also note that Euclid provides an algorithm: he demonstrates how, given any finite list of prime numbers, one calculates a prime number that still is missing.
Most importantly, as we observed already in the previous Section, Euclid in a way lays down the meaning of the word ‘infinite’. His proof suggests how to understand a proposition of the form: ‘there are infinitely many numbers satisfying \(A\)’. One may prove such a thing by doing something like he does in the case of the prime numbers.
Sometimes, a description of Euclid’s proof is given that does no justice to the argument. According to this description, one is invited to assume: there is a finite list containing all the primes. Euclid then reduces this assumption to absurdity and forces one to admit that the initial assumption is false: there is no such finite list, which is to say: there are not finitely many primes.
G.H. Hardy, a great mathematician and a convinced platonist, has this view, see [35, Sect. 12]. In the context of Euclid’s theorem, he calls reductio ad absurdum ‘one of a mathematician’s finest weapons’, but adds a footnote stating: ‘The proof can be arranged so as to avoid a reductio and logicians of some schools would prefer that it should be.’
5 \(\sqrt{2}\) Is Irrational
The theorem that \(\sqrt{2}\) is irrational is also due to the Greeks and dates from 450 B.C.. In those days, mathematicians sometimes were called ‘those who know about the odd and the even’. The theorem uses the following
Lemma 2
For all positive integers \(n\), if \(n\) is odd, then \(n^{2}\) is odd.
Proof
Find \(p\) such that \(n = 2p +1\). Then \(n^{2} = (2p+1)(2p+1)=4p^{2} + 4p +1= 2(2p^{2} +2p) +1\). □
Theorem 3
There are no positive integers \(m,n\) such that \(\sqrt{2}=\frac{m}{n}\).
Proof
Suppose there are. Find such \(m,n\) and assume: at least one of \(m,n\) is odd. Then \(\sqrt{2} =\frac{m}{n}\), so \(2n^{2} = m^{2}\), so \(m^{2}\) is even and, by Lemma 2, also \(m\) is even and 4 divides \(m^{2}=2n^{2}\), so \(n^{2}\) is even and, again by Lemma 2, \(n\) is even. We thus see: both \(m,n\) are even. Contradiction. □
Already in ancient times, some people worried about this proof, in particular about the sentence: ‘Suppose there are.’. How is it possible to suppose that \(\sqrt{2}\) is rational? ‘Suppose’ must mean something like ‘Imagine’. How can one make a clear mental picture of a fact that will turn out to be false? How to imagine the impossible?
In particular, Parmenides (fl. 475 B.C.) and Zeno (fl. 450 B.C.), leading members of the Eleatic school of philosophy, felt this difficulty. The Dutch mathematician G.F.C. Griss (1898-1953) shared their concern and suggested to Brouwer to remove the proposition without proof, negation and the empty set from the discourse of mathematics. He started a redevelopment of intuitionistic mathematics, see, for instance, [33]. Brouwer did not want to go into his suggestion, and offered the somewhat surprising argument that, following it, one would impoverish the subject, see [13]. Nevertheless, in intuitionistic, and, more generally, in constructive mathematics, one avoids negation as much as possible, also for the reason that negative results lack constructive content.
The negatively formulated Theorem 3 may be replaced by a positive and affirmative result, as follows.
Definition 1
A real number \(x\) is positively irrational if and only if, given any rational number \(q = \frac{m}{n}\) one may effectively find a positive integer \(p\) such that \(|x - \frac{m}{n}|\ge \frac{1}{p}\).
Theorem 4
\(\sqrt{2}\) is positively irrational.
Proof
Let \(m,n\) be given. Note \(2n^{2} \neq m^{2}\), and therefore: \(|2n^{2} - m^{2}| \ge 1\) and \(|2 - \frac{m^{2}}{n^{2}}|\ge \frac{1}{n^{2}}\), that is \(|\sqrt{2}+\frac{m}{n}|\cdot |\sqrt{2}-\frac{m}{n}| \ge \frac{1}{n^{2}}\). If \(\frac{m}{n} > 2\), then \(\frac{m}{n} - \sqrt{2}>\frac{1}{2}\) and, if \(\frac{m}{n} \le 2\), then \(|\sqrt{2}+\frac{m}{n}|< 4\) and \(|\sqrt{2}-\frac{m}{n}|> \frac{1}{4n^{2}}\). □
6 Uncountably Many Reals
We sketch how to treat integers and rationals and then define the notion of a real number, essentially like G. Cantor (1845-1918) did it, and Brouwer after him.
6.1 Integers and Rationals
One first introduces, on the set ℕ of the natural numbers, the operations \(+, \cdot , exp\) and the relations <,≤ by recursive definitions, as suggested in Sect. 2, and proves, by induction, their well-known nice properties. One then defines a pairing function from \(\mathbb{N}\times \mathbb{N}\) to ℕ, for instance the function \((m, n) = 2^{m}(2n+1) -1\), with inverse functions \(K,L:\mathbb{N}\rightarrow \mathbb{N}\). We will write \(m'=K(m)\) and \(m''=L(m)\), so, for each \(m\), \(m=(m', m'')\).
Then an equivalence relation \(=_{\mathbb{Z}}\) on ℕ is introduced by:
\(m=_{\mathbb{Z}} n \leftrightarrow m'+n''=m''+n'\). Integers, for us, are just natural numbers and not, as in the usual treatment, the equivalence classes of the relation \(=_{\mathbb{Z}}\). Functions and relations on ℤ are functions and relations on ℕ that respect the relation \(=_{\mathbb{Z}}\). The functions \(+_{\mathbb{Z}}, \cdot _{\mathbb{Z}}\), the relations \(<_{\mathbb{Z}}, \le _{\mathbb{Z}}\), and the special elements \(0_{\mathbb{Z}}, 1_{\mathbb{Z}}\) are defined in the way one would expect.
One then defines \(\mathbb{Q}:=\{m\mid 0_{\mathbb{Z}} <_{\mathbb{Z}} m''\}\). An equivalence relation \(=_{\mathbb{Q}}\) is introduced on ℚ by: \(m=_{\mathbb{Q}} n \leftrightarrow m'\cdot _{\mathbb{Z}} n'' =_{\mathbb{Z}} m'' \cdot _{\mathbb{Z}} n'\). Rationals, for us, are just natural numbers, but, whenever we consider natural numbers as rationals, we respect \(=_{\mathbb{Q}}\). The functions \(+_{\mathbb{Q}}, \cdot _{\mathbb{Q}}\), the relations \(<_{\mathbb{Q}}, \le _{\mathbb{Q}}\), and the special elements \(0_{\mathbb{Q}}, 1_{\mathbb{Q}}\) are defined straightforwardly.
In general, we omit the subscripts ‘\(_{\mathbb{Z}}\)’, ‘\(_{\mathbb{Q}}\)’ unless we fear for confusion.
It is important to realize that all functions and relations mentioned so far are algorithmic. We learned the algorithms at elementary school and know, for instance, how to find out, given rationals \(p,q\), if \(p=_{\mathbb{Q}} q\) or not.
6.2 Real Numbers
We now are ready to introduce the reals.
Definition 2
A real number is an approximation process, an infinite sequence \(x= x(0), x(1), \ldots \) of pairs \(x(n)=\bigl (x'(n), x''(n)\bigr )\) of rationals such that
(i)
\(x\) is shrinking: for all \(n\), \(x'(n)\le x'(n+1)\le x''(n+1)\le x''(n)\) and
(ii)
\(x\) is dwindling: for all \(m\), there exists \(n\) such that \(x''(n) - x'(n) \le \frac{1}{2^{m}}\).
ℛ is the set of all real numbers. We use \(x, y, \ldots \) as variables over ℛ.
Brouwer gave Cantor’s notion his own colouring.
Every real number \(x= x(0), x(1), \ldots \) is an infinite sequence of successive approximations, and, like the infinite sequence \(0,1,2, \ldots \) itself, never finished and always under construction. Even if an algorithm has been given determining the successive values of \(x\), the finding of these successive values keeps us busy forever. The number is the process of approximation itself: it makes no sense to ask for the limit point that the successive approximations are striving for.
For all reals \(x\), for all rationals \(p,q\), for all \(n\), if \(p<_{\mathbb{Q}} x'(n)<_{\mathbb{Q}} x''(n)<_{\mathbb{Q}} q\), we say that \((p,q)\) is an approximation of \(x\) of precision \(q-_{\mathbb{Q}} p\).
Definition 3
For all real numbers \(x, y\), we define:
\(x <_{\mathcal{R}} y\) (\(x\) is smaller than \(y\)) if and only if \(\exists n[x''(n) <_{\mathbb{Q}} y'(n) ]\), and:
\(x\le _{\mathcal{R}} y\) (\(x\) is not greater than \(y\)) if and only if \(\forall n [x'(n)\le _{\mathbb{Q}} y''(n)]\), and:
\(x \;\#_{\mathcal{R}}\; y\) (\(x\) is apart from \(y\)) if and only if either \(x <_{\mathcal{R}} y\) or \(y <_{\mathcal{R}} x\), and:
\(x =_{\mathcal{R}} y\) (\(x\) coincides with \(y\)) if and only if \(x\le _{\mathcal{R}}y\) and \(y\le _{\mathcal{R}}x\).
We suppress the subscript ‘\(_{\mathcal{R}}\)’ if we expect that, doing so, we will not confuse the reader.
Traditionally, our ‘real numbers’ would be called ‘number generators’.
The name ‘real number’ would then be reserved for equivalence classes of the form \([x]=\{y\in \mathcal{R}\mid y =_{\mathcal{R}}x\}\).
Also Brouwer does so, using the terms ‘point’ and ‘point kernel’.
We will not make this distinction but will only consider operations and relations on ℛ that respect the equivalence relation \(=_{\mathcal{R}}\).
The relations \(<_{\mathcal{R}}\) and \(\#_{\mathcal{R}}\) are positive relations. From a constructive point of view, they are more important than the relations \(\le _{\mathcal{R}}\) and \(=_{\mathcal{R}}\). The latter two relations are negative, and, moreover, expressible in terms of the positive relations, as: \(x\le _{\mathcal{R}} y \leftrightarrow \neg (y<_{\mathcal{R}} x)\) and: \(x=_{\mathcal{R}} y \leftrightarrow \neg (x \;\#_{\mathcal{R}}\; y)\). Given real numbers \(x,y\) one may prove: ‘\(x=_{\mathcal{R}} y\)’ by assuming: ‘\(x\;\#_{\mathcal{R}}\; y\)’ and obtaining a contradiction.
It is important that the positive relations \(<_{\mathcal{R}}\) and \(=_{\mathcal{R}}\) are co-transitive, i.e.
\(x<_{\mathcal{R}} y\rightarrow (x<_{\mathcal{R}} z \;\vee \;z<_{\mathcal{R}} y)\) and \(x\;\#_{\mathcal{R}}\; y\rightarrow (x\;\#_{\mathcal{R}}\; z \;\vee \;z\; \#_{\mathcal{R}}\;y)\).
It suffices to prove this for the first relation.
Given \(x,y,z\) such that \(x<_{\mathcal{R}}y\), find \(n\) such that \(z''(n)-z'(n)<_{\mathbb{Q}} y'(n) -x''(n)\) and decide: either \(x''(n)<_{\mathbb{Q}}z'(n)\) and \(x<_{\mathcal{R}} z\) or: \(z''(n)<_{\mathbb{Q}} y'(n)\) and \(z<_{\mathcal{R}}y\).
6.3 Cantor’s Proof
In 1873, Cantor proves the following, see [19, §2]:
Theorem 5
For every infinite sequence \(x_{0}, x_{1}, \dots \) of reals, there exists a real \(x\) apart from every real in the sequence, that is: \(x \;\#_{\mathcal{R}}\; x_{0}, x \;\#_{\mathcal{R}}\; x_{1}, \ldots \)
Proof
Let an infinite sequence \(x_{0}, x_{1}, x_{2}, \ldots \) of reals be given.
Define \(x=x(0), x(1), \ldots \), as follows, step by step.
First, define \(x(0)=(0,1)\).
Now assume \(x(n)\) has been defined and \(x''(n)-x'(n)=_{\mathbb{Q}}\frac{1}{3^{n}}\).
Find \(m_{0} :=\) the least \(m\) such that \(x_{n}''(m)-x_{n}'(m)<_{\mathbb{Q}}\frac{1}{3^{n+1}}\).
Note: either \(\frac{2}{3}x'(n) +_{\mathbb{Q}}\frac{1}{3}x''(n)<_{\mathbb{Q}}x_{n}'(m_{0})\) or \(x_{n}''(m_{0})<_{\mathbb{Q}}\frac{2}{3}x'(n) +_{\mathbb{Q}}\frac{1}{3}x''(n)\).
If \(\frac{2}{3}x'(n) +_{\mathbb{Q}}\frac{1}{3}x''(n)<_{\mathbb{Q}}x_{n}'(m_{0})\), define: \(x(n+1) := \bigl (x'(n), \frac{2}{3}x'(n) +\frac{1}{3}x''(n)\bigr )\) and, if not, define \(x(n+1) := \bigl ( \frac{1}{3}x'(n) +\frac{2}{3}x''(n), x''(n)\bigr )\).
By this choice of \(x(n+1)\), we ensure \(x''(n+1)-x'(n+1)=_{\mathbb{Q}}\frac{1}{3^{n+1}}\) and \(x \;\#_{\mathcal{R}}\; x_{n}\). □
Our constructive argument differs but little from Cantor’s. Cantor makes it perfectly clear how, given any countable list \(x_{0}, x_{1}, \ldots \), of reals, one produces a real positively different from every real on the list.
We thus see that the statement ‘ℛ is uncountable’, essentially, is a positive statement.
Note that, by his exemplary proof, Cantor suggest to us how we should understand and prove a proposition of the form ‘\(A\subseteq \mathcal{R}\) is uncountable’.
One defines operations \(+_{\mathcal{R}}\) and \(\cdot _{\mathcal{R}}\) on ℛ by:
for all \(n\), \((x+_{\mathcal{R}} \;y)(n):=\bigl (x'(n) +_{\mathbb{Q}} y'(n), x''(n)+_{\mathbb{Q}}y''(n)\bigr )\) and
\((x\cdot _{\mathcal{R}} y)(n)= \bigl (\min _{\mathbb{Q}}(x'(n)\cdot _{\mathbb{Q}} y'(n), x'(n)\cdot _{\mathbb{Q}} y''(n),x''(n)\cdot _{\mathbb{Q}} y'(n),x''(n)\cdot _{\mathbb{Q}} y''(n)), \max _{\mathbb{Q}}(x'(n)\cdot _{\mathbb{Q}} y'(n), x'(n)\cdot _{\mathbb{Q}} y''(n),x''(n) \cdot _{\mathbb{Q}} y'(n),x''(n)\cdot _{\mathbb{Q}} y''(n))\bigr )\).
Also subtraction and an absolute value function \(x\mapsto |x|\) may be defined.
For every rational \(q\), we define \(q_{\mathcal{R}}\) in ℛ such that, for all \(n\),
\(q_{\mathcal{R}}(n)= (q-_{\mathbb{Q}}\frac{1}{2^{n}}, q+_{\mathbb{Q}} \frac{1}{2^{n}})\).
We omit subscripts ‘\(_{\mathcal{R}}\)’ where we think it does no harm to do so.
7 Fugitive Integers and Oscillating Reals
The following definition lies at the basis of many counterexamples in Brouwer’s style to various mathematical results that do not stand a constructive reading.
We consider the decimal expansion of \(\pi \), evaluating it step by step, hunting for the first block of 99 consecutive 9’s. We would like to define \(k_{99}\) as the least number \(n\) such that at the places \(n, n+1, \ldots n+98\) in the decimal expansion of \(\pi \) we find the value 9, but we have to be careful as we do not know if such a number \(n\) exists.
Definition 4
The fugitive ‘number’ \(k_{99}\)
Let \(d= d(0), d(1), \ldots \) be the decimal expansion of \(\pi \), that is: \(d\) is the function from ℕ to \(\{0,1, \ldots ,9\}\) such that
\(\pi = 3+\sum _{n =0}^{\infty }d(n)\cdot 10^{-n-1}\).
For each \(n\), we define:
\(k_{99}\le n\) if and only if \(\exists j\le n \forall i < 99[d(j+i) = 9]\), and:
\(n< k_{99}\) if and only if \(\forall j\le n \exists i<99[d(i+j)\neq 9]\), and:
\(n=k_{99}\) if and only if \(k_{99}\le n\) and \(\forall j< n[j< k_{99}]\).
Note that we do not define a natural number \(k_{99}\) but only the meaning of an expression like ‘\(k_{99}\le n\)’.
Also note that, for each \(n\), one may find out, for each of the propositions ‘\(k_{99}\le n\)’, ‘\(n< k_{99}\)’, and ‘\(n=k_{99}\)’, if they are true or not, by simply calculating the first \(n\) values of the decimal expansion of \(\pi \).
The statement ‘\(P:=\exists n[n=k_{99}]\)’ is a prime example of an undecided proposition, i.e. we do not have a proof of \(P\), but we also do not have a proof that we never will find one, and we have no procedure to find either one of these proofs in finitely many steps.
The problem of the 99 9’s in the decimal expansion of \(\pi \) is not important in itself. It only is a pedagogical example, showing that we have no method to solve this kind of problems. Should someone, by historical accident, find the 99 9‘s, then one easily formulates a similar proposition that is still undecided.
Definition 5
The ‘oscillating’ reals \(\rho _{0}, \rho _{1}, \rho _{2}\)
We define real numbers \(0_{\mathcal{R}}\), \(\rho _{0}, \rho _{1}\) and \(\rho _{2}\), as follows.
\(0_{\mathcal{R}}\) is the real number such that, for all \(n\), \(0_{\mathcal{R}}(n)=(-\frac{1}{2^{n}}, \frac{1}{2^{n}})\).
\(\rho _{0}=(\frac{1}{2})^{k_{99}}\) is the real number such that, for all \(n< k_{99}\), \(\rho _{0}(n) :=(-\frac{1}{2^{n}}, \frac{1}{2^{n}})\), and, for all \(n \ge k_{99}\), \(\rho _{0}(n) :=(\frac{1}{2^{k_{99}}}, \frac{1}{2^{k_{99}}})\).
\(\rho _{1}=(-\frac{1}{2})^{k_{99}}\) is the real number such that, for all \(n< k_{99}\), \(\rho _{1}(n) =(-\frac{1}{2^{n}}, \frac{1}{2^{n}})\), and, for all \(n \ge k_{99}\), if \(k_{99}\) is even, then \(\rho _{1}(n):=(\frac{1}{2^{k_{99}}}, \frac{1}{2^{k_{99}}})\), and, if \(k_{99}\) is odd, then \(\rho _{1}(n) :=(-\frac{1}{2^{k_{99}}}, -\frac{1}{2^{k_{99}}})\).
Finally, \(\rho _{2}:= \rho _{0}+_{\mathcal{R}}\rho _{1}\).
Now note the following:
(1) \(0_{\mathcal{R}} =_{\mathcal{R}} \rho _{0}\leftrightarrow \forall n[n < k_{99}]\), and we have no proof of ‘\(\forall n[n < k_{99}]\)’.
Also: \(\neg (0_{\mathcal{R}} =_{\mathcal{R}} \rho _{0})\leftrightarrow \neg \forall n[n < k_{99}]\), and we have no proof of ‘\(\neg \forall n[n < k_{99}]\)’.
Finally: \(0_{\mathcal{R}} <_{\mathcal{R}} \rho _{0}\leftrightarrow \exists n[n=k_{99}]\), and we have no proof of ‘\(\exists n[n = k_{99}]\)’.
We thus see that, in general, given real numbers \(x,y\), we have no means of proving one of the propositions ‘\(x=_{\mathcal{R}} y\)’, ‘\(\neg (x=_{\mathcal{R}} y)\)’, ‘\(x <_{\mathcal{R}}y\)’.
(2) Note: \(0_{\mathcal{R}} \le _{\mathcal{R}}\rho _{0}\), but, as we saw, we have no proof of ‘\(0_{\mathcal{R}}=_{\mathcal{R}} \rho _{0}\)’, nor of ‘\(0_{\mathcal{R}}<_{\mathcal{R}} \rho _{0}\)’.
We thus see that, in general, given real numbers \(x,y\) such that \(x\le _{\mathcal{R}}y\), we have no means of proving either one of the propositions ‘\(x=_{\mathcal{R}} y\)’ or ‘\(x <_{\mathcal{R}} y\)’.
(3) Note: \(0_{\mathcal{R}}\le _{\mathcal{R}} \rho _{1} \leftrightarrow \forall n[n = k_{99}\rightarrow \exists m [n=2m]]\), and we have no proof of: ‘\(\forall n[n = k_{99}\rightarrow \exists m [n=2m]]\)’.
Note: \(\rho _{1}\le _{\mathcal{R}}0_{\mathcal{R}} \leftrightarrow \forall n[n = k_{99} \rightarrow \exists m [n=2m+1]]\), and we have no proof of: ‘\(\forall n[n = k_{99}\rightarrow \exists m [n=2m+1]]\)’.
We thus see that, in general, given real numbers \(x,y\), we have no means of proving either one of the propositions ‘\(x\le _{\mathcal{R}} y\)’, ‘\(y \le _{\mathcal{R}} x\)’.
(4) Note: \(\rho _{2} =_{\mathcal{R}} 2\cdot \rho _{0}\leftrightarrow \forall n[n=k_{99} \rightarrow \exists m[n=2m]]\) and
\(\rho _{2}=_{\mathcal{R}} 0_{\mathcal{R}}\leftrightarrow \forall n[n=k_{99} \rightarrow \exists m[n=2m+1]]\). We have no means of proving either one of the propositions ‘\(\rho _{2}=_{\mathcal{R}} 2\cdot \rho _{0}\)’, ‘\(\rho _{2}=_{\mathcal{R}} 0_{\mathcal{R}}\)’.
We will use the number \(\rho _{2}\) in Sect. 9.
\(\rho _{0}, \rho _{1}, \rho _{2}\) are examples of real numbers oscillating around \(0_{\mathcal{R}}\).
\(\rho _{0}\) oscillates above \(0_{\mathcal{R}}\) and \(\rho _{1}\) oscillates up and down around \(0_{\mathcal{R}}\).
\(\rho _{2}=\rho _{0}+\rho _{1}\) oscillates between \(0_{\mathcal{R}}\) and \(2\cdot \rho _{0}\).
8 Rejecting \(P\;\vee \;\neg P\)
8.1 Mathematics and Logic
Brouwer describes mathematics as being developed by the mind having come to awareness and playfully exploring its possibilities, see, for instance, [14]. Mathematics is not dependent on any evidence from the senses. All other science is applied mathematics, as mathematics recognizes and enforces patterns on the data acquired by observation.
Logic in particular is not a foundational science, prescribing the way one should think, but an observational science. Mathematics is not reigned by logic. Mathematics is a languageless activity of the mind. As we observed already in Sect. 1, only when we want to communicate about mathematics, language comes in. We communicate with other people, trying to induce them to make mathematical constructions like the ones we ourselves are making, and we communicate with ourselves, understanding the weakness of our memory, and hoping to be able to remind ourselves tomorrow of what we did today. Observing ourselves and others when we are busy communicating about mathematics, we take notes of the sounds and signs that are used. We discover patterns and regularities, and then promote such regularities to laws of logic. There is no guarantee, however, that someone, even myself, who is making sounds or giving other signs in accordance with these laws is actually succeeding in making successful mathematical constructions. In this sense, the ‘laws of logic’ are unreliable.
Learning logic is part of learning the language of mathematics. Learning the meaning of the connectives ‘…or…’, ‘…and…’, ‘…if…’, and ‘not:…’, and the quantifiers ‘\(\exists x \in V[\ldots x \ldots ]\)’ and ‘\(\forall x \in V[\dots x\ldots ]\)’, is like learning the meaning of the expressions ‘infinite’ or ‘uncountable’ in the case of Theorems 1 and 5.
A connective ∗ is a general method to obtain a new proposition, \(P\ast Q\), from any two given propositions, \(P\) and \(Q\). Understanding \(P\) and \(Q\) means having some idea about what counts as a proof of \(P,Q\), respectively. If we are able to point out in general terms what we should consider as a proof of \(P\ast Q\), given our understanding of proofs of \(P,Q\), we will have explained the meaning of the connective ∗.
8.2 Disjunction
Let us start with the case of disjunction, ∨.
If someone says to us: ‘I have a proof of \(P \vee Q\), \(P\) or \(Q\)’, we expect, from our experience with earlier situations in which the word ‘or’ occurred, that he will come up with a proof of \(P\) or with a proof of \(Q\). We therefore adopt the rule that a proof of \(P\vee Q\) must consist either in a proof of \(P\) or in a proof of \(Q\).
One might bring forward that disjunction is not always taken in this constructively strong sense. There were other situations too! Some mathematicians might even say: ‘When I make a statement \(P\vee Q\), I merely want to remind my reader that \(\neg P\) and \(\neg Q\) are not both true’.
The intuitionistic mathematician then answers: ‘Sometimes one uses the stronger interpretation and at other times one uses the weaker one. Let us end this confusion and make the first and stronger interpretation the canonical one and always watch what we want to say.’
Our decision implies that the statement: is not a true statement.
$$ \exists n[ k_{99}\le n]\;\vee \;\forall n[n< k_{99}]\mbox{, i.e.}\ \exists n[ k_{99}\le n ]\;\vee \;\neg \exists n[ k_{99}\le n]. $$
Why?
Until now, we did not find a place in the decimal expansion of \(\pi \) where there is an uninterrupted sequence of 99 digits 9: we have no proof of ‘\(\exists n[ k_{99}\le n]\)’.
Until now, we also did not find a clever argument showing that such an uninterrupted sequence of 99 digits 9 never will be found: we have no proof of ‘\(\neg \exists n[ k_{99}\le n]\)’.
Until now, therefore, we have no proof of ‘\(\exists n[ k_{99}\le n]\; \vee \;\neg \exists n[ k_{99}\le n]\)’.
Note that there is an asymmetry in the two horns of the dilemma. The (possible) truth of \(\exists n[k_{99}\le n]\) will become clear to anyone who just patiently calculates the successive values of the decimal expansion of \(\pi \), but the discovery of the (possible) truth of \(\forall n[n< k_{99}]\) requires mathematical ingenuity.
The example shows that the principle
If \(\forall n[P(n)\;\vee \;\neg P(n)]\), then \(\exists n[P(n)]\;\vee \;\neg \exists n[P(n)]\)
is unreliable.
How did we come to trust it?
We unthinkingly generalized our experience with handling finite sets and bounded quantifiers. After all, the following holds, for any given \(m\), even for \(m=10^{10^{10}}\):
If \(\forall n\le m[P(n)\;\vee \;\neg P(n)]\), then \(\exists n\le m[P(n)]\;\vee \;\neg \exists n\le m[P(n)]\),
because, at least in principle, we can check each of the numbers \(0, 1, \ldots , m\) and find out if one of them has the property \(P\).
The case \(\{0,1, \ldots , m\}\) does not extend to the case \(\{0,1,2,\dots \}\).
Checking each of the infinitely many numbers \(0,1,2,\ldots \) is not feasible. If we think we can do it we must imagine ourselves to be angels rather than human beings.
8.3 ‘Reckless’ or ‘Hardy’ Statements
When in a playful mood, we call the statement: a reckless or hardy statement. Actually, it is foul play. We call the mathematician upholding the above statement as true ‘reckless’ because we take him to read the statement constructively. Probably, he will protest.
$$ \exists n[k_{99}=n]\;\vee \;\forall n[n< k_{99}] $$
For us, the terms ‘reckless’ and ‘hardy’ indicate that the statement called so has no constructive proof, although the non-intuitionistic mathematician, using his own reading, sees no objection.
Other examples of reckless statements are:
$$ \neg \forall n[n< k_{99}]\;\vee \;\forall n[n< k_{99}] $$
$$ \exists n[n=k_{88}]\rightarrow \exists n[n=k_{99}] $$
$$ \forall n[2n\neq k_{99}]\;\vee \;\forall n[2n+1\neq k_{99}] $$
$$ \exists n[n=k_{88}]\rightarrow (\forall n[2n\neq k_{99}]\;\vee \; \forall n[2n+1\neq k_{99}]) $$
‘\(n=k_{88}\)’ here stands for: ‘\(n\) is the least number \(m\) such that at the places \(m, m+1, \ldots , m+87\) in the decimal expansion of \(\pi \) we find the value 8’.
Theorems implying a reckless statement themselves will be considered reckless.
8.4 Brouwer’s Example and the Halting Problem
The above example of an undecided proposition, ‘\(\exists n[n=k_{99}]\)’, is simple and very important. A first such example was given by Brouwer in [10].
The example is related to the discovery, in 1936, of the ‘halting problem’ by A.M. Turing (1912-1954). We briefly describe this problem using the approach developed by S.C. Kleene (1909-1994), see [40, Chapter XI].
Natural numbers are used for coding algorithms for (partial) functions from ℕ to ℕ. There is a computable predicate on triples of natural numbers called \(T\). For all \(e,n,z\), \(T(e,n,z)\) if and only if \(z\) codes a successful computation according to the algorithm coded by \(e\) at the argument \(n\). The algorithm coded by \(e\) halts at \(n\) if and only if \(\exists z[T(e,n,z)]\). There is a function \(U\) from ℕ to ℕ that extracts from every \(z\) coding a computation the outcome \(U(z)\) of the computation. A function \(\alpha \) from ℕ to ℕ is computable if and only if there exists \(e\) such that
\(\forall n\exists z[T(e,n,z)\;\wedge \;U(z)=\alpha (n)]\). A number \(e\) with this property is called an index of the function \(\alpha \).
Every number \(e\) determines a partial function \(\varphi _{e}\) from ℕ to ℕ:
for all \(n\), \(\varphi _{e}(n) = U(z)\), where \(z\) is the least number \(w\) such that \(T(e, n, w)\).
\(\varphi _{e}\) is only defined at \(n\) if \(\exists w[T(e,n,w)]\).
The (self-)halting problem is the question if there exists a computable function \(\alpha \) from ℕ to ℕ such that, for each \(e\), Such a computable function \(\alpha \) would be called a solution to the halting problem.
$$ \alpha (e)\neq 0\leftrightarrow \exists z[T(e,e,z)]\leftrightarrow \varphi _{e} \;\mathit{is\;defined\;at\;e}. $$
Turing’s theorem is that there is no solution to the halting problem.
One may prove, without much difficulty, that there exists \(e\) such that
\(\exists n[ k_{99}\le n]\leftrightarrow \exists z[T(e,e,z)]\): the example we considered is one of the problems in the scope of the halting problem. Therefore, a solution to the halting problem would also solve the problem: ‘\(\exists n[k_{99}\le n]\)’. This fact gives some apriori probability to Turing’s result.
8.5 The Other Logical ‘Constants’
The so-called proof-theoretical interpretation of the disjunction we sketched in Sect. 8.2 is extended to the other logical ‘constants’ as follows.
A proof of ‘\(P\) and \(Q\)’ is a proof of ‘\(P\)’ together with a proof of ‘\(Q\)’.
A proof of ‘if \(P\), then Q’ is
a proof of ‘\(Q\)’ possibly using ‘\(P\)’ as an extra assumption.
A proof of ‘not \(P\)’ is a proof of ‘if \(P\), then 0=1’.
For explaining the quantifiers, we need the notion of a propositional function. Let \(V\) be a set and let \(v\mapsto P(v)\) a function that associates to every \(v\) in \(V\) a proposition \(P(v)\). We then may introduce propositions \(\exists x \in V[P(x)]\) and \(\forall x\in V[P(x)]\) by stipulating:
A proof of ‘\(\exists x\in V[P(x)]\)’ consists of an element \(v\) of \(V\) together with a proof of the proposition ‘\(P(v)\)’.
A proof of \(\forall x \in V[P(x)]\) is a function \(v\mapsto p(v)\) associating to every \(v\) in \(V\) a proof \(p(v)\) of the proposition ‘\(P(v)\)’.
These explanations are not to be considered as exact definitions. They only indicate a provisional intention as to how we want to use our words.
9 A Test Case: The Intermediate Value Theorem
9.1 The Theorem
A function from \(\mathcal{X}\subseteq \mathcal{R}\) to ℛ is an effective method \(f\), that, given any input \(x\) from \(\mathcal{X}\), will produce a well-defined outcome \(f(x)\) in ℛ, of course respecting the fundamental relation of real coincidence, i.e.
for all \(x,y\) in \(\mathcal{X}\), if \(x=_{\mathcal{R}}y\), then \(f(x)=_{\mathcal{R}} f(y)\).
We take the notion of a function as a primitive notion, i.e. we do not explain what a function is by using notions that have been introduced before.
Definition 6
Let \(f\) be a function from \(\mathcal{X}\subseteq \mathcal{R}\) to ℛ and let \(x\) in \(\mathcal{X}\) be given.
\(f\) is continuous at \(x\) if and only if \(\forall p\exists m\forall y\in \mathcal{X} [|y-x|<\frac{1}{2^{m}} \rightarrow |f(y)-f(x)|<\frac{1}{2^{p}}]\).
\(f\) is continuous if and only if \(f\) is continuous at every \(x\) in \(\mathcal{X}\).
The Intermediate Value Theorem states the following:
Let \(f\) be a continuous function from \([0,1]\) to ℛ.
Then
\(\forall y \in \mathcal{R}[f(0)\le y \le f(1)\rightarrow \exists x \in [0,1][f(x) = y]]\)
.
The first version of this Theorem dates from 1817 and is due to B. Bolzano (1781-1848), see [5].
Note that the intuitionistic mathematician reads the statement of the Theorem differently from her non-intuitionistic colleague: she understands the logical constants constructively, as sketched in Sect. 8.
9.2 The Proof as We Learnt It
One may use the fruitful method of successive bisection, as follows.
Let \(y\) be given such that \(f(0)\le y\le f(1)\).
Define \(x\) in \([0,1]\), step by step, as follows.
Define \(x(0) := (0,1)\).
Now let \(n\) be given such that \(x(n)\) has been defined already.
Consider \(m:=\frac{x'(n)+x''(n)}{2}\), the midpoint of the rational interval \(\bigl (x'(n), x''(n)\bigr )\).
If \(f(m)\le y\), define \(x(n+1) =\bigl (m, x''(n)\bigr )\).
If \(y< f(m)\), define \(x(n+1)= \bigl ( x'(n),m\bigr )\).
This completes the definition of \(x\).
\(x\) is a well-defined real number, and, as one verifies by induction,
for every \(n\), \(x''(n)-x'(n)=\frac{1}{2^{n}}\) and \(f\bigl (x'(n)\bigr ) \le y \le f\bigl (x''(n)\bigr )\).
We claim: \(f(x) =y\), and we prove this claim as follows.
Assume \(y<_{\mathcal{R}} f(x)\). Using the continuity of \(f\) at \(x\), find \(r\) such that
\(\forall z\in [0,1][|x-z|<\frac{1}{2^{r}}\rightarrow y<_{\mathcal{R}} f(z)]\).
Note: \(|x-x'(r+1)|<\frac{1}{2^{r}}\), and, therefore, \(y<_{\mathcal{R}} f\bigl (x'(r+1)\bigr )]\), but also
\(f\bigl (x'(r+1)\bigr )<_{\mathcal{R}}y\).
Contradiction.
Conclude: \(\neg \bigl (y <_{\mathcal{R}} f(x)\bigr )\), i.e. \(f(x)\le _{\mathcal{R}} y\).
By a similar argument, conclude: \(y \le _{\mathcal{R}} f(x)\) and: \(f(x)=_{\mathcal{R}} y\).
9.3 An Objection to the ‘Proof’
The construction of the point \(x\), in the above argument, can not be carried out, as, in general, we are unable to decide:
$$ f(m)\le _{\mathcal{R}} y\ {\textit{or}}\ \;y< _{\mathcal{R}} f(m). $$
9.4 Two Counterexamples to the Theorem
We give two examples showing that the statement of the theorem, if one reads it constructively, sometimes fails to be true.
First example.
Let \(\rho _{1}=(-\frac{1}{2})^{k_{99}}\) be the number oscillating up and down around \(0_{\mathcal{R}}\) introduced in Definition 5. Define a function \(f_{0}\) from \([0,1]\) to ℛ such that
(i)
\(f_{0}(0) = 0\) and \(f_{0}(1) = 1\) and \(f_{0}(\frac{1}{3})=f_{0}(\frac{2}{3}) = \frac{1}{2}+\rho _{1}\), and
(ii)
\(f_{0}\) is linear on the interval \([0,\frac{1}{3}]\), on the interval \([\frac{1}{3}, \frac{2}{3}]\) and on the interval \([\frac{2}{3},1]\).
Note: \(0 <\rho _{1}\leftrightarrow \forall x\in [\frac{1}{3},1][f_{0}(x)> \frac{1}{2}]\) and
\(\rho _{1}< 0\leftrightarrow \forall x\in [0,\frac{2}{3}][f_{0}(x)< \frac{1}{2}]\).
Assume we find \(x\) such that \(f_{0}(x) = \frac{1}{2}\).
Find \(p\) such that \(x''(p)-x'(p)<\frac{1}{3}\) and note: either \(\frac{1}{3}< x'(p)\) or \(x''(p)< \frac{2}{3}\).
If \(\frac{1}{3}< x'(p)\), then \(\frac{1}{3}< x\) and \(\neg (0<\rho _{1})\), that is: \(\rho _{1}\le 0\), and,
if \(x''(p)<_{\mathbb{Q}} \frac{2}{3}\), then \(x<\frac{2}{3}\) and \(\neg (\rho _{1}<0)\), that is: \(0 \le \rho _{1}\).
Conclude: either \(0\le \rho _{1}\) or \(\rho _{1} \le 0\).
This is a reckless or hardy conclusion.
Second example.
Let \(\rho _{0}=(\frac{1}{2})^{k_{99}}\) the number oscillating above \(0_{\mathcal{R}}\) introduced in Definition 5 and let \(\rho _{2}=\rho _{0}+\rho _{1}=(\frac{1}{2})^{k_{99}}+(-\frac{1}{2})^{k_{99}}\) be the number oscillating between \(0_{\mathcal{R}}\) and \(2\cdot \rho _{0}\), also introduced in Definition 5.
Define a function \(f_{1}\) from \([0,1]\) to ℛ such that
(i)
\(f_{1}(0) = 0\) and \(f_{1}(\frac{1}{2}) =\rho _{0}\) and \(f_{1}(1)=\rho _{2}\), and
(ii)
\(f_{1}\) is linear on the interval \([0,\frac{1}{2}]\) and on the interval \([\frac{1}{2},1]\).
Note: \(f_{1}(0)\le \frac{1}{2}\cdot \rho _{2} \le f_{1}(1)\).
If \(\exists n[2n=k_{99}]\),
then \(0<\rho _{0}\;\wedge \;\rho _{2}=2\cdot \rho _{0}\) and \(\forall x\in [0,1][f_{1}(x) = \frac{1}{2}\cdot \rho _{2} \rightarrow x=\frac{1}{2}]\), and,
if \(\exists n[2n+1=k_{99}]\),
then \(0<\rho _{0} \;\wedge \;\rho _{2}=0\) and \(\forall x\in [0,1][f_{1}(x)= \frac{1}{2}\cdot \rho _{2}\rightarrow (x=0 \;\vee \; x=1)]\).
Suppose we find \(x\) in \([0,1]\) such that \(f_{1}(x)=\frac{1}{2}\cdot \rho _{2}\).
Find \(p\) such that \(x''(p)-x'(p) <\frac{1}{2}\) and note:
either \(x''(p)<\frac{1}{2}\) or \(\frac{1}{2}< x'(p)\) or \(0< x'(p)\) and \(x''(p) <1\).
If \(x''(p)<\frac{1}{2}\) or \(\frac{1}{2}< x'(p)\), then \(\neg \exists n[2n=k_{99}]\).
If \(0< x'(p)\) and \(x''(p) <1\), then \(\neg \exists n[2n+1=k_{99}]\).
We thus see: \(\neg \exists n[2n=k_{99}]\) or \(\neg \exists n[2n+1=k_{99}]\).
This is a reckless or hardy conclusion.
Note that the above counterexamples pose a serious problem to the mathematician. If the Intermediate Value Theorem does not stand a straightforward constructive reading, what then is its meaning? The defender of the theorem must mumble something like: ‘Well, I did not mean that you really could find a point where \(f\) assumes the intermediate value, but …’
She thus is forced to look into her argument and to formulate its conclusion in a more cautious way.
We should not, because of the counterexamples, put aside the Intermediate Value Theorem as completely wrong, but, exercising care and patience, we must try and find related statements that are constructively true and, hopefully, useful.
In the remaining Subsections we show some of the results this policy brings us.
9.5 An Approximate Version
It helps to weaken the conclusion of the Intermediate Value Theorem by requiring only that, for every given accuracy \(\frac{1}{2^{p}}\), there exists a point where the function assumes a value closer to the given intermediate value than \(\frac{1}{2^{p}}\).
Brouwer, who knew his own famous fixed-point theorem to be constructively false, formulated and proved such an approximate fixed-point theorem, see [15].11 Note that the proof of the new theorem still is using the method of successive bisection.
Theorem 6
The Approximate Intermediate Value Theorem
Let \(f\) be a continuous function from \([0,1]\) to ℛ.
Then \(\forall p\forall y \in \mathcal{R}[f(0)\le y \le f(1)\rightarrow \exists x \in [0,1][ y -\frac{1}{2^{p}}< f(x) < y+\frac{1}{2^{p}}]\).
Proof
Let \(p\) be given and let \(y\) be given such that \(f(0)\le y\le f(1)\).
Define \(x\) in \([0,1]\), step by step, as follows.
Define \(x(0) := (0,1)\) and note: \(f\bigl (x'(0)\bigr )-\frac{1}{2^{p+1}}< y< f\bigl (x''(0)\bigr )+ \frac{1}{2^{p+1}}\).
Now let \(n\) be given such that \(x(n)\) has been defined already.
Consider \(m:=\frac{x'(n)+x''(n)}{2}\) and \(z:=f(m)\).
Find \(l\):= the least \(k\) such that both \(z''(k)-z'(k) <\frac{1}{2^{p+1}}\) and
\(y''(k)-y'(k)<\frac{1}{2^{p+1}}\) and define \(s:=z(l)\).
1. If \(s''< y'(l) +\frac{1}{2^{p+1}}\), define \(x(n+1) =(m, x''(n))\).
Then: \(f(m)\le s''< y'(l) +\frac{1}{2^{p+1}}\le y+\frac{1}{2^{p+1}}\) and: \(f(m) -\frac{1}{2^{p+1}}< y\).
2. If not \(s'' < y'(l)+\frac{1}{2^{p+1}}\), define \(x(n+1)= (x'(n), m)\).
Then: \(y''(l)< y'(l)+\frac{1}{2^{p+1}}\le s''< s'+\frac{1}{2^{p+1}}\) and: \(y< f(m)+\frac{1}{2^{p+1}}\).
This completes the definition of \(x\).
\(x\) is a well-defined real number, and,
for every \(n\), \(x''(n)-x'(n)=\frac{1}{2^{n}}\) and \(f\bigl (x'(n)\bigr ) -\frac{1}{2^{p+1}}< y< f\bigl (x''(n)\bigr )+ \frac{1}{2^{p+1}}\).
Using the fact that \(f\) is continuous at \(x\), find \(r\) such that
\(\forall z\in [0,1][x-\frac{1}{2^{r}}< z< x+\frac{1}{2^{r}}\rightarrow f(x) - \frac{1}{2^{p+1}}< f(z)< f(x)+\frac{1}{2^{p+1}}]\).
1. Note: \(x-\frac{1}{2^{r}}< x'(r+1) \le x\), and:
\(f(x)< f\bigl(x'(r+1)\bigr) +\frac{1}{2^{p+1}}< y+\frac{1}{2^{p+1}} + \frac{1}{2^{p+1}} = y +\frac{1}{2^{p}}\).
2. Note: \(x\le x''(r+1)< x+\frac{1}{2^{r}}\), and:
\(y< f\bigl (x''(r+1)\bigr )+\frac{1}{2^{p+1}}< f(x) +\frac{1}{2^{p+1}} + \frac{1}{2^{p+1}}= f(x)+\frac{1}{2^{p}}\).
Conclude: \(y -\frac{1}{2^{p}}< f(x)< y+\frac{1}{2^{p}}\). □
9.6 Locally Non-constant Functions
One may also try to restrict the class of functions to which the Intermediate Value Theorem applies. Observe that the two functions mentioned as counterexamples in Sect. 9.4 have the property that, over a whole interval, one does not know if they change their value. Let us try to forbid such behavior. We require constructive evidence that, for every \(y\), for every interval \((p,q)\), the function does not have, on the interval \((p,q)\), the constant value \(y\).
Definition 7
A function \(f\) from \([0,1]\) to ℛ is locally non-constant if and only if
\(\forall y \in \mathcal{R}\forall p \in \mathbb{Q}\forall q \in \mathbb{Q}[0< p< q<1 \rightarrow \exists x \in [0,1][p<x<q \;\wedge \; f(x) \;\#_{\mathcal{R}}\; y]]\).
The following Lemma says that, if, for a given intermediate value \(y\), the function \(f\) assumes, in any given interval, a value positively different from \(y\), then there is a point where \(f\) assumes the value \(y\).
Lemma 7
Let \(f\) be a continuous function from \([0,1]\) to ℛ.
Let
\(y\)
be given such that
\(f(0)\le y \le f(1)\)
and
\(\forall p \in \mathbb{Q}\forall q \in \mathbb{Q}[0< p< q<1 \rightarrow \exists x \in [0,1][p<x<q \;\wedge \; f(x) \;\#_{\mathcal{R}}\; y]]\).
Then \(\exists x \in [0,1][f(x) = y]\).
Proof
Let \(y\) be given such that \(f(0)\le y \le f(1)\).
Define \(x\) in \([0,1]\), as follows, step by step.
Define \(x(0) := (0,1)\).
Now let \(n\) be given such that \(s:=x(n)\) has been defined.
Using the continuity of \(f\), find a rational number \(q\) such that
\(\frac{2}{3}s'+_{\mathbb{Q}}\frac{1}{3}s''< q<\frac{1}{3}s'+_{\mathbb{Q}} \frac{2}{3}s''\) and \(f(q)\;\#_{\mathcal{R}}\;y\).
If \(f(q)<_{\mathcal{R}} y\), define \(x(n+1):= \bigl (x'(n), q\bigr )\), and,
if \(y<_{\mathcal{R}} f(q)\), define \(x(n+1):= \bigl (q,x''(n)\bigr )\).
This completes the definition of \(x\).
\(x\) is a well-defined real number, as, for each \(n\),
\(x'(n)\le x'(n+1)\le x''(n+1)\le x''(n)\) and \(x''(n+1) -x'(n+1) \le \frac{2}{3}\bigl (x''(n) - x'(n)\bigr )\).
Moreover, for each \(n\), \(f\bigl (x'(n)\bigr ) \le _{\mathcal{R}} y \le _{\mathcal{R}} f\bigl (x''(n) \bigr )\).
Assume: \(f(x) <_{\mathcal{R}} y\).
Find \(p\) such that \(\frac{1}{2^{p}}< y-_{\mathcal{R}} f(x)\), and find \(q\) such that
\(\forall z \in [0,1][|z-x| < \frac{1}{2^{q}} \rightarrow |f(z) - f(x)|<_{\mathcal{R}} \frac{1}{2^{p}}]\).
Then \(\forall z \in [0,1][|z-x| < \frac{1}{2^{q}} \rightarrow f(z) <_{\mathcal{R}} y\). Find \(r\) such that \((\frac{2}{3})^{r}<\frac{1}{2})^{q}\).
Conclude: \(f(x''(r)) <_{\mathcal{R}} y\). Contradiction.
We thus see: \(\neg (f(x) <_{\mathcal{R}} y)\), that is: \(f(x) \ge _{\mathcal{R}} y\).
For similar reasons: \(f(x) \le _{\mathcal{R}} y\). Conclude: \(f(x) =_{\mathcal{R}} y\). □
Theorem 8
The Intermediate Value Theorem for locally non-constant functions
Let \(f\) be a continuous and locally non-constant function from \([0,1]\) to ℛ. Then \(\forall y[f(0)\le y \le f(1)\rightarrow \exists x\in [0,1][f(x)=y]]\).
Proof
Use Lemma 7. □
From a constructive point of view, the next result, Theorem 9 is not a nice result. The result nevertheless is instructive. The intuitionistic mathematician may say: ‘Yes, this explains the classical mathematician’s belief that the Intermediate Value Theorem is true. He means no more than that it is impossible to have constructive evidence, for every point \(x\) in the domain of the function, that the value assumed at \(x\) is apart from the given intermediate value. Unfortunately, even if this impossible, it may also be impossible to find a point where the intermediate value is assumed.’
Theorem 9
The Negative Intermediate Value Theorem
Let \(f\) be a continuous function from \([0,1]\) to ℛ. Then \(\forall y[f(0)\le y\le f(1)\rightarrow \neg \forall x \in [0,1][f(x) \;\#_{\mathcal{R}}\; y]]\).
Proof
Use Lemma 7. □
9.7 At Most Countably Many Exceptions
One may also observe that the Intermediate Value Theorem goes through for ‘most’ intermediate values.
Theorem 10
The Intermediate Value Theorem holds with at most countably many exceptions13
Let \(f\) be a continuous function from \([0,1]\) to ℛ.
There exists an infinite sequence
\(y_{0}, y_{1}, \ldots \)
of elements of
\([0,1]\)
such that
\(\forall y [\bigl (f(0)\le y\le f(1) \;\wedge \;\forall n[ y \;\#_{\mathcal{R}}\; y_{n}]\bigr ) \rightarrow \exists x \in [0,1][f(x) = y]]\).
Proof
Let \(q_{0}, q_{1}, q_{2} \ldots \) be an enumeration of all rational numbers \(q\) in \([0,1]\). For each \(n\), define \(y_{n}:=f(q_{n})\).
Let \(y\) in \([0,1]\) be given such that \(\forall n[ y \;\#_{\mathcal{R}} \;y_{n}]\).
Define \(x\) in \([0,1]\), step by step.
Define \(x(0) := (0,1)\) and note: \(f(0) <_{\mathcal{R}} y<_{\mathcal{R}} f(1) \).
Now let \(n\) be given such that \(x(n)\) is defined and \(f\bigl (x'(n)\bigr ) <_{\mathcal{R}} y <_{\mathcal{R}} f\bigl (x''(n)\bigr )\).
Consider \(m:=\frac{x'(n)+x''(n)}{2}\). If \(f(m) <_{\mathcal{R}} y\), define: \(x(n+1):= (m, x''(n))\), and, if \(y<_{\mathcal{R}} f(m)\), define: \(x(n+1):= (x'(n), m)\). Then
\(f\bigl (x'(n+1)\bigr ) <_{\mathcal{R}} y <_{\mathcal{R}} f(\bigl (x''(n+1) \bigr )\).
This completes the definition of \(x\).
Using the argument given in the last part of the proof of Lemma 7, one proves: \(f(x) =_{\mathcal{R}} y\). □
9.8 Perhaps, Perhaps, Perhaps,…
Suppose we change the conclusion of the Intermediate Value Theorem into
(∗) \(\exists x_{0}[f(x_{0})\;\#_{\mathcal{R}} \;y \rightarrow \exists x_{1}[f(x_{1}) =_{\mathcal{R}} y]]\),
One may think of \((\ast )\) as follows. You are offered \(x_{0}\) where \(f\) should assume the value \(y\). If you discover \(x_{0}\) clearly does not work, you may go back to the shop and ask for a better number and will be offered \(x_{1}\) and \(x_{1}\) certainly will work.
One may reconsider the two counterexamples given in Sect. 9.4, the functions \(f_{0}\) and \(f_{1}\), in the light of this definition.
We have seen that the statement ‘\(f_{0}\) assumes the value \(\frac{1}{2}\)’ is reckless, but, if \(f_{0}(\frac{1}{2}) \;\#_{\mathcal{R}}\; \frac{1}{2}\), then \(\rho _{1}\;\#_{\mathcal{R}}\; 0\) and: either \(0 <_{\mathcal{R}} \rho _{1}\) and \(f_{0}(\frac{1}{3}\cdot \frac{1}{1+2\cdot \rho _{1}})=\frac{1}{2}\), or \(\rho _{1}<_{\mathcal{R}} 0\) and \(f_{0}(\frac{2}{3}-\frac{2\cdot \rho _{1}}{1-2\cdot \rho _{1}})= \frac{1}{2}\). We thus see: perhaps, \(f_{0}\) assumes the value \(\frac{1}{2}\).
We also have seen that the statement ‘\(f_{1}\) assumes the value \(\frac{1}{2}\cdot \rho _{2}\)’ is reckless, but, if \(f_{1}(0)\;\#_{\mathcal{R}} \;\frac{1}{2}\cdot \rho _{2}\), then \(\rho _{2}\;\#_{\mathcal{R}}\;0_{\mathcal{R}}\) and \(\rho _{0}=_{\mathcal{R}}\rho _{1}\) and \(f_{1}(\frac{1}{2})=_{\mathcal{R}}\frac{1}{2}\cdot \rho _{2}\). We thus see: perhaps, \(f_{1}\) assumes the value \(\frac{1}{2}\cdot \rho _{2}\).
The funny thing is that the operation Perhaps may be repeated. One may consider the statement:
\(\exists x_{0}[f(x_{0})\;\#_{\mathcal{R}}\; y \rightarrow \exists x_{1}[f(x_{1}) \#_{\mathcal{R}}\;y \rightarrow \exists x_{2}[f(x_{2})=_{\mathcal{R}}y]]]\),
Perhaps, perhaps, \(f\) Passumes the value \(y\).
We give an example showing that this statement indeed may be weaker than the previous one, with only one ‘perhaps’.
Another example.
Consider \(\rho _{1}=(-\frac{1}{2})^{k_{99}}\) but also \(\rho _{3}:= (-\frac{1}{2})^{k_{88}}\).
Define a function \(f_{2}\) from \([0,1]\) to ℛ such that
(i)
\(f_{2}(0) = 0\) and \(f_{2}(1) = 1\) and \(f_{2}(\frac{1}{5})=f_{2}(\frac{2}{5})= \frac{1}{2}+\rho _{1}\), and
\(f_{2}(\frac{3}{5})=f_{2}(\frac{4}{5})= \frac{1}{2}+\rho _{3}\), and,
(ii)
for each \(i\le 4\), \(f_{2}\) is linear on the interval \([\frac{i}{5},\frac{i+1}{5}]\).
Let us first observe: if \(f_{2}(\frac{1}{5})\;\#_{\mathcal{R}}\; \frac{1}{2}\) and also \(f_{2}(\frac{3}{5})\;\#_{\mathcal{R}}\; \frac{1}{2}\), then \(\rho _{1}\;\#_{\mathcal{R}}\; 0\) and \(\rho _{3} \;\#_{\mathcal{R}} \;0\) and \(\exists x[f(x)=_{\mathcal{R}} \frac{1}{2}]\). Conclude:
Perhaps, perhaps, \(f_{2}\) assumes the value \(\frac{1}{2}\).
Now assume: Perhaps, \(f_{2}\) assumes the value \(\frac{1}{2}\).
Find \(x_{0}\) such that, if \(f_{2}(x_{0})\;\#_{\mathcal{R}}\;\frac{1}{2}\), then \(\exists x_{1}[f_{2}(x_{1}) =_{\mathcal{R}} \frac{1}{2}]\).
Distinguish two cases.
Case (1). \(x_{0} <_{\mathcal{R}} \frac{8}{15}\). Assume: \(\rho _{1}<_{\mathcal{R}} 0\).
Define \(x_{1}:=\sup (x_{0}, \frac{2}{5})\) and note \(f(x_{1}) = f(\frac{2}{5}) + (x_{1}-\frac{2}{5})\cdot 5(\rho _{3}- \rho _{1})= \frac{1}{2} +\rho _{1} + (x_{1}-\frac{2}{5})\cdot 5(\rho _{3}-\rho _{1}) \le _{\mathcal{R}} \frac{1}{2} + \rho _{1} + (\frac{8}{15}-\frac{2}{5}) \cdot 5(\rho _{3}-\rho _{1})= \frac{1}{2} +\frac{1}{3}\rho _{1} + \frac{2}{3}\rho _{3}\).
Conclude: \(f(x_{0})\le _{\mathcal{R}} f(x_{1}) <_{\mathcal{R}} \frac{1}{2}\) or \(0<_{\mathcal{R}} \rho _{3}\).
In both cases, one may conclude:
\(\exists x \in [0,1][f_{2}(x)=_{\mathcal{R}} \frac{1}{2}]\) and: \(0\le _{\mathcal{R}}\rho _{3}\;\vee \; \rho _{3}\le _{\mathcal{R}} 0\).
We thus see: if \(\rho _{1}<_{\mathcal{R}} 0\), then \(0\le _{\mathcal{R}}\rho _{3}\;\vee \; \rho _{3}\le _{\mathcal{R}} 0\), i.e.
if \(\exists n[2n+1=k_{99}]\), then \(\forall n[2n+1\neq k_{88}]\;\vee \; \forall n[2n\neq k_{88}]\),
a reckless or hardy conclusion.
Case (2). \(\frac{7}{15}<_{\mathcal{R}} x_{0} \). By a similar argument, we obtain the result:
if \(0<_{\mathcal{R}} \rho _{3}\), then \(0\le _{\mathcal{R}}\rho _{1}\;\vee \; \rho _{1}\le _{\mathcal{R}} 0\), i.e.
if \(\exists n[2n=k_{88}]\), then \(\forall n[2n+1\neq k_{99}]\;\vee \; \forall n[2n\neq k_{99}]\),
a reckless or hardy conclusion.
We thus see that the statement
has reckless consequences.‘Perhaps, \(f_{2}\) assumes the value \(\frac{1}{2}\)’
One now may define: and, for each \(n\), and also and and prove that in general, all these statements have different meanings. Following this path, increasing the number of ‘perhapses’ further into the transfinite, one finds uncountably many intuitionistically different versions of the notion: ‘\(\exists x[f(x)=_{\mathcal{R}}y]\)’, see [56].
$$ \mathit{Perhaps}_{0}(f,y)\ \mathit{if\ and\ only\ if}\ \exists x[f(x)=y] $$
$$ \mathit{Perhaps}_{n+1}(f, y)\ \mathit{if\ and\ only\ if}\ \exists x[f(x)\;\#_{\mathcal{R}}\;y \rightarrow \mathit{Perhaps}_{n}( f, y)] $$
$$ \mathit{Perhaps}_{\omega }(f, y)\ \mathit{if\ and\ only\ if}\ \exists n[\mathit{Perhaps}_{n}(f, y)], $$
$$ \mathit{Perhaps}_{\omega +1}(f, y)\ \mathit{if\ and\ only\ if}\ \exists x[f(x)\;\#_{\mathcal{R}}\;y\rightarrow \mathit{Perhaps}_{\omega }(f, y)]. $$
10 A Function from ℛ to ℛ Is Nowhere Positively Discontinuous
In the next three Sections we study the intuitionistic claim that every real function is continuous. The first theorem, Theorem 11, is weak and negative.
10.1 No Positive Discontinuity
Definition 8
Let \(f\) be a function from \(\mathcal{X}\subseteq \mathcal{R}\) to ℛ and let \(x\) in \(\mathcal{X}\) be given. \(f\) is positively discontinuous at \(x\) if and only if \(\exists p\forall m\exists y\in \mathcal{X}[|y-x| < \frac{1}{2^{m}} \;\wedge \; | f(y)-f(x)|\ge \frac{1}{2^{p}}]\).
Theorem 11
15Let \(f\) be a function from \(\mathcal{X}\subseteq \mathcal{R}\) to ℛ. Assume there exists \(x\) in \(\mathcal{X}\) such that \(f\) is positively discontinuous at \(x\). Then there exists \(z\) in ℛ such that we can not calculate \(f(z)\), so \(z\) can not belong to \(\mathcal{X}\).
Proof
Let \(\mathcal{X}, f, x\) satisfy the conditions of the theorem.
Without loss of generality, we may assume: \(x=0=f(0)\).
Find \(p\) such that \(\forall m\exists y\in \mathcal{X}[| y |< \frac{1}{2^{m}} \;\wedge \; | f(y)|>\frac{1}{2^{p}}]\).
Find an infinite sequence \(y_{0}, y_{1}, \ldots \) of reals such that
\(\forall m[| y_{m} | < \frac{1}{2^{m}} \;\wedge \; | f(y_{m})|> \frac{1}{2^{p}}]\).
We give two arguments establishing the conclusion of the theorem.
First argument.
I start constructing a real number \(z\) in an infinite sequence of steps, defining successively \(z(0), z(1), z(2), \ldots \).
I promise to take care that for each \(n\), \(z'(n)\le z'(n+1)\le z''(n+1)\le z''(n)\) and \(z''(n)-z'(n) =\frac{1}{2^{n-1}}\). I am free, within these bounds, to choose each \(z(n)\) as I like it.
I have in mind to perhaps ‘freeze’ the free development of \(z\), at some step \(n\), by making a decision that determines all values from that step \(n\) on.
I define \(z(0)=(-1,1)\) and do not freeze \(z\) at step 0. For each \(n>0\), if \(z\) has not yet been frozen at one of the earlier steps, either I do not freeze \(z\) at this step and define \(z(n) = (-\frac{1}{2^{n}}, \frac{1}{2^{n}})\), or I freeze \(z\) by defining, for each \(i\), \(z(n+i) = y_{n-1}(q+i)\), where \(q\) is the least \(k\) such that \(-\frac{1}{2^{n-1}}< y'_{n-1}(k)\le y''_{n-1}(k)<\frac{1}{2^{n-1}}\).
\(z\) is a well-defined real number.
Note: if I never make use of my freedom to freeze \(z\), then \(z=_{\mathcal{R}} 0\) and \(f(z)=_{\mathcal{R}}0\).
Note: if I do use this freedom at some step \(n>0\), then \(z=_{\mathcal{R}}y_{n-1}\) and
\(|f(z)|=_{\mathcal{R}} |f(y_{n-1})|>_{\mathcal{R}}\frac{1}{2^{p}}\).
But I am free and do not know myself if I ever will make use of the possibility to freeze \(z\) or not.
I thus am unable to find an approximation of \(f(z)\) smaller than \(\frac{1}{2^{p}}\).
We must conclude: \(f\) is not defined at the argument \(z\) and \(z\) does not belong to the domain \(\mathcal{X}\) of \(f\).
Second argument.
Define \(z\) such that, for each \(n\),
if \(n< k_{99}\), then \(z(n) = (-\frac{1}{2^{n}}, \frac{1}{2^{n}})\), and, if \(k_{99}\le n\), then \(z(n) = y_{k_{99}}(q +n)\),
where \(q\) is the least \(k\) such that \(-\frac{1}{2^{k_{99}}}< y'_{k_{99}}(k)\le y''_{k_{99}}(k)< \frac{1}{2^{k_{99}}}\).
Note: if \(\forall n[n< k_{99}]\), then \(f(z) =_{\mathcal{R}} f(0_{\mathcal{R}})=_{\mathcal{R}}0\), and,
if \(\exists n[n= k_{99}]\), then \(|f(z)|=_{\mathcal{R}}|f(y_{k_{99}}|>_{\mathcal{R}}\frac{1}{2^{p}}\).
Assume we may calculate \(f(z)\). By finding an approximation of \(f(z)\) smaller than \(\frac{1}{2^{p}}\) we will be able to decide: \(f(z) \;\#_{\mathcal{R}}\; 0\) or \(|f(z)| <_{\mathcal{R}} \frac{1}{2^{p}}\).
Case (a). \(f(z) \;\#_{\mathcal{R}}\;0\), and, therefore: \(\neg \forall n[n< k_{99}]\).
Case (b). \(|f(z)|< \frac{1}{2^{p}}\), and, therefore: \(\forall n[n< k_{99}]\).
Conclude: \(\neg \forall n[n< k_{99}]\;\vee \;\forall n[n< k_{99}]\).
This is a reckless conclusion.
We must admit that, at this point of time, \(f\) is not defined at \(z\) and \(z\) does not belong to the domain \(\mathcal{X}\) of \(f\). □
Clearly, a function from \(\mathcal{X}\subseteq \mathcal{R}\) with a positive discontinuity can not be calculated at every point of ℛ. In Brouwer’s terminology: such a function is not a full function.
11 The Meaning of ‘Not’
11.1 A Weak and a Strong Interpretation
May we conclude, from Theorem 11:
A function \(f\) from ℛ to ℛ is not positively discontinuous at any point \(x\) in ℛ?
We have to be careful. There is some ambiguity in the use of the word ‘not’. When saying:
‘not: \((\exists n[n=k_{99}]\;\vee \; \forall n[n< k_{99}])\)’
we mean no more than:
‘As yet, we have no proof of ‘\(\exists n[n=k_{99}\;\vee \; \forall n[n< k_{99}]\)’.
Most of the time, however, we take a proposition ‘not \(P\)’, \(`\neg P'\), in the stronger sense indicated in Sect. 8.5: ‘Assuming \(P\), one is led to a contradiction’. This strong interpretation of ‘not’ is the canonical one. It follows from reading ‘\(not\)-\(P\)’ as ‘\(P \rightarrow 0=1\)’ and interpreting the implication ‘\(P\rightarrow Q\)’ as: ‘Assuming \(P\), one may prove \(Q\)’.
Following this strong and canonical interpretation, one may prove, for any proposition \(P\), as follows: Assume: \(\neg (P\vee \neg P)\), i.e. \(P\vee \neg P\) leads to a contradiction. Then both \(P\) and \(\neg P\) will lead to a contradiction. We thus see: \(\neg P\) and: \(\neg P\) leads to a contradiction. We therefore have a contradiction.
$$ \neg \neg (P\vee \neg P), $$
Conclude: \(\neg (P\vee \neg P)\) leads to a contradiction, i.e. \(\neg \neg (P\vee \neg P)\).
In particular, we find:
$$ \neg \neg (\exists n[n=k_{99}]\;\vee \;\forall n[n< k_{99}]). $$
11.2 Some Useful Remarks
Defining \(Q:= \exists n[n=k_{99}]\;\vee \;\neg \exists n[n=k_{99}]\), we see that there are propositions \(Q\) such that \(\neg \neg Q\) is true but \(Q\) itself is reckless or hardy. On the other hand, for every proposition \(Q\), if \(Q\), then \(\neg \neg Q\). If \(Q\) has a proof, then \(\neg Q\), (the statement that \(Q\) leads to a contradiction), leads indeed to a contradiction.
Later in this paper, we need the following law of contraposition:
if \(P\rightarrow Q\), then \(\neg Q \rightarrow \neg P\), and its consequence: if \(P\rightarrow Q\), then \(\neg \neg P\rightarrow \neg \neg Q\).
This law is easily seen to be valid for the proof-theoretical interpretation.
Using it, one sees that, as \(Q\rightarrow \neg \neg Q\) is always true, also \(\neg \neg \neg Q\rightarrow \neg Q\) is always true. (The scheme \(\neg \neg \neg Q\rightarrow \neg Q\) was discovered by Brouwer and may be called Brouwer’s first law of logic).
Also note:
if \((P\;\vee \neg P)\rightarrow \neg Q\), then, as \(\neg \neg (P\;\vee \;\neg P)\), one has: \(\neg \neg \neg Q\), and, therefore: \(\neg Q\).
This fact may be useful in practice: if it is our aim to prove a negative statement \(\neg Q\) it does no harm to make an extra assumption \(P\vee \neg P\).
One should keep in mind: \(\neg P\) means: \(P\) is reducible to absurdity. Therefore, the constructive mathematician has nothing to criticize if someone proves \(\neg P\) by reducing \(P\) to absurdity. If one does so, one does what one has to do.16 She feels unhappy, however, if one proves \(P\) itself by reducing \(\neg P\) to absurdity. The conclusion of the latter procedure is \(\neg \neg P\) only, a statement that, most of the time, is weaker than \(P\).
11.3 More Fugitive Numbers
The following Definition extends Definition 4.
Definition 9
The fugitive numbers \(k_{\alpha }\)
Let an infinite sequence
\(\alpha =\alpha (0), \alpha (1), \alpha (2), \ldots \) of natural numbers be given. For each \(n\) we define:17
\(k_{\alpha }\le n\) if and only if \(\exists j\le n [\alpha (j)\neq 0]\), and:
\(n< k_{\alpha }\) if and only if \(\forall j\le n [\alpha (j)=0]\), and:
\(n=k_{\alpha }\) if and only if \(k_{\alpha }\le n\) and \(\forall j< n[j< k_{\alpha }]\), i.e.
\(n\) is the least \(j\) such that \(\alpha (j)\neq 0\).
\(\mathbf{LPO}\), the limited principle of omniscience,18 is the statement
$$ \forall \alpha [\exists n[k_{\alpha }\le n] \;\vee \;\forall n[n< k_{\alpha }]]. $$
\(\mathbf{WLPO}\), the weak limited principle of omniscience is the statement
$$ \forall \alpha [\neg \forall n[n< k_{\alpha }] \;\vee \;\forall n[n< k_{\alpha }]]. $$
Using the second argument in the proof of Theorem 11 one may see:
If a real function from ℛ to ℛ has a positive discontinuity, then \(\mathbf{WLPO}\).
For an informal constructive mathematician like Brouwer, \(\mathbf{LPO}\), and also
\(\mathbf{WLPO}\), represent the absurd, the contradiction, a statement one feels sure never to be able to prove. For her, the argument for Theorem 11 establishes, for every ‘full’ function \(f\) from ℛ to ℛ,
\(\neg\)(there exists \(x\) in ℛ such that \(f\) is positively discontinuous at \(x\)).
12 The Continuity Principle
Let \(f\) be a (‘full’) function from ℛ to ℛ. The statement that there is no point where \(f\) is positively discontinuous is, constructively, a weak statement and not a very useful one. The positive result that \(f\) is continuous at every point is obtained from an axiomatic assumption first used by Brouwer.
12.1 Understanding Brouwer’s Continuity Principle
We first have to agree upon some notation.
In the following definition, we use \(k, n_{0}, n_{1}, \ldots , s, t, u,\ldots \) as variables over the set ℕ.
Definition 10
Coding finite sequences of natural numbers by natural numbers
Let \(p:\mathbb{N}\rightarrow \mathbb{N}\) be the function enumerating the primes: \(p(0)=2, p(1)=3, p(2) = 5, \ldots \).
We define, for each \(k\), for all \(n_{0}, n_{1}, \ldots ,n_{k-1}\), \(\langle n_{0}, n_{1}, \ldots , n_{k-1}\rangle := p(k-1)\cdot \prod _{i< k}p(i)^{n_{i}}-1\).
We also define: \(\langle \;\rangle :=0\).
For all \(s\), for each \(k\), for all \(n_{0}, n_{1}, \ldots ,n_{k-1}\), if \(s=\langle n_{0}, n_{1}, \ldots , n_{k-1}\rangle \), then \(length(s)=k\) and, for all \(i< length(s)\), \(s(i):=n_{i}\).
For all \(k\), \(\omega ^{k}:=\{s\mid length(s) =k\}\).
For all \(k,l\), for all \(s\) in \(\omega ^{k}\), for all \(t\) in \(\omega ^{l}\), \(s\ast t\) is the element of \(\omega ^{k+l}\) satisfying \(\forall i< k[s\ast t(i) =s(i)]\) and \(\forall j< l[s\ast t(k+j)=t(j)]\).
For all \(s,t\), \(s\sqsubseteq t\leftrightarrow \exists u[s\ast u =t]\) and \(s\sqsubset t \leftrightarrow (s\sqsubseteq t \;\wedge \; s\neq t)\).
For all \(s,t\), \(s\perp t\leftrightarrow \neg (s\sqsubseteq t \;\vee \; t\sqsubseteq s)\).
Definition 11
\(\mathcal{N}:=\omega ^{\omega }\) is the set of all infinite sequences \(\alpha =\alpha (0), \alpha (1), \alpha (2),\ldots \) of non-negative integers. We use \(\alpha , \beta , \ldots \varphi , \psi , \ldots \) as variables over \(\mathcal{N}\).
\(\mathcal{N}\) is sometimes called Baire space.
For each \(\alpha \), for each \(m\), \(\overline{\alpha }m :=\langle \alpha (0), \alpha (1), \ldots , \alpha (m-1)\rangle \).
For all \(s\), for all \(\alpha \), \(s\sqsubset \alpha \leftrightarrow \exists n[\overline{\alpha }n = s]\) and \(s\perp \alpha \leftrightarrow \neg (s\sqsubset \alpha )\).
For each \(n\), we let \(\underline{n}\) be the infinite sequence with the constant value \(n\), that is, for all \(i\), \(\underline{n} (i) = n\).
Axiom 1
Brouwer’s Continuity Principle, \(\mathbf{BCP}\)
For every \(R\subseteq \mathcal{N} \times \mathbb{N}\),
if \(\forall \alpha \in \mathcal{N}\exists n[\alpha Rn]\), then \(\forall \alpha \in \mathcal{N}\exists m \exists n \forall \beta \in \mathcal{N}[\overline{\alpha }m \sqsubset \beta \rightarrow \beta R n]\).
How may we convince each other that this axiom is ‘reasonable’ and that we should accept it as a rule for our common mathematical game?
We should ask what we mean by the ‘set’ \(\mathcal{N}\) of all infinite sequences of natural numbers. This ‘set’ is a kind of framework in which all kinds of infinite sequences will grow, although only a very few of them have been realized up to now.
Cantor’s suggestion that a set is the result of taking together its (earlier constructed?) elements is a notion that does not make sense to us.
An infinite sequence \(\alpha \) may be given by a finite description or an algorithm that enables us to find, one by one, the successive values \(\alpha (0), \alpha (1), \ldots \) of \(\alpha \). Brouwer calls such infinite sequences lawlike sequences.
As we saw in the first argument in the proof of Theorem 11, there are also infinite sequences \(\alpha \) that are not governed by a law. The successive values \(\alpha (0), \alpha (1), \alpha (2), \ldots \) of \(\alpha \) then are freely chosen, step by step. At any given moment, only a finite initial part \(\bigl (\alpha (0), \alpha (1), \ldots , \alpha (n-1)\bigr )\) of \(\alpha \) is known. One may ask for further values, but, having received the answers, one still only knows a finite initial part of \(\alpha \), albeit a longer one.
There are intermediate possibilities. Having begun with choosing freely, step by step, \(\alpha (0), \alpha (1), \ldots \alpha (n-1)\) one may decide, to ‘freeze’ \(\alpha \) and to determine the remaining values by means of some rule or algorithm.
There is even a possibility I make \(\alpha \) dependent on my future mathematical experience, by saying, for instance, \(\alpha (n) =0\) if at the moments \(0,1, \ldots , n\), I did not find a proof of the \(abc\)-conjecture, and \(\alpha (n) = 1\), if I did.
If we think of the set \(\mathcal{N}\) as a framework making room for lawlike sequences as well as for free-choice-sequences and sequences that are of some intermediate kind, we are thinking of, what Brouwer calls, the full continuum.
Now assume \(R\subseteq \mathcal{N}\times \mathbb{N}\) is given such that \(\forall \alpha \exists n[\alpha Rn]\). Every infinite sequence \(\alpha \), also a lawlike sequence \(\alpha \), may be thought of as being produced, step by step, by a black box. At the moment we produce a number \(n\) such that \(\alpha Rn\), only finitely many values of \(\alpha \), say \(\alpha (0), \alpha (1), \ldots , \alpha (m-1)\), will have become known. Clearly, for any infinite sequence such that \(\beta (0) =\alpha (0)\), \(\beta (1) = \alpha (1), \ldots \) and \(\beta (m-1) = \alpha (m-1)\), one may conclude: \(\beta Rn\).
Adopting Axiom 1 as a starting point for our further mathematical discourse, we lay down a canonical meaning for expressions of the form ‘\(\forall \alpha \exists n[\alpha Rn]\)’. Earlier, we did so for expressions of the form ‘infinite’, ‘uncountable’ and ‘or’.
Theorem 12
\(\mathbf{BCP} \Rightarrow \neg \mathbf{WLPO}\).
Proof
Assume \(\mathbf{WLPO}\) i.e. \(\forall \alpha [\neg \forall n[n< k_{\alpha }]\;\vee \;\forall n[n< k_{\alpha }]]\), i.e.
\(\forall \alpha [\neg \forall n[\alpha (n)=0]\;\vee \;\forall n[ \alpha (n)=0]]\).
Consider \(\alpha = \underline{0}\) and, applying \(\mathbf{BCP}\), find \(m\) such that
either \(\forall \beta [\overline{\underline{0}}m \sqsubset \beta \rightarrow \neg \forall n[\beta (n)= 0]]\) or \(\forall \beta [ \overline{\underline{0}}m \sqsubset \beta \rightarrow \forall n[\beta (n)= 0]]\).
The first of these two statements is not true, consider: \(\beta = \underline{0}\), and the second one also fails, consider: \(\beta = \underline{\overline{0}}m\ast \underline{1}\).
We thus obtain a contradiction. □
12.2 The (Pointwise) Continuity of Functions from ℛ to ℛ
In the next Definition, we introduce a function \(\alpha \mapsto u_{\alpha }\) associating to every \(\alpha \) in \(\mathcal{N}\) a real number \(u_{\alpha }\).
Definition 12
We let \((r_{0}', r_{0}''), \;(r_{1}', r_{1}''), \;(r_{2}', r_{2}''), \; \ldots \) be a fixed enumeration of all pairs of rationals.
We define a mapping associating to each \(s\neq 0\) a pair \((u_{s}', u_{s}'')\) of rationals, as follows.
For each \(n\), if \(0< r_{n}''-r_{n}' \le 1\), then \((u'_{\langle n \rangle }, u''_{\langle n \rangle })= (r_{n}', r_{n}'')\), and,
if not, then \((u'_{\langle n \rangle }, u''_{\langle n \rangle })= (0,1)\).
For each \(s\neq 0\), for each \(n\), if \(u'_{s}< r'_{n}< r''_{n}< u''_{s}\) and
\(0< r_{n}''-r_{n}' \le \frac{1}{2} (u''_{s}-u'_{s})\), then \((u'_{s\ast \langle n \rangle }, u''_{s\ast \langle n \rangle })=(r_{n}', r_{n}'')\), and,
if not, then \((u'_{s\ast \langle n \rangle }, u''_{s\ast \langle n \rangle })=( \frac{2}{3}u'_{s} + \frac{1}{3}u''_{s},\frac{1}{3}u'_{s} + \frac{2}{3}u''_{s})\).
For each \(\alpha \) in \(\mathcal{N}\) we let \(u_{\alpha }\) be the infinite sequence of pairs of rationals such that,
for all \(n\), \(u_{\alpha }(n)=(u_{\overline{\alpha }(n+1)}', u_{\overline{\alpha }(n+1)}'')\).
Theorem 13
19
(i)
For every \(\alpha \), \(u_{\alpha }\) is a real number.
(ii)
For every real number \(x\), there exists \(\alpha \) such that \(x=_{\mathcal{R}}u_{\alpha }\).
(iii)
\(\mathbf{BCP}\Rightarrow \) Every function from ℛ to ℛ is continuous at every point \(x\).
Proof
The proof of (i) and (ii) is left to the reader.
(iii) Let \(f\) be a real function and let a real \(x\) be given. We shall prove that \(f\) is continuous at \(x\).
Let \(p\) be given. We have to find \(m\) such that, for every real \(y\), if \(|y-x| < \frac{1}{2^{m}}\), then \(|f(y)-f(x)|<\frac{1}{2^{p}}\).
Note: \(\forall \alpha \exists n[r'_{n} < f(u_{\alpha }) < r_{n}'']\) and find \(\alpha \) such that \(x=_{\mathcal{R}} u_{\alpha }\).
Applying \(\mathbf{BCP}\), find \(q, n\) such that \(\forall \beta [\overline{\alpha }q \sqsubset \beta \rightarrow r'_{n} < f(u_{\beta })<r_{n}'']\).
Find \(i,j\) such that \(u_{\alpha }(n-1) = (r_{i}', r_{i}'')\) and \(u_{\alpha }(n)= (r_{j}',r_{j}'')\).
Note: \(r_{i}'<_{\mathbb{Q}} r_{j}'<_{\mathbb{Q}} r_{j}''<_{\mathbb{Q}} r_{i}''\).
Find \(m\) such that \(\frac{1}{2^{m}}<\min _{\mathbb{Q}}(r_{j}'-_{\mathbb{Q}}r_{i}', r_{i}''-_{\mathbb{Q}}r_{j}'')\).
Note: for every real \(y\), if \(|y-x|<\frac{1}{2^{m}}\), then \(r_{i}'< y< r_{i}''\) and there exists \(\beta \) such that \(\overline{\alpha }n \sqsubset \beta \) and \(y=_{\mathcal{R}} u_{\beta }\) and, therefore: \(r_{n}'< f(u_{\beta })<r_{n}''\) and \(r_{n}' < f(y) < r_{n}''\).
Conclude: for every real \(y\), if \(|y-x|<\frac{1}{2^{m}}\) then \(|f(y)-f(x)| < r_{n}''-r_{n}' <\frac{1}{2^{p}}\). □
13 The Fan Theorem
13.1 Proving the Fan Theorem
The intuitionistic mathematician holds not only that every function from \([0,1]\) to ℛ, like every function from ℛ to ℛ, see Theorem 13(iii) is continuous at every point, but also that every function from \([0,1]\) to ℛ is uniformly continuous on \([0,1]\). In order to obtain this result, she first proves the Fan Theorem.
We need some definitions in order to formulate the Fan Theorem.
Definition 13
Let \(\mathcal{X}\subseteq \mathcal{N}\) and \(B\subseteq \mathbb{N}\).
\(B\) is a bar in \(\mathcal{X}\), notation: \(Bar_{\mathcal{X}}(B)\), if and only if: \(\forall \alpha \in \mathcal{X}\exists s \in B[s\sqsubset \alpha ]\).
\(\mathcal{C}:=2^{\omega }:=\{\alpha \mid \forall n[\alpha (n)<2]\}\).
\(\mathcal{C}\) is sometimes called Cantor space.
\(Bin:=2^{<\omega }:=\{s\mid \forall i<length(s)[s(i)<2]\}\).
For each \(n\), \(Bin_{n}:=\{s \in Bin\mid length(s)=n\}=\{s\in \omega ^{n}\mid \forall j< n[s(j)<2]\}\).
Definition 14
For each \(\mathcal{X}\subseteq \mathcal{N}\), for each \(s\), we define: \(\mathcal{X}\cap s:=\{\alpha \in \mathcal{X}|s \sqsubset \alpha \}\).
The Fan Theorem is the statement that every bar in \(\mathcal{C}\) has a finite subbar. Brouwer actually proved the more general but equivalent statement that every bar in a so-called fan has a finite subbar. Here, \(B\subseteq \mathbb{N}\) is called finite if and only if \(\exists u\forall s[s \in B\leftrightarrow \exists i< length(u)[s=u(i)]]\).
We avoid defining the notion of a fan. For understanding the name of the Theorem, it suffices to know every fan is a subset of \(\mathcal{N}\) and that \(\mathcal{C}\) is the prime example of a fan.
The proof of the Fan Theorem turns on a philosophical claim.
Theorem 14
Brouwer’s Fan Theorem
For every \(B\subseteq \mathbb{N}\), if \(Bar_{\mathcal{C}}(B)\), then there exists \(u\) such that \(\forall i < length(u)[u(i) \in B]\) and \(\forall \alpha \in \mathcal{C}\exists i< length(u)[ u(i)\sqsubset \alpha ]\).
Proof
Define, for every \(s\) in \(2^{<\omega }\), \(s\) is \(B\)-safe, or simply: safe, if and only if \(Bar_{\mathcal{C}\cap s}(B)\).
As \(Bar_{\mathcal{C}}(B)\), \(\langle \;\rangle \) is safe.
We now ask the probably somewhat surprising question: ‘How is it possible we know this?’ and, after some reflection, we come forward with the claim: there must be a canonical proof of the fact: ‘\(\langle \;\rangle \) is safe.’
What do we mean by: ‘a canonical proof’?
The canonical proof is an arrangement of statements of the form: ‘\(s\) is safe’. The conclusion of the canonical proof is the statement: ‘\(\langle \;\rangle \) is safe.’
The starting points of the canonical proof have the form:
\(s\in 2^{<\omega }\) and \(s \in B\).
Therefore: \(s\) is safe.
There are only two kinds of reasoning steps: forward reasoning steps and backward reasoning steps.
A forward reasoning step has the form:
\(s\in 2^{<\omega }\), and \(s\ast \langle 0 \rangle\) is safe, and \(s\ast \langle 1 \rangle\) is safe.
Therefore: \(s\) is safe.
A backward reasoning step either has the form:
\(s\in 2^{<\omega }\) and \(s\) is safe.
Therefore: \(s\ast \langle 0 \rangle\) is safe.
or it has the form
\(s\in 2^{<\omega }\) and \(s\) is safe.
Therefore: \(s\ast \langle 1 \rangle\) is safe.
Clearly, the canonical proof may be visualized as a finite tree, with the statement ‘\(\langle \;\rangle \) is safe’ at its bottom node and statements ‘\(s\in B\)’ at its top nodes. Each node that is not a top node has either one or two upstairs neighbours.
One easily sees that all reasoning steps are sound and that a canonical proof of ‘\(\langle \;\rangle \) is safe’ is indeed a proof of ‘\(\langle \;\rangle \) is safe’.
Our claim gives expression to the feeling that, if we know: ‘\(Bar_{\mathcal{C}}(B)\)’, this knowledge must be based upon an orderly organization of elementary pieces of information of the form: ‘\(s\in B\)’.
Now, trusting our claim, let us take a canonical proof of: ‘\(\langle \; \rangle \) is safe.’ We are going to use it in order to build another proof.
Define, for every \(s\) in \(2^{<\omega }\), \(s\) is supersafe if and only if there exists \(u\) such that \(\forall i<\mathit{length}(u)[u(i) \in B]\) and \(\forall \alpha \in \mathcal{C} \cap s\exists i< length(u) [ u(i) \sqsubset \alpha ]\).
Note that the conclusion we are after is: ‘\(\langle \;\rangle \) is supersafe.’
Replace, in the canonical proof of ‘\(\langle \;\rangle \) is safe’, every statement ‘\(s\) is safe’ by the statement ‘\(s\) is supersafe’.
The result will be another valid proof.
Why?
First, the new starting points are sound: if \(s\in 2^{<\omega }\) and \(s\in B\), define: \(u:=\langle s\rangle \) and note: \(u(0)\in B\) and \(\forall \alpha \in \mathcal{C}\cap s[ u(0)\sqsubset \alpha ]\).
Then, the new forward reasoning steps are sound.
For assume: \(s\in 2^{<\omega }\) and both \(s\ast \langle 0 \rangle \) and \(s\ast \langle 1 \rangle \) are supersafe.
Find \(u_{0}, u_{1}\) such that: for each \(j <2\), \(\forall i< \mathit{length}(u_{j})[u_{j}(i)\in B]\) and
\(\forall \alpha \in \mathcal{C}\cap s\ast \langle j\rangle \exists i< \mathit{length}(u_{j})[u_{j}(i)\sqsubset \alpha ]\).
Define \(u:=u_{0}\ast u_{1} \) and note
\(\forall i <\mathit{length}(u)[u(i) \in B]\) and \(\forall \alpha \in \mathcal{F}\cap s \exists i<\mathit{length}(u)[u(i) \sqsubset \alpha ]\),
that is: \(s\) is supersafe.
Also, the new backward reasoning steps are sound.
For assume: \(s\in 2^{<\omega }\) and \(s\) is supersafe.
Find \(u\) such that
\(\forall i <\mathit{length}(u)[u(i) \in B]\) and \(\forall \alpha \in \mathcal{C}\cap s \exists i<\mathit{length}(u)[u(i) \sqsubset \alpha ]\).
Note: for both \(j<2\), \(\mathcal{C} \cap s\ast \langle j\rangle \subseteq \mathcal{C}\cap s\) and \(s\ast \langle j \rangle \) is supersafe.
Conclude: our new proof is sound and its conclusion is true, i.e. \(\langle \;\rangle \) is supersafe. □
Generalizing the proof of Theorem 14 we obtain the following conclusion:
Theorem 15
Bar Induction in \(\mathcal{C}\)
Let \(B\subseteq \mathbb{N}\) be a bar in \(\mathcal{C}\).
(i)
Assume \(B\subseteq C\subseteq 2^{<\omega }\) and, for all \(s\) in \(2^{<\omega }\),
\(s\in C\) if and only if \(\forall j<2[s\ast \langle j\rangle \in C]\). Then \(\langle \;\rangle \in C\).
(ii)
Assume \(B\subseteq C\subseteq 2^{<\omega }\) and, for all \(s\) in \(2^{<\omega }\),
if \(\forall j<2[s\ast \langle j\rangle \in C]\), then \(s\in C\). Then \(\langle \;\rangle \in C\).
Proof
(i) Define, for each \(s\) in \(2^{<\omega }\), \(s\) is safe if and only if \(Bar_{\mathcal{C}\cap s}(B)\). In the canonical proof of: ‘\(\langle \;\rangle \) is safe’, replace every statement ‘\(s\) is safe’ by ‘\(s \in C\)’. The result will be a proof of: ‘\(\langle \;\rangle \in C\)’.
(ii) Define \(C^{\ast }:=\{s \in 2^{<\omega }[\exists t\sqsubseteq s[t\in C]\}\).
Note: for all \(s\) in \(2^{<\omega }\), if \(s\in C^{\ast }\), then \(\forall j<2[s\ast \langle j\rangle \in C^{\ast }]\).
Now assume: \(s\in 2^{<\omega }\) and \(\forall j<2[s\ast \langle j\rangle \in C^{\ast }]\). We may distinguish two cases.
Case 1. \(\forall j<2[ s\ast \langle j \rangle \in C]\). Then \(s \in C\subseteq C^{\ast }\).
Case 2. \(\exists t\sqsubseteq s[t\in C]\). Then \(s\in C^{\ast }\).
We thus see: for all \(s\) in \(2^{<\omega }\), \(s\in C^{\ast }\) if and only if \(\forall j<2[\sigma (s\ast \langle j\rangle \in C^{\ast }]\).
Applying (i), we conclude: \(\langle \;\rangle \in C^{\ast }\), and: \(\langle \;\rangle \in C\). □
13.2 Every Function from \([0,1]\) to ℛ Is Uniformly Continuous
Brouwer’s Continuity Principle implies that every function from \([0,1]\) to ℛ, like every function from ℛ to ℛ, see Theorem 13(iii), is continuous at every point. Using the Fan Theorem, we now prove that every function from \([0,1]\) to ℛ is even uniformly continuous on \([0,1]\). This is historically the first application of the Fan Theorem, see [12].
In the next Definition, we introduce a function \(\alpha \mapsto c_{\alpha }\) associating to every \(\alpha \) in \(\mathcal{C}\) a real number \(c_{\alpha }\) in \([0,1]\).
Definition 15
We define a mapping associating to every \(s\) in \(2^{<\omega }\) a pair \((a_{s}, b_{s})\) of rationals such that \((a_{\langle \;\rangle }, b_{\langle \;\rangle })=(0,1)\) and for each \(s\) in \(2^{<\omega }\),
\((a_{s\ast \langle 0\rangle }, b_{s\ast \langle 0\rangle }) =(a_{s}, \frac{1}{3}a_{s} + \frac{2}{3}b_{s})\) and \((a_{s\ast \langle 1\rangle }, b_{s\ast \langle 1\rangle }) =( \frac{2}{3}a_{s} + \frac{1}{3}b_{s}, b_{s})\).
For each \(\alpha \) in \(\mathcal{C}\) we let \(c_{\alpha }\) be the real \(x\) such that, for each \(n\), \(x(n)=(a_{\overline{\alpha }n}, b_{\overline{\alpha }n})\).
Theorem 16
Uniform-Continuity Theorem
Every function \(f\) from \([0,1]\) to ℛ is uniformly continuous on \([0,1]\), i.e.
$$ \forall p \in \mathbb{N}\exists m\in \mathbb{N}\forall x \in [0,1] \forall y\in [0,1][|x -y| < \frac{1}{2^{m}} \rightarrow |f(x) -f(y)| < \frac{1}{2^{p}}]. $$
Proof
Let \(f\) be a function from \([0,1]\) to ℛ and let \(p\) be given. We want to find \(m\) such that \(\forall x \in [0,1] \forall y\in [0,1][|x -y| < \frac{1}{2^{m}} \rightarrow |f(x) -f(y)| <\frac{1}{2^{p}}]\).
Let \(B\) be the set of all \(s\) in \(2^{<\omega }\) such that, for all \(x,y\) in \([a_{s}, b_{s}]\), \(|f(x)-f(y)|<\frac{1}{2^{p}}\).
We first prove that \(B\) is a bar in \(\mathcal{C}\), i.e. \(Bar_{\mathcal{C}}(B)\).
Let \(\alpha \) in \(\mathcal{C}\) be given. As \(f\) is continuous at \(c_{\alpha }\), see Theorem 13(iii), find \(m\) such that \(\forall y\in [0,1][|c_{\alpha }-y| < \frac{1}{2^{m}} \rightarrow |f(c_{\alpha }) -f(y)| <\frac{1}{2^{p+1}}]\). Find \(n\) such that \(b_{\overline{\alpha }n}-a_{\overline{\alpha }n}<\frac{1}{2^{m}}\) and note: \(\overline{\alpha }n \in B\).
We thus see that every \(\alpha \) in \(\mathcal{C}\) has an initial part in \(B\).
Now let \(C\) be the set of all \(s\) in \(2^{<\omega }\) such that, for some \(m\),
for all \(x,y\) in \([a_{s}, b_{s}]\), if \(|x-y|<\frac{1}{2^{m}}\), then \(|f(x)-f(y)|<\frac{1}{2^{p}}\).
Note: \(B\subseteq C\).
Let \(s\) in \(2^{<\omega }\) be given such that \(\forall i<2[s\ast \langle i \rangle \in C]\). We are going to prove: \(s\in C\).
First find \(m_{0}\) such that, for all \(x,y\) in \((a_{s\ast \langle 0\rangle }, b_{s\ast \langle 0\rangle }) =(a_{s}, \frac{1}{3}a_{s} + \frac{2}{3}b_{s})\), if \(|x-y|<\frac{1}{2^{m_{0}}}\), then \(|f(x)-f(y)|<\frac{1}{2^{p}}\). Then find \(m_{1}\) such that, for all \(x, y\) in \((a_{s\ast \langle 1\rangle }, b_{s\ast \langle 1\rangle }) =( \frac{2}{3}a_{s} + \frac{1}{3}b_{s}, b_{s})\), if \(|x-y|<\frac{1}{2^{m_{1}}}\), then \(|f(x)-f(y)|<\frac{1}{2^{p}}\).
Now find \(n:=length(s)\).
Note: \(b_{s}-a_{s}=(\frac{2}{3})^{n}\), and, for all \(x, y\) in \([a_{s}, b_{s}]\), if \(|x -y|<\frac{1}{3}(\frac{2}{3})^{n}\), then either \(x, y\) both are in \([a_{s}, \frac{1}{3}a_{s} + \frac{2}{3}b_{s}]\) or \(x, y\) both are in \([ \frac{2}{3}a_{s} + \frac{1}{3}b_{s}, b_{s}]\).
Find \(m\) such that \(m\ge m_{0}\) and \(m\ge m_{1}\) and \(\frac{1}{2^{m}} < \frac{1}{3}(\frac{2}{3})^{n}\) and note: for all \(x, y\) in \([a_{s}, b_{s}]\), if \(|x-y|<\frac{1}{2^{m}}\), then \(|f(x)-f(y)|<\frac{1}{2^{p}}\). We thus see: \(s\in C\).
Clearly, for all \(s\) in \(Bin\), if \(\forall i<2[s\ast \langle i \rangle \in C]\), then \(s\in C\).
Using Theorem 15(ii), conclude: \(\langle \;\rangle \in C\), that is:
\(\exists m \forall x \in [0,1]\forall y \in [0,1][ | x -y|< \frac{1}{2^{m}} \rightarrow |f(x) - f(y)| < \frac{1}{2^{n}}]\). □
13.3 The Failure of the Fan Theorem in Computable Analysis
In the next Theorem, we use some notations introduced in Sect. 8.4.
Theorem 17
Kleene’s Alternative21
There exists
\(B^{\ast }\subseteq \mathbb{N}\)
such that
(i)
Every computable \(\alpha \) in \(\mathcal{C}\) has an initial part in \(B\), i.e. \(\exists s\in B^{\ast }[s\sqsubset \alpha ]\).
(ii)
Every finite subset of
\(B\)
positively fails to be a bar in the set
\(\{\alpha \in \mathcal{C}\mid \alpha \; is\; computable\}\), i.e.
for all \(u,p\), if \(length(u)=p>0\) and \(\forall i< p[u(i)\in B^{\ast }]\),
then there exists a computable \(\alpha \) in \(\mathcal{C}\) such that \(\forall i< p[u(i)\perp \alpha ]\).
(iii)
\(B^{\ast }\) is an algorithmically decidable subset of ℕ.
Proof
First, let \(B\) be the set of all \(s\) in \(Bin\) such that, for some \(e\), \(length(s)=e+1\) and \(\forall i\le e\exists z[T(e,i,z) \;\wedge \;U(z) =s(i)]\).
\(\langle \;\rangle \notin B\) and, for every \(e\), there is at most one \(s\) in \(B\) such that \(length(s)=e+1\).
Let \(\alpha \) be a computable element of \(\mathcal{C}\). Find \(e\) such that \(\alpha = \varphi _{e}\).
Note: \(\overline{\alpha }(e+1)=\overline{\varphi _{e}}(e+1)\in B\).
Let \(u,p\) be given such that \(length(u)=p>0\) and \(\forall n< p [u(n) \in B]\).
We may assume: \(0< length\bigl (u(0)\bigr )< length\bigl (u(1)\bigr )<\cdots <length \bigl (u(p-1)\bigr )\) and, therefore, \(\forall n< p[\mathit{length}\bigl (u(n)\bigr ) >n]\). Define \(\alpha \) such that, for each \(n< p\), \(\alpha (n) = 1-\bigl (u(n)\bigr )(n)\), and, for each \(n\ge p\), \(\alpha (n) =0\). Note: \(\alpha \) is computable and \(\forall n< p[u(n)\perp \alpha ]\).
Unfortunately, \(B\) is not an algorithmically decidable subset of ℕ.
We therefore introduce another subset of ℕ.
Let \(B^{\ast }\) be the set of all \(s\) in \(Bin\) such that, for some \(e< \mathit{length}(s)\),
\(\forall i\le e\exists z<\mathit{length}(s)[T(e,i,z) \;\wedge \;U(j) =s(i)]\), and, therefore, \(\overline{s} (e+1) \in B\).
Note that \(B^{\ast }\) is an algorithmically decidable subset of ℕ.
Let \(\alpha \) be a computable element of \(\mathcal{C}\). Find \(e\) such that \(\alpha =\varphi _{e}\). Find \(n>e\) such that \(\forall i\le e\exists z< n[T(e,i,z) \;\wedge \;U(z) =s(i)]\) and conclude: \(\overline{\alpha }n \in B^{\ast }\).
We thus see that every computable \(\alpha \) in \(\mathcal{C}\) has an initial part in \(B^{\ast }\).
Let \(u,p\) be given such that \(length(u)=p>0\) and \(\forall n< p [u(n) \in B^{\ast }]\). Find \(v\) such that \(length(v)=p\) and \(\forall n< p[v(n)\sqsubseteq u(n)\;\wedge \; v(n)\in B]\). Find a computable \(\alpha \) in \(\mathcal{C}\) such that \(\forall n< p[v(n)\perp \alpha ]\) and conclude \(\forall n< p[u(n)\perp \alpha ]\).
We thus see that every finite subset of \(B^{\ast }\) positively fails to be a bar in
\(\{\alpha \in \mathcal{C}\mid \alpha \;is\;computable\}\). □
The subject of computable analysis starts from the assumption that every \(\alpha \) in \(\mathcal{N}\) is given by an algorithm, i.e., if one uses Church’s Thesis, by a Turing-algorithm. One may study this subject from an intuitionistic point of view. As appears from Theorem 17, computable analysis is dramatically different from intuitionistic analysis. For instance, there exists a real function from \([0,1]\) to ℛ that is everywhere continuous but positively unbounded. Many more such results may be found in [60].
14 The Determinacy Theorem as an Equivalent of the Fan Theorem
The Uniform-Continuity Theorem, Theorem 16, is the first application of the Fan Theorem, and may be called the goal for which it was devised. In this Section we want to introduce to the reader to a second and more recent application, an application in the theory of games.
In the first two Subsections we consider two kinds of two-move-games for Players \(I,II\) and define when such games are constructively determinate from the viewpoint of Player \(I\). Games from the first Subsection may fail to have this property but we will see that the Fan Theorem proves that the games from the second Subsection always have it. In the third Subsection we prove that, conversely, this result implies an important case of the Fan Theorem. In the fourth Subsection we introduce the intuitionistic Determinacy Theorem.
14.1 Games in \(2\times \omega \)
For every \(C\subseteq 2\times \omega \), we introduce a game \(\mathcal{G}_{2\times \omega }(C)\).
There are two players, Player \(I\) and Player \(II\). Every play goes a follows. Player \(I\) chooses \(i\) in \(\{0,1\}\), thereafter Player \(II\) chooses \(n\) in \(\omega \) and the play is finished. Player \(I\) wins the play if and only if \(\langle i, n\rangle \in C\). Player \(II\) tries to prevent that Player \(I\) wins the play.
Clearly, Player \(I\) has a winning first move if and only if \(\exists i\forall n[\langle i,n\rangle \in C]\). A strategy for Player \(II\), on the other hand, is a pair of numbers \(\langle p_{0}, p_{1}\rangle \), and the strategy is winning if \(\forall i<2[\langle i, p_{i}\rangle \notin C]\).
The game \(\mathcal{G}_{2\times \omega }(C)\) is called determinate if and only if either Player \(I\) has a winning first move or Player \(II\) has a winning strategy. As one may conjecture, it may happen that this decision can not be taken in a constructive way. We will see this in a moment.
We now define: the game \(\mathcal{G}_{2\times \omega }(C)\) is determinate from the viewpoint of Player \(I\) if and only if:
and ask ourselves the question: is the game \(\mathcal{G}_{\omega \times 2}(C)\) always determinate from the viewpoint of Player \(I\)?If Player \(II\) does not have a winning strategy in the constructively strong sense: \(\forall p_{0}\forall p_{1}[\langle 0, p_{0}\rangle \in C\;\vee \; \langle 1, p_{1}\rangle \in C]\), then Player \(I\) has a winning first move, i.e. \(\exists i<2\forall n[\langle i, n\rangle \in C]\)
The following example shows that, sometimes, it is not.
Define \(C:=\{\langle i, n\rangle \mid k_{99}\le n\rightarrow \exists l[k_{99}=2l+i] \}\).
Let \(p_{0}, p_{1}\) be given. If \(k_{99}\le p_{0}\), one may find \(i<2\) and \(l\) such that \(k_{99}=2l+i\) and \(\langle i, p_{i}\rangle \in C\). If \(p_{0}< k_{99}\), then \(\langle 0, p_{0}\rangle \in C\). We thus see Player \(I\) has an answer to any given strategy of Player \(II\).
On the other hand, if Player \(I\) has a winning first move, then \(\exists i<2\forall n[\langle i, n\rangle \in C]\) and \(\exists i<2[\exists j [j=k_{99}]\rightarrow \exists n[2n+i=k_{99}]]\), i.e. \(\neg \exists n[2n=k_{99}]\;\vee \;\neg \exists n[2n+1=k_{99}]\), a reckless or hardy statement.
Note that the statement: ‘the game \(\mathcal{G}_{2\times \omega }(C)\) is determinate’ is also reckless, as, for every \(C\subseteq 2\times \omega \), if \(\mathcal{G}_{2\times \omega }(C)\) is determinate, then \(\mathcal{G}_{2\times \omega }(C)\) is determinate from the viewpoint of Player \(II\).
14.2 Games in \(\omega \times 2\)22
For every \(C\subseteq \omega \times 2\), we introduce a game \(\mathcal{G}_{ \omega \times 2}(C)\).
There are again two players, Player \(I\) and Player \(II\). Every play goes a follows. Player \(I\) chooses \(n\) in \(\omega \), thereafter Player \(II\) chooses \(i\) in \(\{0,1\}\) and the play is finished. Player \(I\) wins the play if and only if \(\langle n,i\rangle \in C\). Player \(II\) tries to prevent that Player \(I\) wins the play. Clearly, Player \(I\) has a winning first move if and only if \(\exists n\forall i<2[\langle n,i\rangle \in C]\). A strategy for Player \(II\) is an element \(\tau \) of \(\mathcal{C}\) and the strategy \(\tau \) is winning if and only if \(\forall n[\langle n, \tau (n)\rangle \notin C]\).
The game \(\mathcal{G}_{\omega \times 2}(C)\) is called determinate if and only if either Player \(I\) has a winning first move or Player \(II\) has a winning strategy.
Considering the example \(C:=\{\langle n, i\rangle \in \omega \times 2\mid n=k_{99}]\), we see that it may happen that the statement: ‘\(\mathcal{G}_{\omega \times 2}(C)\) is determinate’ is a reckless one.
We now define: the game \(\mathcal{G}_{\omega \times 2}(C)\) is determinate from the viewpoint of Player \(I\) if and only if
If Player \(II\) does not have a winning strategy in the strong sense: \(\forall \tau \in \mathcal{C}\exists n[\langle n, \tau (n)\rangle \in C]\), then Player \(I\) has a winning first move, i.e. \(\exists n\forall i<2[\langle n, i\rangle \in C]\).
The Fan Theorem proves that, for every \(C\subseteq \omega \times 2\), the game \(\mathcal{G}_{\omega \times 2}(C)\) is determinate from the viewpoint of Player \(I\).
For assume \(\forall \tau \in \mathcal{C}\exists n[\langle n, \tau (n)\rangle \in C]\).
Define \(B:=\bigcup _{m}\{ t\in Bin_{m} \mid \exists n< m[\langle n, t(n) \rangle \in C]\}\) and note: \(B\) is a bar in \(\mathcal{C}\). Applying the Fan Theorem, find \(u\) such that \(\forall i< length(u)[u(i)\in B]\) and \(\forall \tau \in \mathcal{C}\exists i< length(u)[u(i)\sqsubset \tau ]\). Find \(m\) such that \(\forall i< m[length(u(i))< m]\) and conclude: \(\forall t \in Bin_{m}\exists n< m[\langle n, t(n)\rangle \in C]\).
We now prove, by backwards induction:
for each \(j\le m\), either \(\forall t \in Bin_{j} \exists n< j[\langle n , t(n)\rangle \in C]\) or \(\exists n\forall i<2[\langle n, i\rangle \in C]\).
This clearly holds if \(j=m\).
Now assume \(j+1\le m\) and \(\forall t \in Bin_{j+1} \exists n< j+1[\langle n, t(n)\rangle \in C]\). For every \(t\) in \(Bin_{j}\), one may consider \(t\ast \langle 0\rangle \) and conclude: \(\exists n< j[\langle n, t(n)\rangle \in C]\) or \(\langle j, 0\rangle \in C\). Therefore: either \(\langle j, 0\rangle \in C\) or \(\forall t \in Bin_{j}\exists n< j[\langle n, t(n)\rangle \in C]\). For similar reasons, either \(\langle j, 1\rangle \in C\) or \(\forall t \in Bin_{j}\exists n< j[\langle n, t(n)\rangle \in C]\). Conclude: either: \(\forall i<2[\langle j, i\rangle \in C]\) and \(\exists n\forall i<2[\langle n , i\rangle \in C]\) or: \(\forall t \in Bin_{j}\exists n< j[\langle n, t(n)\rangle \in C]\). Repeating this step \(m\) times we find the conclusion: \(\exists n\forall i<2[\langle n, i\rangle \in C]\).
14.3 Recovering the Fan Theorem
Let us consider the result of the last subsection:
We prove that this statement implies an important case of the Fan Theorem. The Fan Theorem is the statement that every \(B\subseteq \mathbb{N}\) that is a bar in \(\mathcal{C}\) has a finite subset that is a bar in \(\mathcal{C}\). We prove that \(\#\) implies this statement for the case that \(B\) is a decidable subset of ℕ.\((\#)\) For every \(C\subseteq \omega \times 2\),if \(\forall \tau \in \mathcal{C}\exists n[\langle n, \tau (n)\rangle \in C]\), then \(\exists n[\langle n, 0\rangle \in C\;\wedge \;\langle n, 1\rangle \in C]\).
Assume \((\#)\) and let \(B\subseteq \mathbb{N}\) be given such that \(Bar_{\mathcal{C}}(B)\) and one may decide, for each \(n\), \(n\in B\) or \(n\notin B\). For all \(n\), we define: \(B_{n}:=\{s\in B\mid s< n\}\).
We want to prove the statement \(QED:=\exists n[Bar_{\mathcal{C}}(B_{n})]\).23
We let \(C\) be the set of all pairs \(\langle s, i\rangle \) such that either: \(QED\) or: \(Bar_{\mathcal{C}\cap s\ast \langle i \rangle }(B_{n})\) and not \(Bar_{\mathcal{C}\cap s\ast \langle 1-i \rangle }(B_{n})\). Note that, for each \(s\) in \(Bin\), if both \(s\ast \langle 0\rangle \) and \(s\ast \langle 1\rangle \) are in \(C\), then \(QED\). Also note that \(C\), like \(B\), is a decidable subset of ℕ.
Let \(\tau \) in \(\mathcal{C}\) be given. Find \(\alpha \) in \(\mathcal{C}\) such that \(\forall i[\alpha (i)=\tau (\overline{\alpha }i)]\). Find \(n\) such that \(\overline{\alpha }n \in B\) and define \(m:=\overline{\alpha }n +1\). Note: \(Bar_{C\cap \overline{\alpha }n}(B_{m})\).
Note that, for each \(i\), if \(i+1\le n\) and \(Bar_{\mathcal{C}\cap \overline{\alpha }(i+1)}(B_{m})\), then either: \(Bar_{\mathcal{C}\cap \overline{\alpha }(i)}(B_{m})\) or: \(\neg Bar_{\mathcal{C}\cap \overline{\alpha }(i)\ast \langle 1-\alpha (i) \rangle }(B_{m})\) and \(\langle \overline{\alpha }i, \alpha (i)\rangle \in C\). Using backwards induction,
starting from the fact: \(Bar_{\mathcal{C}\cap \overline{\alpha }n}(B_{m})\), we prove:
for each \(i\le n\), either \(Bar_{\mathcal{C}\cap \overline{\alpha }i}(B_{m})\) or \(\exists j< n[\langle \overline{\alpha }j, \alpha (j)\rangle \in C]\).
Taking \(i=0\), we find: either \(Bar_{\mathcal{C}}(B_{m})\) or \(\exists j[\langle \overline{\alpha }j, \alpha (j)\rangle \in C]\), i.e. either \(QED\) or \(\exists j[\langle \overline{\alpha }j, \tau (\overline{\alpha }j) \rangle \in C]\). In both cases, one may conclude: \(\exists s[\langle s, \tau (s)\rangle \in C]\).
We thus see: \(\forall \tau \in \mathcal{C}\exists s[\langle s, \tau (s)\rangle \in C]\). Using \((\#)\), we conclude:
\(\exists s[s\ast \langle 0 \rangle \in C \;\wedge \;s\ast \langle 1 \rangle \in C]\), and, therefore: \(QED\), i.e. \(\exists n[Bar_{\mathcal{C}}(B_{n})]\).
This shows that every decidable subset \(B\) of ℕ that is a bar in \(\mathcal{C}\) has a finite subset that is a bar in \(\mathcal{C}\).
14.4 The Intuitionistic Determinacy Theorem
We now study games with infinitely many moves rather than two moves only.
Definition 16
\((\omega \times 2)^{\omega }:=\{\alpha \mid \forall n[\alpha (2n+1)<2] \}\).
For each \(\sigma \), for each \(\alpha \in (\omega \times 2)^{\omega }\), \(\alpha \in _{I}\sigma := \forall n[\alpha (2n)=\sigma \bigl ( \overline{\alpha }(2n)\bigr )]\).
For each \(\tau \) in \(\mathcal{C}\), for each \(\alpha \) in \((\omega \times 2)^{\omega }\), \(\alpha \in _{II}\tau := \forall n[\alpha (2n+1)=\tau \bigl ( \overline{\alpha }(2n+1)\bigr )]\).
For every \(\mathcal{X}\subseteq (\omega \times 2)^{\omega }\), we introduce a game \(\mathcal{G}_{(\omega \times 2)^{\omega }}(\mathcal{X})\). There are two players, Player \(I\) and Player \(II\). Every play takes infinitely many moves and goes as follows. Player \(I\) chooses \(n_{0}\) in \(\omega \), thereafter Player \(II\) chooses \(i_{0}\) in \(2=\{0,1\}\), then Player \(I\) chooses \(n_{1}\) in \(\omega \) and, thereafter, Player \(II\) chooses \(i_{1}\) in 2, and so on. Player \(I\) wins the play if the infinite sequence \(n_{0}, i_{0}, n_{1}, i_{1},\ldots \) is in \(\mathcal{X}\). Player \(II\) tries to prevent that Player \(I\) wins the game.
Theorem 18
Intuitionistic Determinacy Theorem
For all \(\mathcal{X}\subseteq (\omega \times 2)^{\omega }\), if \(\forall \tau \in \mathcal{C}\exists \alpha \in (\omega \times 2)^{\omega }[\alpha \in _{II} \tau \;\wedge \; \alpha \in \mathcal{X}]\), then \(\exists \sigma \forall \alpha \in (\omega \times 2)^{\omega }[\alpha \in _{I} \sigma \rightarrow \alpha \in \mathcal{X}]\).
The Theorem is good news for Player \(I\). Suppose \(\mathcal{X}\subseteq \mathcal{(}\omega \times 2)^{\omega }\) is such that Player \(I\) is able, once Player \(II\) has told her the strategy \(\tau \) she intends to follow, to find a play following \(\tau \) that is in \(\mathcal{X}\). She then may devise a strategy \(\sigma \), such that every play following \(\sigma \) is in \(\mathcal{X}\). Using \(\sigma \), Player \(I\) can do without information about the strategy followed by Player \(II\).
We will not give the proof of Theorem 18.24 As in Sect. 14.2, the Fan Theorem plays a key rôle in the argument. From Sect. 14.1, one may see it is crucial for Theorem 18 that, in \((\omega \times 2)^{\omega }\), Player \(II\) has, at each one of her moves, only 2 choices. The theorem extends to the case that Player \(II\) has, at each one of her moves, finitely many choices.
15 Brouwer’s Thesis
15.1 The Principle of Bar Induction
The key point in the proof of the next Theorem is a philosophical assumption25 one might call Brouwer’s Thesis (on bars in \(\mathcal{N}\)).26
Theorem 19
Bar Induction
Let \(B\subseteq \mathbb{N}\) be given such that \(Bar_{\mathcal{N}}(B)\). Let \(C\subseteq \mathbb{N}\) be given such that \(B\subseteq C\) and, for all \(s\), \(s\in C\) if and only if \(\forall n[s\ast \langle n \rangle \in C]\). Then \(\langle \;\rangle \in C\).
Proof
Let \(B\subseteq \mathbb{N}\) be given such that \(Bar_{\mathcal{N}}(B)\).
Define, for every \(s\), \(s\) is B-safe, or simply: safe, if and only if \(Bar_{\mathcal{N}\cap s}(B)\).
Note: \(\langle \;\rangle \) is safe.
There must exist a canonical proof of the fact:
$$ \langle \;\rangle\mbox{ is safe}. $$
The conclusion of the canonical proof is: ‘\(\langle \; \rangle \) is safe.’
The starting points of the canonical proof have the form:
\(s \in B\).
Therefore: \(s\) is safe.
There are two kinds of reasoning steps, forward steps and backward steps.
A forward reasoning step has infinitely many premises and is of the following form:
\(s\ast \langle 0 \rangle\) is safe, \(s\ast \langle 1 \rangle\) is safe, \(s\ast \langle 2 \rangle\) is safe, …
Therefore: \(s\) is safe.
A backward reasoning step has the form:
\(s\) is safe.
Therefore: \(s\ast \langle n \rangle\) is safe.
The canonical proof is not a finite tree but an infinite one. The canonical proof can not be written out explicitly as a finite text.
Let \(C\subseteq \mathbb{N}\) be given such that \(B\subseteq C\) and, for all \(s\), \(s\in C\) if and only if \(\forall n[s\ast \langle n \rangle \in C]\).
Now replace in the canonical proof every statement ‘\(s\) is safe’ by the statement ‘\(s\in C\)’. The result will be another valid proof.
Why?
As \(B\subseteq C\), the new starting points are sound.
As, for every \(s\), if \(\forall n[s\ast \langle n \rangle \in C]\), then \(s\in C\),27 the new forward reasoning steps are sound.
As, for every \(s\), for every \(n\), if \(s\in C\), then \(s\ast \langle n \rangle \in C\),28 the new backward reasoning steps are sound.
We must conclude: the new conclusion is true, that is: \(\langle \;\rangle \in C\). □
15.2 One Needs Backward Steps
Theorem 20
Kleene’s example29
There exist \(B\subseteq C\subseteq \mathbb{N}\) such that \(Bar_{\mathcal{N}}(B)\) and, for all \(s\), if \(\forall n[s\ast \langle n \rangle \in C]\), then \(s\in C\), while the statement ‘\(\langle \;\rangle \in C\)’ is a reckless one.
Proof
Let \(B\) consist of all \(s\) such that
either: \(\exists n< k_{99}[s = \langle n \rangle ]\) or: \(s = \langle \;\rangle \) and \(\exists n[n=k_{99}]\vee \forall n[n< k_{99}]\).
Let \(\alpha \) be given. Either \(\alpha (0) < k_{99}\) and \(\overline{\alpha }1 \in B\), or \(\alpha (0)\ge k_{99}\) and \(\langle \;\rangle =\overline{\alpha }0 \in B\). We thus see: \(Bar_{\mathcal{N}}(B)\).
Let \(C\) coincide with \(B\).
For all \(s\), if, for all \(n\), \(s\ast \langle n \rangle \in C\), then \(s=\langle \;\rangle \) and \(\forall n[n< k_{99}]\) and \(\langle \;\rangle \in C\).
The statement ‘\(\langle \;\rangle \in C\)’ is equivalent to ‘\(\exists n[n=k_{99}] \vee \forall n[n< k_{99}]\)’, and is reckless. □
Consider the set \(B\) mentioned in the proof of Theorem 20. Note that every canonical proof of ‘\(\langle \; \rangle \) is (B-)safe’ must use backward steps. The last step in a canonical proof of ‘\(\langle \;\rangle \) is (B-)safe’ must be a forward step: \(\langle \;\rangle \) is safe because: \(\langle 0\rangle \) is safe, \(\langle 1\rangle \) is safe, \(\langle 2\rangle \) is safe, …. For each \(n< k_{99}\) the conclusion: \(\langle n \rangle \) is safe follows by a basic step from: \(\langle n \rangle \in B\). For each \(n \ge k_{99}\) the conclusion: \(\langle n \rangle \) is safe follows by a backward step from: \(\langle \; \rangle \) is safe and that follows in its turn by a basic step from: \(\langle \;\rangle \in B\) (as \(n\ge k_{99}\)).
16 Open Induction in \([0,1]\)
Brouwer’s main application of the Principle of Bar Induction, Theorem 19, is the Fan Theorem. We now give an example of a stronger consequence of the Principle.
Definition 17
We let \((r_{0}', r_{0}''), \;(r_{1}', r_{1}''), \;(r_{2}', r_{2}''), \; \ldots \) be a fixed enumeration of all pairs of rationals.
For each \(\alpha \), \(\mathcal{G}_{\alpha }:=\{x \in \mathcal{R}|\exists n[r_{\alpha (n)}'< x< r_{ \alpha (n)}'']\}\).
For each \(a\), \(\mathcal{G}_{a}:=\{x\in \mathcal{R}\mid \exists n< length(a)[r'_{a(n)}< x< r''_{a(n)}] \}\).
\(\mathcal{G}\subseteq \mathcal{R}\) is open if and only if, for some \(\alpha \), \(\mathcal{G} = \mathcal{G}_{\alpha }\).
For all \(x,y\) in ℛ such that \(x< y\), we define \([x,y):=\{z\in \mathcal{R}\mid x\le _{\mathcal{R}} z<_{\mathcal{R}}y\}\).
\(\mathcal{G}\subseteq \mathcal{R}\) is progressive in \([0,1]\) if and only if \(\forall x \in [0,1][[0, x)\subseteq \mathcal{G} \rightarrow x \in \mathcal{G}]\).
Theorem 21
Principle of Open Induction in \({[}0,1{]}\)
For every open \(\mathcal{G}\subseteq \mathcal{R}\), if \(\mathcal{G}\) is progressive in \([0,1]\), then \([0,1]\subseteq \mathcal{G}\).
Although the theorem may be new to the reader, É. Borel in fact introduced and used it when he proved, in 1895, see [6], what is now called the Heine-Borel Theorem:
Borel’s argument may be described as follows. Let \(\alpha \) be given such that \([0,1]\subseteq \mathcal{G}_{\alpha }\). Define \(\mathcal{H}:=\{y\in \mathcal{R}\mid \exists n[[0,y]\subseteq \mathcal{G}_{\overline{\alpha }n}]\}\). Note that ℋ is open and progressive in \([0,1]\). Applying the principle of Open Induction on \([0,1]\), conclude: \(1 \in \mathcal{H}\) and \(\exists n[[0,1]\subseteq \mathcal{G}_{\overline{\alpha }n}]\).for each \(\alpha \), if \([0,1]\subseteq \mathcal{G}_{\alpha }\), then \(\exists n[[0,1]\subseteq \mathcal{G}_{\overline{\alpha }n}]\).
How does the classical mathematician convince herself of the validity of the Principle of Open Induction in \([0,1]\)?
Given an open \(\mathcal{G}\subseteq \mathcal{R}\) that is progressive in \([0,1]\), she starts defining an infinite sequence \(x_{0}, x_{1}, \ldots \) of reals. She defines \(x_{0}:=0\) and notes \(x_{0}\in \mathcal{G}\). She then finds \(x_{1}>x_{0}\) such that \([0,x_{1})\subseteq \mathcal{G}\). If \(x_{1}\ge 1\), she is done and defines, for each \(n\ge 1\), \(x_{n}=1\). If not, she observes: \(x_{1} \in \mathcal{G}\) and finds \(x_{2}>x_{1}\) such that \([0,x_{2})\subseteq \mathcal{G}\). If \(x_{2} \ge 1\) she is done and defines, for each \(n\ge 2\), \(x_{n}=1\). If not, she observes: \(x_{2} \in \mathcal{G}\) and finds \(x_{3}>x_{2}\) such that \([0,x_{3})\subseteq \mathcal{G}\). And so on. She thus finds an infinite sequence \(0\le x_{0} \le x_{1} \le x_{2}\le \ldots \) of reals such that, for each \(n\), \([0, x_{n})\subseteq \mathcal{G}\) and: \(x_{n+1}=x_{n}\) if and only if \(x_{n}=1\). The infinite non-decreasing sequence \(x_{0}, x_{1}, \ldots \) is bounded by 1 and thus converges, to, say, \(x_{\omega +0}=x_{\omega }\). Then: \(x_{\omega }\in \mathcal{G}\) as \([x,x_{\omega })\subseteq \mathcal{G}\). If \(x_{\omega }\ge 1\), she is done and defines, for each \(n\ge 0\), \(x_{\omega +n}=1\). If not, she starts again and finds suitable \(x_{\omega +1}, x_{\omega +2}, \ldots \) such that, for each \(n\), \([0, x_{\omega +n})\subseteq \mathcal{G}\) and \(x_{\omega +n}\le x_{\omega +n+1}\) and: \(x_{\omega +n+1}=x_{\omega +n}\) if and only if \(x_{\omega +n}\ge 1\). She then considers \(x_{\omega \cdot 2}= x_{\omega +\omega }:=\lim _{n} x_{\omega +n}\). She has inexhaustible energy and, if needed, finds \(x_{\omega \cdot 3}\) \(x_{\omega \cdot 4}, \ldots x_{\omega \cdot \omega }, \ldots \). She thus continues her infinite sequence through the countable ordinals.
She believes this procedure will come to an end, that is: there must exist a countable ordinal \(\beta \) such that \(x_{\beta }=1\). She argues a follows. For each \(k>0\) there can be only \(k\) countable ordinals \(\alpha \) such that \(x_{\alpha }+\frac{1}{k}< x_{\alpha +1}\). Therefore, there are only countably many countable ordinals such that \(x_{\alpha }< x_{\alpha +1}\). Find a countable ordinal \(\beta \) that lies beyond every countable ordinal \(\alpha \) such that \(x_{\alpha }< x_{\alpha +1}\). Then \(x_{\beta }=x_{\beta +1}\) and: \(x_{\beta }=1\).
Borel argued in this way, proudly using the countable ordinals introduced by Cantor some 20 years earlier, see [34].
This argument, from a constructive point of view, is quite fantastic. We parted company with the classical mathematician already at the point where she believed to find \(x_{\omega }\). It is not true, constructively, that every non-decreasing bounded infinite sequence of reals has a limit: consider the sequence defined by: \(x_{n}=0\) if \(n< k_{99}\) and \(x_{n}=1\) if \(k_{99}\le n\). 30
The classical mathematician may propose a second line of thought. She might use a classical mathematician’s finest weapon,31 as follows. Assume \(\mathcal{G}\neq [0,1]\). Consider \(y:=\inf ([0,1]\setminus \mathcal{G})\). As \(\mathcal{G}\) is open, \(y\notin \mathcal{G}\), but also \([0,y)\subseteq \mathcal{G}\). Contradiction.
Again, we can not partake in her joy. It is not clear that we may construct \(y\). And, of course, it is not clear that, having proved: \(\neg \exists x\in [0,1][x\notin \mathcal{G}]\), we might conclude: \(\forall x\in [0,1][x\in \mathcal{G}]\).
In order to make the problem more pictorial, let us define: Achilles32arrives at \(x\) if and only if \([0,x)\subseteq \mathcal{G}\).
How might we, constructive mathematicians, convince ourselves that Achilles arrives at 1? We should first prove that Achilles will arrive at \(\frac{1}{2}\), but it does not seem easier to prove that Achilles will arrive at \(\frac{1}{2}\) than to prove that he will arrive at 1.
Proof
33Let \(\mathcal{G}\subseteq \mathcal{R}\) be open and progressive in \([0,1]\). Find \(\alpha \) such that \(\mathcal{G} = \mathcal{G}_{\alpha }\). We define a mapping \(s\mapsto (c_{s}, d_{s})\) that associates to every \(s\) in ℕ a pair of rationals. The elements \(s\) of ℕ are thought of as coding finite sequences of natural numbers, see Sect. 12.1, Definition 10. Note: for each \(s\), \((c_{s\ast \langle 0\rangle } , d_{s\ast \langle 0\rangle })=(c_{s}, \frac{c_{s}+d_{s}}{2})\).
(i)
\((c_{\langle \;\rangle }, d_{\langle \;\rangle }):=(0,1)\).
(ii)
For each \(s\), for each \(n\), find out if \(\forall x \in [0, \frac{c(s)+ d(s)}{2}]\exists i < n [r'_{\alpha (i)}<x < r''_{\alpha (i)}]\).34
If so, define \((c_{s\ast \langle n\rangle } , d_{s\ast \langle n\rangle })=( \frac{c_{s}+d_{s}}{2}, d_{s})\), and
if not, define \((c_{s\ast \langle n\rangle } , d_{s\ast \langle n\rangle })=( c_{s}, \frac{c_{s}+d_{s}}{2})\).
Also note: for each \(s\), \(\exists n\forall x \in [0,c_{s}) \exists i< n[r'_{\alpha (i)}< x< r''_{ \alpha (i)}]\).
One proves this by induction on the length of \(s\).
For each \(\beta \) in \(\mathcal{N}\), we let \(x_{\beta }\) be the real number such that, for each \(n\),
\(x_{\beta }(n)=(c_{\overline{\beta }n}, d_{\overline{\beta }n})\). Note: for each \(\beta \), \([0, x_{\beta })\subseteq \mathcal{G}\) and thus \(x_{\beta }\in \mathcal{G}\).
Let \(B\) be the set of all \(s\) such that \(\exists n\forall x\in [0, d_{s}]\exists i< n[r'_{\alpha (i)}<x<r''_{ \alpha (i)}]\).
Let \(\beta \) be given. Using the fact: \(x_{\beta }\in \mathcal{G}\), find \(q\) such that \(r'_{\alpha (q)}< x_{\beta }< r''_{\alpha (q)}\).
Find \(m\) such that \(r'_{\alpha (q)}< c_{\overline{\beta }m}< d_{\overline{\beta }m}< r''_{ \alpha (q)}\).
Find \(p\) such that \(\forall x \in [0, c_{\overline{\beta }m}]\exists i< p[r'_{\alpha (i)}< x< r''_{ \alpha (i)}]\).
Define \(n:=\max (p, q+1)\).
Conclude: \(\forall x \in [0, d_{\overline{\beta }m}]\exists i< p][r'_{\alpha (i)} < x<r''_{\alpha (i)}]]\) and: \(\overline{\beta }m \in B\).
We thus see: \(Bar_{\mathcal{N}}(B)\), i.e.: B is a bar in \(\mathcal{N}\).
Note: \(B\) is monotone, i.e.: for all \(s\), if \(s\in B\), then \(\forall n[s\ast \langle n \rangle \in B]\).
We now prove that \(B\) is also inductive.
Let \(s\) be given such that \(\forall n[s\ast \langle n \rangle \in B]\). Then, in particular: \(s\ast \langle 0\rangle \in B\).
Note \(d_{s\ast \langle 0 \rangle }=\frac{c_{s}+d_{s}}{2}\) and find \(n\) such that \(\forall x \in [0, \frac{c_{s}+d_{s}}{2}]\exists i< n[r'_{\alpha (i)}< x< r''_{ \alpha (i)}]\).
Conclude: \((c_{s\ast \langle n \rangle }, d_{s\ast \langle n \rangle })= ( \frac{c_{s}+d_{s}}{2}, d_{s})\). Using the fact: \(s\ast \langle n \rangle \in B\), find \(m\) such that \(\forall x \in [0, d_{s\ast \langle n\rangle }]\exists i< m[r'_{\alpha (i)}< x< r''_{ \alpha (i)}]\).
Note: \(d_{s\ast \langle n \rangle }= d_{s}\) and conclude: \(s \in B\).
We thus see: if \(\forall n[s\ast \langle n \rangle \in B]\), then \(s\in B\).
As \(Bar_{\mathcal{N}}(B)\) and \(\forall s[s\in B\leftrightarrow \forall n[s\ast \langle n \rangle \in B]]\), we may conclude, using Theorem 19: \(\langle \;\rangle \in B\), that is: \(\exists n \forall x\in [0,1]\exists i< n[r'_{\alpha (i)}< x < r''_{ \alpha (i)}]\) and: \([0,1]\subseteq \mathcal{G}\). □
The Principle of Open Induction in \([0,1]\) plays a large rôle in [62].
17 Brouwer’s Thesis, Again
17.1 Using Stumps
In intuitionistic analysis, stumps play the rôle fulfilled by countable ordinals in classical analysis.
Definition 18
For every \(s\) in ℕ, for every \(A\subseteq \mathbb{N}\), \(s\ast A := \{s\ast t \mid t \in A\}\).
\(\mathbf{Stp}\), a collection of subsets of ℕ, called stumps, is defined as follows.
(i)
\(\emptyset \in \mathbf{Stp}\), and
(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 \mathbb{N}} \langle n \rangle \ast S_{n}\) is again an element of \(\mathbf{Stp}\), and
(iii)
nothing more: every element of \(\mathbf{Stp}\) is obtained by starting from \(\emptyset \) and applying the operation mentioned in (ii) repeatedly.
Note that, for every stump \(S\), either \(S = \emptyset \) or \(\langle \;\rangle \in S\).
Definition 19
For every \(A\subseteq \mathbb{N}\), for every \(n\), \(A\upharpoonright \langle n \rangle := \{s\mid \langle n \rangle \ast s\in A\}\).
For every non-empty stump \(S\), for every \(n\), \(S\upharpoonright \langle n\rangle \) is again a stump.
\(S\upharpoonright \langle n\rangle \) is called the \(n\)-th immediate substump of \(S\).
Axiom 2
Principle of Induction on \(\mathbf{Stp}\)
Let \(P\subseteq \mathbf{Stp}\) be given. If one may conclude: \(\mathbf{Stp}= P\).
(i)
\(\emptyset \in P\), and,
(ii)
for every non-empty stump \(S\), if \(\forall n[S\upharpoonright \langle n\rangle \in P]\), then \(S \in P\),
Theorem 22
Brouwer’s Thesis on bars in \(\mathcal{N}\)35
For every \(B\subseteq \mathbb{N}\) such that \(Bar_{\mathcal{N}}(B)\), there exists a stump \(S\) such that \(Bar_{\mathcal{N}}(S \cap B)\).
Proof
Let \(B\subseteq \mathbb{N}\) be given such that \(Bar_{\mathcal{N}}(B)\).
Let \(C\) be the set of all \(s\) such that, for some stump \(S\),
\(\forall \alpha \exists n[ \overline{\alpha }n \in S\;\wedge \; \exists t\sqsubseteq s\ast \overline{\alpha }n[t\in B]]\).
Let \(s\) be given such that \(s\in B\). Define \(S:=\{\langle \;\rangle \}\) and note:
\(\forall \alpha [ \overline{\alpha }0 \in S \;\wedge \; s\ast \overline{\alpha }0 \in B]\).
We thus see: \(B\subseteq C\).
We now prove that \(C\) is inductive.
Let \(s\) be given such that \(\forall m[s\ast \langle m \rangle \in C]\).
Find an infinite sequence \(S_{0}, S_{1}, \ldots \) of stumps such that
\(\forall m \forall \alpha \exists n[ \overline{\alpha }n \in S_{m} \; \wedge \; \exists t\sqsubseteq s\ast \langle m \rangle \ast \overline{\alpha }n[t \in B]]\). Define a non-empty stump \(S\) such that, for each \(m\), \(S\upharpoonright \langle m\rangle =S_{m}\) and conclude: \(\forall \alpha \exists n[ \overline{\alpha }n \in S \;\wedge \; \exists t\sqsubseteq s\ast \overline{\alpha }n[t \in B]\) and: \(s\in C\).
We thus see: for each \(s\), if \(\forall m[s\ast \langle m \rangle \in C]\), then \(s\in C\).
Finally, we show that \(C\) is monotone.
Let \(s\) in \(C\) be given.
Find a stump \(S\) such that \(\forall \alpha \exists n[ \overline{\alpha }n \in S \;\wedge \; \exists t\sqsubseteq s\ast \overline{\alpha }n[t\in B]]\).
Let \(m\) be given and distinguish two cases:
Case (1). \(S\upharpoonright \langle m\rangle \neq \emptyset \). Then \(\forall \alpha \exists n[ \overline{\alpha }n \in S\upharpoonright \langle m\rangle \;\wedge \; \exists t\sqsubseteq s\ast \langle m \rangle \ast \overline{\alpha }n [t\in B]]\), and: \(s\ast \langle m\rangle \in C\).
Case (2). \(S\upharpoonright \langle m\rangle = \emptyset \). Define \(T := \{\langle \;\rangle \}\) and note:
\(\forall \alpha [ \overline{\alpha }0 \in T \;\wedge \; \exists t \sqsubseteq s\ast \langle m \rangle \ast \overline{\alpha }0[t\in B]]\), and: \(s\ast \langle m \rangle \in C\).
We thus see: for all \(s\), for all \(m\), if \(s\in C\), then \(s\ast \langle m \rangle \in C\).
Using Theorem 19, we conclude: \(\langle \;\rangle \in C\), that is: there exists a stump \(S\) such that \(\forall \alpha \exists n[ \overline{\alpha }n \in S \;\wedge \; \overline{\alpha }n \in B]\), that is: \(Bar_{\mathcal{N}}(S\cap B)\). □
18 Ramseyan Theorems
18.1 Dickson’s Lemma
Definition 20
For all \(\alpha , \beta \) in \(\mathcal{N}\), \(\alpha \circ \beta \) is the element of \(\mathcal{N}\) such that, for each \(n\), \(\alpha \circ \beta (n) = \alpha \bigl (\beta (n)\bigr )\).
\([\omega ]^{\omega }:=\{\zeta \in \mathcal{N}\mid \forall i[\zeta (i) < \zeta (i+1)]\}\).
The following Lemma, a humble member of a family of results called Ramseyan Theorems, plays a rôle in Computer Algebra. The Lemma lies at the basis of Buchberger’s algorithm.36 The Lemma is due to L.E. Dickson, see [24].
Theorem 23
Dickson’s Lemma
For all \(p>0\), for all \(\alpha _{0}, \alpha _{1}, \ldots \alpha _{p-1}\) in \(\mathcal{N}\), there exist \(i,j\) such that \(i< j\) and \(\forall k< p[\alpha _{k}(i)\le \alpha _{k}(j)]\).
We first sketch a proof along traditional lines that fails to be constructive.
The proof is by induction to \(p\).
First consider the case \(p=1\). Let \(\alpha _{0}\) be given and consider \(\alpha _{0}(0)\). Note: \(\exists i\le \alpha _{0}(0)[\alpha _{0}(i)\le \alpha _{0}(i+1)]\).
Now let \(p\) be given such that the case \(p\) of the Theorem has been established. We want to prove the case \(p+1\).
Let \(\alpha _{0}, \alpha _{1}, \ldots , \alpha _{p}\) be given.
\((\flat )\) Find \(\zeta \) in \([\omega ]^{\omega }\) such that \(\forall i[\alpha _{p}\circ \zeta (i)\le \alpha _{p}\circ \zeta (i+1)]\).
Applying the induction hypothesis, determine \(i,j\) such that, for all \(k< p\),
\(\alpha \circ \zeta (i)\le \alpha \circ \zeta (j)\) and conclude: for all \(k\le p+1\), \(\alpha \circ \zeta (i)\le \alpha \circ \zeta (j)\).
This completes the proof of the induction step.
Unfortunately, there are difficulties with \((\flat )\). It is, in general, not possible to find \(\zeta \) in \([\omega ]^{\omega }\) such that \(\forall i[\alpha _{p}\circ \zeta (i)\le \alpha _{p}\circ \zeta (i+1)]\). The following example makes this clear.
Define \(\alpha \) such that, for all \(n\), if \(n< k_{99}\), then \(\alpha (n)=1\), and, if \(k_{99}\le n\), then \(\alpha (n)=0\). Suppose we find \(\zeta \) in \([\omega ]^{\omega }\) such that \(\forall i[\alpha \circ \zeta (i)\le \alpha \circ \zeta (i+1)]\).
If \(\alpha \circ \zeta (0) =0\), then \(k_{99}\le \zeta (0)\), and, if \(\alpha \circ \zeta (0)=1\), then \(\forall n[n< k_{99}]\).
The statement ‘\(\exists \zeta \in [\omega ]^{\omega }\forall i[\alpha \circ \zeta (i)\le \alpha \circ \zeta (i+1)]\)’ thus is reckless or hardy.
We now give a constructive proof of Dickson’s Lemma.
Proof
37 The proof is by induction on \(p\). The case \(p=1\) is easy and is done as in the sketch preceding this proof. Now let \(p\) given such that the case \(p\) has been established. We prove the case \(p+1\).
Let \(\alpha _{0}, \alpha _{1}, \ldots , \alpha _{p}\) be given.
Define38\(QED:=\exists i \exists j[i< j\;\wedge \;\forall k\le p[\alpha _{k}(i) \le \alpha _{k}(j)]\).
We first prove:
This again is done by induction. Note that the case \(m=0\) is trivial.\((\ast )\) for each \(m\), \(\forall n\exists j\ge n[m\le \alpha _{p}(j)\;\vee \;QED]\).
Now assume \(m\) is given and the case \(m\) has been established.
We prove the case \(m+1\).
Let \(n\) be given.
Using the induction hypothesis, find \(\zeta \) in \([\omega ]^{\omega }\) such that \(\forall i[\alpha _{p}\circ \zeta (i)\ge m \;\vee \;QED]\).
Find \(i,j\) such that \(n< i< j\) and \(\forall k< p[\alpha _{k}\circ \zeta (i)\le \alpha _{k}\circ \zeta (j)]\).
Note: either: \(m+1\le \alpha _{p}\circ \zeta (i)\) or: \(m+1\le \alpha _{p}\circ \zeta (j)\) or: \(\alpha_{p}\circ\zeta(i)=\alpha_{p}\circ\zeta(j)=m \) and \(QED\).
We thus see: \(\forall n\exists j\ge n[m+1\le \alpha _{p}(j)\;\vee \;QED]\). This completes the proof of \((\ast )\).
Using \((\ast )\) we find \(\zeta \) in \([\omega ]^{\omega }\) such that \(\forall n[\alpha _{p}\circ \zeta (n)\le \alpha _{p}\circ \zeta (n+1) \;\vee \;QED]\).
Find \(i,j\) such that \(i< j\) and \(\forall k< p[\alpha _{k}\circ \zeta (i)\le \alpha _{k}\circ \zeta (j)]\).
Note: \(\alpha _{p}\circ \zeta (i)\le \alpha _{p}\circ \zeta (j)\;\vee \;QED\) and conclude: \(QED\).
This concludes the proof of the case \(p+1\).
The theorem thus is proven by induction. □
18.2 How to Formulate and Extend Ramsey’s Theorem?
Definition 21
For all \(\alpha \), for all \(n\), for all \(s\) in \(\omega ^{n}\), \(\alpha \circ s\) is the element of \(\omega ^{n}\) such that, for each \(i< n\), \(\alpha \circ s (i) = \alpha \bigl (s(i)\bigr )\).
For all \(m\), for all \(s\) in \(\omega ^{m}\), for all \(n\), for all \(t\) in \(\omega ^{n}\) such that \(\forall i< n[ t(i)< m]\), \(s\circ t\) is the element of \(\omega ^{n}\) such that for each \(i< n\), \(s\circ t(i) = s\bigl (t(i)\bigr )\).
\([\omega ]^{n}:=\{s\in \omega ^{n}\mid \forall i[i+1< n\rightarrow s(i)< s(i+1)] \}\).
\([\omega ]^{<\omega } :=\bigcup _{n}[\omega ]^{n}\).
Definition 22
\(A\subseteq \mathbb{N}\) is almost-full if and only if \(\forall \zeta \in [\omega ]^{\omega }\exists s\in [\omega ]^{<\omega }[ \zeta \circ s\in A]\).
Let \(k>0\) be given. The \(k\)-dimensional case of Ramsey’s Theorem is the following statement:
\(\mathbf{IRT}(k)\): For all \(A,B\subseteq [\omega ]^{k}\),if \(A,B\) are almost-full, then \(A\cap B\) is almost-full.
As, for all \(A\subseteq [\omega ]^{k}\), \(A\cap ([\omega ]^{k} \setminus A)=\emptyset \) is not almost-full, the classical mathematician draws the following conclusion from \(\mathbf{IRT}(k)\):
i.e.\(\mathbf{IRT}(k)_{class}\): For all \(A\subseteq [\omega ]^{k}\),either \(A\) is not almost-full or \([\omega ]^{k}\setminus A\) is not almost-full,
either \(\exists \zeta \in [\omega ]^{\omega }\forall s\in [\omega ]^{k}[\zeta \circ s\in A]\) or \(\exists \zeta \in [\omega ]^{\omega }\forall s\in [\omega ]^{k}[\zeta \circ s\notin A]\).
This is the formulation of the theorem that will be familiar to the classical reader. She also will be able to conclude (her reading of) \(\mathbf{IRT}(k)\) from \(\mathbf{IRT}(k)_{class}\).40
F.P. Ramsey proved: \(\forall k>0[\mathbf{IRT}(k)_{class}]\), see [46].
There is an extension of Ramsey’s result into the transfinite that is called the Clopen Ramsey Theorem.
We need the following definition.
Definition 23
For every stump \(U\), we define \(\overline{U}:=\{s\mid s \notin U \;\wedge \;\forall t\sqsubset s[t \in U]\}\). The set \(\overline{U}\) is called the border of the stump \(U\).
Let a stump \(U\) be given. We introduce the following statement:
\(\mathbf{IRT}(\overline{U})\): For all \(A,B\subseteq \overline{U} \),if \(A,B\) are almost-full, then \(A\cap B\) is almost-full.
for every stump
\(U\)
,
\(\mathbf{IRT}(\overline{U})\)
.
The Infinite Ramsey Theorem,42\(\mathbf{IRT}\), is the statement: for all \(k\), \(\mathbf{IRT}(k)\).
\(\mathbf{IRT}_{class}\) is the (constructively wrong) statement: for all \(k\), \(\mathbf{IRT}(k)_{class}\).
18.3 The Proof of the Clopen Ramsey Theorem43
Definition 24
For each \(n\), for each \(k\), \([n]^{k}:=\{s\in [\omega ]^{k}\mid \forall i< k[s(i)< n]\}\).
For each \(n\), for each \(k\), \([n]^{< k}:=\bigcup _{i< k}[n]^{i}\).
Let a stump \(S\) be given. For every \(A\subseteq \mathbb{N}\), \(S\) secures \(A\) if and only if
\(\exists m\forall \zeta \in [\omega ]^{\omega }[\zeta (0)>m\rightarrow \exists n\exists s \in [n]^{< n+1}[\overline{\zeta }n \in S\;\wedge \; \overline{\zeta }n\circ s \in A]]\).
Corollary 24
For each \(A\subseteq \mathbb{N}\), if \(A\) is almost-full, then there exists a stump \(S\) securing \(A\).
Proof
Let \(A\subseteq \mathbb{N}\) be almost-full.
Define \(B:=\bigcup _{n}\{u \in \omega ^{n}\mid u \notin [\omega ]^{n} \; \vee \; \exists s\in [n]^{< n+1}[u\circ s \in A]\}\).
We prove that \(B\) is a bar in \(\mathcal{N}\).
Let \(\alpha \) be given. Define \(\zeta \) such that \(\zeta (0)=\alpha (0)\) and, for each \(n>0\),
if \(\overline{\alpha }(n+1)\in [\omega ]^{n+1}\), then \(\zeta (n)=\alpha (n)\), and, if not, then \(\zeta (n)=\zeta (n-1)+1\).
Note: \(\zeta \in [\omega ]^{\omega }\).
Find \(n\) such that \(\exists s\in [n]^{< n+1}[\overline{\zeta }n \circ s \in A]\), and, therefore, \(\overline{\zeta }n \in B\).
Note: if \(\overline{\alpha }n \neq \overline{\zeta }n\), then \(\overline{\alpha }n \notin [\omega ]^{n}\), and also: \(\overline{\alpha }n \in B\).
In any case, therefore, \(\overline{\alpha }n \in B\).
We thus see: \(Bar_{\mathcal{N}}(B)\).
Note: \(S\) secures \(A\). □
Definition 25
Let a stump \(U\) be given and assume \(A\subseteq \overline{U}\) and \(u\in U\cup \overline{U}\).
\(u\;\;U\)-secures \(A\) if and only if either: \(u\in A\) or: \(u\in U\) and \(\forall t\in \overline{U}[u\sqsubset t\rightarrow t\in A]\).
Let also a stump \(S\) be given. \(S\;\;U\)-secures \(A\) if and only if
\(\exists m\forall \zeta \in [\omega ]^{\omega }[\zeta (0)>m\rightarrow \exists n[\overline{\zeta }n \in S\;\wedge \;\exists s \in [n]^{< n+1} [ \overline{\zeta }n\circ s\;\; U\)-secures \(A]]\).
Corollary 25
For all stumps \(U\), for each \(A\subseteq \overline{U}\), if \(A\) is almost-full, then there exists a stump \(S\) \(U\)-securing \(A\).
Proof
Theorem 26
Intuitionistic Ramsey Theorem
(i)
\(\mathbf{CRT}\): For all stumps \(U\), for all \(A,B\subseteq \overline{U}\),
if \(A,B\) are both almost-full, then \(A\cap B\) is almost-full.
(ii)
\(\mathbf{IRT}\): For all \(k\), for all \(A,B\subseteq [\omega ]^{k}\),
if \(A,B\) are both almost-full, then \(A\cap B\) is almost-full.
Proof
for all stumps \(U\), \(P(U)\),
where \(P(U)\) is the statement: for all stumps \(S\), \(Q(U,S)\),
where \(Q(U,S)\) is the statement: for all stumps \(T\), \(R(U,S,T)\),
where \(R( U,S,T)\) is the statement:
for all \(A,B\subseteq \overline{U}\), if \(S\) \(U\)-secures \(A\), and \(T\) \(U\)-secures \(B\), then \(A\cap B\) is almost-full.
We use Axiom 2 from Sect. 17.1, the principle of induction on the set \(\mathbf{Stp}\) of stumps. Our proof is a proof by triple induction.
1. Note: \(\overline{\emptyset }=\{\langle \; \rangle \}\).
For all \(A,B\subseteq \{\langle \;\rangle \}\), if \(A,B\) are almost-full, then \(A=B=A\cap B=\{\langle \;\rangle \}\).
We thus see that \(P(\emptyset )\) is true.
2. Let a non-empty stump \(U\) be given such that, for all \(n\), \(P(U\upharpoonright \langle n\rangle )\).
We intend to prove \(P(U)\), that is: for all stumps \(S\), \(Q(U, S)\).
We use again use Axiom 2.
2.1. Note that \(Q(U, \emptyset )\) holds a trivial reason: no subset of ℕ is secured by \(\emptyset \).
2.2. Let a non-empty stump \(S\) be given such that, for all \(n\), \(Q(U,S\upharpoonright \langle n \rangle )\).
We intend to prove: \(Q(U, S)\), that is, for all stumps \(T\), \(R(U, S,T)\).
Again, we use Axiom 2.
2.2.1. Note that \(R(U, S, \emptyset )\) holds for a trivial reason: no subset of ℕ is secured by \(\emptyset \).
2.2.2. Let a non-empty stump \(T\) be given such that, for all \(n\), \(R(U,S, T\upharpoonright \langle n \rangle )\).
We intend to prove: \(R(U,S,T)\).
Let \(A,B\subseteq \overline{U}\) be given such that \(S\) \(U\)-secures \(A\) and \(T\) \(U\)-secures \(B\).
We have to prove that \(A\cap B\) is almost-full, i.e.
\((\ast )\;\forall \zeta \in [\omega ]^{\omega }\exists s\in [\omega ]^{< \omega }[\zeta \circ s\in A\cap B]\).
It is useful, however, to first prove a slightly weaker statement:
\((\ast \ast )\ \forall \zeta \in [\omega ]^{\omega }\exists s\in [ \omega ]^{<\omega }[\zeta \circ s\in A\cap B\;\vee\;(s\neq 0 \;\wedge \;s(0)=0\;\wedge \; \zeta \circ s \in A)]\).
Let \(\zeta \) in \([\omega ]^{\omega }\) be given.
We distinguish two cases.
Case (a). \(S\upharpoonright \langle \zeta (0)\rangle =\emptyset \). Note: \(\{\langle \;\rangle \}\; U\)-secures \(A\), and \(A=\overline{U}\) and \(A\cap B=B\) is almost-full. One may conclude: \((\ast )\), and, in particular, \(\exists s \in [\omega ]^{<\omega }[\zeta \circ s \in A\cap B]\).
Case (b). \(S\upharpoonright \langle \zeta (0)\rangle \neq \emptyset \). Then \(\langle \;\rangle \in S\upharpoonright \langle \zeta (0) \rangle \).
Define a statement44
\(QED_{1}:=\exists s\in [\omega ]^{<\omega }\setminus \{0\} [s(0)=0\; \wedge \;\zeta \circ s \in A]\).
Define \(A_{\zeta }:=\{u \in \overline{U}\mid \neg \exists t[u =\zeta \circ t] \;\vee \; u\in A \;\vee \;QED_{1}\}\).
Note that, for all \(u\) in \(U\cup \overline{U}\), if \(\neg \exists t[u=\zeta \circ t]\), then \(u\) \(U\)-secures \(A\) and also \(A_{\zeta }\).
We now want to prove:
$$ S\upharpoonright \langle \zeta (0)\rangle\ U\mbox{-secures}\ A_{\zeta }. $$
First, using the fact that \(S\) \(U\)-secures \(A\), find \(m\) such that
\(\forall \eta \in [\omega ]^{\omega }[\eta (0)>m\rightarrow \exists n[ \overline{\eta }n \in S \;\wedge \; \exists s \in [n]^{< n+1}[ \overline{\eta }n \circ s\) \(U\)-secures \(A]]]\).
Define \(q:=\max \bigl (m,\zeta (0)\bigr )\).
Now let \(\rho \) in \([\omega ]^{\omega }\) be given such that \(\rho (0)>q\).
We want to prove: \(\exists n [\overline{\rho }n \in S\upharpoonright \langle \zeta (0) \rangle \;\wedge \; \exists t \in [\omega ]^{<\omega }[\overline{\rho }n \circ t\) \(U\)-secures \(A_{\zeta }]]\).
Consider \(\eta :=\langle \zeta (0) \rangle \ast \rho \).
Find \(n,s\) such that \(\overline{\eta }n \in S\) and \(s\in [n]^{< n+1}\) and \(\overline{\eta }n \circ s\) \(U\)-secures \(A\).
If \(s=\langle \;\rangle \), then \(\langle \;\rangle =\rho \circ \langle \;\rangle \) \(U\)-secures \(A\) and also \(A_{\zeta }\).
We thus may assume \(s\neq \langle \;\rangle \). Note: \(\overline{\rho }(n-1)\in S\upharpoonright \langle \zeta (0)\rangle \).
There are two cases.
Case (ba). \(s(0)>0\). Find \(u\) such that \(length(u)=length(s)\) and
\(\forall i< length(u)[u(i)=s(i)-1]\).
Note: \(\overline{\rho }(n-1)\circ u=\overline{\eta }n \circ s\) \(U\)-secures \(A\) and also \(A_{\zeta }\).
Case (bb). \(s(0)=0\). Find \(u\) such that \(s =\langle 0\rangle \ast u\). Note: \(s(0)=\eta (0)=\zeta (0)\).
If \(\neg \exists t[\overline{\rho }n \circ u=\zeta \circ t]\), then also \(\neg \exists t[\overline{\rho }(n-1) \circ u=\zeta \circ t]\) and \(\overline{\rho }(n-1)\circ u\) \(U\)-secures \(A\) and also \(A_{\zeta }\).
If \(\exists t[\overline{\rho }(n-1)\circ u =\zeta \circ t]\), find \(\eta \) in \([\omega ]^{\omega }\) such that \(\zeta \circ s\sqsubset \eta \) and \(\forall i\exists j[\eta (i)=\zeta (j)]\), so \(\eta \) is a subsequence of \(\zeta \). Find \(n\) such that \(\overline{\eta }n \in \overline{U}\). As \(\zeta \circ s\) \(U\)-secures \(A\), we may conclude: \(\overline{\eta }n \in A\). Taking \(t:=\overline{\eta }n\), we see: \(\exists t[t\neq 0\;\wedge \;t(0)=0 \;\wedge \; \zeta \circ t \in A]\), i.e. \(QED_{1}\) and we may conclude: \(\overline{\rho }(n-1)\circ \langle \;\rangle =\langle \;\rangle \;U\)-secures \(A_{\zeta }\).
We thus see: for all \(\rho \) in \([\omega ]^{\omega }\), if \(\rho (0)>q\), then
\(\exists n [\overline{\rho }n \in S\upharpoonright \langle \zeta (0) \rangle \;\wedge \; \exists t \in [\omega ]^{<\omega }[\overline{\rho }n \circ t\) \(U\)-secures \(A_{\zeta }]]\), that is:
$$ S\upharpoonright \langle \zeta (0)\rangle U\mbox{-secures}\ A_{\zeta }. $$
Also: Using the assumption \(R(U, S\upharpoonright \langle \zeta (0)\rangle , T)\), we conclude: \(A_{\zeta }\cap B\) is almost-full.
$$ T\ U\mbox{-secures}\ B. $$
In particular, we may find \(s\) in \([\omega ]^{<\omega }\) such that \(\zeta \circ s \in A_{\zeta }\cap B\), and therefore, either \(\zeta \circ s \in A\cap B\) or \(QED_{1}\).
We thus see: \(\forall \zeta \in [\omega ]^{\omega }\exists s\in [\omega ]^{<\omega }[ \zeta \circ s\in A\cap B\;\vee \; (s\neq 0\;\wedge \;s(0)=0\;\wedge \; \zeta \circ s \in A)]\).
Now let \(\zeta \) in \([\omega ]^{\omega }\) be given.
Define a statement Also define
$$ QED_{2}:=\exists s \in [\omega ]^{< \omega }[\zeta \circ s \in A\cap B]. $$
$$ C:=\{u\in \overline{U\upharpoonright \langle \zeta (0)\rangle }\mid \neg \exists t \in [\omega ]^{< \omega }][u=\zeta \circ t]\;\vee \; \langle \zeta (0)\rangle \ast u \in A\;\vee \;QED_{2}\}. $$
We want to prove that \(C\) is almost-full.
First, note that, for each \(\eta \) in \([\omega ]^{\omega }\), if \(\eta (0)=\zeta (0)\) and \(\eta \) is a subsequence of \(\zeta \), i.e.: \(\forall i\exists j[\eta (i)=\zeta (j)]\), then either \(\exists s\in [\omega ]^{<\omega }[\eta \circ s \in A\cap B]\), and, therefore, \(QED_{2}\), or \(\exists s\in [\omega ]^{<\omega }\setminus \{0\}[s(0)=0\;\wedge \; \eta \circ s \in A]\), and, therefore, \(\exists s \in [\omega ]^{<\omega }[\langle \zeta (0)\rangle \ast ( \eta \circ s) \in A]\).
We may even conclude: for every \(\eta \) in \([\omega ]^{\omega }\) that is a subsequence of \(\zeta \), either \(QED_{2}\), or \(\exists s \in [\omega ]^{<\omega }[\langle \zeta (0)\rangle \ast ( \eta \circ s) \in A]\), for, given \(\eta \) such that \(\eta (0)\neq \zeta (0)\) we may apply the previous result to the sequence \(\eta ^{+}:=\langle \zeta (0)\rangle \ast \eta \).
We thus see that, for every \(\eta \) in \([\omega ]^{\omega }\) that is a subsequence of \(\zeta \), there exists \(s\) in \([\omega ]^{<\omega }\) such that \(\eta \circ s \in C\).
Now let \(\eta \) in \([\omega ]^{\omega }\) be given. Define \(\eta _{\zeta }\) in \([\omega ]^{\omega }\) as follows.
If \(\exists i[\eta (0)=\zeta (i)]\), define \(\eta _{\zeta }(0)=\eta (0)\), and, if not, define \(\eta _{\zeta }(0) =\zeta (0)\).
For each \(n\), if \(\exists t \in [\omega ]^{n+2}[\overline{\eta }(n+2) = \zeta \circ t]\), then \(\eta _{\zeta }(n+1)=\eta (n+1)\), and, if not, then \(\eta _{\zeta }(n+1)=\zeta (i+1)\), where \(i\) satisfies \(\eta _{\zeta }(n)=\zeta (i)\).
As \(\eta _{\zeta }\) is a subsequence of \(\zeta \), find \(s\) in \([\omega ]^{<\omega }\) such that \(\eta _{\zeta }\circ s \in C\).
Either \(\eta \circ s = \eta _{\zeta }\circ s \in C\) or \(\eta \circ s\neq \eta _{\zeta }\circ s \). In the latter case, let \(n_{0}\) be the least \(n\) such that \(\neg \exists i[\eta (n)=\zeta (i)]\). Define \(\rho \) in \([\omega ]^{\omega }\) such that \(\forall n[\rho (n)=n_{0}+n]\) and find \(m\) such that \(\overline{\eta \circ \rho }(m) \in \overline{U\upharpoonright \langle \zeta (0)\rangle }\). Define \(s:=\overline{\rho }m\) and note: \(\overline{\eta \circ \rho } (m) = \eta \circ s\) and \(\neg \exists u\in [\omega ]^{<\omega }[ \eta \circ s = \zeta \circ u]\) and \(\eta \circ s \in C\).
We thus see that \(C\) is almost-full.
We obtained this result using the assumption: \(Q(U,S\upharpoonright \langle \zeta (0) \rangle )\).
Now define
$$ D:=\{u\in \overline{U\upharpoonright \langle \zeta (0)\rangle }\mid \neg \exists t \in [\omega ]^{< \omega }][u=\zeta \circ t]\;\vee \; \langle \zeta (0)\rangle \ast u \in B\;\vee \;QED_{2}\}.$$
Using the assumption: \(R(U, S, T\upharpoonright \langle \zeta (0)\rangle )\), one may prove: \(D\) is almost-full, by an argument similar to the one that established that \(C\) is almost-full.
Using the assumption \(P(U\upharpoonright \langle \zeta (0)\rangle )\), one then concludes: \(C\cap D\) is almost-full.
Find \(s\) in \([\omega ]^{<\omega }\) such that \(\zeta \circ s \in C\cap D\) or \(\langle \zeta (0)\rangle \ast \zeta \circ s \in A\cap B\), so, in any case, \(QED_{2}\).
Using the assumptions: for all \(n\), \(P(U\upharpoonright \langle n \rangle )\) (2), and: for all \(n\), \(Q(U, S\upharpoonright \langle n \rangle )\) (2.2) and: for all \(n\), \(R(U, S, T\upharpoonright \langle n \rangle )\) (2.2.2), one thus proves: \(R(U,S,T)\), i.e.: for all \(A,B\subseteq \overline{U}\), if \(S,T\) \(U\)-secure \(A,B\), respectively, then \(A\cap B\) is almost-full, i.e.: \(\forall \zeta \in {\omega }^{\omega }\exists s\in [\omega ]^{<\omega }[ \zeta \circ s \in A\cap B]\).
(ii) This immediately follows from (i), as, for all \(k\), \(\omega ^{< k}\) is a stump and
\(\overline{\omega ^{< k}}=\omega ^{k}\).45 □
Corollary 27
For all \(k>0\), for all \(r>0\), for all subsets \(A_{0},A_{1}, \dots , A_{r-1}\) of \([\omega ]^{k}\), if, for each \(j< r\), \(A_{j}\) is almost-full, then \(\bigcap _{j< r} A_{j}\) is almost-full.
Proof
Straightforward, by induction. □
18.4 The (Extended) Finite Ramsey Theorem and the ‘Compactness Argument’
The following Definition extends Definition 24 in Sect. 18.3. Note that, deviating from the usual treatment of Ramsey theorems, we consider finite increasing sequences of nonnegative integers rather than finite sets of nonnegative integers.
Definition 26
For all \(r>0\), \(r^{<\omega }:=\{s\mid \forall i<length(s)[s(i)<r]\}\).
For all positive integers \(c,m,k,r\),
\(c:[m]^{k}\rightarrow r\), (\(c\) is an \(r\)-colouring of \([m]^{k})\), if and only if
\(c\in r^{<\omega }\) and \(\forall s \in [m]^{k}[s <\mathit{length}(c)]\).
If \(c:[m]^{k}\rightarrow r\), one may consider \(c\) as an \(r\)-colouring of the \(k\)-element subsets of \(m=\{0,1,\ldots ,m-1\}\).
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
\(\exists j< r\forall u \in [n]^{k}[ c(t\circ u)=j]\), i.e. \(t\) is \(c\)-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.
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,p\) such that \(p\ge n\) and
\(t\in [M]^{p}\) and \(p=t(0)\) and \(\exists j< r\forall u \in [p]^{k}[ c(t\circ u)=j]\).
The meaning of this statement is similar to that of the previous one but now the \(p\)-element subset \(A=\{t(0), t(1), \ldots t(p-1)\}\) of \(M\) is required to satisfy the conditions \(n\le p\) and \(p= \min (A)= t(0)\). A finite set \(A\) with the property \(\#(A)\ge \min (A)\) is sometimes called relatively large, see [44].
\(\mathbf{FRT}\), the Finite Ramsey Theorem, is the statement:
$$ \forall k \forall r \forall n\exists M[M\rightarrow (n)^{k}_{r}]. $$
\(\mathbf{FRT}_{PH}\), the Extended Finite Ramsey Theorem, is the statement:
$$ \forall k \forall r \forall n\exists M[M\rightarrow _{\ast }(n)^{k}_{r}]. $$
Ramsey thought proving \(\mathbf{IRT}_{class}\) was a useful training for someone who wanted to prove \(\mathbf{FRT}\). \(\mathbf{FRT}\) was given an independent proof.
Around 1950, it was seen that a so-called compactness argument proves \(\mathbf{FRT}\) from \(\mathbf{IRT}_{class}\), see [18] and [32, §1.7 and §6.3].
In 1976, the stronger statement \(\mathbf{FRT}_{PH}\) was formulated by J. Paris and L. Harrington. Also \(\mathbf{FRT}_{PH}\) may be proven (classically) from \(\mathbf{IRT}_{class}\) by a compactness argument, see [44] but \(\mathbf{FRT}_{PH}\), although it may be formulated in the language of Peano Arithmetic, can not be proven from the axioms of \(PA\).46 Paris and Harrington thus found a mathematical Incompleteness Theorem, thereby creating a stir in the logic community.
The proof of the next Theorem is an intuitionistic version of the compactness argument deriving \(\mathbf{FRT}_{PH}\) from \(\mathbf{IRT}_{class}\).
Definition 27
For each \(r>0\), \(r^{\omega }:=\{\chi \mid \forall i[\chi (i)< r]\}\).
Theorem 28
\(\mathbf{IRT} \rightarrow \mathbf{FRT}_{PH}\).
Proof
47 Let \(n,k,r\) be given positive integers. Let \(\chi \) be an element of \(r^{\omega }\). We want to prove: For each \(j< r\), define: \(A_{j}:=\{t \in [\omega ]^{k}\mid \chi (t) \neq j \;\vee \; QED_{3}\}\).
$$ QED_{3}:= \exists p\ge n\exists t\in [\omega ]^{p}[t(0) = p \;\wedge \exists j < r\forall u\in [p]^{k}[\chi (t\circ u) =j]]. $$
Let \(j< r\) and \(\zeta \) in \([\omega ]^{\omega }\) be given. Find \(p:=\max \bigl ( n, \zeta (0)\bigr )\) and define \(t:=\overline{\zeta }p\). Either: \(\forall u\in [p]^{k}[\chi (t\circ u)=j]\) and \(QED_{3}\), or: \(\exists u \in [p]^{k}[\chi (t\circ u)\neq j]\).
We thus see: for each \(j< r\), \(A_{j}\) is almost-full.
In particular, \(\bigcap _{j< r} A_{j}\) is inhabited and, therefore, \(QED_{3}\).
We thus see: \(\forall \chi \in r^{\omega }\exists p\ge n \exists t\in [\omega ]^{p}[(t(0) = p\;\wedge \;\exists j< r \forall u\in [p]^{k}[\chi (t\circ u) =j]]\).
Now let \(B\) be the set of all \(c\) in \(r^{<\omega }\) such that
$$ \exists p\ge n \exists t\in [\omega ]^{p}[t(0)= p\;\wedge \; \exists j< r \forall u\in [p]^{k}[t\circ u< \mathit{length}(c)\;\wedge \;c(t\circ u) =j]]. $$
Note: \(Bar_{r^{\omega }}(B)\) and: \(r^{\omega }\) is a fan. Using the Fan Theorem, Theorem 14, find \(z,m\) such that \(length(z)=m\) and \(\forall i< m[z(i)\in B]\) and \(\forall \chi \in r^{\omega }\exists i< m[z(i)\sqsubset \chi ]\).
Define \(N:=\max _{i< m}length\bigl (z(i)\bigr )\).
Find \(M\) such that \(\forall u< N\forall j< length(u)[u(j)< M]\).
Then: \(M\rightarrow _{\ast }(n)^{k}_{r}\). □
19 Borel Sets
19.1 Some Preparations
We introduce the important notion of a spread.
Definition 28
Let \(\beta \) be given. \(\beta \) is a spread-law if and only if
\(\forall s[\beta (s)=0 \leftrightarrow \exists n[\beta (s\ast \langle n \rangle )=0]]\).
\(\mathcal{X}\subseteq \mathcal{N}\) is a spread if and only if there exists a spread-law \(\beta \) such that
\(\mathcal{X}=\mathcal{F}_{\beta }:=\{\alpha \mid \forall n[\beta ( \overline{\alpha }n)=0]\}\).
Note that the spread-law \(\beta \) in a sense governs the set \(\mathcal{F}_{\beta }\). The law makes clear which steps are allowed during the step-by-step construction of an element \(\alpha =\alpha (0), \alpha (1), \ldots \) of \(\mathcal{F}_{\beta }\). In his early publications, Brouwer used the term ‘set, Menge’ for what he later called spreads. This is because the notion expresses his view in what sense a totality like for instance ℛ might be called a set.
Brouwer’s Continuity Principle, Axiom 1, extends to spreads:
Theorem 29
The extended Continuity Principle
-
Let \(\beta \) be a spread-law and let \(R\) be a subset of \(\mathcal{F}_{\beta }\times \mathbb{N}\).
-
If \(\forall \alpha \in \mathcal{F}_{\beta }\exists n[\alpha Rn]\), then \(\forall \alpha \in \mathcal{F}_{\beta }\exists m \exists n \forall \beta \in \mathcal{F}_{\beta }[\overline{\alpha }m \sqsubset \beta \rightarrow \beta R n]\).
Proof
Let \(\beta \) be a spread-law such that \(\beta (\langle \;\rangle )=0\).
Define \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\) such that, for each \(\alpha \), for each \(n\),
if \(\beta (\overline{\alpha }\bigl (n+1) \bigr )=0\), then \((\varphi |\alpha )(n)=\alpha (n)\), and,
if not, then \((\varphi |\alpha )(n)= \) the least \(p\) such that \(\beta \bigl (\overline{(\varphi |\alpha )}n\ast \langle p\rangle \bigr )=0]\).
Note: \(\forall \alpha [\varphi |\alpha \in \mathcal{F}_{\beta }]\) and \(\forall \alpha \in \mathcal{F}_{\beta }[\varphi |\alpha =\alpha ]\).
The function \(\varphi \) is called a retraction of \(\mathcal{N}\) onto \(\mathcal{F}_{\beta }\).
Now assume: \(\forall \alpha \in \mathcal{F}_{\beta }\exists n[\alpha Rn]\). Then \(\forall \alpha \exists n[(\varphi |\alpha )Rn]\). Using Axiom 1 conclude: \(\forall \alpha \exists m\forall \beta [\overline{\alpha }m \sqsubset \beta \rightarrow (\varphi |\beta )Rn]\) and: \(\forall \alpha \in \mathcal{F}_{\beta }\exists m \exists n \forall \beta \in \mathcal{F}_{\beta }[\overline{\alpha }m \sqsubset \beta \rightarrow \beta R n]\). □
Definition 29
For each \(\alpha \) in \(\mathcal{N}\), for each \(n\), we define \(\alpha ^{n}\) in \(\mathcal{N}\) by:
\(\forall m[\alpha ^{n}(m)=\alpha \bigl (2^{m}(2n+1)-1\bigr )]\).
\(\alpha ^{n}\) is called the \(n\)-th subsequence of \(\alpha \).
For all \(\alpha \), for all \(n,j\), we define: \(\alpha ^{n,j}:=(\alpha ^{n})^{j}\).
The next definition explains how continuous functions from \(\mathcal{N}\) to ℕ and continuous functions from \(\mathcal{N}\) to \(\mathcal{N}\) are coded by elements of \(\mathcal{N}\).
Definition 30
For each \(\varphi \), we define: \(\varphi :\mathcal{N}\rightarrow \mathbb{N}\) if and only if \(\forall \alpha \exists n[\varphi (\overline{\alpha }n)\neq 0]\).
For each \(\varphi \) such that \(\varphi :\mathcal{N}\rightarrow \mathbb{N}\), for each \(\alpha \), we let \(\varphi (\alpha )\) be the number \(p\) such that \(\exists n[\varphi (\overline{\alpha }n)=p+1]\;\wedge \;\forall i< n[ \varphi (\overline{\alpha }i)=0]]\).
For each \(\varphi \), we define: \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\) if and only if \(\forall n[\varphi ^{n}:\mathcal{N}\rightarrow \mathbb{N}]\).
For each \(\varphi \) such that \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\), for each \(\alpha \), we let \(\varphi |\alpha \) be the element \(\beta \) of \(\mathcal{N}\) such that \(\forall n[\beta (n)=\varphi ^{n}(\alpha )]\).
The following notion plays a key rôle in intuitionistic descriptive set theory, the theory of Borel and projective sets.
Definition 31
Reducibility48
For all \(\mathcal{X}, \mathcal{Y}\subseteq \mathcal{N}\), for all \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\), we define: \(\varphi \) reduces \(\mathcal{X}\) to \(\mathcal{Y}\), if and only if \(\forall \alpha [\alpha \in \mathcal{X}\leftrightarrow \varphi | \alpha \in \mathcal{Y}]\).
For all \(\mathcal{X}, \mathcal{Y}\subseteq \mathcal{N}\), we define: \(\mathcal{X}\preceq \mathcal{Y}\), \(\mathcal{X}\) reduces to \(\mathcal{Y}\), if and only if there exists \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\) reducing \(\mathcal{X}\) to \(\mathcal{Y}\).
If \(\varphi \) reduces \(\mathcal{X}\) to \(\mathcal{Y}\), then, for each \(\alpha \), the question
Does \(\alpha \) belong to \(\mathcal{X}\)?
is reduced to the question:
Does \(\varphi |\alpha \) belong to \(\mathcal{Y}\)?
19.2 Borel Sets of Finite Rank
We first introduce open subsets and closed subsets of \(\mathcal{N}=\omega ^{\omega }\).
Definition 32
For each \(\beta \), we define \(\mathcal{G}^{1}_{\beta }:=\{\alpha \mid \exists n[\beta ( \overline{\alpha }n)\neq 0]\}\) and
\(\mathcal{F}^{1}_{\beta }:=\mathcal{N}\setminus \mathcal{G}^{1}_{\beta }= \{\alpha \mid \forall n[\beta (\overline{\alpha }n)=0]\}\).
We define \(\mathcal{E}_{1}:=\{\alpha \mid \exists n[\alpha (n)\neq 0]\}\) and
\(\mathcal{A}_{1}:=\mathcal{N}\setminus \mathcal{E}_{1} =\{\alpha \mid \forall n[\alpha (n)=0]\}=\{\underline{0}\}\).
\(\mathcal{X}\subseteq \mathcal{N}\) is open, or: \(\boldsymbol{\Sigma }^{0}_{1}\), if and only if \(\exists \beta [\mathcal{X}=\mathcal{G}^{1}_{\beta }]\),
and closed, or: \(\boldsymbol{\Pi }^{0}_{1}\), if and only if \(\exists \beta [\mathcal{X}=\mathcal{F}^{1}_{\beta }]\).
Note that spreads, as introduced in Definition 28, are closed subsets of \(\mathcal{N}\). It is not true that every closed subset of \(\mathcal{N}\) is a spread. A closed subset ℱ of \(\mathcal{N}\) is a spread if and only if it is located, i.e. \(\exists \beta \forall s[\exists \alpha \in \mathcal{F}[s\sqsubset \alpha ]\leftrightarrow \beta (s)=0]\).
Note that, if \(\mathcal{G}\subseteq \mathcal{N}\) is open, then its complement \(\mathcal{N}\setminus \mathcal{G}\) is a closed subset of \(\mathcal{N}\). It is not true that the complement of a closed subset of \(\mathcal{N}\) always is an open subset of \(\mathcal{N}\).
We now introduce Borel sets of finite rank. Note that we avoid the operation of taking the complement of a given Borel set.
Definition 33
For each \(n>0\), for each \(\beta \), we define, inductively,
\(\mathcal{G}^{n+1}_{\beta }=\bigcup _{m} \mathcal{F}^{n}_{\beta ^{m}}\), and \(\mathcal{F}_{\beta }^{n+1}=\bigcap _{m} \mathcal{F}^{n}_{\beta ^{m}}\).
For each \(n>0\), we define, inductively,
\(\mathcal{E}_{n+1}:=\{\alpha \mid \exists m[\alpha ^{m} \in \mathcal{A}_{n}]\}\) and \(\mathcal{A}_{n+1}:=\{\alpha \mid \forall m[\alpha ^{m} \in \mathcal{E}_{n}]\}\).
For each \(n>0\), \(\mathcal{X}\subseteq \mathcal{N}\) is \(\boldsymbol{\Sigma }^{0}_{n}\) if and only if \(\exists \beta [\mathcal{X}=\mathcal{G}^{n}_{\beta }]\) and
\(\mathcal{X}\) is \(\boldsymbol{\Pi }^{0}_{n}\) if and only if \(\exists \beta [\mathcal{X}=\mathcal{F}^{n}_{\beta }]\).
\(\mathcal{X}\subseteq \mathcal{N}\) belongs to \(\boldsymbol{\Sigma }^{0}_{n+1}\) if and only if there exists an infinite sequence \(\mathcal{Y}_{0}, \mathcal{Y}_{1}, \ldots \) of elements of \(\boldsymbol{\Pi }^{0}_{n}\) such that \(\mathcal{X}=\bigcup _{m} \mathcal{Y}_{m}\).
\(\mathcal{X}\subseteq \mathcal{N}\) belongs to \(\boldsymbol{\Pi }^{0}_{n+1}\) if and only if there exists an infinite sequence \(\mathcal{Y}_{0}, \mathcal{Y}_{1}, \ldots \) of elements of \(\boldsymbol{\Sigma }^{0}_{n}\) such that \(\mathcal{X}=\bigcap _{m} \mathcal{Y}_{m}\).
19.3 The Fine Structure of the Borel Hierarchy
One may prove that the union of two opens sets is open again but it is not true that the union of two closed sets is a closed sets itself. It is useful to introduce the following operation.
Definition 34
For each \(n>0\), for each \(\mathcal{X}\subseteq \mathcal{N}\), we define
\(\mathbb{D}^{n}(\mathcal{X})=\{\alpha \mid \exists i< n[\alpha ^{i} \in \mathcal{X}]\}\).
The next Theorem, Theorem 30, offers an example of a union of two closed subsets of \(\mathcal{N}\) that is not an intersection of countably many open subsets of \(\mathcal{N}\) and, therefore, certainly not a closed subset of \(\mathcal{N}\), see item (iii). Theorem 30(iv) makes it clear that there are unions of three closed sets not coinciding with any union of two closed sets, and unions of four closed sets not coinciding with any union of three closed sets, and so on.
Theorem 30
(i)
For all \(\mathcal{X}\subseteq \mathcal{N}\), \(\mathcal{X}\) is \(\boldsymbol{\Pi }^{0}_{1}\) if and only if \(\mathcal{X}\preceq \mathcal{A}_{1}\).
(ii)
For all \(\mathcal{X}\subseteq \mathcal{N}\), for all \(n>0\), \(X\preceq \mathbb{D}^{n}(\mathcal{A}_{1})\) if and only if there exists \(\boldsymbol{\Pi }^{0}_{1}\) sets \(\mathcal{F}_{0}, \mathcal{F}_{1}, \ldots , \mathcal{F}_{n-1}\) such that \(\mathcal{X}=\bigcup _{i< n}\mathcal{F}_{i}\).
(iii)
\(\mathbb{D}^{2}(\mathcal{A}_{1})\) is not \(\boldsymbol{\Pi }^{0}_{2}\).
(iv)
For all \(n>0\), \(\mathbb{D}^{n+1}(\mathcal{A}_{1})\npreceq \mathbb{D}^{n}(\mathcal{A}_{1})\).
Proof
The proofs of (i) and (ii) are left to the reader.
(iii) Define \(\mathcal{T}:=\{\alpha \mid \forall m\forall n[\bigl (\alpha (m)\neq 0 \;\wedge \;\alpha (n)\neq 0\bigr )\rightarrow m=n]\}\).
\(\mathcal{T}\) is the set of all \(\alpha \) that assume at most one time a value different from 0.
Note that \(\mathcal{T}\) is a spread.
Assume \(\mathbb{D}^{2}(\mathcal{A}_{1})\) is \(\boldsymbol{\Pi }^{0}_{2}\). Find \(\beta \) such that \(\mathbb{D}^{2}(\mathcal{A}_{1})=\{\alpha \mid \forall m \exists n[ \beta ^{m}(\overline{\alpha }n)\neq 0]\}\).
Let \(\alpha \) in \(\mathcal{T}\) be given. Let \(m\) be given. Define \(\alpha _{0}, \alpha _{1}\) such that, for all \(n\), for both \(i<2\), \((\alpha _{i})^{i}=\underline{0}\) and, for all \(s\), if \(\neg \exists p[s=\langle i, p\rangle ]\), then \(\alpha _{i}(n)=\alpha (n)\).
Note: for both \(i<2\), \(\alpha ^{i} \in \mathbb{D}^{2}(\mathcal{A}_{1})\). Also note: \(\forall n[\overline{\alpha }n =\overline{\alpha _{0}}n\;\vee \; \overline{\alpha }n =\overline{\alpha _{1}}n]\).
Find \(n_{0}, n_{1}\) such that, for both \(i<2\), \(\beta ^{m}(\overline{\alpha }_{i} n_{i})\neq 0\). Note: either \(\overline{\alpha }_{0} n_{0}\sqsubset \alpha \) or \(\overline{\alpha }_{1} n_{1}\sqsubset \alpha \), and, in both cases, \(\exists n [ \beta ^{m}(\overline{\alpha }n)\neq 0]\).
We thus see: \(\forall \alpha \in \mathcal{T}[\alpha \in \mathbb{D}^{2}(\mathcal{A}_{1})]\). Using Theorem 29, find \(m,i\) such that \(i<2\) and \(\forall \alpha \in \mathcal{T}[\overline{\underline{0}}m\sqsubset \alpha \rightarrow \alpha ^{i}=\underline{0}]\). This gives a contradiction as one may find \(\alpha \) in \(\mathcal{T}\) such that \(\overline{\underline{0}}m \sqsubset \alpha \) and \(\alpha ^{i}\neq \underline{0}\).
We may conclude: \(\mathbb{D}^{2}(\mathcal{A}_{1})\) is not \(\boldsymbol{\Pi }^{0}_{2}\).
(iv) Again, consider \(\mathcal{T}:=\{\alpha \mid \forall m\forall n[\bigl (\alpha (m)\neq 0 \;\wedge \;\alpha (n)\neq 0\bigr )\rightarrow m=n]\}\).
Let \(n>0\) be given such that \(\mathbb{D}^{n+1}(\mathcal{A}_{1})\preceq \mathbb{D}^{n}(\mathcal{A}_{1})\).
Find \(\beta \) such that \(\mathbb{D}^{n+1}(\mathcal{A}_{1})=\{\alpha \mid \exists i< n\forall j[ \beta ^{i}(\overline{\alpha }j)=0]\}\).
For each \(i\), define \(\mathcal{B}_{i}:=\{\alpha \mid \alpha ^{i}=\underline{0}\}\). Note that each \(\mathcal{B}_{i}\) is a spread.
Also note: \(\mathbb{D}^{n+1}(\mathcal{A}_{1})= \bigcup _{i< n+1}\mathcal{B}_{i}\).
\(\forall \alpha \in \mathcal{B}_{i}[\underline{\overline{0}}m_{i} \sqsubset \alpha \rightarrow \forall n[\beta ^{k_{i}}( \overline{\alpha }n)=0]]\).
Find \(i_{0}, i_{1}< n+1\) such that \(i_{0}< i_{1}\) and \(k_{i_{0}}=k_{i_{1}}\). Define \(k:=k_{i_{0}}\).
Let \(\alpha \) in \(\mathcal{T}\) be given. Define \(\alpha _{0}, \alpha _{1}\) such that, for all \(n\), for both \(j<2\), \((\alpha _{j})^{i_{j}}=\underline{0}\) and, for all \(s\), if \(\neg \exists p[s=\langle i_{j}, p\rangle ]\), then \(\alpha _{j}(n)=\alpha (n)\).
Note: for both \(j<2\), \(\alpha _{j} \in \mathcal{B}_{i_{j}}\) and \(\underline{\overline{0}}m_{i_{j}}\sqsubset \alpha_{j} \rightarrow \forall n[\beta^{k}(\overline{\alpha_{j}} n)=0]\).
Define \(m:=\max(m_{i_{0}}, m_{i_{1}})\) and distinguish two cases.
Case (a). \(\underline{\overline{0}} m\perp \alpha\). Then \(\alpha \in \mathbb{D}^{n+1}(\mathcal{A}_{1})\).
Case (b). \(\underline{\overline{0}} m\sqsubset \alpha\). Then also \(\forall j<2[\underline{\overline{0}} m\sqsubset \alpha_{j}]\) and \(\forall j<2\forall n[\beta^{k}(\overline{\alpha_{j}}n)=0]\).
As \(\forall n\exists j<2[\overline{\alpha }n =\overline{\alpha _{j}}n]\), conclude: \(\forall n[\beta^{k}(\overline{\alpha}n)=0]\) and \(\alpha\in \mathbb{D}^{n+1}(\mathcal{A}_{1})\).
We thus see: \(\forall \alpha \in \mathcal{T}[\alpha \in \mathbb{D}^{n+1}( \mathcal{A}_{1})]\). Using Theorem 29, find \(m,i\) such that \(i< n+1\) and \(\forall \alpha [\overline{\underline{0}}m\sqsubset \alpha \rightarrow \alpha ^{i}=\underline{0}]\). This gives a contradiction as one may find \(\alpha \) in \(\mathcal{T}\) such that \(\overline{\underline{0}}m \sqsubset \alpha \) and \(\alpha ^{i}\neq \underline{0}\). □
19.4 The Borel Hierarchy Theorem
The next Theorem, Theorem 31, makes a start with establishing the Borel hierarchy itself.
Theorem 31
(i)
For all \(n>0\), for all \(\mathcal{X}\subseteq \mathcal{N}\), \(\mathcal{X}\) is \(\boldsymbol{\Sigma }^{0}_{n}\) if and only if \(\mathcal{X}\preceq \mathcal{E}_{n}\), and \(\mathcal{X}\) is \(\boldsymbol{\Pi }^{0}_{n}\) if and only if \(\mathcal{X}\preceq \mathcal{A}_{n}\).
(ii)
For every \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\), there exists \(\alpha \) such that,
for all \(m\), \(\alpha ^{m}\in \mathcal{E}_{1}\leftrightarrow (\varphi |\alpha )^{m} \in \mathcal{E}_{1}\), and, therefore,
\(\alpha \in \mathcal{A}_{2} \leftrightarrow \varphi |\alpha \in \mathcal{A}_{2}\) and \(\alpha \in \mathcal{E}_{2} \leftrightarrow \varphi |\alpha \in \mathcal{E}_{2}\).
(iii)
For every \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\),
if \(\forall \alpha [\alpha \in \mathcal{E}_{2}\rightarrow \varphi | \alpha \in \mathcal{A}_{2}]\), then \(\exists \alpha [\alpha \in \mathcal{A}_{2}\;\wedge \;\varphi | \alpha \in \mathcal{A}_{2}]\).
(iv)
For every \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\), if \(\forall \alpha [\alpha \in \mathcal{A}_{2}\rightarrow \varphi | \alpha \in \mathcal{E}_{2}]\), then \(\exists \alpha [\alpha \in \mathcal{E}_{2}\;\wedge \;\varphi | \alpha \in \mathcal{E}_{2}]\).
Proof
(i) The proof is left to the reader.
(ii) Let \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\) be given. Define \(\alpha \), inductively, as follows.
Let \(p\) be given such that \(\alpha (0), \alpha (1), \ldots , \alpha (p-1)\) have been defined already.
Find \(m,n\) such that such that \(p= 2^{n}(2m+1)-1\).
Define \(\alpha (p)=\alpha ^{m}(n):=1\) if \(\exists q< p[\varphi ^{m}(\overline{\alpha }q) >1\;\wedge \;\forall i< q[ \varphi ^{m}(\overline{\alpha }i)=0]]\),
and \(\alpha (p):=0\) if not.
Note that, for all \(m\), \(\exists n[\alpha ^{m}(n)\neq 0] \leftrightarrow \exists n[(\varphi | \alpha )^{m} (n)\neq 0]\), and, therefore,
\(\alpha ^{m}\in \mathcal{E}_{1}\leftrightarrow (\varphi |\alpha )^{m} \in \mathcal{E}_{1}\) and \(\alpha ^{m}\in \mathcal{A}_{1}\leftrightarrow (\varphi |\alpha )^{m} \in \mathcal{A}_{1}\).
(iii) Let \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\) be given such that \(\forall \alpha [\alpha \in \mathcal{E}_{2}\rightarrow \varphi | \alpha \in \mathcal{A}_{2}]\).
Using (i), find \(\alpha \) such that \(\forall m[\alpha ^{m}\in \mathcal{E}_{1}\leftrightarrow (\varphi | \alpha )^{m} \in \mathcal{E}_{1}]\).
Let \(m\) be given.
Define \(\alpha _{0}\) such that \((\alpha _{0})^{m}=\underline{0}\) and, for all \(n\neq m\), \((\alpha _{0})^{n}=\alpha ^{n}\).
Note: \(\alpha _{0}\in \mathcal{E}_{2}\), and, therefore, \(\varphi |\alpha _{0} \in \mathcal{A}_{2}\) and \((\varphi |\alpha _{0})^{m}\in \mathcal{E}_{1}\).
Find \(n\) such that \((\varphi |\alpha _{0})^{m}(n)\neq 0\).
Either \((\varphi |\alpha )^{m}(n)\neq 0\) and \((\varphi |\alpha )^{m} \in \mathcal{E}_{1}\) and also \(\alpha ^{m} \in \mathcal{E}_{1}\),
or \((\varphi |\alpha _{0})^{m}(n)=0 \) and \(\varphi |\alpha \perp \varphi |\alpha _{0}\) and \(\alpha \perp \alpha _{0}\) and \(\alpha ^{m}\perp \underline{0}\) and \(\alpha ^{m} \in \mathcal{E}_{1}\).
We thus see: \(\forall m[\alpha ^{m} \in \mathcal{E}_{1}]\). Therefore, both \(\alpha \) and \(\varphi |\alpha \) are in \(\mathcal{A}_{2}\).
(iv) The following observation is easy but crucial:
\(\forall \alpha [ \exists \sigma \forall m[\alpha ^{m}\bigl (\sigma (m) \bigr )\neq 0]\rightarrow \alpha \in \mathcal{A}_{2}]\).
For each \(\alpha \), for each \(\sigma \), we let \(\sigma \Join \alpha \) be the element of \(\mathcal{N}\) such that, for each \(m\), \((\sigma \Join \alpha )^{m}\bigl (\sigma (m)\bigr )=\max \bigl (1, \alpha ^{m}\bigl (\sigma (m))\bigr )\) and, for all \(n \neq \sigma (m)\),
\((\sigma \Join \alpha )^{m}(n)= \alpha ^{m}(n)]\). \(\sigma \Join \alpha \) may be thought of as ‘\(\alpha \)-corrected-by-\(\sigma \)’.
Note: \(\forall \alpha [ \exists \sigma [\alpha =\sigma \Join \alpha ] \rightarrow \alpha \in \mathcal{A}_{2}]\).
Now let \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\) be given such that \(\forall \alpha [\alpha \in \mathcal{A}_{2}\rightarrow \varphi | \alpha \in \mathcal{E}_{2}]\).
Conclude: \(\forall \alpha \exists n[\bigl ((\varphi |(\alpha ^{0}\Join \alpha ^{1}) \bigr )^{n}=\underline{0}]\).
Using Axiom 1, find \(m,n\) such that \(\forall \alpha [\underline{\overline{0}}m\sqsubset \alpha \rightarrow \bigl ((\varphi |(\alpha ^{0}\Join \alpha ^{1})\bigr )^{n}=\underline{0}]\).
Define \(\beta \) in \(\mathcal{C}\) such that \(\forall i\forall j [\beta ^{i}(j)=1\leftrightarrow (i< m \;\wedge \;j=0)]\).
Let \(j\) be given. Find \(p\) such that \(\varphi ^{n,j}(\overline{\beta }p) \neq 0\) and \(\forall i< p[\varphi ^{n,j}(\overline{\beta }i)=0]\).
Find \(\alpha \) such that \(\overline{\underline{0}}m\sqsubset \alpha \) and \(\overline{\beta }p\sqsubset \alpha ^{0} \Join \alpha ^{1}\).
Conclude: \((\varphi |\beta )^{n}(j)= \bigl (\varphi |(\alpha ^{0}\Join \alpha ^{1}) \bigr )^{n}(j) =0\) and \(\varphi ^{n,j}(\overline{\beta }p)=1\).
We thus see: \(\forall j[(\varphi |\beta )^{n}(j)=0]\) and \((\varphi |\beta )^{n}=\underline{0}\) and \(\varphi |\beta \in \mathcal{E}_{2}\).
We thus found \(\beta \) such that both \(\beta \) and \(\varphi |\beta \) are in \(\mathcal{E}_{2}\). □
Note that the proofs of Theorem 31(ii) and (iii) are elementary in the sense that they do not use intuitionistic axioms like the Continuity Principle or the Fan Theorem. The constructive argument for Theorem 31(ii) extends to a constructive argument establishing
Unfortunately, one can’t conclude from this, constructively, that \(\mathcal{A}_{n}\) does not reduce to \(\mathcal{E}_{n}\). Assuming that \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\) reduces \(\mathcal{A}_{n}\) to \(\mathcal{E}_{n}\), one finds, using Theorem 31(ii), \(\alpha \) such that \(\alpha \in \mathcal{A}_{n}\leftrightarrow \alpha \in \mathcal{E}_{n}\). If \(n>1\), one can’t derive a contradiction from this statement.For each \(n>0\), for each \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\), there exists \(\alpha \) such that\(\alpha \in \mathcal{E}_{n}\leftrightarrow \varphi |\alpha \in \mathcal{E}_{n}\) and \(\alpha \in \mathcal{A}_{n}\leftrightarrow \varphi |\alpha \in \mathcal{A}_{n}\).
The intervention of the Continuity Principle in the proof of Theorem 31(iv) is crucial. One may extend this argument to a proof of:
For each \(n>0\), for each \(\varphi :\mathcal{N}\rightarrow \mathcal{N}\),if \(\forall \alpha [\alpha \in \mathcal{E}_{n}\rightarrow \varphi | \alpha \in \mathcal{A}_{n}]\), then \(\exists \alpha [\alpha \in \mathcal{A}_{n}\;\wedge \;\varphi | \alpha \in \mathcal{A}_{n}]\), and,if \(\forall \alpha [\alpha \in \mathcal{A}_{n}\rightarrow \varphi | \alpha \in \mathcal{E}_{n}]\), then \(\exists \alpha [\alpha \in \mathcal{E}_{n}\;\wedge \;\varphi | \alpha \in \mathcal{E}_{n}]\).
This shows that \(\mathcal{E}_{n}\) positively refuses to reduce to \(\mathcal{A}_{n}\), and \(\mathcal{A}_{n}\) positively refuses to reduce to \(\mathcal{E}_{n}\).
The theorem extends into the transfinite and then may be called the Intuitionistic Borel Hierarchy Theorem, see [58, Theorems 7.9 and 7.10].
20 Notions of Finiteness
20.1 Some Examples
We study decidable subsets of the set ℕ.
Such sets may be called ‘finite’ in various constructively different ways.
Definition 35
For every \(\alpha \), we define \(D_{\alpha }:=\{n\mid \alpha (n)\neq 0\}\).
\(D_{\alpha }\) is called the subset of ℕ decided by \(\alpha \).
\(\mathbf{Fin}:=\{\alpha \mid \exists n\forall m>n[\alpha (m)=0]\}\).
\(D_{\alpha }\) is finite if and only if \(\alpha \in \mathbf{Fin}\).
Note: \(\alpha \in \mathbf{Fin}\) if and only if we can calculate the number of elements of \(D_{\alpha }\).
Definition 36
For every \(\mathcal{X}\subseteq \mathcal{N}\), we define:
\(\mathcal{X}^{+}:=\{\alpha \mid \exists n\forall m>n [\alpha (m)\neq 0 \rightarrow \alpha \in \mathcal{X}]\}\).
\(D_{\alpha }\) is perhaps-perhaps-finite if and only if \(\alpha \in \mathbf{Fin}^{++}=(\mathbf{Fin}^{+})^{+}\),
Some examples are useful.
1. Define \(\alpha \) such that \(\forall n[\alpha (n)\neq 0\leftrightarrow n=k_{99}]\). Then \(\{k_{99}\}=\{n\mid n=k_{99}\}\) is a decidable subset of ℕ. The statement ‘\(\alpha \in \mathbf{Fin}\)’ is equivalent to ‘\(\exists n[n=k_{99}]\) or \(\forall n[n< k_{99}]\)’ and thus is reckless or hardy. We do know \(D_{\alpha }\) has at most one element, but we do not know if the number of elements of \(D_{\alpha }\) is 0 or 1.
On the other hand, \(\alpha \in \mathbf{Fin}^{+}\). For assume we find \(m\) such that \(\alpha (m)\neq 0\), then \(m=k_{99}\) and \(D_{\alpha }=\{m\}\) is finite. Therefore: \(\forall m[\alpha (m)\neq 0 \rightarrow \alpha \in \mathbf{Fin}]\) and: \(\alpha \in \mathbf{Fin}^{+}\).
2. Define \(\alpha \) such that \(\forall n[\alpha (n)\neq 0\leftrightarrow k_{99}\le n <2\cdot k_{99}]\). Again, the statement ‘\(\alpha \in \mathbf{Fin}\)’ is reckless, and again, \(D_{\alpha }\) is perhaps-finite, although, unlike in the case of example 1, we are unable to give an upper bound for the number of elements of \(D_{\alpha }\).
3. Let \(\gamma ,\delta \) be given and define \(\alpha \) such that \(\forall n[\alpha (n)\neq 0\leftrightarrow (n=k_{\gamma }\;\vee \;n=k_{\delta })]\), so \(D_{\alpha }=\{k_{\gamma }, k_{\delta }\}\). The reader may find out herself that \(D_{\alpha }\) is perhaps-perhaps-finite and that the statement: ‘\(D_{\alpha }\) is perhaps-finite’ may be reckless.
20.2 Extension into the Transfinite
The process of taking so-called ‘perhapsive extensions’ of the set \(\mathbf{Fin}\) may be continued into the transfinite.
Definition 37
We define a collection ℰ of subsets of \(\mathcal{N}\) by means of the following inductive definition.
(i)
\(\mathbf{Fin} \in \mathcal{E}\).
(ii)
For every \(\mathcal{X}\) in ℰ, also \(\mathcal{X}^{+}\in \mathcal{E}\).
(iii)
For every infinite sequence \(\mathcal{X}_{0}, \mathcal{X}_{1}, \ldots \) of elements of ℰ, such that, for each \(n\), \((\mathcal{X}_{n})^{+}\subseteq \mathcal{X}_{n+1}\), also \(\bigcup _{n}\mathcal{X}_{n} \in \mathcal{E}\).
(iv)
Clauses (i), (ii), (iii) produce all elements of ℰ.
Definition 38
For every \(\mathcal{X}\subseteq \mathcal{N}\), \(\mathcal{X}^{\neg }:=\mathcal{N}\setminus \mathcal{X}:=\{\alpha \mid \neg (\alpha \in \mathcal{X})\}\) and
\(\mathcal{X}^{\neg \neg }=(\mathcal{X}^{\neg })^{\neg }\).
Theorem 32
(i)
For all \(\mathcal{X}\) in ℰ, \(\mathbf{Fin}\subseteq \mathcal{X}\subseteq \mathbf{Fin}^{\neg \neg }\).
(ii)
For all \(\mathcal{X}\) in ℰ, for all \(\alpha \), \(\forall s[\alpha \in \mathcal{X}\leftrightarrow s\ast \alpha \in \mathcal{X}]\).
(iii)
For all \(\mathcal{X}\) in ℰ, \(\mathcal{X}\subsetneq \mathcal{X}^{+}\).
Proof
50 (i) The proof is by induction, following the definition of the class ℰ.
1. Obviously, \(\mathbf{Fin}\subseteq \mathbf{Fin}^{\neg \neg }\), see Sect. 11.2.
2. Assume \(\mathbf{Fin}\subseteq \mathcal{X}\subseteq \mathbf{Fin}^{\neg \neg }\). Assume \(\alpha \in \mathcal{X}^{+}\).
Find \(m\) such that \(\forall n>m[\alpha (n)\neq 0 \rightarrow \alpha \in \mathcal{X}\) and distinguish two cases:
Case (a). \(\exists n>m[\alpha (n)\neq 0]\). Then \(\alpha \in \mathcal{X}\) and, therefore: \(\alpha \in \mathbf{Fin}^{\neg \neg }\).
Case (b). \(\neg \exists n>m[\alpha (n) \neq 0]\). Then \(\forall n>m[\alpha (n)=0]\), so \(\alpha \in \mathbf{Fin}\subseteq \mathbf{Fin}^{\neg \neg }\).
We thus see: if \(\exists n>m[\alpha (n)\neq 0]\;\vee \;\neg \exists n>m[\alpha (n) \neq 0]\), then \(\alpha \in \mathbf{Fin}^{\neg \neg }\).
We may conclude: \(\alpha \in \mathbf{Fin}^{\neg \neg }\), see Sect. 11.2.
We thus see: \(\forall \alpha \in \mathcal{X}^{+}[\alpha \in \mathbf{Fin}^{\neg \neg }]\), and conclude: \(\mathbf{Fin}\subseteq \mathcal{X}\subseteq \mathcal{X}^{+}\subseteq \mathbf{Fin}^{\neg \neg }\).
3. Assume: for all \(n\), \(\mathbf{Fin}\subseteq \mathcal{X}_{n}\subseteq \mathbf{Fin}^{\neg \neg }\). Clearly, then \(\mathbf{Fin}\subseteq \bigcup _{n} \mathcal{X}_{n}\subseteq \mathbf{Fin}^{\neg \neg }\).
(ii) We again use induction on the definition of the class ℰ.
1. Note: \(\forall \alpha \forall s[\alpha \in \mathbf{Fin}\leftrightarrow s \ast \alpha \in \mathbf{Fin}]\).
2. Let \(\mathcal{X}\) in ℰ be given such that \(\forall \alpha \forall s[\alpha \in \mathcal{X}\leftrightarrow s \ast \alpha \in \mathcal{X}]\). Let \(s,\alpha \) be given. If \(s\ast \alpha \in \mathcal{X}^{+}\), find \(m\) such that \(\forall n>m[s\ast \alpha (n)\neq 0\rightarrow s\ast \alpha \in \mathcal{X}]\) and conclude: for all \(n>m\), if \(\alpha (n)\neq 0\) then \(length(s)+n >m\) and \(s\ast \alpha \in \mathcal{X}\) and \(\alpha \in \mathcal{X}\), i.e. \(\alpha \in \mathcal{X}^{+}\). Conversely, if \(\alpha \in \mathcal{X}^{+}\), find \(m\) such that \(\forall n>m[\alpha (n)\neq 0\rightarrow \alpha \in \mathcal{X}]\) and conclude: for all \(n>m+length(s)\), if \(s\ast \alpha (n)\neq 0\), then \(\alpha \bigl (n-length(s)\bigr )\neq 0\) and \(n-length(s)>m\) and \(\alpha \in \mathcal{X}\) and \(s\ast \alpha \in \mathcal{X}\), i.e. \(s\ast \alpha \in \mathcal{X}^{+}\).
3. Assume: for all \(n\), \(\forall \alpha \forall s[\alpha \in \mathcal{X}_{n} \leftrightarrow s \ast \alpha \in \mathcal{X}_{n}]\).
Clearly, then \(\forall \alpha \forall s[\alpha \in \bigcup _{n}\mathcal{X}_{n} \leftrightarrow s\ast \alpha \in \bigcup _{n}\mathcal{X}_{n}\).
(iii) We shall prove: for all \(\mathcal{X}\) in ℰ there exists a spread ℱ such that \(\mathcal{F}\subseteq \mathcal{X}^{+}\) and not \(\mathcal{F}\subseteq \mathcal{X}\). The proof is by induction, following the definition of the class ℰ.
1. Consider \(\mathcal{T}=\{\alpha \mid \forall m\forall n[\bigl (\alpha (m)\neq 0 \;\wedge \;\alpha (n)\neq 0\bigr )\rightarrow m=n]\}\).
Note that \(\mathcal{T}\) is a spread. Note that, for every \(\alpha \) in \(\mathcal{T}\), for every \(n\), if \(\alpha (n)\neq 0\), then \(\forall m>n[\alpha (m)=0]\) and \(\alpha \in \mathbf{Fin}\). We thus see: \(\mathcal{T}\subseteq \mathbf{Fin}^{+}\)
Now assume \(\mathcal{T}\subseteq \mathbf{Fin}\). Then \(\forall \alpha \in \mathcal{T}\exists n\forall m>n[\alpha (m)=0]]\).
Using Theorem 29, find \(p,n\) such that \(\forall \alpha \in \mathcal{T}[\overline{\underline{0}}p\sqsubset \alpha \rightarrow \forall m>n[\alpha (m)=0]]\).
Conclude: \(n+1\ge p\) and consider \(\alpha :=\overline{\underline{0}} (n+1)\ast \langle 1 \rangle \ast \underline{0}\).
Note: \(\alpha \in \mathcal{T}\), \(\overline{\underline{0}}p\sqsubset \alpha \) and \(\alpha (n+1)\neq 0\).
Clearly, we reached a contradiction.
2. Let \(\mathcal{X}\) in ℰ be given and let ℱ be a spread such that \(\mathcal{F}\subseteq \mathcal{X}^{+}\) and not \(\mathcal{F}\subseteq \mathcal{X}\). Define \(\mathcal{F}^{\ast }:=\{\alpha \mid \forall n \forall p\forall \beta [ \alpha =\overline{\underline{0}}n\ast \langle p+1\rangle \ast \beta \rightarrow \beta \in \mathcal{F}]\}\).
Note: \(\mathcal{F}^{\ast }\) is a spread and \(\underline{0} \in \mathcal{F}^{\ast }\).
Note that, for every \(\alpha \) in \(\mathcal{F}^{\ast }\), for every \(n\), if \(\underline{\overline{0}}n\sqsubset \alpha \) and \(\alpha (n)\neq 0\), then there exists \(\beta \) in ℱ such that \(\alpha =\overline{\alpha }(n+1)\ast \beta \), and by (ii), also \(\alpha \in \mathcal{F}\) and \(\alpha \in \mathcal{X}^{+}\).
We thus see: \(\mathcal{F}^{\ast }\subseteq \mathcal{X}^{++}\).
Now assume \(\mathcal{F}^{\ast }\subseteq \mathcal{X}^{+}\).
Then \(\forall \alpha \in \mathcal{F}^{\ast }\exists n\forall m>n[ \alpha (m) \neq 0\rightarrow \alpha \in \mathcal{X}]\). Using Theorem 29,
find \(p,n\) such that \(\forall \alpha \in \mathcal{F}^{\ast }[\overline{\underline{0}}p \sqsubset \alpha \rightarrow \forall m>n[\alpha (m)\neq 0\rightarrow \alpha \in \mathcal{X}]]\).
We may assume \(n+1>p\). Note that, for each \(\beta \) in ℱ, \(\overline{\underline{0}}n\ast \langle 1\rangle \ast \beta \in \mathcal{F}^{\ast }\) and: \(\overline{\underline{0}}n\ast \langle 1\rangle \ast \beta \in \mathcal{X}\), and by (ii), \(\beta \in \mathcal{X}\).
We thus see: \(\mathcal{F}\subseteq \mathcal{X}\) and we know that this leads to a contradiction.
Conclude: not: \(\mathcal{F}\subseteq \mathcal{X}^{+}\).
3. Let \(\mathcal{X}_{0}, \mathcal{X}_{1},\ldots \) be an infinite sequence of elements of ℰ such that, for each \(n\), \((\mathcal{X}_{n})^{+}\subseteq \mathcal{X}_{n+1}\), and let \(\mathcal{F}_{0}, \mathcal{F}_{1}, \ldots \) be an infinite sequence of spreads such that, for each \(n\), \(\mathcal{F}_{n}\subseteq (\mathcal{X}_{n})^{+}\subseteq \mathcal{X}_{n+1}\) and not \(\mathcal{F}_{n}\subseteq \mathcal{X}_{n}\).
Define \(\mathcal{F}^{\ast }:=\{\alpha \mid \forall n\forall p\forall \beta [ \alpha =\underline{\overline{0}}n\ast \langle p+1\rangle \ast \beta \rightarrow \beta \in \mathcal{F}_{n}\}\).
Note: \(\mathcal{F}^{\ast }\) is a spread and \(\underline{0}\in \mathcal{F}^{\ast }\).
Note that, for every \(\alpha \) in \(\mathcal{F}^{\ast }\), for every \(n\), if \(\overline{\underline{0}}n\sqsubset \alpha \) en \(\alpha (n)\neq 0\), then there exists \(\beta \) in \(\mathcal{F}_{n}\subseteq \mathcal{X}_{n+1}\) such that \(\alpha =\overline{\alpha }(n+1)\ast \beta \), and by (ii), also \(\alpha \in \mathcal{X}_{n+1}\subseteq \bigcup _{i}\mathcal{X}_{i}\).
We thus see: \(\mathcal{F}^{\ast }\subseteq (\bigcup _{i}\mathcal{X}_{i})^{+}\).
Now assume: \(\mathcal{F}^{\ast }\subseteq \bigcup _{i}\mathcal{X}_{i}\). Using Theorem 29, find \(p,i\) such that
\(\forall \alpha \in \mathcal{F}^{\ast }[\overline{\underline{0}}p \sqsubset \alpha \rightarrow \alpha \in \mathcal{X}_{i}]\). Define \(n:=\max (p,i)\) and note: for all \(\beta \) in \(\mathcal{F}_{n}\), \(\overline{\underline{0}}n\ast \langle 1 \rangle \ast \beta \in \mathcal{F}^{\ast }\), so \(\overline{\underline{0}}n\ast \langle 1 \rangle \ast \beta \in \mathcal{X}_{i}\), and, by (ii), also \(\beta \in \mathcal{X}_{i}\).
We thus see: \(\mathcal{F}_{n} \subseteq \mathcal{X}_{i}\subseteq \mathcal{X}_{n}\). Contradiction. □
Theorem 32 shows the expressive power of the language of intuitionistic mathematics. In Theorem 32(i) the set \(\mathbf{Fin}^{\neg \neg }\) might be replaced by the set as one may prove: \(\bigcup \mathcal{E}\subseteq \mathbf{AlmostFin}\).
$$ \mathbf{AlmostFin}:=\{\alpha \mid \forall \zeta \in [\omega ]^{\omega }\exists n[\alpha \circ \zeta (n)=0]\}, $$
Using Theorem 22, one may prove: \(\mathbf{AlmostFin}\subseteq \bigcup \mathcal{E}\subseteq \mathbf{Fin}^{\neg \neg }\).
The set \(\mathbf{AlmostFin}\) is an example of a ‘simple’ \(\boldsymbol{\Pi }^{1}_{1}\) or co-analytic set that fails to be positively Borel, see [55, §3].
21 Avoiding Brouwer’s ‘Axioms’
21.1 Bishop-Style Constructivism
E. Bishop (1928-1983) started his own school of constructive mathematics in the 1960s, see [3] and [4]. Although Bishop admired Brouwer for his criticism of the non-constructive nature of much of mathematics, and for his heroic attempt to do something about it, he also had strong hesitations about Brouwer’s work. He did not accept Brouwer’s adoption of the Continuity Principle and the Fan Theorem. He thought the arguments in favour of these principles bizarre, metaphysical and mystical and judged that Brouwer, by bringing them in, had spoiled his own good cause. He declared Brouwer’s intuitionism to be dead and wanted a new beginning.
Nevertheless, developing his constructive mathematics, he felt the need for some of the consequences of Brouwer’s principles.
Bishop’s course was the following. He declared the notion of ‘pointwise continuity’ of real functions to be ‘irrelevant’. There is no need then for arguments as given in Sect. 12. He defined a function from ℛ to ℛ to be continuous if and only if it is uniformly continuous on every closed and bounded subinterval of ℛ. He thus buys for nothing what was for Brouwer the main consequence of the Fan Theorem, Theorem 16. There is no need then for arguments ‘proving’ the Fan Theorem as given in Sect. 13.51
Bishop’s attitude might perhaps be called ‘pragmatic’ in view of Brouwer’s more deeply going analysis of mathematical thinking. The principles proposed by Brouwer, even if one does not want to subscribe to the way he defends them, deserve to be discussed as possible starting points for our common mathematical discourse. Not doing so, Bishop denied himself the possibility of a further going perspective.
Bishop calls his own attitude realistic, contrasting it with the attitude of the ‘classical’ mathematician who uses non-constructive arguments. Unlike Brouwer, he does not fiercely attack the classical mathematician but calls him ‘idealistic’. In view of Sect. 3.2, where the platonists were dubbed ‘realists’, this terminology is funny.
21.2 Martin-Löf’s ‘Constructive Mathematics’
P. Martin-Löf made a serious study of Brouwer’s work and came to the following view in [42]. Every object in constructive mathematics should be given by a ‘a finite configuration of signs’. Therefore, an infinite sequence \(\alpha \) of natural numbers always should be given by a (finitely given) algorithm. Creating \(\alpha \) by choosing its values \(\alpha (0), \alpha (1), \ldots \) one-by-one in an infinite process of free choices, as Brouwer wanted to do, is out of the question. As we saw in Sect. 13.3, the Fan Theorem fails in such a context. Nevertheless, Martin-Löf formulates and upholds a ‘Fan Theorem’. His strategy is similar to Bishop’s as sketched in the previous Subsection. He redefines the meaning of the statement ‘\(\forall \alpha \in \mathcal{C}\exists n[\overline{\alpha }n \in B]\)’. Presenting his definition somewhat freely, one might say: he proposes to define ‘\(\forall \alpha \in \mathcal{C}\exists s \in B[s\sqsubset \alpha ]\)’ as: ‘there exists a canonical proof of ‘\(\langle \;\rangle \) is \(B\)-secure’ as we explained this in Sect. 13. Martin-Löf extends this strategy to the Bar Theorem, see the proof of Theorem 19.
21.3 An Application
The Fan Theorem and Brouwer’s Continuity Principle are used for a reconstruction of Cantor’s Uniqueness Theorem in [63].
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.