[FOM] powerset {0} = {0,{0}} in intuitionistic set theory?
Florian Rabe
f.rabe at jacobs-university.de
Mon Oct 19 14:20:10 EDT 2009
Hello,
I've recently done some formalization of set theory. I wasn't sure whether I should use classical or intuitionistic ZF. So I decided to start with intuitionistic ZF and see how far I'd get.
My axioms are essentially those of IZF at http://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html. I introduce symbols for empty set, pair, union, powerset, and {x in A | phi(x)} after proving that those sets exist uniquely.
Then, writing 0 for the empty set, I tried to prove
(*) powerset {0} = {0,{0}}
and was surprised to find that (*) seems to be equivalent to excluded middle.
Intuitively, I feel that (*) has to be true. Now I wonder whether that makes me a classical mathematician or whether there are intuitionistic set theories in which (*) holds.
I'd appreciate any answer or pointer to the literature.
Thanks,
Florian
More information about the FOM
mailing list