2 ms·

There's more than one way to prove the real numbers uncountable. All of them assume something though! https://link.springer.com/content/pdf/bbm:978-1-4614-8854-

There's more than one way to prove the real numbers uncountable. All of them assume something though! https://link.springer.com/content/pdf/bbm:978-1-4614-8854-5/1.pdf https://link.springer.com/content/pdf/bbm:978-1-4614-8854-5/... There's a recursive subdivision approach that goes back to Cantor. If the subdivisions form a disjoint cover, then the Law Of Excluded Middle (actually, the weaker Limited Principle Of Omniscience) gets used. This proof is equivalent to the popular decimal-digits proof. The problem is that the decimal digits of a real number may not be computable, so there is a dependence on Excluded Middle. If the subdivisions form an open cover, then Dependent Choice gets used to resolve the ambiguity created by open sets overlapping, but LEM gets avoided. This forms an algorithm you can do on a computer, to produce a real number not in a given sequence. The dependence on Dependent Choice can be improved to Countable Choice, which effectively parallelises the algorithm. There's another approach based on the fact that countable sets have measure 0. This then implies that the reals have measure 0. To actually get a rigorous contradiction, you need to use the compactness of the interval [0,1]. In constructive logic, this is a consequence of Open Induction (but can be improved to use the "Fan Theorem"). So you need either LEM (really, LPO), Dependent Choice (really, Countable Choice), or Open Induction (really, Fan Theorem). The Dependent Choice approach even determines an explicit algorithm. But there's no unconditional proof. And if the result in the video is correct, there can never be one, because it's possible that the real numbers are countable.

mjburgess 4y ago
It's "possible" presumably only in the sense in which one can assign a True/False value to any proposition. I guess one could see a logic as deciding if a set of propositions is inconsistent. And one could imagine a "trivial logic" which says "Yes" for any set, consistent?(props | logic) = Yes. Then as we add more structure to the logic, more sets become inconsistent: consistent?(CountableReals | LawExMiddle) = No. What value is there to saying the reals are "possibly" countable when it seems we're basically enforcing no consistency in the set of propositions which would constitute a "proof" of such a thing?
- chriswarbo 4y ago
  Euclidean geometry is a common example of this: if we remove the parallel postulate, we get a weaker theory; unable to prove various "facts". However, this weaker theory is also more general, applying to curved spaces too; where those facts are not true. It turns out that the physical universe is curved, and hence those original "facts" don't hold in the 'real world'. It seems like a similar thing is happening here: we can prove that the set of reals is uncountable, but only if we use classical axioms which don't account for computability. Using a weaker (intuitionistic/constructive) theory prevents us proving that the reals are uncountable; that turns out to be necessary, because some of the alternatives cause the reals to be countable. Since the physical universe is computable (or at least, computably indistinguishable from being computable), these alternatives may be better descriptions of the 'real world' than classical logic.

mjburgess 4y ago

It's "possible" presumably only in the sense in which one can assign a True/False value to any proposition. I guess one could see a logic as deciding if a set of propositions is inconsistent. And one could imagine a "trivial logic" which says "Yes" for any set, consistent?(props | logic) = Yes. Then as we add more structure to the logic, more sets become inconsistent: consistent?(CountableReals | LawExMiddle) = No. What value is there to saying the reals are "possibly" countable when it seems we're basically enforcing no consistency in the set of propositions which would constitute a "proof" of such a thing?

chriswarbo 4y ago
Euclidean geometry is a common example of this: if we remove the parallel postulate, we get a weaker theory; unable to prove various "facts". However, this weaker theory is also more general, applying to curved spaces too; where those facts are not true. It turns out that the physical universe is curved, and hence those original "facts" don't hold in the 'real world'. It seems like a similar thing is happening here: we can prove that the set of reals is uncountable, but only if we use classical axioms which don't account for computability. Using a weaker (intuitionistic/constructive) theory prevents us proving that the reals are uncountable; that turns out to be necessary, because some of the alternatives cause the reals to be countable. Since the physical universe is computable (or at least, computably indistinguishable from being computable), these alternatives may be better descriptions of the 'real world' than classical logic.