Is the real number line actually real when we construct it?

Question

Intuitionism is akin to constructivism in mathematics but not quite the same from what I can tell.

In the usual treatment of the real line, the additional numbers are found between the rationals by supremum, that is for a sequence of rationals like 3,31/10,314/100,.. we can approaches the real number pi.

But constructively can we allow such a principle since we are positing the existence of such a number, without in fact actually constructing it - we are just getting arbitrarily close to it.

Wikipedia explains this as a choice sequence

In intuitionistic mathematics, a choice sequence is a constructive formulation of a sequence. Since the Intuitionistic school of mathematics, as formulated by L. E. J. Brouwer, rejects the idea of a completed infinity, in order to use a sequence (which is, in classical mathematics, an infinite object), we must have a formulation of a finite, constructible object which can serve the same purpose as a sequence. Thus, Brouwer formulated the choice sequence, which is given as a construction, rather than an abstract, infinite object.

It suggests that Brouwer rejects the real line as a completed infinite object (a real object) and uses instead choice sequences to somehow test for points in an indeterminate, in some sense, real line.

This explains the question in the title: The real line, or rather the continuum (because the real line refers to the classical construction by either Dedekind cuts or Cauchy sequences, and thinking of the continuum is a notional object before being axiomatised), when constructed (in the philosophy of constructivism), by rejecting completed infinities, cannot take the ideal points produced by the Dedekind cuts or Cauchy sequences as constructed, but somehow must work with, it appears with the sequences themselves.

Answer 1

Preliminary "terminological" note.

There are several approach to constructive mathematics: one of them is intuitionistic one.

Intuitionism was founded by Brouwer: he formulated a "kantian-like" philosophy of mathematics (regarding numbers, not geometry). His philosophy is not usually followed by mathematicians.

From intuitionism the intuitionistic logic has born: it is very interesting and widely studued today. Brouwer did not liked formalization; he was not interested in formal logic.

There are current development of constructive analysis (Bishop, Bridges, Beeson) that do not use intuitionistic logic, but the classical one.

---

What is the common future of those approach : the rejection of some usual methods of proof used in mathematics. First of all so-caled "non-constructive" proofs.

See Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 26 :

Classical logic contains the principle of indirect proof: If ~A leads to a contradiction, A can be inferred. Axiomatically expressed, this principle is contained in the law of double negation, ~~ A => A. The law of excluded middle, A v ~ A, is a somewhat stronger way of expressing the same principle.

Under the constructive interpretation, the law of excluded middle is not an empty "tautology," but expresses the decidability of proposition A. Similarly, a direct proof of an existential proposition Exists x A consists of a proof of A for some a. Classically, we can prove existence indirectly by assuming that there is no x such that A, then deriving a contradiction, and concluding that such an x exists. Here the classical law of double negation is used for deriving Exists x A from ~~ Exists x A.

In conclusion, what all constructivists share is the rejection of the above method of proof : if I want to show that a number with a certain property P exists, I have "to show" a number n such that P(n). I'm not licensed to assert that a number with a property P exists, only when I'm able to derive a contradiction from the assumption that such a number does not exists.

You can exploit this "rejection" through intuitionistic logic, where the above rule of proof is not sound, or through a "careful" use of classical logic, i.e. avoiding this kind of proofs.

---

Second "terminological" note.

In order to avoid misreading I sugegst to use the description "real number line" as a definite description: the "real" must not be extrapolated and used as an adjective.

So, when we read "is the real number line real ?" we are not alluding to some "heideggerian mistery"; we are simply asking if we stay with the existence of a certain specific "kind" of numbers.

According to the constructivists, we can legitimately "speak of" only those real numbers that we are able to "construct": they are all the rationals, the algebraic ones and all the "baptized" irrationals, like SQRT(2), 3,14..., e, and so on.

A "classical" approach to constructive analysis is through "computable" numbers, i.e. all those numbers that are approximable through some algorithms (all the above are).

It is obviuos that computable numbers are countable : an algorithm is a finite set of instructions (all of which are finite strings of symbols).

Now, if we take into account Cantor's proof of the uncountability of the real, we have that no bijection exists from the natural numbers to the point in [0,1]. The classical approach conclude to the existence of uncountable many real numbers: I do not "see them" but they are "there" ...

Thus (and I beg your pardon for so long a post) the constructivist objection :

if the numbers that we may "know" (speak of, define them, name them) are countable, what kind of "reality" do have "all other" (uncountably many) (ir-)real numbers that we will never know ?

I personally appreciate the constructive manifesto of Errett Bishop, Foundations of constructive analysis (1967), page 2:

The primary concern of mathematics is number, and this means the positive integers. [...] Mathematics belongs to man, not to God. We are not interested in properties of the positive integers that have no descriptive meaning for finite man. When a man proves a positive integer to exist, he should show how to find it. If God has mathematics of his own that needs to be done, let him do it himself.

Almost equal in importance to number are the constructions by which we ascend from number to the higher levels of mathematical existence. [...] A set is not an entity which has an ideal existence. A set exists only when it has been defined. To define a set we prescribe, at least implicitly, what we (the constructing intelligence) must do in order to construct an element of the set, and what we must do to show that two elements of the set are equal. Building on the positive integers, weaving a web of ever more sets and more functions, we get the basic structures of mathematics: the rational number system, the real number system, the euclidean spaces, the complex number system, and so forth.

Thus even the most abstract mathematical statement has a computational basis.

The transcendence of mathematics demands that it should not be confined to computations that I can perform, or you can perform, or 100 men ,vorking 100 years ,vith 100 digital computers can perform. Any computation that can be performed by a finite intelligence - any computation that has a finite number of steps - is permissible.

Answer 2

Depends on what you take a "construction" to be. Some self-described constructivists accept the Axiom of Choice (Bishop) and therefore accepts the existence of all reals. Other constructivists do not accept their existence, although as far as I know, everyone thinks their expression is well-formed. While the common way of expressing a real is "something you approach by a sequence of rationals, which is not rational" it isn't necessary to do so. You can just ask "Does this sequence converge, and if so, does it converge to a point that exists?" Some constructivists would agree that the sequence converges (distances become arbitrarily constrained as the sequence continues), but that it does not converge to a point. I suppose a very hard-lining finitist constructivist might not accept the formulation of infinite sequences, but that's a pretty zealous constructivist.

Answer 3

Since time is an intuition and time is continuous, the continuum is an object in intuitionism. There is no problem with geometry, Euclidean or non-Euclidean, for instance.

But because of things like Zeno's paradox, we have to accept our intuition fails to make the points on the real line clear as individual objects that can be constructed. There is nothing wrong with the basic notion of convergence, but if in subdividing time and space you are always converging to some given place you actually do have to listen to Zeno, which contradicts the notion of moving time.

So, from an intuitionistic POV Dedekind cuts are out and Cauchy sequences are useful, but do not necessarily exist for every point, and surely do not define the set of real numbers. Then, if the points are only procedural approximations and not real objects, clearly the collection of them as a completed object cannot be constructed.

Motion is an essential part of the intuition of continuous time. And since Brouwer sees continuous space as deriving out of that intuition, movement is part of the notion of space through the notion of continuity itself. Intuitionism quite notably demolishes the analytic and topological definitions of continuity in static terms, making either all or none of the functions from R to R continuous. So it needed a different notion of contiunity, all its own.

Meanwhile, the mapping of digit sequences to approximations via construction steps seems obvious. So Brouwer was kind of obsessed with delineating the degree to which these two pictures could be drawn together into an efficient way of looking at analysis without discarding the notion of movement inherent to the concept of continuity and therefore of the continuum. Kleene's two books on intuitionism (references to which I do not have at hand) lay out first Brouwer's own defense of the usability of intuitionistic approaches to analytic problems, which involve the cumbrous and obsessive notions of choice and securability, and then shows that they are formally equivalent to a clearer kind of constructivism tied to recursive functions.