I'll not take offense, nor will I spout off about metaphysics here, but I can't let it pass without noting that Cantor's diagonal argument is in fact constructi

I'll not take offense, nor will I spout off about metaphysics here, but I can't let it pass without noting that Cantor's diagonal argument is in fact constructively valid --- given a function from a set S to its power set 2^S, Cantor constructs an element of 2^S which can't be in the image of f. The subtlety here is that there are statements equivalent to Cantor's theorem in classical settings that are not intuitionistically valid, for instance that there's no injection from 2^S -> S.