Comment by drdeca

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.