How real are real numbers? (2004)

The point is straightforward - the fact that you have defined a country on a map, doesnt mean you have defined all its cities and towns. Especially if the number of markers you have are less than the number of towns.

Also, we can talk about definable numbers as long as we choose some specific system which we assume is consistent. So we are talking about numbers which are definable by predicates using the language of ZFC or Peano Axioms.

There is no need to invoke computability, just definability is sufficient. There are lots of definable numbers which are not computable(like Chaitins constant or the real number whose digits encode information about halting of Turing Machines).

But even with this more relaxed constraint, we still dont have enough definable numbers.

>How does analysis require the existence of uncomputable reals?

I don't know what the other person was referring to, but from many important theorems of analysis you can prove the existence of uncomputable reals. For example, from the theorem that a continuous function on a bounded interval is uniformly continuous you can prove that there exist uncomputable reals. If we think that this theorem and many more like it are necessary for analysis, we must conclude that analysis requires the existence of uncomputable reals.

The above fact comes from the area of mathematical logic known as reverse mathematics. The idea is in the name: rather than proving theorems from axioms, we go in reverse. We take some theorem and we see what axioms we can derive from it (using a weak background theory). This gives us a sense of the logical strength of a theorem; the stronger the axioms we can prove from it the stronger the theorem.

An amazing fact is that most classical theorems of mathematics have their logical strength captured by one of five sets of axioms. The weakest are those which are outright provable from the weak background theory (briefly, the background theory, called RCA_0, says that you're allowed to do computable processes). The next is the theory WKL_0, formed from RCA_0 by adding an additional axiom, which goes by the name weak Kőnig's lemma. This axiom states that any infinite binary tree has a cofinal branch (it's a lemma in 'ordinary' mathematics but in reverse mathematics gets treated as an axiom). This is the theory which captures the logical strength of the theorem I mentioned in the first paragraph. From weak Kőnig's lemma we can prove the existence of uncomputable reals. We can construct a computable infinite binary tree so that any branch through it must be uncomputable. From such a branch one can build an uncomputable real, say by insisting that the nth bit in its binary expansion is 1 if and only if the branch went left at level n.

(The easiest way to build such a tree is to go through the halting problem. The basic idea is to construct a tree of attempts to solve the halting problem. It turns out this can be done in a computable way, and any branch through the tree will allow us to solve the halting problem and thus must be uncomputable. The key fact used is that while there's no computable procedure to check whether a Turing machine halts at some time, you just want to know whether it halts in n steps (for fixed n), then you can check that with a computer. The program is easy: simply simulate running the Turing machine for n steps and see whether it stops at some point.

To build our tree: list the Turing machine programs as p_0, p_1, p_2, ... (This listing can be done in a computable way.) We will associate level n+1 on the tree with p_n. Start with a single node for the root of the tree. Then, to build the (n+1)-st level of the tree, look at each node t on the nth level. Check, in a computable way, whether p_0, p_1, ..., p_(n-1) halt within n steps. If none of them halt, then t has a left and right child at the next level. If p_k does halt within n steps, then look below t to see whether you took the left or right path at level k to get to the node t. If you took the right path, then t gets no child nodes. Otherwise, if you took the left path whenever p_k halts within n steps, then t gets two child nodes. Intuitively speaking, at stage n we keep our options open and don't decide whether p_n halts. But if we later see that it does halt, then we retroactively fix any mistake by not going any further along paths where we guessed wrongly before.

For example, it could be that p_0 halts but it takes 1000 steps for this to happen. So while building the tree when you get to level 1000 you'll suddenly stop building any further the entire right half of the tree, since you finally learned that p_0 halts and that you wanted to go left at the root node all along.

This process for generating the tree is computable, so by definition it's a computable tree. It's infinite, because you can keep building the tree upward if you happened to have guessed correctly whether each Turing machine so far halts. However, no branch through this tree can be computable. This is because a branch goes right at level n if and only if p_n didn't halt within k steps for any k. That is, the branch goes right at level n if and only if p_n doesn't halt, so from a branch we can decide the halting problem.)

----

Probably the best reference for reverse mathematics is Stephen Simpson's book Subsystems of Second-order Arithmetic. The first chapter is freely available on his website. It nicely lays out the philosophy behind the project and the major results while deferring (most of) the technical details to the rest of the book. http://www.personal.psu.edu/t20/sosoa/chapter1.pdf

Besides that, the wikipedia page for reverse mathematics isn't awful, but neither is it very good. https://en.wikipedia.org/wiki/Reverse_mathematics

The discussion really helps me understand the problem. Real numbers are infinity in disguise. Because infinity is not really defined, real numbers are not really defined. Just saying infinity is not finite does not make much sense (in the sense of adding anything helpful). Any real number that you can finitely describe can be included in a finitely described counting scheme. Let's use the counting schemes of rational numbers, I'll hit arbitrary numbers to arbitrary precisions. Taking a limit, it is not clear that I miss any numbers (including pi). To defeat this scheme, the adversary has to keep adding digits to his real number, as well as keep shrinking his allowed precision infinitely. Now both the number (that is being infinitely being described) and my counting process is infinite, we didn't and can't prove anything. There is simply no conclusions to be drawn.

> I'll try to physicalize countability.

> Start counting the naturals: 1, 2, 3, ...

> At future timelike infinity you'll reach infinity.

> Now for the reals. Your goal is to step from 0 to 1, by way of 0.1, 0.01, and so forth.

> 0 0.0........

> At future timelike infinity you still haven't stopped adding in zeroes to the right of the decimal point.

> In the first case, at any finite time before \breve{i}^+ you will have counted out some finite natural number. In the second case, you will not yet have counted out your first nonzero real.

The same reasoning applies for rationals, yet they can still be counted.

The definition of «can be counted» means there is a bijection between your set and the naturals. Such kind of bijection can easily be created for the rationals[1] and Cantor's diagonal argument[2] shows that you can't create such bijection for reals.

There is nothing really intuitive about this concept, but fortunately the proofs are pretty straigtforward which give a kind of «intuition» around this.

[1] https://en.wikipedia.org/wiki/Pairing_function#/media/File:D...

[2] https://en.wikipedia.org/wiki/Cantor%27s_diagonal_argument

I think you're right on the money bringing Turing into this.

I don't have a real, formal horse in this race, but the way that I have things arranged in my mind is that these are all disagreements on the notion two things in logical foundations: the need to consider time/resources and the conception of logical systems as closed or open.

Brouwer and Hilbert accept that time is a factor, but handle it in different implicit ways. Hilbert differentiates between finite (time accessible) and infinite (not finite) and then makes a plea that this divide doesn't much matter. His Program sought to prove it and then Turing and Godel and the like shattered that dream. Brouwer philosophically treated proof as communication and thus Intuitionism handles time and resource naturally (though not explicitly like a Kripke model).

Brouwer was forced by this choice to leave his mathematical foundations open ended as well. At any given level of effort there is a finite set of things we can prove/talk about/know and the rest must be left unknown, but likewise at any point in time we can incrementally increase our knowledge. Intuitionism is complex in order to handle that openness.

Bringing Turing in makes openness and expense/time immediately obvious. Turing machines are a model for an open world of knowledge: once you have a partial halting oracle G I can build a new program which your oracle fails on. Godel took it to the next level: your own formal system cannot prove its own consistency, but using it I can create a larger universe where it can be proven consistent.

In each case, the result arises from wanting a formal closure of your foundation and both use self-reference to create a (co-)inductive means of incrementally enlarging your system forever.

So I think Brouwer beats them to the punch in a certain way by taking that continuous finitary expansion as foundational itself.

Free choice can't be modeled formally by "Turing machines" because we possess a means for writing them all down. On the other hand, if I give you the trace of a Turing machine you have no (finite) means to predict it so "Turing machine traces" do provide the largeness you need. I don't really know how to handle the fact that someone might want to form a bijection between the two. To me it makes me think immediately of information hiding behind an abstract interface: even though you could eventually know an implementation of the interface, you spend most of your time working ignorant to it and often have more power for doing so.

I'm definitely no expert here, but I think it's all really fascinating. Definitely agree that Brouwer didn't produce anything of much use to day-to-day mathematicians, but that's sort of Hilbert's (and Turing's) point: practical common sense doesn't seem too impeded by this.

I think as computer scientists we're essentially carrying out a certain mathematical/philosophical program in this debate, fwiw. Turing showed that if you take working computationally very seriously that you will run into open-endedness and time-as-resource constraints very quickly. Programming is a long exercise in discovering just have very seriously you have to take both of those things (interfaces, abstraction on one side, resources, human patience on the other).

Brouwer and intuitionism are subsequently having a bit of a resurgence in mechanized proving. The non-computability of reals shows its ugly head every time someone working in computational optimization has to write `compare_espilon` instead of just `equals`. Or, perhaps even better, every time someone gets bitten by thinking IEEE reals are "mathematical reals".

I also really like to imagine this because I love this idea that each programmer is unknowingly taking very tiny steps along a grand philosophical program. Unromantically it's obviously true, but there's something fun in trying to imagine just how profoundly computers may yet still impact our understanding of the world.