Mark Van Atten

Mark Van

Atten 2018 Weyl

Halshs-01730473v2

Weyl and intuitionistic infinitesimals

teaching and research institutions in France or abroad, or from public or private research centers.

Introduction

In the 1920s, Weyl doubted that non-Archimedean number systems could serve to develop real analysis with infinitesimals. 1 In his 'Philosophy of Mathematics and Natural Science' of 1926, Weyl advanced the following argument:

But once the limit concept has been grasped, it is seen to render the infinitely small superfluous. Infinitesimal analysis proposes to draw conclusions by integration from the behavior in the infinitely small, which is governed by elementary laws, to the behaviour in the large … If the infinitely small is not interpreted 'potentially' here, in the sense of the limiting process, then the one has nothing to do with the other, the processes in infinitesimal and in finite dimensions become independent of each other, the tie which binds them together is cut. Here Eudoxus undoubtedly saw right [in stating what became known as the Archimedean axiom]. [START_REF] Weyl | Philosophie der Mathematik und Naturwissenschaft. Leibniz Verlag[END_REF], 35-36/Weyl 1949, 44-45.) In the 1960s Abraham Robinson showed how to handle this fully in ZFC and classical model theory, introducing non-standard analysis with * SND (CNRS / Paris IV), 1 rue Victor Cousin, 75005 Paris, France. vanattenmark@gmail.com.

1. There are similar contemporary statements in e.g. Fraenkel 1929, 116-117 andSkolem 1929, 208. There are many studies of the history of infinitesimals, e.g., for the early history, [START_REF] Baron | The Origins of Infinitesimal Calculus[END_REF][START_REF] Mancosu | Philosophy of Mathematics and Mathematical Practice in the Seventeenth Century[END_REF][START_REF] Schubring | Conflicts between Generalization, Rigor, and Intuition[END_REF]. See Fletcher et al. 2017 for an overview of later approaches.

1 its transfer principle. This encouraged Edward Nelson to develop an approach likewise based on ZFC but axiomatic. Constructive versions of their theories have also been developed (yielding, as expected, in general somewhat weaker principles). But Weyl for some years embraced Brouwer's intuitionism, and continued to see it as a philosophical ideal even after he had convinced himself that it is a practical necessity for science to go beyond intuitionistic mathematics and adopt a formalist attitude. As Hans Freudenthal wrote in his obituary of his friend Weyl, He decides in favour of Brouwer's intuitionistic explanation of mathematics, but, averse to system-building, he spurns Brouwer's method that aims for generality. That is no treason, then the essence of his mathematics was and remained intuitionistic. [START_REF] Hermann Weyl | Der Dolmetscher zwischen Mathematikern und Physikern um die moderne Interpretation von Raum, Zeit und Materie[END_REF] quoted in van Dalen 2005, p.880n44, trl. mine)

After a brief look at classical approaches and constructivisations of them, I will discuss three attempts at introducing infinitesimals that were proposed as not only constructive but, in different ways, explicitly Brouwerian: one by early Brouwer, one by Vesley based on later Brouwer, and one by Reeb.

These will not be compared with more recent constructive versions of formalised nonstandard analysis as to their mathematical merits. 2 They are discussed primarily because they stay close to Weyl's own interest in both Brouwerian intuitionism and infinitesimals, but to some extent also for their own sake, as they remain among the lesser known. It would be very interesting to see a further mathematical development of Vesley's approach, as it is, by design, fully integrated in Brouwerian analysis with choice sequences; and Reeb's Brouwerian look at Nelson's classical nonstandard analysis is of considerable philosophical interest, and would have been so, I suspect, to Weyl.

Classical and constructive approaches

Robinson's approach is model-theoretical. It exploits the fact that a theory may have non-isomorphic models to distinguish which would require a stronger logic. That Peano Arithmetic with first-order logic has a model that is not isomorphic to the intended one was shown, by classical means, in [START_REF] Skolem | Über die Nicht-charakterisierbarkeit der Zahlenreihe mittels endlich oder abzählbar unendlich vieler Aussagen mit ausschliesslich Zahlenvariablen[END_REF]. Robinson established the same for the theory of analysis with first-order logic. The field of real numbers ℝ has an Archimedean or-der:

∀𝑥, 𝑦 ∈ ℝ(𝑥 < 𝑦 → ∃𝑛 ∈ ℕ(𝑛 ⋅ 𝑥 > 𝑦))

The non-standard infinite elements in Robinson's non-standard model give rise to a non-Archimedean order, and he proceeded in such a way that the larger structure is again a field, ℝ * . By definition, a field 𝐹 contains, for each of its elements except 0, also its multiplicative inverse: ∀𝑥 ∈ 𝐹(𝑥 ≠ 0 → ∃𝑦 ∈ 𝐹(𝑥 ⋅ 𝑦 = 1))

The multiplicative inverses of the infinitely large elements in ℝ * are infinitesimals.

Robinson's method enabled him to show

ℝ * ⊨ 𝜙 ⇔ ℝ ⊨ 𝜙
for 𝜙 limited to first-order formulas. First-order logic is not strong enough to distinguish between non-isomorphic models of the theory of real numbers. The equivalence (2) is called the Transfer Principle because it states that, for first-order 𝜙, truth in ℝ * transfers to truth in ℝ, and vice versa.

Robinson observed that the philosophical importance of the Transfer Principle is that, within the limitation to stay with first-order logic, it is a mathematical rendering of Leibniz's Continuity Principle: G.W. Leibniz argued that the theory of infinitesimals implies the introduction of ideal numbers which might be infinitely small or infinitely large compared with the real numbers but which were to possess the same properties as the latter. 3However, neither he nor his disciples and successors were able to give a rational development leading up to a system of this sort. As a result, the theory of infinitesimals gradually fell into disrepute and was replaced eventually by the classical theory of limits.

It is shown in this book that Leibniz' ideas can be fully vindicated and that they lead to a novel and fruitful approach to classical Analysis and to many other branches of mathematics. (Robinson, 1966, p.2

, original emphasis)

A largely constructive, version of non-standard analysis had been developed by [START_REF] Schmieden | Eine Erweiterung der Infinitesimalrechnung[END_REF] even before Robinson's classical work. Their non-standard objects can be considered to be constructive -they are infinite sequences of arbitrary rational numbers -but classical reasoning is used to reason about their properties. Also their transfer principle was limited; their ℝ * was not a field but only a partially ordered ring. Inspired by Schmieden and Laugwitz, a fully constructive counterpart to Robinson's work has been developed by Erik Palmgren. It turns out that full Transfer would require a change in the logic: the following is the argument presented in Palmgren 1998, p.234. Theorem 1 (Moerdijk and Palmgren). A full constructivisation of Robinson's Transfer Principle demands a nonstandard interpretation of the logical symbols.

Proof 2. Assume that ∀𝑥𝑃(𝑥) is an as yet undecided formula in arithmetic, where 𝑃 contains no unbounded quantifiers. (Goldbach's conjecture is of this form.) We can decide all instances up to any given bound, so ℕ ⊨ ∀𝑚(∀𝑛 < 𝑚𝑃(𝑛) ∨ ∃𝑛 < 𝑚¬𝑃(𝑛))

Suppose now we have a Transfer Principle:

ℕ * ⊨ 𝜙 ⇔ ℕ ⊨ 𝜙 Let 𝑚 ∈ ℕ * be infinite. By transfer from ℕ to ℕ * , either for all 𝑛 we have ℕ * ⊨ 𝑃(𝑛 * ), where 𝑛 * is the image of 𝑛 ∈ ℕ in ℕ * , or ℕ * ⊨ ∃𝑛 < 𝑚¬𝑃(𝑛).
Transfer back from ℕ * to ℕ yields ℕ ⊨ ∀𝑥𝑃(𝑥) ∨ ¬∀𝑥𝑃(𝑥). This contradicts our assumption.

Inspired by Robinson's theory, but wishing to reconstruct it in syntactic rather than model-theoretical terms, Edward Nelson proposed Internal Set Theory (IST) [START_REF] Nelson | Internal set theory: A new approach to nonstandard analysis[END_REF]. 4 Another syntactic approach had been invented just before him by Hrbaček, and closely related work (but incompatible with ZFC) by Vopenka had begun even earlier; for the historical details, I refer to the rich footnote 7 in Kanovei and Reeken 2004, p.vii. I will here look at IST, and in some detail, not so much because it is the best known and most used syntactical nonstandard analysis, but because it was part of Reeb's Brouwerian approach that we will see in section 8. It should be mentioned, however, that further development of both Nelson's and Hrbaček's work have led to theories with more attractive metamathematical properties. 5 Instead of enriching the ontology by adding nonstandard objects to the set of classical real numbers, Nelson enriches the language we have to talk about the latter. 6 The idea is that, from a formal point of view, a distinction between standard and nonstandard numbers useful for the develop-4. For an introduction to Nelson's approach, see his more explanatory first chapter of a projected book [START_REF] Nelson | First chapter of an unfinished book on nonstandard analysis[END_REF]Robert 1988. 5. The culmination of this is HST in [START_REF] Kanovei | Nonstandard Analysis, Axiomatically[END_REF]; but it does not contain full ZFC as a proper part. See also footnote 45, below. 6. It is, in fact, possible to look at Robinson's nonstandard analysis in an entirely formalistic way, and take it not to introduce new objects, but new ways of deducing theorems.

Robinson points this out at the very end of his book: ment of analysis can already be made within the set of classical real numbers; what matters is that this is done in such a way that the right formulas become provable.

Nelson adds an undefined predicate 'standard' to the language of ZFC and adds three axioms to the theory that regulate its use; just as in ZFC, the relation ∈ is undefined. As the phrase goes, 'its meaning is implicitly defined by the axioms'; but course that is not a specification of a meaning in the sense of presenting a construction method or a meaning explanation in the sense of, for example, Dummett and Martin-Löf.

In the axioms for 'standard', the following shorthand is used: 7

∃ st 𝑥𝜙(𝑥) for ∃𝑥(𝑥 standard ∧ 𝜙(𝑥)) ∀ st 𝑥𝜙(𝑥) for ∀𝑥(𝑥 standard → 𝜙(𝑥)) ∀ st fin 𝑥𝜙(𝑥) for ∀𝑥((𝑥 standard ∧ 𝑥 finite) → 𝜙(𝑥)) ∀ st inf 𝑥𝜙(𝑥) for ∀𝑥((𝑥 standard ∧ 𝑥 infinite) → 𝜙(𝑥))
Then the new axioms are introduced, formally, and without pausing to motivate them. Formulas not containing the predicate 'standard' are said to be internal (namely, to ZFC), those containing it external:

The axioms of IST are the axioms of ZFC together with three additional axiom schemes which we call the transfer principle (T), the principle of idealization (I), and the principle of standardization (S). They are as follows.

Let 𝐴(𝑥, 𝑡 1 , … , 𝑡 𝑘 ) be an internal formula with free variables 𝑥, 𝑡 1 , … , 𝑡 𝑘 and no other free variables. Then (T)

∀ st 𝑡 1 … ∀ st 𝑡 𝑘 (∀ st 𝑥𝐴(𝑥, 𝑡 1 , … , 𝑡 𝑘 ) → ∀𝑥𝐴(𝑥, 𝑡 1 , … , 𝑡 𝑘 ))
Let 𝐵(𝑥, 𝑦) be an internal formula with free variables 𝑥, 𝑦 and possibly other free variables. Then (I) ∀ st fin 𝑧∃𝑥∀𝑦 ∈ 𝑧𝐵(𝑥, 𝑦) ↔ ∃𝑥∀ st 𝑦𝐵(𝑥, 𝑦).

Finally, let 𝐶(𝑧) be a formula, internal or external, with free variable

Returning now to the theory of this book, we observe that it is presented, naturally, within the framework of contemporary Mathematics, and thus appears to affirm the existence of all sorts of infinitary entities. However, from a formalist point of view we may look at our theory syntactically and may consider that what we have done is to introduce new deductive procedures rather than new mathematical entities. (Robinson, 1966, p.282) I have not highlighted this in the main text, so as to be able to show the contrast between the model-theoretical and the syntactical approaches. 7. The predicates 'finite' and 'infinite' are defined as usual, in terms of the presence or absence of a bijection between 𝑥 and the set {𝑚 | 𝑚 < 𝑛} for some 𝑛 ∈ ℕ.

z and possibly other free variables. Then (S) ∀ st 𝑥∃ st 𝑦∀ st 𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑥 ∧ 𝐶(𝑧)). [START_REF] Nelson | Internal set theory: A new approach to nonstandard analysis[END_REF](Nelson, , p.1166) ) We may not use external predicates to define subsets, as the axioms of ZFC that would have to be used to prove the existence of these subsets do not know how to interact with the undefined predicate 'standard'. (It is for this reason that not all of Robinson's nonstandard analysis can be reconstructed in IST.) It is the role of the standardization axiom (S) to form standard subsets of standard sets. Note that standard sets may well contain nonstandard elements; we will see that ℕ does, and in a sense that is the whole point of IST.

As IST is not an ontological enrichment of ℝ, Weyl's question how the dimensions of the finite and the infinitesimal are related for IST does not point to a problem with an ontological aspect.

William Powell proved, by model-theoretical means, that IST is conservative over ZFC and hence consistent relative to ZFC (Nelson, 1977, section 8). 8 In the following, we will look at a few theorems of IST, in order to demonstrate how IST proves that ℕ contains nonstandard numbers, which are greater than any standard number; this mostly with an eye on the discussion of Reeb's Brouwerian take on IST in section 8. 9 Their reciprocals are infinitesimals. 10 First, a strengthening of (T) together with its dual form:

Theorem 3 (T 𝑠 ). ∀ st 𝑡 1 … ∀ st 𝑡 𝑘 (∀ st 𝑥𝐴(𝑥, 𝑡 1 , … , 𝑡 𝑘 ) ↔ ∀𝑥𝐴(𝑥, 𝑡 1 , … , 𝑡 𝑘 ))
Proof 4. From (T) and ∀𝑥𝜙(𝑥) → ∀ st 𝑥𝜙(𝑥).

Theorem 5 (T 𝑠𝑑 ).

∀ st 𝑡 1 … ∀ st 𝑡 𝑘 (∃ st 𝑥𝐴(𝑥, 𝑡 1 , … , 𝑡 𝑘 ) ↔ ∃𝑥𝐴(𝑥, 𝑡 1 , … , 𝑡 𝑘 ))
Proof 6. Apply T 𝑠 to ¬𝐴, negate both sides of the bi-implication, and use ¬∀𝑥¬𝐴 ↔ ∃𝑥𝐴.

An immediate consequence of T 𝑠𝑑 is:

Theorem 7. If ∃!𝑥𝐴(𝑥), and 𝐴(𝑥) is internal, then 𝑥 is standard.

In particular, ℕ is standard.

There is a dual of (I):

8. Nelson himself later provided a purely syntactical proof that proofs in IST can be reduced to proofs in a standard system ZFC[V] which is itself conservative over ZFC [START_REF] Nelson | The syntax of nonstandard analysis[END_REF]. Kanovei and Reeken have shown that actually the presentation of IST there is stronger than that in [START_REF] Nelson | Internal set theory: A new approach to nonstandard analysis[END_REF] that not all properties of the later version are shared by the earlier one. However, they add that this is the case if only bounded sets are considered, and that in practice these are the ones that matter (Kanovei and Reeken, 2004, p.128). 9. The references for theorems 3-15 are [START_REF] Nelson | Internal set theory: A new approach to nonstandard analysis[END_REF]Nelson 2002. 10. In IST it is also possible to prove of ℝ directly that it contains infinitesimals. But the approach through ℕ fits Reeb's motivation better.

Theorem 8 (I 𝑑 ). ∃ st fin 𝑧∀𝑥∃𝑦 ∈ 𝑧𝐵(𝑥, 𝑦) ↔ ∀𝑥∃ st 𝑦𝐵(𝑥, 𝑦)

Proof 9. Apply (I) to ¬𝐵(𝑥, 𝑦), negate both sides, push the negations inward, and cancel double negations.

The key theorem of IST is this, which entails that nonstandard objects exist formally:

Theorem 10. Let 𝑋 be a set. Then 𝑋 is a standard finite set ⇔ Every element of 𝑋 is standard Corollary 11. Every infinite set has a non-standard element. In fact, it has infinitely many non-standard elements, because whenever we remove one non-standard element from it, the theorem applies again.

First we prove

Lemma 12.

𝑋 is a subset of a standard finite set ⇔ Every element of 𝑋 is standard Proof 13. Set 𝐵(𝑥, 𝑦) = 𝑥 ∈ 𝑋 ∧ 𝑥 ≠ 𝑦 and apply the dual of idealisation (I 𝑑 ) to ¬𝐵(𝑥, 𝑦):

∃ st fin 𝑧∀𝑥∃𝑦 ∈ 𝑧¬(𝑥 ∈ 𝑋 ∧ 𝑥 ≠ 𝑦) ↔ ∀𝑥∃ st 𝑦¬(𝑥 ∈ 𝑋 ∧ 𝑥 ≠ 𝑦)
Applying logic to the the right hand side, we get ∃ st fin 𝑧∀𝑥∃𝑦 ∈ 𝑧¬(𝑥 ∈ 𝑋 ∧ 𝑥 ≠ 𝑦) ↔ ∀𝑥 ∈ 𝑋 (𝑥 standard) and to the left hand side, ∃ st fin 𝑧(𝑋 ⊆ 𝑧) ↔ ∀𝑥 ∈ 𝑋(𝑥 standard) Proof 14 (Proof of Theorem 10). Left to right: The assumption that 𝑋 is a standard finite set gives, together with 𝑋 ⊆ 𝑋, ∃ st fin 𝑧(𝑋 ⊆ 𝑧), and now apply Lemma 12 from left to right.

Right to left: Assume that every element of 𝑋 is standard. By Lemma 12, from right to left, we have ∃ st fin 𝑧(𝑋 ⊆ 𝑧). By ZFC, the power set of 𝑧, 𝑃(𝑧), exists:

∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧)
This formula is internal, and 𝑃(𝑧) is unique, so, by Theorem 7, 𝑃(𝑧) is standard. It is also finite, because 𝑧 is. Applying the proof in the previous paragraph for the direction from left to right to 𝑃(𝑧), all elements of 𝑃(𝑧) are standard, and as 𝑋 ∈ 𝑃(𝑧), in particular 𝑋 is. Finally, 𝑋 is finite because 𝑧 is.

By the corollary to Theorem 10, ℕ contains a nonstandard number; this may be thought of as a proof that the natural numbers we usually work with, 0, 1, 2, … do not exhaust ℕ. This idea became important to Reeb; see below, section 8. Also by the corollary, there is no set containing exactly those natural numbers that are standard natural numbers; as mentioned, the set-forming principles of ZFC do not have a grip on the predicate 'standard'. Finally, we have Theorem 15. The nonstandard numbers in ℕ are greater than all its standard elements. From a radically formalist position the axioms could be left unmotivated, once the axioms are shown or at least believed to be consistent. Nelson's paper includes a (relative) consistency proof; in his later book chapter, there are informal considerations for accepting them. I single out the one for (I), as it is the one that formally implies the existence of nonstandard objects:

The intuition behind (I) is that we can only fix a finite number of objects at a time. To say that there is a 𝑦 such that for all fixed 𝑥 we have 𝐴 [i.e., 𝐵(𝑥, 𝑦)] is the same as saying that for any fixed finite set of 𝑥's there is a 𝑦 such that 𝐴 holds for all of them. (Nelson, 2002, p.5) Nelson acknowledged of course that there is informal discourse in mathematics, and the term 'fixed' belongs to that realm (Nelson, 2002, p.1). But since Nelson's reflected judgement is that there is no mathematical reality, be it intuitionistic or Platonic, and that strictly speaking mathematics consists in formal systems, 12 the strict counterpart of the informal dis-11. But (S) does not guarantee that it does not also contain nonstandard elements. 12. See on this also chapter 32, 'A modified Hilbert Program', in Nelson 1986. course's notion of being fixed for him must be found in a property of formal proofs. The statement 'we can only fix a finite number of objects at a time' is then mapped to the fact that each proof in the formal system at hand is a finite object, which therefore leaves room for only finitely many occasions to define (fix) individual objects and prove or assume their existence.

An analogous argument for a simpler case is this (presentation after [START_REF] Palmgren | A note on mathematics of infinity[END_REF]Palmgren , p.1195):

Theorem 19. Extend Peano Arithmetic with a constant 𝜔 and the axiom schema 𝜔 > 𝑛, to obtain a nonstandard theory PA * . Then PA * is conservative over PA.

Proof 20. Assume we have a formal proof of 𝐴(𝜔). As the formal proof is finite, only finitely many instances of the schema occur in it, 𝜔 > 𝑛 1 , … , 𝜔 > 𝑛 𝑘 . Define 𝑚 = max(𝑛 1 , … , 𝑛 𝑘 ) + 1, and replace, in the original proof, 𝜔 by 𝑚 everywhere.

Below, in section 8, we will see that according to Reeb, who was not a formalist and who held that there is a mathematical reality which furthermore is constructive, there is in mathematical reality a motivation for introducing the predicate 'standard' in ZFC, and from there for accepting the formal theory IST.

3 Three Brouwerian desiderata Turning now to Brouwer's writings, one may distill three desiderata for constructions of infinitesimals:

1. They should be intuitionistic constructions, i.e., be built up starting from 'the basic intuition of mathematics':

the substratum of all perception of change, which is divested of all quality, a unity of continuous and discrete, a possibility of the thinking together of several units, connected by a 'between', which never exhausts itself by the interpolation of new units. [START_REF] Brouwer | Over de grondslagen der wiskunde[END_REF], p.8, trl. Brouwer 1975, p.17):

Further on in the dissertation Brouwer specifies that this basic intuition consists in the awareness of time as pure change (Brouwer 1907, pp.98-99) that it and our construction acts on it are not of a linguistic nature (Brouwer 1907, p.169) and that there is not also a spatial continuum that is a priori given to us (Brouwer 1907, p.121).

2. Logical reasoning about them should be done according to the nature of mental constructions. This respects the essential non-linguistic character of mathematical construction, and the nature of logic, such as Brouwer describes it, as a study of the patterns in descriptions of that activity (Brouwer 1907, pp.131-132;[START_REF] Brouwer | De onbetrouwbaarheid der logische principes[END_REF]. Whatever logical principle one has recognised as correct on this conception should be allowed in one's reasoning.

3. They should be geometrical in nature. Brouwer defines geometry as follows:

Geometry is concerned with the properties of spaces of one or more dimensions. In particular it investigates and classifies sets, transformations and transformation groups in these spaces.

The spaces under consideration are built up out of one or more Cartesian simplices, 13 which can be connected in different ways; consequently a space is not completely defined by its dimension alone. [START_REF] Brouwer | Het wezen der meetkunde[END_REF], p.15, trl. Brouwer 1975, p.116) The classical and constructive nonstandard-models of the previous section obviously do not meet these desiderata, and neither does a purely axiomatic approach. But it is of course just as clear that there will be no direct intuitive construction of infinitesimals on the one-dimensional continuum. If in the next section the reason for this is spelled out, that is because it adds relief to Brouwer's construction in section 6 of a real number that is greater than 0, but of which we cannot indicate a positive distance from 0; this is the kind of construction that Vesley took up, as we will see in section 7. At the same time, it should also be noted that even in classical nonstandard analysis there is a large constructive element om the following sense: Once non-constructive methods have been employed to obtain infinitesimals, the reasoning often proceeds constructively, employing standardisation at the very end to return to the realm of the standard. That topic has recently been explored in great detail in Sanders 2018. 4 The impossibility of a direct construction on the one-dimensional continuum

The intuitive continuum as given in what Brouwer calls the basic intuition of mathematics has no scale on it. 14 Brouwer's 'between' is not intrinsically tied to intervals of any size, because if there is no scale then there are no sizes, in particular no infinitesimal ones. This intuitive 'between' precedes the construction of a scale, and the scale is constructed by 'the interpolation of new units' on it.

Putting a scale on the intuitive continuum is itself a construction process that takes place over time. The human mind is limited in such a way that in a given time interval we can only place finitely many points of a scale on the intuitive continuum, or begin a potentially infinite sequence of such placements. Between any two previously placed points, an intuitive continuum remains, and if we choose to do so, we can place a further point on this 'between', and thereby continue the construction of our scale into it. If we iterate this everywhere, in a potentially infinite process, we construct a countable, everywhere dense scale. We can correlate the points on this scale with any number system we have constructed of the order type of ℚ; we may begin by correlating an arbitrary point on the scale with 0 and another one with 1. We thus obtain a 'measurable continuum' (Brouwer 1907, p.11).

Once the construction process of the rational scale has begun, we then construct points or real numbers (including the embedding of the rationals) 𝑝 by constructing potentially infinite sequences of nested intervals with endpoints on the scale 𝑝 0 , 𝑝 1 , 𝑝 2 , … As a point does not exist on the continuum prior to our construction, it is identified with the developing sequence, as opposed to an independently existing limit to which the sequence converges. If two points 𝑝 and 𝑞 are not equal, this unequality must consist in the fact that starting from a finite index 𝑛, the intervals 𝑝 𝑛 and 𝑞 𝑛 do not overlap. As the intervals are determined by rationals, we can determine a natural number 𝑚 such that 𝑚𝑝 > 𝑞 or, as the case may be, 𝑚𝑞 > 𝑝. So the system is Archimedean, and infinitesimals or intervals of infinitesimal length do not exist. To construct an infinitesimal interval on the intuitive continuum, we would have to be able to construct a point 𝑝 such that ¬(𝑝 = 0) but of which it is contradictory to assume that the unequality to 0 arises at some 𝑝 𝑛 for natural 𝑛 (i.e., at a rational distance from 0). That is impossible.

We will see in section 6 that, with the admission into intuitionism of choice sequences, we can construct a real number 𝑟 that is unequal to 0 and of which we cannot indicate the interval 𝑟 𝑛 at which the unequality to 0 arises until a certain proposition 𝑃 has been decided. But before 𝑃 has been decided we can already show that it is contradictory to suppose that the unequality to 0 arises at no finitely indexed interval.

The fact that there are, in the basic intuition of mathematics, no direct motivation and no direct construction for infinitesimals (as objects constructed on the one-dimensional continuum), the development of a theory would have to proceed, just as in the classical case, either by an embedding of the standard real numbers into a more-dimensional structure, and thereby no longer take propositions in analysis of the one-dimensional continuum at face value, or construe talk about nonstandard objects as talk about certain standard objects. 5 Brouwer's non-Archimedean numbers Early Brouwer's construction of non-Archimedean numbers discussed in this section was not meant to lead up to a form of infinitesimal analysis. However, that would have been a first step, so the general considerations are of interest to the present discussion.

When Brouwer was working on his dissertation, non-Archimedean fields and geometries had been constructed by notably Veronese, Levi-Civita, Pasch, Hilbert, and Vahlen, 15 and these he refers to in his notebooks and in his thesis, with an emphasis on Hilbert. Brouwer criticised these approaches: Veronese's was not constructive in his sense, and those of Pasch, Hilbert and Vahlen are not geometrical in his sense.

In Veronese's Fondamenti di Geometria of 1891, a real number is construed as the ratio of two magnitudes (both of the same species), one of which is designated to be the unit; and the existence of a segment that is infinitesimal with respect to another is postulated. Veronese can do so because, as he states in his introduction, 'A thing postulated by thought one can consider as given to thought, and inversely' (Veronese, 1891, Introduzione, section 18, trl. mine). For Brouwer, on the other hand, only that what has been constructed from the basic intuition qualifies as given. In a notebook that predates his dissertation, he comments:

Veronese's fuss, with his constantly introducing hypotheses, is nothing but forming logical assemblies; if for certain things (I do not know whether they exist) such and such relations hold, then also such and such relations. (Brouwer, 1904-1907, Notebook 3, p.35, trl. mine) Hilbert's non-Archimedean geometries are criticised for their non-geometrical nature. In the synopsis for his dissertation, Brouwer writes: Hilbert's pseudo-geometries are (in contrast to the non-Euclidian) of little importance, because they have been built within a rather 'farfetched' building [i.e., construction] (while the non-Euclidian in the ordinary Cartesian space). (Brouwer 1904(Brouwer -1907, p.405, trl. mine) , p.405, trl. mine) Brouwer is referring to the fact that the coordinates of points in the space are not real numbers but objects of a higher type, namely certain algebraic functions on the real numbers (Hilbert, 1899, p.25). Such algebraic functions may themselves be represented (extensionally) geometrically, but Brouwer's hesitation here would be that each such representation is not a point in a (𝑛-dimensional) Cartesian space. Hilbert, of course, proposed his non-Archimedean geometry first of all in the service of an independence proof of the Archimedean axiom, and then Brouwer's considerations are not that important. But such geometries soon turned out to be of inter-15. An extensive historical treatment is [START_REF] Ehrlich | The Rise of non-Archimedean Mathematics and the Roots of a Misconception I: The Emergence of non-Archimedean Systems of Magnitudes[END_REF] est in their own right.

In his dissertation, Brouwer presents an alternative non-Archimedean continuum, a(n intended) construction in his specific, non-axiomatic sense of that term, in an ordinary Cartesian space (Brouwer 1907, pp.67-73). It is, he states (Brouwer 1907, p.140n) a generalization of that in Hilbert 1899, section 34. By Brouwer's de facto phenomenological consideration, given in the previous section, a non-Archimedean (mathematical) continuum cannot be constructed on the one-dimensional intuitive one. His strategy therefore was to construct a multi-dimensional mathematical continuum and define a subset on it which he calls 'the pseudo-continuum'. The pseudocontinuum can be linearly ordered and the one-dimensional continuum embedded into it.

Brouwer starts with an infinite-dimensional Cartesian space of (𝜔 * + 𝜔) 𝑛 dimensions, where 𝜔 * is … , -3, -2, -1. Each coordinate has (instead of a letter) an ordinal number in between -𝜔 𝑛 and 𝜔 𝑛 , which can be written in the form 𝑎 1 𝜔 𝑛-1 + ⋯ + 𝑎 𝑛-1 𝜔 + 𝑎 𝑛 , with -𝜔 < 𝑎 𝑖 < 𝜔. To the coordinate then is associated the 𝑛-tuple of indices ⟨𝑎 1 , … , 𝑎 𝑛 ⟩.

The 'pseudo-continuum' now consists of the subset of points in the space with the property that for all their coordinates whose value is not 0 we can indicate lower bounds on the 𝑎 𝑖 : the property, in other words, that non-zero values are not found at arbitrarily low coordinate numbers. This in turn means that the coordinate numbers corresponding to those 𝑛-tuples form a well-ordered set (i.e., a set of which each non-empty subset has a first element). So for any two distinct points 𝑝, 𝑞 there will be a smallest coordinate number at which they differ, and therefore the set can be linearly ordered.

The one-dimensional Archimedean continuum is embedded into the pseudo-continuum by assigning the point on the former with coordinate 𝑥 to the point on the latter whose coordinates are all 0 except that its 0coordinate is 𝑥. One may view the pseudo-continuum as a real continuum with infinitely many points inserted to the right and left of each real point, and with infinitely many pseudo points to the left and right of the real continuum as a whole.

The operations + and × are understood group-theoretically, that is, as parametrised transformation operations +𝑎 and ×𝑎.

Theorem 21 [START_REF] Brouwer | Over de grondslagen der wiskunde[END_REF]. On a measurable continuum, there is only one construction for a two-parameter continuous uniform transformation group

𝑥 ′ = 𝑐 1 × 𝑥 + 𝑐 2
namely the one in which + and × are ordinary addition and multiplication (and hence commutative). (Brouwer 1907, pp.32-33) On the pseudo-continuum he then defines a two-parameter continuous uniform transformation group that preserves + and × on the embedded one-dimensional continuum, but whose multiplication is not commutative on the pseudo-continuum as a whole.

The group operation + on the pseudo-continuum is induced by the + operation on the scale of each of the coordinates. It is associative and commutative. The operation × on the pseudo-continuum is defined as an operation that shifts coordinates; 1 1 × shifts the number of a coordinate to the right by one while mapping the 1-points of the scales of each coordinate onto one another. Likewise, 1 𝜔 × shifts the number of a coordinate to the right by 𝜔 while mapping the 1-points onto one another. Brouwer determines conditions on the the choices of the 1-points on the scales of coordinates 1, 𝜔, 𝜔 2 , … that will guarantee that × is associative and distributive with +.

But × on the pseudo-continuum has been defined so as not to be commutative: for example,

1 1 × 1 𝜔 = 1 𝜔+1 but 1 𝜔 × 1 1 = 𝑝 𝜔+1
where 𝑝 is the point on the scale of coordinate 1 chosen to be the 1-point on that scale. In general, 1 𝜔+1 and 𝑝 𝜔+1 are not equal.

Theorem 21 then implies that this pseudo-continuum is not a measurable one. Brouwer remarks that this pseudo-continuum is not continuous in Dedekind's sense (which would have implied it is Archimedean), but it is in Veronese's (Brouwer 1907, pp.72-73 ). 16 An objection to the way the pseudo-continuum is constructed is that it presupposes the Principle of the Excluded Middle: In order to obtain the linear ordering of its points, it must be possible to decide whether a sequence that proceeds infinitely to both sides is from a certain element onward constant zero to the left. This is similar to a problem in another part of his thesis, which is flagged and discussed in the corrections that he published in 1917: When moving down along a branch in a tree, one cannot, in general, decide whether each future node will have a unique descendant (Brouwer 1917, p.440).

At the time, Brouwer accepted the Principle of the Excluded Middle because he took 𝑃 ∨ ¬𝑃 to be equivalent to ¬𝑃 → ¬𝑃 (van Dalen, 1999, pp.106-107). Constructively, it is not; Brouwer presented the correct reading, according to which PEM is valid only for decidable propositions, in [START_REF] Brouwer | De onbetrouwbaarheid der logische principes[END_REF]The unreliability of the logical principles'. 17 Moreover, Brouwer's construction, if successful, would not be a field extension of the real numbers, so it could not have been used to develop a nonstandard analysis. It is not surprising, then, that Brouwer did not develop the theory of this pseudo-continuum any further.The work on non-Archimedean numbers was superseded by Hahn's paper 'Über die nichtarchimedischen Größensysteme' (1907), which appeared just too late to be taken into consideration in Brouwer's thesis, which was defended on February 19 of the same year. But in 1917, Brouwer referred to it in his list of additions and corrections to his dissertation specifically for its treatment of commutative principal operations (Brouwer 1917, p.441).

One of the few people who seem actually to have studied Brouwer's pseudo-continuum is Kurt Gödel. In 1941, by which time he had emigrated to the United States, he asked his brother who had remained in Vienna, to order a copy of Brouwer's dissertation for him (van Atten, 2015, pp.190-191). And indeed, in one of Gödel's notebooks, probably filled in 1942, one finds reading notes on Brouwer's construction. 18 Gödel at the time was interested in the question if there could be non-human beings in whose awareness time is ordered in a non-Archimedean way (Gödel, 1906-1978, Max Phil VI (?-July 1942), pp.431-432).

Brouwer made one last remark on non-Archimedean geometry in his second lecture in Vienna 1928 -with Hahn, who had in the meantime become a friend of his, in the audience: 19The initial, negative attitude towards these [non-Euclidean or non-Archimedean] geometries was completely overcome by their arithmetisation due to Riemann, Beltrami, Cayley, and, respectively, Levi-Civita and Hahn. In the process, the peculiar fact came about that the non-Archimedean continuum, which had proved to fulfill the a priori conditions on the continuum just as well as the Archimedean, was brought about in a plausible manner only with the aid of the latter, so that the calling into question of the a priori necessity of the Archimedean continuum had to be founded precisely on the a priori consistency of this continuum. (Brouwer 1930, p.1, trl. mine) 6 Brouwer: a real number that is greater than 0, but not measurably greater Around 1916, Brouwer introduced choice sequences into intuitionistic analysis. 20 A choice sequence is a sequence of natural or rational numbers that are freely chosen by the Creating Subject, which is moreover free to impose restrictions on its choices. Thus we have sequences without any restriction on the choices (lawless sequences) and sequences determined by an algorithm or law (lawlike sequences). For Brouwer these are the extreme cases, with many other kinds of choice sequence in between, notably also choice sequences for which the Creating Subject lets its choices depend on some of its other mathematical activities. (We will see examples of this latter kind in this section and the next.) Brouwer's rationale for reconstructing analysis in a theory of choice sequences is that this gives a mathematical, fully constructive model of the intuitive continuum that faithfully mirrors, not only epistemologically but ontologically, the fact that the latter is not a composition out of discrete elements.

Weyl, in his intuitionistic period, accepted the theory of choice sequences in a modified form that, however, made it incoherent (van Atten et al., 2002, section 3). Be that as it may, of some interest for our present theme is Weyl's intention to accept universal quantification over lawless sequences but to insist that instantiations are lawlike, for in this way he is in effect treating lawless sequences as nonstandard objects. For Weyl, only lawlike choice sequences could exist as individuals. Brouwer's particular choice sequence that is the topic of the present section would not have been acknowledged as an individual mathematical object by Weyl.

The introduction of choice sequences did not affect early Brouwer's observation on the impossibility to construct a non-Archimedean scale. The reason is that the latter observation is made at such a high level of generality that it also subsumes choice sequences. Yet, in the Cambridge Lectures (1946Lectures ( -1951) ) Brouwer states that the intuitive 'between' surely requires as well that the continuum contains further point cores between, for instance, the origin on the one hand and all rational point cores on the other. (Brouwer, 1981, p.50) A 'point core' is an equivalence class (or rather a 'species') of choice sequences, the criterion being that they are all co-convergent. Brouwer seems to be saying here that one can construct points that are not 0 yet whose distance from 0 is smaller than any rational number we will ever construct; he seems to be saying that we can construct infinitesimals. It will turn out that this is not quite what is meant. 21To show Brouwer's argument for this claim, his definitions of some order relations are needed [START_REF] Brouwer | Consciousness, philosophy and mathematics[END_REF]. Let 𝛽 and 𝛾 be two real numbers, i.e., two convergent infinite sequences of rational numbers 𝛽(𝑛) and 𝛾(𝑛). Define 𝛽 <∘ 𝛾, '𝛽 is measurably smaller than 𝛾' as

∃𝑚, 𝑛 ∈ ℕ∀𝑣 ∈ ℕ (𝑣 ≥ 𝑚 → 𝛾(𝑣) -𝛽(𝑣) > 1 2 𝑛 )
Correspondingly, 𝛾 ∘ > 𝛽 means that 𝛾 is 'measurably greater' than 𝛽 (Brouwer, 1951, p.3). Write 𝛽 ≠ 𝛾 for ¬(𝛽 = 𝛾) 𝛽 ≥ 𝛾 for ¬(𝛽 <∘ 𝛾) 𝛽 > 𝛾 for 𝛽 ≥ 𝛾 ∧ 𝛽 ≠ 𝛾 So being measurably greater, defined as a double existential statement, is a positive property, while being greater, defined as in effect a conjunction of two negations, is a negative property.

The apartness relation [START_REF] Brouwer | Consciousness, philosophy and mathematics[END_REF]) is defined as follows:

𝛽 # 𝛾 ≡ ∃𝑘 ∈ ℕ (|𝛽 -𝛾| > 1 2 𝑘 )
or, equivalently,

𝛽 # 𝛾 ≡ 𝛽 <∘ 𝛾 ∨ 𝛽 ∘ > 𝛾
The definition of a choice sequence, and so in particular of a point core that it represents, may be made to depend on what goes on in the subject's other activities in between the choices of the elements in this sequence, notably with respect to attempts to settle a certain problem. For example, in between two choices, the subject may have decided a proposition 𝑃, or have tested it. A proposition 𝑃 is decided by either proving 𝑃 or proving ¬𝑃; it is tested by either proving ¬𝑃 or ¬¬𝑃. Decidability implies testability. If 𝑃 holds, then so does ¬¬𝑃, and if ¬𝑃, then ¬𝑃; so 𝑃 ∨ ¬𝑃 implies ¬𝑃 ∨ ¬¬𝑃. But testability does not imply decidability. For suppose we can prove ¬¬𝑃 but not (yet) 𝑃; then 𝑃 has been tested but is still undecided.

Weak counterexample 22 (Brouwer). There is no hope of showing that ∀𝛼(𝛼 > 0 → 𝛼 ∘ > 0). 22 Plausibility argument 23. Let 𝑃 be a proposition that we cannot test, in the weak sense that we do not now possess a proof of ¬𝑃 ∨ ¬¬𝑃. 23 22. In the next section, we will see that Brouwer also had a proof of the actual negation, ¬∀𝛼(𝛼 > 0 → 𝛼 ∘ > 0) (Theorem 28). 23. Brouwer could have given this argument in terms of an undecidable proposition instead of an untestable one. The reason he uses an untestable one is that in his paper he exploits almost the same construction to prove that ≠ cannot be defined as a disjunction of < and >, as that would lead to the contradiction that an untestable proposition is testable. For further discussion of Brouwer's weak and strong counterexamples, see van Atten forth-

The Creating Subject constructs a real number 𝛼 in a choice sequence of rational numbers 𝛼(𝑛), as follows:

• As long as, when making the choice of 𝛼(𝑛), the Creating Subject has obtained evidence neither of 𝑃 nor of ¬𝑃, 𝛼(𝑛) is chosen to be 0.

• If between the choice of 𝛼(𝑛 -1) and 𝛼(𝑛), the Creating Subject has obtained evidence of 𝑃, or has obtained evidence of ¬𝑃, 𝛼(𝑛) and all 𝛼(𝑛 + 𝑘) are chosen to be ( 1 2 ) 𝑛 .

The choice sequence 𝛼 converges, hence is a real number. 24 We have

𝛼 = 0 ↔ ¬𝑃 ∧ ¬¬𝑃
Hence 𝛼 ≠ 0. We also have ¬(𝛼 <∘ 0) because, by definition of 𝛼, no 𝛼(𝑛) is ever smaller than 0; and their conjunction gives 𝛼 > 0.

But we do not have the stronger 𝛼 ∘ > 0 because if we had, then

∃𝑚, 𝑛 ∈ ℕ∀𝑣 ∈ ℕ (𝑣 ≥ 𝑚 → 𝛼(𝑣) > 1 2 𝑛 )
and this is only possible if 𝑃 would have been decided, and hence tested; but this contradicts the hypothesis that 𝑃 cannot be tested yet.

This is what Brouwer means when, in the quotation from the Cambridge Lectures above, he says that there are point cores between the origin and all positive rational point cores. If, by developing more mathematics, we do come in a position to test 𝑃, that is we can find a proof of ¬𝑃 or a proof of ¬¬𝑃, then the number 𝛼 becomes rational, and, in the sense of these order relations, no longer lies between 0 and all rational point cores. Note that this does not mean that 𝛼 was irrational before. 25 Brouwer does not go on to connect his example of a number between 0 and all the rationals in any way to infinitesimals. That would be done by Vesley.

Vesley's 𝛼-infinitesimals

Vesley realised that real numbers like the one in Brouwer's example are, although not infinitesimals in an ontological sense, in an important recoming. 24. Let 𝜀 be given, and determine an 𝑛 such that 2 -𝑛 < 𝜀. Construct the sequence 𝛼 up to 𝛼(𝑛), which can be done as each choice is decidable. If 𝛼(𝑛) = 0, all further choices will be in the interval [0, 2 -(𝑛+1) ] and hence within 𝜀 from one another. If 𝛼(𝑛) ≠ 0, then the choices in 𝛼 have already been fixed, and hence within 𝜀 from one another. 25. Before, it was a growing construction for a real number that had yet acquired neither the property of being rational, nor that of being irrational.

spect similar to infinitesimals [START_REF] Vesley | An intuitionistic infinitesimal calculus[END_REF]. 26 The same observation was made independently in van Dalen 1988, p.191. Vesley appeals to Kripke's Schema:

(KS) ∃𝛼(∃𝑛 𝛼(𝑛) = 1 ↔ 𝑃)
where 𝑃 is a variable for propositions, and 𝛼 for choice sequences. Brouwer had demonstrated this before Kripke did but never used it again, and instead reasoned from the general principles from which KS quickly follows. 27 These principles were later codified by Kreisel in the so-called 'Theory of the Creative Subject' (or 'Creating Subject'). For discussion of the Creating Subject and KS, see Myhill 1966;[START_REF] Kreisel | Informal rigour and completeness proofs[END_REF]Troelstra and van Dalen 1988, ch.4;van Atten 2004, ch.5; and van Atten forthcoming. I will adapt Vesley's construction somewhat to Brouwer's way. Let 𝛼 be a choice sequence (whether of convergent rationals or not). Define a real number 𝑥 as follows:

• As long as, when making the choice of 𝑥(𝑛), the Creating Subject has obtained evidence of neither ∀𝑛𝛼(𝑛) = 0 nor of ¬∀𝑛𝛼(𝑛) = 0, 𝑥(𝑛) is chosen to be 0.

• If between the choice of 𝑥(𝑛 -1)and 𝑥(𝑛), the Creating Subject has obtained evidence of ∀𝑛𝛼(𝑛) = 0, 𝑥(𝑛) and all 𝑥(𝑛 + 𝑘) are chosen to be ( 1 2 ) 𝑛 .

• If between the choice of 𝑥(𝑛 -1) and 𝑥(𝑛), the Creating Subject has obtained evidence of ¬∀𝑛𝛼(𝑛) = 0, 𝑥(𝑛) and all 𝑥(𝑛 + 𝑘) are chosen to be -( 1 2 ) 𝑛 .

Then we have

∃𝑥 ∈ ℝ[(𝑥 ∘ > 0 ↔ ∀𝑛𝛼(𝑛) = 0) ∧ (𝑥 <∘ 0 ↔ ¬∀𝑛𝛼(𝑛) = 0)]
and, since 𝛼 was an arbitrary choice sequence,

∀𝛼∃𝑥 ∈ ℝ[(𝑥 ∘ > 0 ↔ ∀𝑛𝛼(𝑛) = 0) ∧ (𝑥 <∘ 0 ↔ ¬∀𝑛𝛼(𝑛) = 0)]
Define for every choice sequence the species of real numbers 𝐿(𝛼) and 26. I don't think Vesley knew of that particular passage in Brouwer, which was published only in 1981, but he was of course very familiar with this kind of reasoning, e.g. [START_REF] Kleene | The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions[END_REF]. 27. See Brouwer 1954, p.4 for Brouwer's demonstration, and Myhill 1966, p.295 for the observation that this is KS. Brouwer does not literally state KS; he constructs, from an arbitrary proposition 𝑃 that as yet cannot be tested, an infinite sequence 𝐶(𝛾, 𝑃), and shows that truth of 𝑃 and rationality of 𝐶(𝛾, 𝑃) are equivalent. However, the construction of a witness for KS from 𝐶(𝛾, 𝑃) is immediate; and Brouwer's reasoning towards the existence of 𝐶(𝛾, 𝑃) goes through for any 𝑃, not only untestable ones.

𝑀(𝛼)

:

𝑥 ∈ 𝐿(𝛼) ≡ [𝑥 # 0 ↔ ∀𝑛𝛼(𝑛) = 0 ∨ ¬∀𝑛𝛼(𝑛) = 0] 𝑥 ∈ 𝑀(𝛼) ≡ ∃𝑦 ∈ 𝐿(𝛼)¬(|𝑥| ∘ > |𝑦|)
Vesley points out that one can then prove:

Theorem 24. 𝑀(𝛼) is a subring of the intuitionistic ℝ.

Theorem 25. ¬∀𝛼∃𝑥 ∈ 𝑀(𝛼)∃𝑛(𝑛 ⋅ 𝑥 ∘ > 1)

The species 𝑀(𝛼) is called that of the -infinitesimals. These are elements of (intuitionistic) ℝ, and in this sense the conception is a little like that in Nelson's IST, where the infinitesimals are elements of classical ℝ.

Vesley observes that, although we want to think of the -infinitesimals as very small, and for that reason give them this suggestive name, should the question whether is 0 everywhere be decided, 𝑀(𝛼) becomes ℝ. This goes against the very idea of an infinitesimal. On the one hand, in light of open-endedness of mathematics, there will always be new open problems, so this is not much of an objection against the existence of -infinitesimals in general. On the other hand, this also means that these infinitesimals only behave as infinitesimals under universal quantification. We cannot prove that all species of -infinitesimals are non-Archimedean; only that it is not the case that none of them is. Instead of

∀𝛼¬∃𝑥 ∈ 𝑀(𝛼)∃𝑛(𝑛 ⋅ 𝑥 ∘ > 1)
we only have

¬∀𝛼∃𝑥 ∈ 𝑀(𝛼)∃𝑛(𝑛 ⋅ 𝑥 ∘ > 1)

And that the latter cannot be strengthened to the former is intrinsic to the whole construction. An individual 𝑀(𝛼) will be non-Archimedean as long as it is undecided whether the values of 𝛼 are 0 everywhere or not, but becomes Archmedean as soon as this has been decided. And there cannot be a particular 𝛼 for which this is never decided, for that would imply the existence of an absolutely undecidable proposition, which is impossible: 28 Theorem 26 [START_REF] Brouwer | Over de grondslagen der wiskunde[END_REF][START_REF] Brouwer | De onbetrouwbaarheid der logische principes[END_REF]. There exist no absolutely undecidable propositions.

Proof 27. 'Can one ever demonstrate of a proposition, that it can never be decided? No, because one would have to so by reductio ad absurdum.

28. One might think the permanent existence of an -infinitesimal can be assured by starting a sequence starting with 0's and stipulating that one will never make the decision between (a) restricting the remaining choices to 0 and (b) making a choice that is not 0. This however will not do, because by choosing 0 until that decision is made, and at the same time resolving always to postpone that decision, the result is that the sequence will be constant 0.

So one would have to say: assume that the proposition has been decided in sense A, and from that deduce a contradiction. But then it would have been proved that not-A is true, and the proposition is decided after all.' (Note by Brouwer, as quoted in van Dalen 2001, p.174 note a; translation mine)

That ¬(𝑃 ∨ ¬𝑃) is contradictory, and hence that PEM is consistent, was pointed out in Brouwer 1908. The quoted argument was never published by Brouwer, but Wavre 1926, p.66 andHeyting 1934, p.16 made the same observation.

Van Dalen, who as mentioned made the same connection between Brouwer's weak counterexample and infinitesimals, considered it 'highly unsatisfactory to include subjective phrases such as "it cannot be shown" in mathematical texts' (van Dalen, 1988, p.191), and points out that in Brouwer 1949a this result is strengthened from the weak counterexample 'there are real numbers 𝛼 that are greater than 0 yet cannot be shown to be measurably greater than 0' to the strong counterexample Theorem 28 (Brouwer 1949). ¬∀𝛼(𝛼 > 0 → 𝛼 ∘ > 0) (Note that intuitionistically this does not imply ∃𝛼¬(𝛼 > 0 → 𝛼 ∘ > 0), which is contradictory.) Indeed, in the demonstration of this theorem, instead of one open problem and unbounded time to solve it, Brouwer considers the infinity of open and solved problems '𝛼 ∈ ℚ' for all 𝛼 ∈ [0, 1] with the added condition, which arises from the applicability of the fan theorem to functions defined on that interval, that they should all be solved on the basis of an initial segment of 𝛼 of uniform length. 29 And then not only it cannot be shown that this condition can be met (weak negation), it can be shown that it is leads to contradictions if it could (strong negation).

Vesley observes that in this version of nonstandard analysis, 'the elegance of classical nonstandard analysis is missing for the familiar reason that more distinctions must be recognized intuitionistically' (Vesley, 1981, p.211), but because of the dependency of his infinitesimals on universal quantification he also sees a similarity to the synthetic differential geometry of Lawvere and Kock, 30 which has been developed much further [START_REF] Kock | Synthetic Differential Geometry[END_REF]. From a Brouwerian perspective, Vesley's approach would philosophically be preferable to synthetic differential geometry (smooth infinitesimal analysis) in that the latter involves a postulation of the existence of a line segment of infinitesimal length, which is certainly not given to us in mathematical intuition. 31 Vesley announced a sequel paper to develop the approach further and to see whether it has advantages of its own. Unfortunately, it seems that he gave up on the project. 29. Strictly speaking, Brouwer does not consider the question of rationality of each 𝛼 ∈ [0, 1],

but of each 𝛼 ∈ 𝐽, where 𝐽 is a fan that coincides with [0, 1]. Note also that our notational use of is different from that in Brouwer 1949a. 30. There, 'nilpotents', which are 𝛿 such that 𝛿 ≠ 0 but 𝛿 2 = 0, may be cancelled when universally quantified. 31. Compare Brouwer's objection to Veronese's postulate above, p. 12. 8 Reeb: An intuitionistic take on IST An approach to infinitesimals that is Brouwerian in a rather different sense than that defined by the three desiderata of section 3, and one that would have been of interest to Weyl, was proposed and enthusiastically defended by Georges Reeb at the University of Strasbourg. 32 The mathematical content of nonstandard analyis as advocated by him is that of his friend Nelson's IST, 33 described in section 2. The originality of Reeb's approach lies in the fact that, instead of construing IST as an axiomatic theory, in which the predicate 'standard' is taken to be implictly defined by the axioms, he proposes a specifically Brouwerian motivation for accepting IST as a formal theory. It is, he notes, a train of thought that starts from intuitionistic observations on ZFC and concludes to 'the plausibility or the naturalness of IST' (Reeb, 1989, p.151); 34 and the article he dedicated to giving his most elaborate account of this, written with Jacques Harthong, was, indeed, titled 'Intuitionnisme 84' [START_REF] Reeb | Intuitionnisme 84[END_REF]. 35 The title was, of course, at the same time a reference to Robinson's 'Formalism 64' [START_REF] Robinson | Formalism 64[END_REF]. Just as Robinson asked what formalism could be in 1964, Reeb and Harthong had a view on what intuitionism could be in 1984. In addition, formalism is an essential component of Reeb's approach, but with a specifically Brouwerian view on it. On the other hand, Reeb was not a Brouwerian intuitionist, and did not aspire to be. Reeb and Harthong acknowledge the difference when they speak of 'the intuitionistic conception (ours just as much as that of Brouwer) …' (Reeb and Harthong, 1989, p.52). 36 Also Harthong in his afterword to the 1989 reprint of Int84 in La mathématique nonstandard is quite forthcoming on this point (Harthong, 1989, pp.265-267). Some differences will be touched upon 32. For Reeb's (philosophy of) nonstandard analysis, see, in French, [START_REF] Reeb | La mathématique non standard vieille de soixante ans ?[END_REF][START_REF] Reeb | La mathématique non standard vieille de soixante ans ? Cahiers de topologie et géométrie différentielle catégoriques[END_REF][START_REF] Barreau | La Mathématique non standard[END_REF][START_REF] Diener | Analyse non standard[END_REF][START_REF] Gerhardt | Et pourtant… ils ne remplissent pas N. Aléas[END_REF][START_REF] Reeb | Intuitionnisme 84[END_REF][START_REF] Ouvert | Numéro spécial Georges Reeb[END_REF][START_REF] Salanskis | Le Constructivisme non standard[END_REF]. There is not much about Reeb's (philosophy of) nonstandard analysis in English; see [START_REF] Fletcher | Approaches to analysis with infinitesimals following Robinson, Nelson, and others[END_REF] for a few recent remarks.

Nelson has written:

One of the most treasured experiences of my life is my friendship with Georges Reeb. We had many strong discussions together, intuitionist versus formalist. What he created was unique in my experience. His rare spirit, gentle but fiercely demanding of the highest standards, inspired a group of younger mathematicians with an unmatched ethos of collegiality. And their discoveries are extraordinary. Reeb found, and led others to find, not only knowledge and beauty in mathematics, but also virtue. His insights into the nature of mathematics will point the way towards the mathematics of the future. (Nelson, 1996, p.8) 34. In Reeb 1981, p.153, he had stated that his notion of naïve numbers leads to ideas that 'show some analogy with IST', and this is what one expects of a motivation in constructive reality of a distinction in an idealised, classical formal theory. Note that Reeb in his writings does not much discuss his philosophical differences with Nelson. On Nelson's philosophy of mathematics, see, besides his own papers, also [START_REF] Van Dalen | Nelson's work on logic and foundations and other reflections on foundations of mthematics[END_REF]Buss . 35. 1984 is the year in which a first version was written and began to circulate. 36. 'la conception intuitionniste (aussi bien la nôtre que celle de Brouwer) …' below.

Reeb holds that there is a mathematical reality, constructive, indepent of theory, and which intuitionists aim to describe; 37 formal theories such as ZFC and IST as constructive objects that codify ideal(ised) theories of that reality, just as we have idealised theories of physical reality [START_REF] Reeb | Intuitionnisme 84[END_REF], sections 2 and 5). Accordingly, the notion of motivation for an axiom takes on a richer sense that relates the formal axiom to mathematical reality. That relation need not be as strong as the axiom being fully interpretable in that reality; it may rather be construed as an idealisation. This sounds Hilbertian, and it is, 38 but it must be remembered that it was intuitionistic criticism of his earlier program that led Hilbert to adopt that particular view, which itself goes back to Brouwer's dissertation (1907). 39 The terms of the formal theory do, as such, not refer, but if we construe that theory as an idealisation of reality we must be prepared to act as if they refer to ideal(ised) objects (Salanskis, 1994, p.30). Consistency or conservativeness of the formal theory is therefore not the whole criterion: if ZFC is extended with an independent proposition 𝑃, or, alternatively, ¬𝑃, Reeb expresses a preference for the one that seems in a sense closer to mathematical reality than another: writing about Fermat's Last Theorem in 1989, he says that if it turns out to be an undecidable proposition, one could of course add its negation to ZFC, but 'the intuitionist will consider this choice … far removed from concrete reality' -in which by then no counterexample had been found (Reeb, 1989, p.158).

The importance of Brouwer in Reeb's view is epistemological, and defined by the insistence that a formal theory, even if shown consistent, cannot, once constructed, replace mathematical reality [START_REF] Reeb | Intuitionnisme 84[END_REF], section 4), and that, in particular, accepting the Principle of the Excluded Middle in the formal theory does not mean that every problem in mathematical reality can be solved. Reeb's main reference for this is 'Intuitionistic reflections on formalism' of 1928, in which Brouwer writes:

The disagreement over which is correct, the formalistic way of founding mathematics anew or the intuitionistic way of reconstructing it, will vanish, and the choice between the two activities be reduced to a matter of taste, as soon as the following insights, which pertain primarily to formalism but were first formulated in the intuitionistic literature, are generally accepted. The acceptance of these insights is only a question of time, since they are the results of pure reflection and hence contain no disputable element, so that anyone who has 37. This attitude was later described by Sundholm and myself as the intuitionists' 'ontological descriptivism', an attitude they share with Platonists, the disagreement being over the nature of that reality (Sundholm and van Atten, 2008, p.71). If we had known the paper by Reeb and Harthong then, we would surely have taken it into account. 38. Besides the main influence Brouwer, in Reeb one finds quotations or echos from for example Hilbert, Poincaré, Löwenheim, Skolem, and Von Neumann. 39. Brouwer makes the point in [START_REF] Brouwer | Intuitionistische Betrachtungen über den Formalismus[END_REF] once understood them must accept them. Two of the four insights have so far been understood and accepted in the formalistic literature. When the same state of affairs has been reached with respect to the other two, it will mean the end of the controversy concerning the foundations of mathematics.

First insight. The differentiation, among the formalistic endeavors, between a construction of the 'inventory of mathematical formulas' (formalistic view of mathematics) and an intuitive (contentual)40 theory of the laws of this construction, as well as the recognition of the fact that for the latter theory the intuitionistic mathematics of the set of natural numbers is indispensable.

Second insight. The rejection of the thoughtless use of the logical principle of excluded middle, as well as the recognition, first, of the fact that the investigation of the question why the principle mentioned is justified and to what extent it is valid constitutes an essential object of research in the foundations of mathematics, and, second, of the fact that in intuitive (contentual) mathematics this principle is valid only for finite systems.

Third insight. The identification of the principle of excluded middle with the principle of the solvability of every mathematical problem.

Fourth insight. The recognition of the fact that the (contentual) justification of formalistic mathematics by means of the proof of its consistency contains a vicious circle, since this justification rests upon the (contentual) correctness of the proposition that from the consistency of a proposition the correctness of the proposition follows, that is, upon the (contentual) correctness of the principle of excluded middle. [START_REF] Brouwer | Intuitionistische Betrachtungen über den Formalismus[END_REF], p.375, trl. van Heijenoort 1967, pp.490-491) The distinction in the First insight Brouwer had made first in [START_REF] Brouwer | De onbetrouwbaarheid der logische principes[END_REF], in which he had shown that ¬¬(𝑃 ∨ ¬𝑃), and in 1924 this led him to comment on Hilbert's aim of a consistency proof for formalised classical mathematics that 'We need by no means despair of reaching this goal' [START_REF] Brouwer | Über die Bedeutung des Satzes vom ausgeschlossenen Dritten in der Mathematik, insbesondere in der Funktionentheorie[END_REF], p.3, trl. van Heijenoort 1967, p.336). In 'Intuitionistic reflections on formalism' he added a proof that finite conjunctions of instances of PEM are also consistent, and in his first Vienna lecture he voiced the expectation that 'An appropriate mechanization of the language of this intuitionistically non-contradictory mathematics should therefore deliver precisely what the formalist school has set as its goal' (Brouwer 1929, p.164, trl. mine).

Against this background, the question that led Reeb to embrace IST is (as I formulate it) the following. If for example the classical logic in the formal theory is taken to be an idealisation of the constructive logic of mathematical reality, is there, similarly, an aspect of constructive reality that, when idealised, would lead to the notion of a standard number in the formal theory? What is asked for is an intuitive motivation, for introducing the predicate 'standard' in the idealised theory IST, not a formal proof (of the existence of formal nonstandard models).

Reeb answers that the standard numbers in a formal theory may be seen as an idealisation of what he calls the naïve whole numbers in reality ('les entiers naïfs'). They are the numbers 'that exist independently from the theory one uses to describe them' (Reeb and Harthong, 1989, p.63), and are obtained by just putting units together, Reeb's (necessarily informal) definition is (Reeb 1979, p.277, p.286n3;Reeb 1989, p.152):

1. 0 is naïve; 2. if 𝑛 is naïve, so is 𝑛 + 1; 3. No other 𝑛 is naïve.
Although the property of being naïve is not in any sense vague, so there is no threat of Wang's Paradox, 41 Reeb resists the argument by induction that the naïve numbers form a set in the classical sense, as we will see in a moment. It should also be noted that Reeb's position is dissociated from finitism: a naïve number may be constructed in an algorithm or program of any complexity (Reeb and Harthong, 1989, section 15). It is implied, then, that there is also a naïve notion of algorithm. This coincides with the idea that formal recursion theory, if to be understood as a theory of computability, presupposes such a pre-theoretical notion. 42 At this point Reeb invokes Brouwer's weak counterexamples to classical theorems. Assume the consistency of the formal theory and suppose that there is a predicate 𝐴 such that • the formal theory proves ∃𝑥¬𝐴(𝑥), or it can be shown that ∃𝑥¬𝐴(𝑥)

is independent and we are willing to add it as an axiom;

• 𝐴 and its evaluation at a naïve 𝑛 can be understood in naïve terms,

• but we do not have yet a naïve construction for such a counterexample.

In that case ZFC proves the formal existence of a natural number for which we do not have a construction in reality yet. It is a formal number in the 41. Wang's Paradox is: 0 is a small number; if 𝑛 is a small number, so is 𝑛 + 1; therefore, all numbers are small. This has generated quite some discussion; the classical papers are [START_REF] Dummett | Wang's Paradox[END_REF]Wright 1975. 42. Briefly, the point is that a recursive function is defined by a set of equations, and if the function is to be considered as computable, there must be an effective method to determine that set; but now to understand 'effective' as ' recursive' would be circular. A detailed presentation is given in Heyting 1958, pp. 340-342. For discussion and further references, see [START_REF] Coquand | Recursive functions and constructive mathematics[END_REF][START_REF] Sundholm | Constructive recursive functions, Church's thesis, and Brouwer's theory of the creating subject: afterthoughts on a Parisian Joint Session[END_REF] formal set ℕ to which corresponds no naïve number in reality (in any case not yet), and which is greater than any naïve number interpreted in the theory. Hence Reeb's slogan Q: 'The naïve whole numbers do not fill ℕ' ('Les naifs ne remplissent pas ℕ'). At first, Reeb called Q an observation ('constat'), later a slogan ('slogan'). As Salanskis points out, the latter is much more appropriate, as seeing things the way Reeb does is not a matter of direct perception but requires accepting a certain philosophical view (Salanskis, 1994, p.29). Furthermore, it requires the conviction that there always will be such predicates 𝐴 that can be understood and evaluated in naïvely.

Reeb supposed that Fermat's conjecture provided such a predicate 𝐴, writing, for example, in 1989: Consider the unique object 𝑎 in ℕ defined by the formula (not well formalised, but the reader will know how to write a perfect formula):

If the statement known as Fermat's Great Theorem is true, 𝑎 = 0, otherwise 𝑎 = 𝑥 + 𝑦 + 𝑧 + 𝑛, where 𝑛 > 3, 𝑥 + 𝑦 𝑛 = 𝑧 𝑛 , 𝑥, 𝑦, 𝑧 > 1, and 𝑥, 𝑦, 𝑧 and 𝑛 chosen such that 𝑎 is as small as possible.

At the moment I am writing this, it is not possible to convince oneself that 𝑎 is naïve. (Reeb, 1989, p.152, trl. mine) It follows from Wiles' proof, published in 1995, that 𝑎 = 0; one may think of Goldbach's conjecture instead. At times, Reeb did not invoke potential examples and limited his motivation to pointing out that the existence of such predicates 𝐴 cannot be excluded. 43 Of course, should a naïve number 𝑛 be found such that ¬𝐴(𝑛), one looks for another predicate of that type. 44 The step to IST is made by idealising the distinction between the (constructive) naïve numbers and the surplus of formal numbers in the formal set ℕ, whose existence is expressed in Q, to that between the classical standard ones and the nonstandard ones. 45 Given the differences between the notions of constructive existence in reality and formal existence in a classical theory, it is only to be expected that the idealisation will be one by analogy:

It is now a matter of drawing up a suitable list of simple and formal 43. Personal communication from Jean-Michel Salanskis, who was a member of Reeb's group. 44. For Reeb, a constructive proof can exist without having been found: 'ou bien il y a une démonstration constructive, déjà connue ou non …' (Reeb and Harthong, 1989, section 16). For Brouwer, on the contrary, the only sense in which a proof can be said to exist is that it has been constructed. However, for the matter at hand this makes no difference. 45. This idealisation need not lead to IST; it was the theory Reeb knew and liked, but closely related axiomatic nonstandard theories have been developed in the meantime [START_REF] Kanovei | Nonstandard Analysis, Axiomatically[END_REF]. Just as in the natural sciences, different theories of the same phenomena in reality may be developed, and have different theoretical virtues.

properties verified (or simply suggested) by the naïve numbers, and to consider the formal theory consisting of the statements on this list together with the axioms of classical mathematics. The theory known by the abbreviation IST developed by E. Nelson realises this program efficiently. But like every formal theory, it does not escape observation Q (i.e., 'The naïve numbers do not fill the standard whole numbers of IST'). (Reeb, 1979, p.287, trl. mine) To illustrate that last remark: the number 𝑎 defined in terms of Fermat's Last Theorem exists classically and is unique, and hence, as was clear also before Wiles' demonstration, a standard object in IST (Theorem 7, page 6).

In 'La mathématique non standard vieille de soixante ans ?', Reeb presents a beginning of such a list of properties of the naïve numbers, which, somewhat abbreviated, runs as follows (Reeb, 1979, pp.278-279): 46 Let 𝜔 be a fixed, non-naïve number.

• Property 1. If 𝑎 is naïve, then 𝜔 > 𝑎. • Property 6. If 𝑋 is a set of which every element is a naïve whole number, then 𝑋 is finite.

Reeb's argument for Property 4 is that, if the naïve whole numbers formed a set, then by induction this set would be identical to ℕ, and that would contradict Slogan Q.

If in this list one replaces '(non-)naïve number' with '(non-)standard number', and construes these statements not contentually but formally, one gets theorems of IST.

Reeb also notices (current) limitation of this motivation (Reeb, 1979, p.287): 46. As Salanskis emphasises (Salanskis, 1999, p.140), Reeb writes 'properties', not 'theorems', so as to distinguish assertions about reality from provable formulas in a formal system.

1. He should like to have a notion of 'naïve object' that extends beyond natural numbers. In the formal counterpart, IST, the predicate 'standard' can be meaningfully applied to any set, hence to any object in its universe (and thereby yield either a truth or a falsehood); but Reeb does not have a correspondingly general notion of construction. (Note that Reeb was aware of, but does not embrace, Brouwer's wider notion of constructivity.)

2. He has not been able to find a justification for the claim that whenever all naïve whole numbers have a certain internal property, all numbers in ℕ have it. (An analogue to Transfer.)

3. Likewise, while for a given naïve function such as 𝑒 𝑥 it is easily shown that an infinitesimal increase in the argument leads to an infinitesimal increase in the value, it remains to be shown that this is equivalent to (𝜀 -𝛿-)continuity of the function, which would require an analogue to Standardization.

But Transfer and Standardization are, in their full generality, by and large nonconstructive; see the fine-grained analysis by Sanders in Sanders 2017. Although Sanders' analysis is concerned with relations of the formal standard objects with the nonstandard ones, and not with Reeb's naïve objects, his results strongly suggest that such justifications as Reeb hoped to find will not be forthcoming. That is far from saying that his attempt to find a natural way into IST fails; but it does mean that the idealisations involved in moving from the distinction between naïve and non-naïve numbers to IST are stronger than perhaps was expected. 47To make the transition from the naïve numbers in reality to the standard numbers in IST more explicit, Reeb introduced a middle term, 'Naïve' (Reeb 1981, pp.453-454;Reeb 1989, pp.153-154). This term applies to all objects whose existence in ZFC is established by proving a formula of the form

∃!𝑥𝐴(𝑥)

This includes all naïve whole numbers, but much more: ℕ, ℚ, ℝ, 𝑃(ℕ), exp, sin, 𝜋, … The key principle then would be: 'There exists a finite set 𝐹 that contains every Naïve object. One could even decide to do nonstandard analysis using this informal concept. Reeb remarks that, on the one hand, the advantage of doing this is allow one to reconstruct non-standard analysis in a way of which the consistency and conservativeness are evident; on the other hand, as an informal concept Naïve may be more difficult to work with than Nelson's formal theory (Reeb, 1981, p.154). Moreover, it would require quite a sophisticated argument to justify the key principle (Reeb, 1989, p.154). His conclusion is that 'in this sense, the formalized theory IST is superior to our consideration of Naïve objects, whose interest is limited to the didactical or heuristic sphere' (Reeb, 1981, p.154). It seems to me that, as a motivation for the introduction of a distinction in an idealised formal theory, a good heuristic will fit the bill.

As is clear from the list of four 'insights', the idea that one may simultaneously accept (not just finitary but even) intuitionistic mathematics as true and formalized classical mathematics as consistent was shared by Brouwer, who at the time was even optimistic about the prospects of a formal consistency proof. Yet, Brouwer would not have called non-standard analysis in the form of IST an idealised formal theory of the mathematical reality that is the intuitive continuum. After all, IST is a syntactical enrichment of ZFC and in particular of the theory of the classical real numbers, but is not an ontological enrichment of the latter. The objects of IST are the classical real numbers. However, those can not be construed as idealisations of intuitionistic choice sequences. This is clearest from the mathematical contrast provided by Brouwer's strong counterxamples, which show that the intuitive continuum of mathematical reality, analysed in terms of choice sequences, has properties that in classical analysis with its discrete continuum are contradictory. (As we saw, IST is, on the contrary, conservative over ZFC.) Illustrative are the following: Theorem 29. ¬∀𝑥 ∈ ℝ(𝑥 ∈ ℚ ∨ 𝑥 ∉ ℚ) [START_REF] Brouwer | Über Definitionsbereiche von Funktionen[END_REF] Theorem 30. ¬∀𝑥 ∈ ℝ(¬¬𝑥 > 0 → 𝑥 > 0) (Brouwer, 1949a) Theorem 31. ¬∀𝑥 ∈ ℝ(𝑥 ≠ 0 → 𝑥 < 0 ∨ 𝑥 > 0) (Brouwer, 1949b) For Reeb these theorems are not relevant, as these they depend on intuitionistic considerations that go beyond the finitary mathematics he accepts as mathematical reality. 9 Weyl and infinitesimal analysis Overall, one suspects that to Brouwer, the glass that Reeb offers would have seemed to be half empty, what with its essential involvement of a formalism and its limitation of mathematical reality to the finitary.

For Weyl this would probably have been different. As is well known, Weyl acknowledged the epistemological superiority of intuitionism in pure mathematics:

With Brouwer, mathematics gains the highest intuitive clarity; his doctrine is the culmination of idealism in mathematics.

However, Weyl continues:

But with pain the mathematician sees the greater part of his highrising theories dissolve into the fog. (Weyl, 1925, p.24) Weyl had come to convince himself that it is necessary to abandon the intuitionistic program because he took it to be a fact that intuitionistic mathematics is not able to found the mathematics required in physics, whereas 'mathematics should put itself to the service of the natural sciences' [START_REF] Weyl | Philosophie der Mathematik und Naturwissenschaft. Leibniz Verlag[END_REF]. 48 This pushed Weyl towards a formalist foundation of classical mathematics. 49 In various physical contexts it is, conceptually, natural to apply nonstandard analysis, for example when phenomena are involved at greatly different scales, or where the difference between the observable and the unobservable plays a role. 50 In a more foundational spirit, Robert notes that, although tangent vectors can be said to represent infinitesimal displacements at a point in a differentiable manifold, it would be important to have further analyses of differentiability and of continuity, neither of which can be based on the concept of a differential; a theory of infinitesimals would be one, and moreover supply an algebra of differentials (Robert, 1988, p.xiv).

That last remark brings us to Weyl's infinitesimal geometry in his theory of spacetime, and also to the quotation from Weyl with which this paper begun. For, as Laugwitz aptly observed, And even if Hermann Weyl declared the infinitesimals to have been eliminated, his book Space-Time-Matter, widely available in several editions since 1919, is a perfect example of infinitesimal mathematics in action. (Laugwitz, 1986, p.241, trl. mine) Weyl's infinitesimal geometry is not, in fact, constructive. The fundamental notions are introduced axiomatically, instead of being constructed out of basic intuition, and the proof of uniqueness of Pythagorean metric of 1922 is, in its dependence on the excluded middle, classical. 51 Brouwer, no less of an idealist than Weyl, always was a conventionalist about the structure of physical space: 'a question of convenience, of taste, 48. For a detailed account of that episode, see for example Mancosu and Ryckman 2002, section 6.2.1 and Tieszen 2000, section 7. A recent philosophical discussion on constructive mathematics in physics is Ardourel 2012. 49. But, as we have seen (the four 'insights', p. 23), Brouwerian intuitionism does not exclude a formalist foundation of classical mathematics; it includes it as a proper part. However, it is not the part of intuitionistic mathematics that is concerned with the development of contentual mathematics; and the contentual mathematics that Brouwer sought to develop is far richer than the minimum required to get the formalist foundation going. 50. Given the properties of human vision, even at an everyday scale infinitesimal analysis can be useful, as shown by the analysis of the moiré effect in Harthong 1981. Further applications are presented in, e.g., [START_REF] Cutland | Nonstandard Analysis and its Applications[END_REF][START_REF] Arkeryd | Nonstandard Analysis[END_REF][START_REF] Lobry | Non-standard analysis and representation of reality[END_REF]. A recent view from a philosopher of science is Wenmackers 2016. 51. On Weyl's non-constructive mathematics in physics, see Weyl 1922, p.146;Weyl 1988, p.7;Scholz 2001, pp.95-97;and Eckes 2011, pp.277, 608-610, 777-778. or of custom', he wrote in 1909, in a paper to which in a reprint of 1919 he added a note stating that the general theory of relativity 'would not affect the conclusions on the theory of knowledge' he had reached [START_REF] Brouwer | Het wezen der meetkunde[END_REF], p.14, trl. Brouwer 1975, p.116;[START_REF] Brouwer | Wiskunde, waarheid, werkelijkheid[END_REF], p.vi, trl. Brouwer 1975, p.120).

Weyl was well aware of the discrepancy between his constructivist philosophy of pure mathematics and his classical practice in mathematical physics. Did Weyl ever hope to give his infinitesimal geometry a constructive foundation later -Brouwer had taken that attitude towards his own theorems in classical topology -, 52 and can a notion of subjectivity be motivated that supports, as Weyl's philosophical foundation of physics requires, the idea of a subject located in a point and whose intuitive space is of infinitesimal size 53 without, at the same time, idealising beyond a notion of subject appropriate for constructive mathematics? To investigate these questions would go beyond the scope of the present paper. But if there is no construction allowing to treat infinitesimals as individual objects, then to Weyl, Reeb's approach, what with its combination of a classical formalism for nonstandard analysis and a nevertheless intuitionistic epistemology, might have made the glass seem at least half full. 54 Acknowledgement. Earlier versions of this paper were presented at the conference 'Weyl and the Problem of Space: From Science to Philosophy', University of Konstanz, May 2015, and at the workshop 'Workshop on the Continuum in the Foundations of Mathematics and Physics', University of Amsterdam, April 2017. I am grateful to the organisers for their invitations, and to the audiences for their questions and comments. I have also benefited from exchanges with Julien Bernard (who also shared his instructive, unpublished manuscript 'New insights on Weyl's Problem of Space, from the correspondence with Becker' with me), Dirk van Dalen, Bruno Dinis, Mikhail Katz, Carlos Lobo, David Rabouin, Jean-Michel Salanskis, Sam Sanders, Wim Veldman, and Freek Wiedijk. Gödel's shorthand notes on the non-Archimedean number system in Brouwer's dissertation, mentioned in footnote 5, were kindly transcribed by Eva-Maria Engelen. These notes are owned by the Institute for Advanced Study and kept in the Department of Rare Books and Special Collections at the Firestone Library, 52. In a retrospective remark of 1920 Brouwer wrote that, when he had just begun to develop intuitionism, 'in my contemporary philosophy-free mathematical papers I have frequently also used the old [i.e., non-intuitionistic] methods, trying however to derive only such results as could be hoped to find, after the completion of a systematic construction of intuitionistic set theory, a place in the new system and claim a value, perhaps in modified form.' (Brouwer, 1920, p.204, trl. mine) 53. See in particular Bernard 2013, pp. 246-248, and Bernard's instructive, unpublished manuscript Bernard. 54. Palmgren indicates that Nelson's nonstandard analysis, which corresponds to part but not all of Robinson's, may well lend itself to constructivisation (Palmgren, 1998, p.234). Weyl, on the other hand, would presumably have been interested in the classical formalism.

Princeton University. 55

  Apply (T) to 𝐴(𝑥, 𝑡 1 , 𝑡 2 ) = 𝑥 ∈ 𝑡 1 ↔ 𝑥 ∈ 𝑡 2 .Proof 18 (Proof of Theorem 15). Let 𝑛 ∈ ℕ be nonstandard. By (S), there exists a standard subset of ℕ, notation 𝑆 {𝑧 ∈ ℕ | 𝑧 < 𝑛}, such that it includes all standard elements of ℕ that satisfy 𝑧 < 𝑛; by Lemma 16, that set is unique.11 Obviously, any standard element of 𝑆 {𝑧 ∈ ℕ | 𝑧 < 𝑛} is a standard element of ℕ. On the other hand, if 𝑧 is a standard element of ℕ, then the set {𝑤 ∈ ℕ | 𝑤 ≤ 𝑧} is a standard finite set. Theorem 10 entails that all its elements are standard, hence 𝑛 ∉ {𝑤 ∈ ℕ | 𝑤 ≤ 𝑧}, and 𝑧 < 𝑛. It follows that 𝑆 {𝑧 ∈ ℕ | 𝑧 < 𝑛} and ℕ have the same standard elements. Both are standard sets, so Lemma 16 applies and 𝑆 {𝑧 ∈ ℕ | 𝑧 < 𝑛} = ℕ.

	First we prove
	Lemma 16. Two standard sets are equal if they have the same standard
	elements.
	Proof 17.

  16. See on this pointEhrlich 2006, 69-71. 17. A recent English translation and introduction is van Atten and Sundholm 2017.

  • Property 2. … , 𝜔 -𝑎, … , 𝜔 -2, 𝜔 -1, 𝜔, 𝜔 + 1, 𝜔 + 2, … , 𝜔 + 𝑎, … (where 𝑎 is naïve) are non-naïve elements of ℕ. Likewise, the following elements of ℕ are non-naïve (where 𝑎 is naïve): 𝜔 2 , 𝜔 3 , … , 𝜔 𝑎 , … , [ 𝜔 𝑎 ] , stands as usual for the whole part of 𝑥; 𝑝 𝜔 , prime number and 𝑝 𝜔 > 𝜔 (such 𝑝 𝜔 certainly exist). The number 𝜔! is not naïve and has every naïve whole number as divisor.• Property 3. If 𝑎 > 1 is naïve, then 𝑎 𝜔 > 𝜔 𝑎 .• Property 4. There exists no set 𝑋 such that '𝑥 ∈ 𝑋' is equivalent to '𝑥 is a naïve whole number'.

a √ 𝜔 where [𝑥] • Property 5. Let 𝑋 ⊂ ℕ be a set such that 𝑛 ∈ 𝑋 for every naïve 𝑛 [respectively, 𝜔 ∈ 𝑋 for every non-naïve 𝜔]. Then there exists a nonnaïve 𝛼 such that 𝛼 ∈ 𝑋 [respectively, a naïve 𝑎 such that 𝑎 ∈ 𝑋].

See, e.g.,[START_REF] Palmgren | A constructive approach to nonstandard analysis[END_REF][START_REF] Van Den Berg | A functional interpretation for nonstandard arithmetic[END_REF][START_REF] Ferreira | Nonstandardness and the bounded functional interpretation[END_REF][START_REF] Sanders | To be or not to be constructive, that is not the question[END_REF][START_REF] Van Den Berg | Reverse mathematics and parameter-free transfer[END_REF][START_REF] Dinis | Intuitionistic nonstandard bounded modified realisability and functional interpretation[END_REF]. Such approaches are of particular interest for 'proof mining', which is the extraction of explicit information from proofs (e.g., explicit bounds for existential quantifiers, or rates of convergence).

[Note MvA: An example of Leibniz' saying this is found in his well-known letter to Varignon of February 2, 1702(Leibniz, 1859, pp.93-94).]

In two dimensions a simplex is a triangle with all its interior points; in three dimensions a pyramid with a triangle as its base.

The primary reference for this paragraph and the next is Brouwer's dissertation,Brouwer 1907, pp.8-11, but the argument is general.

Gödel 1906-1978, Arbeitsheft 14, pp.21-23; see its page 14 for the year.

Brouwer's Vienna lectures were invited by a committee of which Hahn was a member(van Dalen, 2005, p.561).

For an introduction to choice sequences, with particular attention to philosophical and mathematical differences between Brouwer's theory and Weyl's adaptation of it, see van[START_REF] Van Atten | Brouwer and Weyl: the phenomenology and mathematics of the intuitive continuum[END_REF] for their history, Troelstra 1982.

The same construction is also inBrouwer 1948, but there Brouwer does not add the comment quoted above.

[The role of Brouwer's 'contentual' mathematics' corresponds to that of Reeb's 'mathematical reality'; but the former is richer than the latter.]

This last consideration is one among several that leads to the question of constructive analogues to IST (which was not a particular concern to Reeb, to whom, on the contrary, the idea of using a classical formal theory was attractive). For this, I refer to the papers mentioned in footnote 2.