Ok I think what happens here is that we assume for the real numbers an increasing sequence which is bounded converges. I think that a number system with this property is probably already hard to construct in constructive math.
No. The real numbers are constructed as located Dedekind cuts, or modulated Cauchy sequences. There are no issues with this construction in constructive mathematics.
You are indeed right that you can't show that an increasing and bounded sequence of real numbers has a limit. But you can prove constructively that if a sequence of real numbers is Cauchy then it has a limit. And it is that last property which is the defining property of the real numbers (Cauchy completeness).
So the problem that constructive math has for real numbers is that it's hard to show real numbers exist at all, not that it's uncountable if you have its properties. Also the deeper point is that you have all the properties of the real numbers you can actually derive the law of excluded middle. (Coming from the supremum axiom)
> So the problem that constructive math has for real numbers is that it's hard to show real numbers exist at all
No. They exist in any topos with a Natural Number Object. In other words, they exist in all varieties of constructive mathematics that admit a set of natural numbers.
Brouwer (father of intuitionism) rejected actual infinity. He would not admit the axiom of infinity and therefore reject the set of all natural numbers. Tough to do things that way though.
Brouwer distinguished between actual infinity and potential infinity, with the former inadmissible in intuitionism. He would say “the largest natural number” is a meaningless statement. You could only have the “largest so far”.
Intuitionism invites you to construct as large of a natural number as you want. It simply does not admit “the complete set of all natural numbers”.
The point of intuitionism is the idea that all mathematics is constructed by human creativity and logic. Brouwer rejected the idea that mathematics was “already out there, waiting to be discovered”. This is a subtle point. It says that mathematical objects do not exist in some mind-independent realm of truth. It has the nice property of avoiding some of the problems of classical mathematics that Hilbert got caught up in.
“So far” with respect to some particular problem you’re solving or process you’re following. If you’re talking about all problems, you’d have to do some research. Perhaps OEIS [1] could help you. Or you could interview some number theorists to find out who is working in large numbers and ask them.
Asking the question in general, though, is equivalent to asking “what is the largest number anyone has thought of?” I would have to interrogate your motives to know why you would want to ask such a question.
Intuitionists would scoff at the idea of a “number larger than anyone could describe.” That’s heading into the territory of the interesting number paradox [2]. Intuitionism avoids this paradox by stating that numbers (and sets of numbers) have no existence independent of their construction.
" “what is the largest number anyone has thought of?” I would have to interrogate your motives to know why you would want to ask such a question..."
I ask because it's absurd. A particular large number is a logical thing regardless of whether a person thought of it before or whether it describes a distinct natural phenomenon. This follows from the set theory axioms, as well as Real numbers and infinitely many other number systems. To restrict our capacity to think of numbers to only numbers that people can enumerate or numbers that describe natural phenomena seems arbitrary and onerous. We construct the Real number simply by considering the limits of convergent sequences to be numbers. I don't see anything transgressive about this idea. Sure, some numbers are not computable, and other numbers can't be represented with marbles; they still have utility and there is no reason to make the concept of "numbers" exclusive.
Certainly in Agda I've personally proved that the "Cauchy sequences of rationals" formulation is a partially ordered ring.
However, I believe (but have not tried it and have not proved) that if you stick with Agda's incredibly strict and purely computational logic, the proof does indeed fall over. The problem is that Bob can't identify in general whether one real is less than another (indeed, this would imply solving the halting problem), so he can't know whether he's allowed to pick s_n at time n or not: he can't know whether s_n is less than his current number and hence a valid choice.
This is really interesting. I'm not surprised by axiom of choice being based on real numbers. I've been thinking about that lately but I don't have a good intuition why. Do you have a link?
I'd be very surprised if it were true in general. But there certainly has to be some non-computational component to the reals being a complete totally ordered Archimedean field, because the question of deciding the equality of two reals is uncomputable, so there is no procedure to decide the total order.
