[FOM] powerset {0} = {0,{0}} in intuitionistic set theory?
Thomas Forster
T.Forster at dpmms.cam.ac.uk
Mon Oct 19 22:48:14 EDT 2009
This is known to be equivalent to excluded middle. However the proof
relies on the fact that in ZF separation holds for *all* formulae. If you
work in a fragment of ZF which has separation on for formulae in some
class Gamma, then it implies excluded middle on;y for formulae in Gamma.
And there is nothing special about the (singleton on the) empty set here,
either. Any singleton will do.
On Mon, 19 Oct 2009, Florian Rabe wrote:
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
--
URL: www.dpmms.cam.ac.uk/~tf;
DPMMS ph: +44-1223-337981;
UEA ph: +44-1603-592719
mobile in UK +44-7887-701-562;
(Currently in the UK but
mobile in NZ +64-210580093.
Canterbury office fone:
+64-3-3642987 x 8152)
More information about the FOM
mailing list