[mbid]

I don't understand this. For a constructivist, "¬A" means "from A, falsity is derivable". You can derive falsity from the statement "there is a countable enumeration of the real numbers". A diagonal function given such an enumeration is constructively definable, and it is also constructively true that it is not equal to any of the enumerated ones (because 0 != 1 is true constructively). Thus, the diagonal is not enumerated all real numbers, but it also is by assumption, thus falsity.

What does make real numbers weird when working constructively is that you cannot conclude |x| > 0 from x != 0. This means that 1 / x need not exist even if x != 0, so the real numbers do not form a field in the classical sense.

If you don't trust me, maybe you'll trust wikipedia: https://en.wikipedia.org/wiki/Constructivism_(mathematics)#C....

[mietek]

> The interpretation of Cantor's result will depend upon one's view of mathematics. To constructivists, the argument shows no more than that there is no bijection between the natural numbers and T.

https://en.wikipedia.org/wiki/Cantor%27s_diagonal_argument#I...

[Confusion]

A surjection seems silly: doesn't that imply that some reals would be indistinguishable? Or can you indeed not prove that more than the natural number of reals are distinguishable in constructive mathematics?

[mbid]

Honestly, the result hinted at in the wikipedia article caught me by surprise as well: There are some flavors of constructive mathematics (notably CZF), that are still consistent if you also add the statement "There is a subset A of the natural numbers such that there is a surjection from A onto the real numbers". Note that this does not imply that you can prove this in CZF, it only means that you cannot disprove it. See http://www1.maths.leeds.ac.uk/~rathjen/acend.pdf prop. 8.2 if you're interested.

Wikipedia says that the Cantor argument shows "no more" than that there is no bijection between the natural numbers and the real numbers. As far as I can tell, it also proves that there is no surjection from the natural numbers onto the reals in every system of constructive mathematics I know of, so I think this is slightly misleading.

What do you mean by "distinguishable"? In constructivism, a set A such that x = y or x != y for all x, y in A is sometimes called decidable. And yes, it is indeed not true that the real numbers are decidable. This would imply that there is an algorithm that decides whether two infinite sequences of ones and zeroes will differ at some point or agree indefinitely, which is pretty much equivalent to solving the halting problem. On the other hand, the natural numbers, integers, rational numbers and every finite algebraic extension of the rational numbers (for example Q[i], "rational imaginary numbers") is decidable.

[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.

[Confusion]

OK, then it isn't as silly as I thought. I guess 'distinguishable' was my layman's approximation of the formal term 'decidable'.