Are the reals really uncountable?

Stream: new members

[Niels Voss]

I apologize if this question is too philosophical in nature, but there's been something about the reals that I've been wondering about.

My understanding of how the reals are defined in mathlib is that they are the quotient of a Cauchy sequence under some equivalence relation, and a Cauchy sequence is just a function f : nat -> rat with some special properties. If we ignore the quotienting and the special properties of the function, then a real is kind of close to a function nat -> rat. However, in Lean, all functions are built out of finitely many symbols, so there are a countably infinite number of functions that we can actually define. This means that there are also a countably infinite number of real numbers that we can actually define as well.

What confuses me is this: isn't real the type of all terms we can construct using these functions from nat -> rat? Wouldn't that mean that the reals are countable? Or does real include terms that we can't describe in any way (which contradicts what I know about inductive types)?

I don't know how cardinal.not_countable_real is proven, but lets say for a second that you could potentially prove it if, given any countable set of reals, you produce a real that isn't in that set. If you were to take the set of reals that are expressible in Lean, you wouldn't be able to produce any new real number not in that set, because then that real would be, by definition, expressible.

As far as I know, this set of expressible real numbers cannot be defined from within Lean, and so cannot be used to derive a contradiction. But to me, it seems like we haven't proven that there is no countable set containing all reals numbers, we've just proven that there is no countable set containing all real numbers that we can define from within Lean. So would proving something isn't countable in Lean just show that there isn't a way to construct a bijection to nat, and not that one doesn't exist?

[Kevin Buzzard]

It's not true that in Lean all functions are "built out of finitely many symbols". It's just the case that the functions you can explicitly write down are built from finitely many symbols. You can only write down countably many real numbers but you can still prove there are uncountably many, most of which do not have names.

[Michael Stoll]

This is a well-known apparent paradox and not specific to Lean. See Skolem's paradox.

[Matt Diamond]

the Stanford Encyclopedia of Philosophy also has a nice overview of Skolem's paradox: https://plato.stanford.edu/entries/paradox-skolem/