Proofs by contradiction are not accepted in some flavors of mathematics, like constructive mathematics. In fact, constructive mathematicians believe in a definition of real numbers that is more in line with what this paper talks about.
A true proof by contradiction would be "Assume [0, 1] is not uncountable. That leads to a contradiction, so [0, 1] is not not uncountable. By the law of the excluded middle, [0, 1] is therefore uncountable."
This proof seems to be "Assume [0, 1] is countable. That leads to a contradiction, so [0, 1] is not countable." That's not a proof by contradiction - it's just how you prove a negative.
This is a nice blog post about the distinction: https://existentialtype.wordpress.com/2017/03/04/a-proof-by-...
The terminology gets abused a lot, even by professors. It's actually hard to find theorems which really require proof by contradiction.
Nitpick: that's not excluded middle, that's double negation elimination. They're both non-constructive and (IIRC) equivalent in most formalizations, but they're not the same thing.
Could you provide a citation for this? I can vaguely see how that might work, being ~~Q->Q for the special case where Q can be decomposed into Q = ~P, but it's obviously rather difficult to search for.
A statement about the reals which is provable under constructive mathematics does not reduce to a statement about the computable reals and vice versa. A set can be constructively definable without all of its elements being constructively enumerable.
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.
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.
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.
[2] https://en.wikipedia.org/wiki/Interesting_number_paradox
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.
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.
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).