[btilly]

And this is the key result that I am thinking of.

Furthermore if we limit all mathematics to things that can in principle be done on a Turing machine, then this statement is trivially true because all possible Turing machines is a countable set.

Moving from Turing machines to a Turing-complete programming language, we could define a real number as an equivalence class of functions from positive integers to fractions such that for each function |f(n) - f(m)| <= 1/n + 1/m, and two such functions are equivalent if |f(n) - g(n)| <= 2/n for all positive n.

The question of whether a given function is actually a real number is in general undecidable. The question of whether two functions represent the same real number is also undecidable. However it is easy to create a set of functions that will definitely include all real numbers under this definition (and a few things that are not), but some of those real numbers will be included multiple times.

And the really important point about this is that suddenly "uncountable" doesn't mean "more". It just means that there is an undecidable question or three creating complexity in the way of generating the mapping.