Talk:Cantor's Theorem/Proof 2

From ProofWiki
Jump to navigation Jump to search

I think it should be pretty clear how one could translate this into a formal proof without LEM. Intuition about why this works intuitionistically (which is not necessary to see that it does, but hey, maybe it will be helpful): given a mapping $f$, we construct $T$ in an entirely deterministic way. We aren't abstractly proving "there is a $T$ not in the image of $f$" or even "one of the following two sets is not in the image of $f$". We can get very very specific about a specific set that is not in the image of $f$. --Dfeuer (talk) 03:42, 4 May 2013 (UTC)