Comment by psychoslave
2 days ago
>You misunderstand the concept of infinity. Cantor's diagonal argument proves that such a bigger number must always exist. "Infinity'th" is not a place in a number line; Infinity is a set that may be countable or uncountable, depending on what kind of infinity you're working with.
Diagonal argument doesn’t work in a constructive ground. It’s not a matter of whether the conclusion is valid, but if we have blind faith in the premises and are fine about speaking of something we can’t build.
They are things that humans will never be able to construct, no matter how far their control over the universe surrounding them might go. To start with, humans can create the universe, — whether it’s infinite or not.
We can construct a function G, which, given a function f : N -> N -> {0,1} returns a function G(f) = h : N -> {0,1} defined by h(i):=not(f(i)(i))
This h=G(f) has the property that, for all i, there exists a j such that f(i)(j)≠h(j) . In particular, j=i will work for this.
It seems to me that this is all constructive.
The only out that I see is to not consider the class of “functions from N to {0,1}” to be something that exists (as a set, or type, or whatever).
Like, you can fairly reasonably hold the position that there is no powerset of the natural numbers, but you can’t reasonably hold the position that it exists and that there is a surjection from the natural numbers to it. (Likewise with any other set N. This isn’t specific to the natural numbers.)
We have a constructive refutation of that claim, in the sense that we have a construction of a function which, given such a surjection (as in, a function along with a promise that the provided function is such a surjection), produces a contradiction.