For those interested in constructive and intuitionistic approaches here Dummett's [0] Elements of Intuitionism is an extremely good read.
Intuitionism is a form of a constructive foundation for mathematics which (a) notes that any attempt to deny the uncountability of reals leads to difficulties and (b) any attempt to internally define them violates constructivity.
The resolution proposed is to posit the existence of "free choice sequences". These are essentially "unpredictable" sequences of potentially infinite binary choices. As there is no a priori reason to believe that they can be predicted they are able to be much larger than what is computable and thus can be used to give a characterization of the reals. Atop this you build a constructive understanding of free choice reals which behaves very nicely (at least foundationally... it points out all kinds of weirdnesses about what we assume classically to be the structure of reals).
What's very nice about this solution is that it sidesteps the difficulty. Free choice is a weaker thing to ask for than finite/constructive reals, but finite/constructive reals could be transparently encoded into free choice sequences and all the math would just work.
Intuitionism is a form of a constructive foundation for mathematics which (a) notes that any attempt to deny the uncountability of reals leads to difficulties and (b) any attempt to internally define them violates constructivity.
The resolution proposed is to posit the existence of "free choice sequences". These are essentially "unpredictable" sequences of potentially infinite binary choices. As there is no a priori reason to believe that they can be predicted they are able to be much larger than what is computable and thus can be used to give a characterization of the reals. Atop this you build a constructive understanding of free choice reals which behaves very nicely (at least foundationally... it points out all kinds of weirdnesses about what we assume classically to be the structure of reals).
What's very nice about this solution is that it sidesteps the difficulty. Free choice is a weaker thing to ask for than finite/constructive reals, but finite/constructive reals could be transparently encoded into free choice sequences and all the math would just work.
[0] https://www.amazon.com/Elements-Intuitionism-Oxford-Logic-Gu...