# Troelstra's Paradox and Markov's Principle

Mark van Atten

► To cite this version:

Mark van Atten. Troelstra's Paradox and Markov's Principle. 2016. hal-01415603

HAL Id: hal-01415603

https://hal.science/hal-01415603

Preprint submitted on 13 Dec 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Troelstra's Paradox and Markov's Principle

Mark van Atten*

December 13, 2016

## 1 Introduction

A prominent problem for the Theory of the Creating Subject is Troelstra's Paradox. As is well known, the construction of that paradox depends on the acceptability of a certain impredicativity, of a kind that some intuitionists accept and others do not. After a presentation of the Theory of the Creating Subject and the paradox, I argue that the paradox moreover depends on Markov's Principle, in a form that no intuitionist should accept. A postscript discusses a new version of the paradox that Troelstra has proposed in reaction to my argument.

## 2 The Theory of the Creating Subject

Brouwer's intuitionism as he developed it is first of all a theoretical model for our activity of making mathematical constructions. Like most other varieties of constructivism but unlike finitism, the mathematician who carries out mathematical constructions in his mind is conceived of in an idealised way. For example, Brouwer accepts the natural numbers as a potentially infinite sequence, of which any initial segment can always be extended, yet it is an an empirical fact that no actual human mathematician can do so, as a human life comprises only finitely many acts.

It is certainly possible to study what unidealised humans can and cannot construct. One may call that the study of feasible constructions. But there is also the idea that limitations on the length of one's life and, similarly, on the strength of one's memory or on one's accuracy in doing mathematics, do not touch on what mathematical constructions as such are. On the other hand, the observed property of our mind that we cannot complete infinitely many acts is taken to correspond to a characteristic property of mathematical constructions, namely that they cannot have an actual infinity of parts. This is a theoretical stance according to which some of the observed properties of

<footnote>* SND (CNRS / Paris IV), 1 rue Victor Cousin, 75005 Paris, France. vanattenmark@gmail.com. A version of this paper will be published in the volume *Dutch Significs and Early Criticism of the Vienna Circle* (G. Alberts, L. Bergmans, and F. Muller, eds), which includes a part on Brouwer and his philosophy. Closely related work in progress titled 'Kripke's Schema, transfinite proofs, and Troelstra's Paradox' will be published in a special issue of *Indagationes Mathematicae* dedicated to Brouwerian topics.</footnote>
our minds are taken to be essential to what a mathematical construction is,
and others are not.

The stance that Brouwer assumes is of a kind with Turing's, who devised
his theoretical analysis of (mechanical) computation in terms of an idealised
human, not a machine; Gandy proposed the term 'computor' [20, sections
10.1 and 10.3]. Brouwer's theoretical stance is also of a kind with Chom-
sky's, who gave his theoretical analysis of grammar in terms of an idealised
speaker/listener. To put it in Chomsky's terms, these theories of constructiv-
ity, computability, and grammaticality are all theories of competence and not
of performance.<fnref n="1" /> Chomsky describes competence as follows:

Linguistic theory is concerned primarily with an ideal speaker-listener,
in a completely homogeneous speech-community, who knows its
language perfectly and is unaffected by such gramatically irrelevant
conditions as memory limitations, distractions, shifts of attention
and interest, and errors (random or characteristic) in applying his
knowledge of the language in actual performance [17, p.3]

Brouwer first thematised the idealised constructor in 'Willen, Weten,
Spreken' [8], a lecture held in 1932 (and published in 1933):<fnref n="2" />

If on the basis of rational reflection the exactness of mathematics,
in the sense of impossibility of misunderstanding and error, cannot
be assured in any linguistic way, the question arises whether this
assurance can be found by other means. The answer to this question
must be that the languageless constructions originating in the self-
unfolding of the primordial intuition, on the basis of their presence
in memory alone, are exact and correct; that, however, the human
power of memory, which has to oversee these constructions, by its
very nature is limited and fallible. In a human mind empowered with
unlimited memory therefore pure mathematics, practised in solitude
and without the use of linguistic symbols would be exact. [33, p. 427,
translation Van Stigt]

<footnote n="1">1. The claim that Brouwer's intuitionism should be understood as a theory of competence I made in [1]; see also [21, 148-151]. I have since found an earlier and much more elaborate paper defending the position that Brouwer and Chomsky operate with similar idealisations, [22, esp. pp.234-235].</footnote>

<footnote n="2">2. Brouwer not the first to think of mathematics in terms of an ideal mathematician, with eternal life and unlimited memory, and who observed his own actions; so had Moritz Pasch in [31].</footnote>
The term ‘Creating Subject’ (Dutch: *scheppend subject*) was introduced in print in ‘Essentieel negatieve eigenschappen’ [10].

One may think of the Creating Subject as a generalisation *avant la lettre* of Turing's computor: the generalisation consisting in the fact that the Creating Subject is not limited to making mechanical calculations, but can also engage in constructions that are potentially infinite, that depend on free choices, or on reflection on its own acts. Brouwer noticed that the Creating Subject can register not only what objects it has created so far but also how and when, and that this reflection can be exploited to demonstrate mathematical theorems. An example is Brouwer's argument published in [10] to the conclusion that we have at present no evidence for

$$ \forall x \in \mathbb{R}(x \neq 0 \rightarrow x \neq 0) $$

where the number sign or octothorpe is apartness:

$$ a \# b \equiv \exists k \in \mathbb{N} \left( |a - b| > \frac{1}{2^k} \right) $$

His argument, slightly simplified, ran as follows.

Let $p$ be a proposition that cannot, as yet, be decided, that is, for which we for the moment have no method to establish either $p$ or $\neg p$.<fnref n="3" />

The Creating Subject constructs a real number $\alpha$ in a choice sequence of rational numbers $\alpha_n$, as follows:

* As long as, when making the choice of $\alpha_n$, the Creating Subject has obtained evidence neither of $p$ nor of $\neg p$, $\alpha_n$ is chosen to be $0$.

* If between the choice of $\alpha_{n-1}$ and $\alpha_n$, the Creating Subject has obtained evidence of $p$, $\alpha_n$ and all $\alpha_{n+k}$ ($k = 1, 2, ...$) are chosen to be $(\frac{1}{2})^n$.

* If between the choice of $\alpha_{n-1}$ and $\alpha_n$, the Creating Subject has obtained evidence of $\neg p$, $\alpha_n$ and all $\alpha_{n+k}$ ($k = 1, 2, ...$) are chosen to be $-(\frac{1}{2})^n$.

<footnote n="3">³ In his actual argument, Brouwer used an *untested* proposition, that is, one for which we at the moment have no method to establish either $\neg p$ or $\neg \neg p$. This is because he not only wanted to show that inequality does not amount to apartness, but also that inequality cannot be defined as a disjunction of < and >, which for Brouwer are negatively defined notions. See, e.g., [5, p. 461] and [7, pp. 8-9].</footnote>
The choice sequence $\alpha$ converges, hence $\alpha$ is a real number. We have

$$ \alpha = 0 \leftrightarrow \neg p \wedge \neg\neg p $$

Hence the Creating Subject knows that $\alpha \neq 0$. But also

$$ \alpha \# 0 \leftrightarrow \exists n \alpha_n \# 0 \leftrightarrow p \vee \neg p $$

So as long as $p$ can not be decided, we cannot prove $\alpha \# 0$.

This is a weak counterexample to $\forall x \in R(x \neq 0 \rightarrow x \# 0)$. However, using the fan theorem in a somewhat more complicated argument, Brouwer also showed that not only is there little hope of ever showing $\forall x \in R(x \neq 0 \rightarrow x \# 0)$, it is contradictory [II]:

$$ \neg\forall x \in R(x \neq 0 \rightarrow x \# 0) $$

Note that $\forall x \in R(x \neq 0 \rightarrow x \# 0)$ is equivalent to Markov's Principle (in the form relevant to my present purpose; there are really a number of closely related ones):

$$ \neg\neg\exists n.\alpha(n) = 1 \rightarrow \exists n.\alpha(n) = 1 $$

where $\alpha$ is a variable for infinite sequences [36, vol. I, 205-206].

The validity of Markov's Principle obviously depends on what kind of sequences it is meant to apply to.<fnref n="4" /> Markov devised it for recursive se-

<footnote n="4">4. There is an argument according to which the validity of Markov's Principle has nothing to do with what kind of sequences it is meant to apply to, but only with the structure of the natural numbers: As we can generate the natural numbers one after the other, in their natural order, then if it is impossible that there is no natural number with a certain decidable property P, there must be one, and we must find it by simply going through the series of natural numbers, because, by hypothesis, it is impossible that we will not. It has been debated whether this consideration is sufficient to fulfill the requirements for a constructive existence claim. Be that as it may, there is another consideration to be made. As recalled further on in the text, there is an argument against the validity of Markov's Principle for lawless sequences. The explanation of this apparent contradiction is that the first argument, in abstracting from differences in kind between sequences, also presupposes that, if there is a proof of the antecedent of (an instance of) Markov's Principle. that proof does not depend on information that distinguishing different kinds might give. The counterargument for lawless sequences, on the other hand, depends on precisely such information; so that, when in these two arguments it is assumed that we have a proof of the antecedent, the content of this assumption is not the same in both</footnote>
quences, in which case, to my mind, it is highly plausible. First note that on
the Brouwerian conception of logic, $p \to q$ means 'Whenever a construction
for p has been effected, it can be continued into a construction for q'. *That*
a construction for p has been effected may of course be wholly hypotheti-
cal. So on this conception, to assume that we have proved $\neg\neg\exists x\alpha(x) = 1$
is to assume that we have shown that the hypothesis that we have proved
$\neg\exists x\alpha(x) = 1$ leads to a contradiction. On the basis of what kind of in-
formation can we have done this? In the case of recursive $\alpha$, such a proof
must proceed either from the initial segment so far, or from the function
that determines $\alpha$; proofs of the first type can be converted into proofs of
the second type. All information present is first-order, in the sense that it
is directly concerned with the elements of the sequence themselves. But if
information that contradicts the absence of a 1 in the sequence is first-order,
then it seems it should be information that there is a 1 in the sequence.

While that plausibility argument needs further investigation, it is clear
that Markov's Principle, which was certainly not devised for lawless se-
quences, does not hold for them. A lawless sequence is one for which the
choices of its elements may never be restricted. In other words, there is a
second-order restriction that there be no first-order restriction. Let $\alpha$ be a
lawless sequence in which no 1 has been chosen yet. Then the antecedent
of Markov's Principle holds, because a future choice of 1 in $\alpha$ can, because
$\alpha$ is lawless, not be ruled out. But the consequent cannot be shown to hold
now, as the future choice of a 1 in $\alpha$ cannot be guaranteed, again because $\alpha$ is
lawless. Hence the consequent does not follow from the antecedent.

Creating subject arguments have not been universally accepted even
among intuitionists. The problem, as many saw and see it, is that here a
mathematical conclusion is drawn from considerations on something that
seems to be non-mathematical, namely, the activity of some ideal mathe-
matician. Brouwer's theorems would seem to depend on what happens, and
when, in some domain outside mathematics. It is this objection that Heyt-
ing makes in his book *Intuitionism. An Introduction* of 1956. He discusses
Brouwer's arguments in a chapter titled 'Controversial subjects'; would that
be a pun on 'Creating subject'? The same objection is made by Kleene in his
joint book with Vesley, *The Foundations of Intuitionistic Mathematics* of
1965 [26, p. 175].

Then Kreisel made the proposal – the ‘salutary proposal’, as he might
have put it – to analyse Brouwer’s arguments and make explicit the exact
properties of the Creating Subject that Brouwer used to construct his coun-

<footnote>cases. The intuitionistic approach, it seems to me, is to honour such distinctions.</footnote>
terexamples. Thus, in 1967 Kreisel presented the axioms of his so-called
'Theory of the Creating Subject' [27]. The idea is that the Creating Subject
carries outs its constructive activities in an ω-sequence of stages. This is not
made explicit by Brouwer, but is implied when he says that intuitionistic
mathematics '[comes] into being by "self-unfolding" of the basic intuition
of mathematics' [9]. This ensures that at any given moment, only finitely
many constructions will have been carried out, with an open horizon for
further ones. Against this background, Kreisel formulates three schemata
involving the propositional operator □<sub>n</sub> p, meaning 'At stage n the Creating
Subject has evidence for asserting p'. The way to obtain evidence for assert-
ing p is to carry out an appropriate mental construction process such that
the constructed objects and relations are correctly described by the proposi-
tion p.

$$
(\mathbf{CS1}) \qquad \forall n (\Box_n p \lor \neg \Box_n p)
$$

At any stage, it is decidable for the Creating Subject whether it has evidence
for asserting p.

$$
(\mathbf{CS2}) \qquad \forall n \forall m (\Box_n p \to \Box_{n+m} p)
$$

Once the Creating Subject has evidence for asserting p, it will always have
this.

$$
(\mathbf{CS3}) \qquad p \leftrightarrow \exists n \Box_n p
$$

A proposition p is true if and only if the Creating Subject has evidence for
asserting it at some stage.

Kreisel's original setup and notation were slightly different. He wrote
Σ ⊢<sub>m</sub> A where Σ is a variable for thinking subjects [27, p.159]. Most later
discussions assume only one thinking subject, the idea being that mathe-
matics is such that in principle a single subject could construct all of it. Also,
the ⊢ rather suggests formal derivability, which is not what is meant. Finally,
Kreisel did not have CS<sub>3</sub> but (specialised to one subject) the weaker

$p \rightarrow \neg\neg\exists n \Box n p \wedge \exists n \Box n p \rightarrow p$

But in a moment I will argue that the stronger, now common version CS₃ is
indeed correct on Brouwer's views.
These schemata are easily justified from a Brouwerian point of view.

CS1: If n is in the past, the subject inspects its perfect memory; if n is in the future, it can postpone its decision for the finite number of stages required and then check again.

CS2: This just makes the presence of perfect memory explicit. When Brouwer made his first remark about the ideal mathematician in print, in his article 'Volition, knowledge, speech' of 1933, it was notably the perfect memory that he emphasised (see above, p. 2).

CS3: Recall that for Brouwer, mathematics is first of all a mental activity, and has no independent existence. So if a mathematical object exists, this can only be because at some point the Creating Subject constructed it. Similarly, the only ground on which a mathematical proposition can be evident to the Subject, and therefore true, is that the Creating Subject at some point constructed objects and relations between them that made that proposition evident. This is why Brouwer wrote, 'truth is only in reality i.e. in the present and past experiences of consciousness ... there are no non-experienced truths' [12, p. 1243]. So 'p is true' means 'A construction for p *has been made*'; and 'Assume that p is true' means 'Assume that a construction for p *has been made*'.<fnref n="5" /> And whenever the subject has actually effected a construction for p, it has done so at a particular moment in time; and when it is assumed that the subject has effected a construction for p, it must also be assumed that it did so at a particular moment in time. CS3, read from left to right, simply says that the Creating Subject can make that moment explicit.

A common and let us say more enthusiastic understanding of CS3, from left to right, is that it claims that 'If p is true, whether the subject now knows this or not, then at some point the subject *will* have evidence for asserting it'. But as a reading of Brouwer, this is misguided, because it presupposes that truths may exist before the subjects knows them, before the subject has experienced them, and this is incompatible with Brouwer's characterisation of truth.

### 3 Troelstra's Paradox

#### 3.1 The paradox stated

Although these principles seem evident, soon after Kreisel's publication Anne Troelstra found a paradox in the Theory of the Creating Subject. As Troelstra informed me, he told Kreisel about it at the conference 'Intu-

<footnote n="5">5. This is different from Natural Deduction. See the discussion in [34].</footnote>
itionism and Proof Theory' in Buffalo in 1968;<fnref n="6" /> neither Troelstra nor I are
aware of a published comment by Kreisel on the paradox. Troelstra included
the paradox in his *Principles of Intuitionism*, which came out in 1969 [35,
pp. 105–106]; I will use here the slightly different version in *Constructivism in
Mathematics* [36, vol. 2, p. 845].

As the Paradox depends on a diagonal argument, we may first recall the
familiar diagonal argument to the effect that the total recursive functions are
not enumerable by a total recursive function. For assume that there is such
an enumeration $f_n$. Define the function

$$g := \lambda n. f_n(n) + 1$$

So $g$ takes the diagonal of the enumeration and adds $1$ to each number on it. On the assumption that the enumeration $f$ exists, $g$ is a total recursive function, and should itself be somewhere in the enumeration: $g = f_k$ for some $k$. But then $g(k) = f_k(k) = f_k(k) + 1$, contradiction.

Now instead of total recursive functions, take choice sequences fixed by a recipe, perhaps by explicit reference to the stages of the Creating Subject's activity. 'Fixed by a recipe' is the term that Troelstra uses.<fnref n="7" /> It certainly includes the total recursive functions, but is much wider. It also includes sequences whose elements are fixed not by an algorithm, but relative to data that itself includes free choices. An example of such data is the record or log that lists each earlier stage of the Creating Subject's activity, together with the propositions that it made evident at that stage. Troelstra makes the assumption that at each stage $n$ the subject makes evident exactly one proposition $A^{(n)}$.

Troelstra then arrives at a paradox as follows.

consider statements of the form ‘$\alpha$ is a sequence in $N \to N$ fixed by a
recipe (possibly by explicit reference to the stages of the IM’s activity)’. By inspection the IM can see whether an $A^{(n)}$ is of this form or not, so we may enumerate all sequences appearing in this manner in some $\square_n A^{(n)}$; let $\beta_n$ be the $n$-th such sequence. Then

$$\gamma := \lambda n. \beta_n(n) + 1$$

is a sequence fixed by a recipe which therefore should appear at some

<footnote n="6">6. Email Troelstra to MvA, May 1, 2016.</footnote>

<footnote n="7">7. [The 1969 version has ‘lawlike’ instead of ‘fixed by a recipe’.]</footnote>
stage as $\beta_m$, say; but then $\beta_m(m) = \beta_m(m)+1$ gives a contradiction.
[36, vol. 2, p. 845]

## 3.2 Proposed solutions

### 3.2.1 Troelstra

The first solution Troelstra indicates is to drop the assumption that at each stage the subject makes evident exactly one proposition. The idea would be that, besides $A^{(n)}$, the Creating Subject makes various consequences of $A^{(n)}$ evident *implicitly*. But Troelstra argues [35, p. 106] that doing so is problematic, because by CS1 decidability is still required, and this constrains the closure condition that determines the range of the implicitly evident; for example, ‘derivability from $A^{(n)}$ in first-order predicate logic’ would not work.

Moreover, one might say that ‘one conclusion at a time’ is forced by the intuitionistic conception of the relation between language and mathematical constructions. Logic describes patterns in linguistic descriptions of mathematical construction activities, and the Creating Subject must be assumed to carry out its conscious constructions one at a time, like us, so as not to overidealise.<fnref n="8" />

The second part of the assumption, on the other hand, that each conclusion should be *new* is not what one should ask if the idealisations involved in the theory are only meant to place the subject in ideal circumstances. In fact Brouwer, in his proofs of the Bar Theorem, explicitly takes into account the possibility that in a canonical proof some conclusions are arrived at more than once.<fnref n="9" /> The strong condition of novelty on $A^{(n)}$ may in fact be lifted, as it does not actually play a role in the construction of the paradox.

Another solution by Troelstra consists in stratifying the constructions and propositions involving $\square_n$ according to the nesting of that operator involved. In the presentation of 1969 (where Kreisel’s notation $\vdash_n$) was used):

> Another possibility which is suggested by the 'paradox' is, that the primary cause of our trouble is not so much in the assumption of the 'one-conclusion-at-a-time' axiom, as well as in the unrestricted possibilities for self-reference implicit in our axioms for the creative

<footnote n="8">8. This point was forcibly made by Martino in [29, pp.313–314].</footnote>

<footnote n="9">9. While in the first proof, that of 1924 [3, 4], he proceeds by eliminating such detours, in the second proof, that of 1927 [6], he shows that you may just well leave them in.</footnote>
subject. Specifically: although assertions like $\vdash_n A$ and $\vdash_m (\vdash_n A)$ do belong to different 'levels of self-reflection' (self-reflection = mathematical consideration of the course of our own mathematical activities) we did not distinguish between them in this respect. [35, p. 106]

Indeed, by distinguishing levels of self-reflection, the sequence $\gamma$, defined in terms of the enumeration of the $\beta_n$, will be a construction of a higher level than they are, and $\gamma$ will therefore not occur among them. This solution was notably accepted by Dummett in *Elements of Intuitionism* [19, p. 347].<fnref n="10" /> Dummett adds the argument that such a stratification should be introduced even independently of Troelstra's paradox. The operator $\square$ is impredicative because there is no restriction on its appearances in the proposition it is applied to. Dummett claims that we can have no firm grasp of an impredicative notion. Yet, the solution was criticized by Troelstra and Van Dalen in 1988 [36, vol. 2, p. 845]. The reason for Troelstra's change of mind<fnref n="11" /> is that in certain cases, he wants to allow impredicative definitions of subsets in a species; e.g., to prove the existence of least upper bounds in the theory of the so-called extended reals.<fnref n="12" /> The crucial question here is whether constructive sense can be made of quantification over subsets that are not species. I will not investigate this further now, as the solution that I will develop is independent of the answer to this question. In that same discussion of 1988, Troelstra and Van Dalen write that 'the solution proposed by Niekus (1987) deserves further investigation' [36, vol. 2, p. 845].

### 3.2.2 Niekus

Niekus [30] proposes to modify the meaning of $\square_n$ by letting n range only over the future, and not also over past and present. We can then conclude *now* that $\gamma$ is fixed by a recipe; and because Niekus accepts Troelstra's restriction that the Creating Subject always draws a *new* conclusion at each stage, this conclusion will never show up again. As a consequence, the sequence $\gamma$ will not occur in the enumeration of the $\beta_n$. The insistence that the conclusion at each stage be new is essential to Niekus' solution, but not to Troelstra's (of stratification). Niekus' solution is therefore correspondingly more sensitive to the descriptive inadequacy of that restriction that I

<footnote n="10">10. Page 241 of the second edition (2000).</footnote>

<footnote n="11">11. Email Troelstra to MvA, February 2, 2014.</footnote>

<footnote n="12">12. The notion of an extended real is a weakening of that of a Dedekind real [36, vol. 1, p. 270].</footnote>
noted. Moreover, to my mind, the restriction that Niekus introduces on the
range of the subscripts n of □_n is ad hoc: If the Creating Subject is supposed
to have a perfect memory, which assures that evidence does not get lost, there
seems to be no other motivation for not including the past and present in
the range of the n than the fact that doing so blocks the paradox.

### 3.3 A new solution

My claim is that the sequence

$$ \gamma := \lambda n. \beta_n(n) + 1 $$

is constructively not well-defined not only at its intersection with the diagonal, but at every argument corresponding to a sequence in the future. This is so, because the construction of the sequence turns out to presuppose Markov's Principle, in a form that no intuitionist should accept. And as we will see, the ground on which the dependence on Markov's Principle arises remains present in both Troelstra's and Niekus' proposed solutions.

How would the subject know that the sequence $\gamma$ exists as sequence of the type $N \to N$? That would require that, for given $n$, the subject can determine, within finitely many steps, *what* the $n$-th sequence is of which it will prove that it is fixed by a recipe; and, by implication, it would require that the subject can determine, within finitely many steps, *by what stage* it will have begun constructing that sequence; for an object exists only if it has been constructed at some stage.

Assume that the Creating Subject has so far begun constructing a certain number of the sequences $\beta$. The subject can determine this number by consulting its perfect memory. Now the Subject has the freedom, at any particular absolute stage of its activity, to choose what construction it will work on. This also means that, at any particular absolute stage, it has the freedom *not* to work on a certain construction. But then it is impossible to put a bound on the absolute stage by which the Subject will have begun the construction of the next of these sequences $\beta$.

So the argument turns on the distinction between two kinds of bounds:

1. a bound on the number of stages needed to effect a certain construction, and

2. a bound on the absolute stage by which a certain construction must have been made.
A bound of the first kind is what is required for constructive well-definedness of an object,<fnref n="13" /> whereas bounds of the second kind are impossible, because of the freedom the Subject enjoys. The sequence $\gamma$, however, is defined in such a way that the existence of bounds of the first kind on the construction of each of its elements implies the existence of bounds of the second kind on the construction of each of the $\beta_n$. Hence, the assumed enumeration of the $\beta_n$ is not constructive, and for that reason, so even without considering the diagonal, neither is $\gamma$, into the definition of which that enumeration enters.

A different way of putting it is to say that for Troelstra's Paradox to work, one must accept a version of Markov's Principle. To relate the two, we introduce a bookkeeping device. Associate to each sequence $\beta_n$ a sequence $\beta_n^*$ such that $\beta_n^*(i)$ is 0 if by stage i the construction of $\beta_n$ has not yet begun, and 1 if it has.

By the argument I gave, we do not have, for each $n$,

$$ \exists k. \beta_n^*(k) = 1 $$

for the Creating Subject cannot be forced to begin constructing the sequence $\beta_n$ at a given stage $k$. On the other hand, we do have

$$ \neg\neg\exists k. \beta_n^*(k) = 1 $$

for it is absurd to assume that there will never be a stage at which the Creating Subject begins constructing the sequence $\beta_n$. This is because the same creative freedom that allows the subject to postpone the construction of a $\beta_n$ beyond any given bound also allows it to work diligently towards bringing that sequence about.

So for the sequences $\beta_n^*$ the antecedent of Markov's Principle holds, but the consequent does not. Hence Markov's Principle is not valid for those sequences. However, for the sequence $\gamma$ in Troelstra's Paradox to be well-defined, Markov's Principle should have been valid for the $\beta_n^*$. Although the sequences $\beta_n^*$ are not lawless, because the choices of their elements depend on other mathematical activity of the subject, the other activity in question does itself contain an element of free choice. So the argument is of course essentially the same as the well-known refutation of Markov's Principle for lawless sequences.

<footnote n="13">13. It is not required that, when carrying out that construction, these stages follow immediately upon one another.</footnote>
Both Troelstra's and Niekus' solution leave the dependence on Markov's Principle intact. Niekus' $\gamma$ with re-interpreted $\square_n$ is, even though it only concerns future constructions, still an enumeration of mathematical constructions depending on the stage at which they are constructed. And also Troelstra's stratification, while ruling out that $\gamma$ occurs among the $\beta_n$, still allows an enumeration of the $\beta_n$ themselves.

I should like to elaborate somewhat on the freedom the subject has in going about its constructive ways. As Brouwer once remarked in a letter to Van Dantzig,

> the intuitionistic Creating Subject can from the outset put restrictions (or prohibitions of restrictions) on a specific growing mathematical entity that is its creation, but not on its own possibilities of creation.<fnref n="14" />

Why can't the Creating Subject impose restrictions (of first or higher order) on its possibilities to create?

The Creating Subject is a hypothetical being; it is, by definition, the correlate on the subject side of all possible mathematical constructions on the object side. If it could limit itself, it would no longer be the Creating Subject. Note the analogy to the medieval arguments against 'divine self-limitation', which argue that an omnipotent God cannot make himself not omnipotent (or a maximally powerful God cannot make himself less than maximally powerful).

So however one wishes to fill in the details of the notion of intuitionistic possibility, if a certain construction is intuitionistically possible at all, then for that reason the Creating Subject is capable of carrying it out.<fnref n="15" /> A condition on the stage by which the Creating Subject has created a certain object, i.e., a bound of the second kind, is automatically a restriction on its possibilities to create, as the presence of such a condition means that constructions that at a given stage are possible without this condition will now be ruled

<footnote n="14">14. Brouwer to David van Dantzig, August 24, 1949 [16, p. 439; translation modified]. The original passage reads: 'Zoals ik je reeds mondeling zei, is mijn betrokken voorbeeld daarom voor het principieele intuïtionisme zooveel onaantastbaarder dan voor andersdenkenden, omdat het intuïtionistische scheppende subject wél aan een bepaalde groeiende wiskundige entiteit die zijn schepping is, doch niet aan zijn eigen scheppingsmogelijkheden bij voorbaat beperkingen (of beperkings-verboden) kan opleggen.' [16, online supplement, p. 2460]</footnote>

<footnote n="15">15. Correspondingly, actual human beings can instantiate, as far as it goes, the Creating Subject. But if, while doing so, they impose (further) limits on their (already limited) ability to create, they are no longer instantiating, however imperfectly, the Creating Subject.</footnote>
out if they do not meet it.

## 4 The subject's full inwardness

I will end by relating Troelstra's Paradox to a witty observation by Gödel. The story is told by Rudy Rucker in his book *Infinity and the Mind* [32, pp. 180–181]:

> Gödel seemed to believe that not only is the future already there, but worse, that it is, in principle, possible to predict completely the actions of some given person.

> I objected that if there were a completely accurate theory predicting my actions, then I could prove the theory false — by learning the theory and then doing the opposite of what it predicted. According to my notes, Gödel's response went as follows: 'It should be possible to form a complete theory of human behavior, i.e., to predict from the hereditary and environmental givens what a person will do. However, if a mischievous person learns of this theory, he can act in a way so as to negate it. Hence I conclude that such a theory exists, but that no mischievous person will learn of it. In the same way, time-travel is possible, but no person will ever manage to kill his past self.' Gödel laughed his laugh then, and concluded, 'The *a priori* is greatly neglected. Logic is very powerful.'

Gödel did not make this remark in the context of Brouwer's Creating Subject, but to some it may immediately suggest the following transposition: 'The enumeration of sequences fixed by a recipe that leads to problems in Troelstra's Paradox, an enumeration that would be a way of predicting part of the Creating Subject's future, does exist, but the Creating Subject will never learn of it, hence no contradiction arises.' Such an argument, in accepting the existence of a mathematical construction that the Creating Subject will never know, and hence that there is a proposition p for which $p \wedge \neg\exists n \Box_n p$ holds, is in effect a denial of schema CS₃ read from left to right, $p \rightarrow \exists n \Box_n p$, and even of $p \rightarrow \neg\neg\exists n \Box_n p$. But I have tried to argue that Troelstra's Paradox does not reach so far as to oblige one to give up the Theory of the Creating Subject; by itself, it cannot spoil appreciation of, to use a term that Kreisel liked, the Creating Subject's 'full inwardness'.
*Postscript, July 2016.* After the above had essentially been completed, Prof. Troelstra accepted, in an e-mail exchange, the objection developed there. He also presented a new version of the paradox, which he kindly permitted me to reproduce:

Let $b_n$ be defined for each natural number $n$ as follows. As long as the Creating Subject (CS) has not proved a statement $S(b')$ of the form 'b' is a well-defined sequence given by a recipe' up till and including stage $n$, we take $b_n$ to be the zero-function. And in general, $b_{n+1} = b_n$ if the CS at stage $n + 1$ does *not* establish a statement of the form $S(b')$. But if the CS establishes at stage $n + 1$ a statement $S(b')$ then take $b_{n+1}$ equal to $b'$.

Now the diagonal function which assigns to $n$ the value $b_n(n)$ is well-defined by a recipe relative to the activity of the CS (we just have to run through the first $n$ stages), and so is the function $f$ which assigns to each $n$ the value $b_n(n) + 1$. But this function differs at least at one argument from every function $b'$ for which the CS establishes at some stage $m$ the assertion $S(b')$, namely for the argument $m$.<fnref n="16" />

This second version of the paradox is designed to avoid the assumption that the $b_n$ are given by an enumeration; they cannot be numbered in advance, but to each well-defined sequence given by a recipe a different number can be assigned as it appears.<fnref n="17" /> The diagonal function, then, must be a growing object, too. However, I would argue that the existence of the diagonal function used in this version, and hence of $f$, is inconsistent with Brouwer's theory of species.<fnref n="18" />

In the *Cambridge Lectures*, which are contemporaneous with Brouwer's publications of Creating Subject arguments, Brouwer defines a species as

> properties supposable for mathematical entities previously acquired ...
> By the *elements* of a species we understand the mathematical entities
> previously acquired for which the property in question holds.

And in a footnote to this definition he points out that

<footnote n="16">16. Email Troelstra to MvA, June 27, 2016.</footnote>

<footnote n="17">17. In Brouwer's terminology, the species of the well-defined sequences given by a recipe is 'abzählbar', but not 'aufzählbar' [2, p. 7]. Dutch: 'opsombaar', not 'aftelbaar' [24, pp. 51-52]; English: 'denumerable', not 'enumerable' [18, p. 328].</footnote>

<footnote n="18">18. On the genesis of spreads and their relations to species, as developed by Brouwer over the years, Van Stigt's detailed discussion very useful [33, pp. 370-377].</footnote>
It follows that during the development of intuitionist mathematics some species may have to be considered as being tacitly defined again and again in the same way. [15, p. 8]<fnref n="19" />

Entities may be considered to have been ‘acquired’ either when the subject has explicitly constructed each of them individually, or when it has a method to generate them. But there are species of which the subject will never have acquired all elements in either of these two ways; for example, the species of real numbers. It is such species that have to be considered to be defined again and again in the same way, namely each time a further entity is acquired that possesses the property in question. Functions that have such a species for their domain will have to be defined again as well, as the definition of a function includes a specification of its domain. These redefinitions can be taken to occur ‘tacitly’ in the sense that although the domain changes each time (because it grows), the way in which the function acts on the elements of the domain remains the same.<fnref n="20" />

As a function defined on a species always acts on entities previously acquired, it cannot specify an element to be added to a species and depend on that element. In particular, to a species of sequences it is impossible to add as m-th element a sequence of which the m-th term is defined in terms of the m-th element. Therefore the diagonal function that figures in the new version of the paradox is, when considered as a sequence, not well-defined as an element of the species of the $b_n$, and, a fortiori, neither is the function $f$.

One can, of course, construct a diagonal function on the finite domain of the sequences $b_n$ constructed *so far*, but that function, considered as a sequence, lies outside its domain. Thus we see that the paradox in this second version is blocked by a stratification of constructions, as in the solution proposed by Troelstra in 1969 to the paradox in the first version. A difference is that the stratification here follows from the general concept of species and is not motivated by the paradox itself.

Finally, note that in my arguments, I do not question the notion of ‘given by a recipe’. On the contrary, it seems rather doubtful to me that it could be denied that the sequences ‘given by a recipe’ form a Brouwerian

<footnote n="19">19. Also [13, p. 142].</footnote>

<footnote n="20">20. In Heyting’s definition ‘After a species S has been defined, any mathematical entity which has been or might have been defined before S and which satisfies the condition S, is a *member* of the species S’ [25, p. 37], the phrase ‘or might have been’ hides the tacit redefinitions somewhat. Similar for Troelstra’s formulation in [35, p. 14]: ‘It will be clear that an element $x$ of $\mathcal{A}$ can only be admitted as an *element* of *member* of P* ($x \in P$) *if x has been or might have been defined before (independently of) P.’</footnote>
species. The point of my arguments is rather that in both versions of the
paradox, the way in which a contradiction in that notion is concluded to
is not correct. It will be clear that argumentation in this matter, be it for
or against the correctness of the paradox, is extraordinarily sensitive to the
exact understandings of even the most basic notions that one works with,
such as truth, implication, and species. Perhaps one can motivate a sense
of constructivity in which these notions are such that some version of the
paradox works; but in Brouwer I do not find such motivation.

*Acknowledgement*. I am grateful in particular to Anne Troelstra for a num-
ber of discussions, and also to Dirk van Dalen, Saul Kripke, Joan Moschovakis,
Yannis Moschovakis, Joop Niekus, Göran Sundholm, and Wim Veldman.
Versions of parts of this paper were presented at the conference 'Functions,
Proofs, Constructions', Tübingen, 2014; the 'Michael Dummett Paris Con-
ference', 2014; the 'Fifth Formal Topology Workshop', Mittag-Leffler In-
stitute, Djursholm, 2015; the 'PhilMath Intersem', Paris, 2015; 'Significa
néerlandaise et la critique précoce du Cercle de Vienne', Paris, 2015; at 'In-
tuitionism, Computation, and Proof: Selected themes from the research of
G. Kreisel', Paris, 2016; at 'Constructive Semantics', Friedrichshafen, 2016;
and at 'L.E.J. Brouwer, Fifty Years Later', Amsterdam, 2016. I thank the
audiences for their questions and comments.

References

[1] Mark van Atten. Intuitionistic remarks on Husserl's analysis of finite number in the Philosophy of Arithmetic. *Graduate Faculty Philosophy Journal*, 25(2):205-225, 2004.

[2] L.E.J. Brouwer. Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil, Allgemeine Mengenlehre. *KNAW Verhandelingen*, 5:1-43, 1918B.

[3] L.E.J. Brouwer. Bewijs dat iedere volle functie gelijkmatig continu is. *KNAW Verslagen*, 33:189-193, 1924D1. English translation [28, pp. 36-39].

[4] L.E.J. Brouwer. Bemerkungen zum Beweise der gleichmässigen Stetigkeit voller Funktionen. *KNAW Proceedings*, 27:644-646, 1924G2.

[5] L.E.J. Brouwer. Zur Begründung der intuitionistischen Mathematik, II. *Mathematische Annalen*, 95:453-472, 1926A.
[6] L.E.J. Brouwer. Über Definitionsbereiche von Funktionen. *Mathematische Annalen*, 97:60–75, 1927B. English translation of sections 1–3 in [23, pp. 457–463].

[7] L.E.J. Brouwer. Die Struktur des Kontinuums. Komitee zur Veranstaltung von Gastvorträgen ausländischer Gelehrter der exakten Wissenschaften, Wien, 1930A. English translation [28, pp. 54–63].

[8] L.E.J. Brouwer. Willen, weten, spreken. In L.E.J. Brouwer et al., editors, *De Uitdrukkingswijze der Wetenschap*, pages 45–63. Noordhoff, Groningen, 1933A2. English translation [33, pp. 418–431].

[9] L.E.J. Brouwer. Richtlijnen der intuïtionistische wiskunde. *Indagaciones Mathematicae*, 9:197, 1947. English translation [14, p. 477].

[10] L.E.J. Brouwer. Essentieel negatieve eigenschappen. *Indagaciones Mathematicae*, 10:322–323, 1948A. English translation [14, pp. 478–479].

[11] L.E.J. Brouwer. De non-aequivalentie van de constructieve en de negatieve orderelatie in het continuum. *Indagationes Mathematicae*, 11:37–39, 1949A. English translation [14, pp. 495–496].

[12] L.E.J. Brouwer. Consciousness, philosophy and mathematics. In E.W. Beth, H.J. Pos, J.H.A. Hollak, editors, *Proceedings of the 10th International Congress of Philosophy, Amsterdam 1948*, vol. 3, 1235–1249. North-Holland, Amsterdam, 1949C.

[13] L.E.J. Brouwer. Historical background, principles and methods of intuitionism. *South African journal of science*, 49:139–146, 1952B.

[14] L.E.J. Brouwer. *Collected works I. Philosophy and Foundations of mathematics*. North-Holland, Amsterdam, 1975.

[15] L.E.J. Brouwer. *Brouwer's Cambridge Lectures on Intuitionism*, ed. D. van Dalen. Cambridge University Press, Cambridge, 1981A.

[16] L.E.J. Brouwer. *The Selected Correspondence of L.E.J. Brouwer*. Springer, London, 2011. With an online supplement.

[17] N. Chomsky. *Aspects of the Theory of Syntax*. MIT Press, Cambridge, 1965.
[18] D. van Dalen. *Mystic, Geometer, and Intuitionist. The Life of L.E.J. Brouwer. 1: The Dawning Revolution*. Clarendon Press, Oxford, 1999.

[19] M. Dummett. *Elements of Intuitionism*. Oxford University Press, Oxford, 1977. (Second edition 2000.)

[20] R. Gandy. The confluence of ideas in 1936. In R. Erken, editor, *The Universal Turing Machine. A Half-Century Survey*, pages 51-102. Springer, Wien, 1995. (First edition 1988.)

[21] A. George. The conveyability of intuitionism, an essay on mathematical cognition. *Journal of Philosophical Logic*, 17(2):133-156, 1988.

[22] D. Gil. Intuitionism, transformational grammar and mental acts. *Studies in History and Philosophy of Science*, 14(3):232-254, 1983.

[23] J. van Heijenoort, editor. *From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879-1931*. Harvard University Press, Cambridge MA, 1967.

[24] A. Heyting. De telbaarheidspraedicaten van Prof. Brouwer. *naw*, 16:47-58, 1929.

[25] A. Heyting. *Intuitionism. An Introduction*. North-Holland, Amsterdam, 1956.

[26] S.C. Kleene and R.E. Vesley. *Foundations of Intuitionistic Mathematics*. North-Holland, Amsterdam, 1965.

[27] G. Kreisel. Informal rigour and completeness proofs. In I. Lakatos, editor, *Problems in the Philosophy of Mathematics*, pages 138-186. North-Holland, Amsterdam, 1967.

[28] P. Mancosu, editor. *From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s*. Oxford University Press, Oxford, 1998.

[29] E. Martino. Creative subject and bar theorem. In A.S. Troelstra and D. van Dalen, editors, *The L.E.J. Brouwer Centenary Symposium*, pages 311-318. North-Holland, Amsterdam, 1982.

[30] J. Niekus. The method of the creative subject. *KNAW Proceedings*, 90(4):431-443, 1987.
[31] Moritz Pasch. Der Ursprung des Zahlbegriffs. *Archiv der Mathematik und Physik*, pages 17–33, 1919.

[32] R. Rucker. *Infinity and the Mind*. Birkhäuser, Basel, 1983.

[33] W. van Stigt. *Brouwer's Intuitionism*. North-Holland, Amsterdam, 1990.

[34] G. Sundholm and M. van Atten. The proper explanation of intuitionistic logic: on Brouwer's proof of the Bar Theorem. In M. van Atten, P. Boldini, M. Bourdeau, and G. Heinzmann, editors, *One Hundred Years of Intuitionism (1907–2007). The Cerisy Conference*, pages 60–77. Birkhäuser, Basel, 2008.

[35] A. Troelstra. *Principles of Intuitionism*. Springer, Berlin, 1969.

[36] A. Troelstra and D. van Dalen. *Constructivism in Mathematics*, 2 vols. North-Holland, Amsterdam, 1988.