[gylterud]

There is nothing uncomputable with the cantor diagonalisation. The Russians gladly accept it, I assure you. Here is a Haskell implementation:

diag :: (nat -> (nat -> Bool)) -> (nat -> Bool)

diag f n = not (f n n)

The following argument is also constructive. Just like in classical mathematics, crustructive mathematics proves the negation of A by assuming A and deriving a contradiction. (But you cannot prove A by assuming it’s negation and deriving a contraction):

Assume a surjectiom f :: nat -> Bool. Then there is x such that f x = diag f. Since these two functions are equal, they take equal values when we evaluate them in any point. In particular f x x = diag f x, but since diag f x = not (f x x), by definition, we have that f x x = not (f x x). This is a contradiction since not does not have fixed points.

( I made nat a type variable here since this works for any type / set )