Mayhap.

>A constructivist would state the result in a variety of ways. But none of them would involve a potentially self-referential construction based on the absolute truth of an infinite number of statements. Which really does rule out Cantor's argument.

But in any case you misunderstand Cantor's argument and constructive mathematics.

mbid is correct; Cantor's diagonalization argument constructively proves the uncountability of the real numbers, see e.g. Bishop-Bridges' CONSTRUCTIVE ANALYSIS, Theorem 2.19, page 29.

You didn't prove that statement, and actually Cantor's diagonal arguments [1] proves you wrong:

Consider the set of «all real numbers which you can actually specify IN ANY FASHION AT ALL». If you can count it, you can order them in a certain fashion: n0, n1, n2, n3 … It's easy to specify a number X which is not part of this set (which is in contradiction with the definition of this set, and demonstrates ad absurdum that this set is not countable). To build such X, consider the n-th decimal of the n-th number: if it's zero, the n-th decimal of X is 1, otherwise the n-th decimal is 0. Then by construction, X is different from any number of this set, which mean X is not a part of the set. ?

[1]: https://en.wikipedia.org/wiki/Cantor%27s_diagonal_argument

The distance between discrete infinite sets (countable) and continuous infinite sets (uncountable) is a pretty large gap. Are you saying that there is no gap? There are pretty well studied proofs showing that uncountable sets are much bigger than countable.

What's your take on this? Got a counter proof to Cantor?

It does follow because the set of finite collections of symbols is countable.

> How could the diagonal construction ever finish to allow a "check" of whether the result of that process is actually on the list.

> The diagonal just seems like a shortcut to a number that we know the first process hasn't gotten to yet?

I think you are mixing up the enumeration of the (hypothetically countable) reals with the existance of said set of reals, and viewing the construction of the counterexample as an actual process that involves programmatically iterating over the list instead of a description of how the digits of said new real number is created.

There is no pause or setp-by-step of this iteration that's required, since it's only telling you that the i'th digit of the counterexample will be distinct from the i'th digit of the i'th number (thereby creating a real not in your countable set, since you have created a number outside of your 1-1 mapping onto the natural numbers).

What exactly happens when you try to apply Cantor's diagonal argument to this model?

I guess that at some step, you get an answer like "outside of the model, yes this exists, but inside the model the answer is no", but I would like to see it precisely, how exactly the in-model reasoning diverges from the outside-model reasoning.

> In such a sense then, we can trivially "count" the real numbers unless we hold the philosophical view that there are real numbers that are not expressible. This is where it becomes a question of philosophy of mathematics, not mathematics proper.

I'm not disagreeing with your interpretation of Cantor's diagonal proof, I'm merely pointing out that this interpretation depends on a very specific philosophical view of mathematics, namely the platonist view that the real numbers exist independently from their expressions in any natural or formal language and that it makes sense to say that there are real numbers that are not expressible.

And yeah, nearly all working mathematicians will agree with this view and from their perspective the real numbers are uncountable, period, and you are right that what I sketched "doesn't work".

But I think it's important to remember that there are or could be alternative philosophical views of mathematics that lead to a different interpretation, which will reject not the mathematical validity of Cantor's diagonal proof, but rather its usefulness or relevance. After all, how can you convince someone that there are real numbers that are not expressible? By their very nature they cannot be practically used in any calculation, so how could you convince someone who is not convinced by this philosophical assumption of Cantor's diagonal proof?

In other words, Cantor's diagonal proof cannot prove that there are real numbers that are not expressible, because the proof only makes (philosophical) sense if you accept this viewpoint in the first place.

You seem to be thinking of a real as a string of digits, or a block of bits, which is just the representation of a real. Like, a number doesn't exist until you think of it. That view doesn't help much in thinking about these matters.

> So then what Cantors proof is saying is that if you could somehow count to infinity and get to a result, some infinities would have more elements than others. But that is a contradiction, because you can’t finish counting to infinity.

So you're saying Cantor's "proof" embodies a contradiction. You must be a very great mathematician. I'm not a mathematician, so I'd better just bow out now. Anyway, I'm way too old to start thinking of numbers as some kind of generative process.

It opens:

> In 1874 Georg Cantor published a theorem stating that every sequence of reals is avoided by some real, thereby showing that the reals are not countable.

> Cantor's proof uses classical logic.

> There are constructive proofs, although they all rely on the axiom of countable choice. Can the real numbers be shown uncountable without excluded middle and without the axiom of choice?

>An answer has not been found so far, although not for lack of trying.

> We show that there is a topos in which the real numbers are countable, i.e., there is an epimorphism from the object of natural numbers to the object of Dedekind reals.

> Therefore, higher-order intuitionistic logic cannot show the reals to be uncountable.

No. Inside the model, there is exactly such a surjection. We don't care what happens outside of it.

Maybe you already knew this, but to clarify: "Countable" means that there exists a surjection, not necessarily a bijection. For instance, the set {a,b,c} is countable, but there is clearly no bijection Nat -> {a,b,c} as one set is infinite and the other's finite.

> It's not too surprising

On the contrary: It's a ground-breaking result IMO.

I don't know what you mean by "process". Any list of numerals like this will be missing (at least) a numerals is what he says.

Maybe let's take a step back.

It needs a proof by contraposition. The "normal" position is "S -> T" (so if S then T), which also fixes the contraposition "(not T) -> (not S)".

Cantor's idea is to have a list of (possibly infinite length) binary literals representing real numbers between 0 and 1 (and if those are uncountable, so are ALL the real numbers :P).

The important part is that first consider the set of all such literals, whether countable or not. Let's call those T (for "total"). But then consider the subset of those that can be enumerated. Let's call those S (for "subset").

The countability means that you have a function that literally enumerates those (i.e. a function "natural number -> literal", 1:1)

Enumerate the literal and enumerate the digit at some position in the literal.

Let a_n be the nth literal. The a_n need to be unique (in order for those to be an enumeration).

Let d(n, m) be the nth literal's digit at position n.

Now construct a new literal q that differs from the first string in the first position, from the second string in the second position and so on.

This q is NOT IN S. (it differs from any of the elements of S in at least one position each)

Thereby, we proved that if S is countable, then it's not all of T. (because we found some literal that's not on the list; the list of all needs to be bigger!)

So the "position" proof is: "Assume S is countable. Then show it's not all of T."

But that, by contraposition, means, if it's all of T then it's not countable. Which is what we wanted.

This wouldn't be correct, it's never the case that the set of rational numbers can satisfy a theory of real numbers, it's more subtle than that.

It's that for any theory of the real numbers, there exist subsets of the real numbers that are countable that satisfy that theory. For example the subset of all computable real numbers will satisfy any theory of real numbers despite it being countable. It's simply not possible to define a first order theory that describes the real numbers as a whole and only the real numbers as a whole.

However, there will never be any theory of real numbers that can be satisfied by the set of rational numbers. At a minimum any theory of real numbers would imply theorems that require the existence of a number that when squared was equal to 2. The rational numbers can not satisfy such a theorem.

It looks like my point's been misunderstood. I'm pointing out that the whole reason that Cantor's proof works (and it does work) is because we're forced to provide our complete list up-front. Or, for those who don't like the idea of 'writing down' something infinite, we must provide a 'description' or 'program' which uniquely defines/generates our list.

You say as much here:

> you can't run his algorithm until you've committed to yours.

Exactly. In Cantor's 'game', his counter-example (a real number not in our list) is generated with full knowledge of our list. Our list is generated with no knowledge of his counter-example.

That's Cantor's proof, and it is not what I'm talking about.

I'm talking about a different 'game', where the dependency is reversed: the "counter-example" is generated with no knowledge of the list; the list is generated with full knowledge of the "counter-example", and hence is able to refute it (by including the "counter-example" in the list).

This 'inverted' setup has two important differences from Cantor's setup:

1) We must replace the program/description of 'a list of reals' with a program/description of 'a function from a real to a list of reals'.

2) We must replace the program/description of 'a function from a list of reals to a real' with a program/description of 'a real number'

In particular, point (2) means that diagonalization is irrelevant in this setup (which I repeat is not Cantor's setup!). It is irrelevant because it doesn't have the right type: it is a function from a list of real numbers to a real number but there is no place for such a function in this alternative setup; instead, we need a plain old real number. This is what I was trying to get across by saying it must be 'written down up-front' (i.e. not after waiting for us to think of a list), or being 'self-contained' (i.e. not requiring an input/reference to our list).

I hope that makes it clear why the following refutations aren't applicable:

> > if Cantor gives us his (self-contained) program up-front,

> Which he did. Diagonalization is an algorithm (and a trivial one at that).

Given what I've said above, we see that diagonalization is not self-contained/provided-up-front/fully-written-down or any of the other phrases I've tried to use to get my point across. Yes, we can write a program for diagonalization, but such a program encodes a function, which has no place in this scenario (which is not the one in Cantor's proof!).

> one of the inputs to his algorithm is your algorithm

Again, the algorithm cannot take my/your/anyone's algorithm as an input, since it cannot take anything as an input, since it is not a function, since I am not talking about Cantor's proof by diagonalization of the uncountability of the real numbers. I am talking about a different situation, in which the "counter-example" is just a number, and hence cannot be provided with any inputs, whether they be algorithms or unicorns.

> > Both games are a win for whoever goes second.

> That's right. But Cantor has to go second.

By "both games" I mean Cantor's proof and this different situation. Cantor doesn't have to go second; that's my point! Cantor wins because he chooses to go second. If we choose to go second, then we will win, by constructing a list which includes the supposed "counter-example".

> That's why his proof is correct.

I know it is; but I've never claimed otherwise, and that is completely beside the point.

The point is that Cantor's proof isn't actually about the real numbers! Instead, it's about how some infinite structures (like "all numbers") are too rich to be completely captured by any particular finite representation (there will always be missing numbers). It suffices to use a countable infinity, like the computable numbers.

Alternatively, we can think of Cantor's proof as talking about computational resources: diagonalization is trivial to state, as you say, but it is computationally difficult to run. This is because it runs the list-generator as a subroutine (to find the digits), which can be made arbitrarily hard by generating the list in an arbitrarily complex way. Since diagonalization then adds 1 mod 10, it always ends up doing slightly more work than it takes to generate the list. Hence we can see Cantor's proof as statement that more powerful computers can always beat less powerful computers, assuming the code is all globally known, because the faster computers can simulate the slower ones to see what they'll do. That the essence of the second player always winning.

Haven't you only demonstrated a countable list of all possible things that might possibly represent a computable number, or some similar concept?

You need to decide whether you want to define counting as “there being a next element”, or “being able to produce those elements in a finite way with a predefined order”.

The issue here is that you are trying to make a finite/determinate assertion about an infinite process.

There are no reals in between 0.001 and 0.002, unless you generate them. And when you do, you can count them one by one until you finish generating them.

Just like you could never finish counting infinite real numbers, you could never finish counting infinite natural numbers.

So then what Cantors proof is saying is that if you could somehow count to infinity and get to a result, some infinities would have more elements than others. But that is a contradiction, because you can’t finish counting to infinity.

Hence, you cannot know infinity nor its cardinality. Not for the real numbers and not for the natural numbers either.

So, there is no list of all the real numbers between 0 and 1, but you are claiming there are uncountably infinite of them?

I'm saying that ^ sentence makes no sense to me, I don't know how to parse it formally. If you start talking about the set of "definable" numbers (not computable, but specifically "definable"), I believe you're gonna run into paradoxes as it's an ill-defined concept, similar (in spirit) to "all integers described under 100 words". In fact, the linked article actually talks about it in 2.3.

> For any given language, like for instance ZFC, we can say that definable numbers are a countable subset. Hence measure zero.

If I can describe a set of objects, then we're all set as far as I'm concerned (mathematically speaking). Being able to efficiently construct individual elements of this set using Turing machines or other computational devices is an orthogonal problem.

Also, I don't think having only countable number of utterances in ZFC precludes you from having well-defined uncountable sets described in that system (quite obviously, for any set S take 2^S which is very well-defined).

The claim is that all of them are on the list. The constructed number proves that claim false.

It's a proof by contradiction. If you assume there is any way to write an infinite numbered list of all reals, then Cantor shows it's possible to come up with a number not on your list. The construction uses your list as input, and given any list, can always produce a real number not on that list. Therefore there is no way to write an infinite numbered list of all reals.

It relies on the fact that real numbers have (countably) infinite digits, and therefore infinite "degrees of freedom" to be different. This may be one reason it's hard to accept. A "true" real number can contain infinite information in a single number. For instance, we can jam all of the naturals into a single real by just concatenating their decimal representations: 0.1234567891011121314151617181920212223...

This one single real number encodes the full infinite natural number line. That hopefully gives you a sense of why the "infinite digits" definitions of reals makes them qualitatively "bigger" than any number that has finite representation.