Talk:Set Equivalence Less One Element

This can't be done without LEM either, can it? This construction of $g$ requires dividing into cases based on whether an element of $S$ is or is not equal to $f^{-1}(b)$. If however you construct $g$ by taking the intersection of $f$ with the product of the set differences and adding $(f^{-1}(b),f(a))$, then you need LEM to prove that $g$ is a mapping on $S \setminus \{ a \}$. In the finite case, I imagine proof by cases will do the trick. --Dfeuer (talk) 20:22, 12 March 2013 (UTC)

Inclined to leave this comment until someone else knowledgeable about LEM comes around and assesses it proper. Sorry. — Lord_Farin (talk) 21:55, 12 March 2013 (UTC)

That's fine. We can just ignore LEM outside of proplog. My main point, to the extent that I have one, is that LEM (or principles that imply it) is used all over the place, so if we ever in the misty future want to build one or more constructive theories, we will have to go much further than just Category:Logic. --Dfeuer (talk) 22:18, 12 March 2013 (UTC)