[FOM] powerset {0} = {0,{0}} in intuitionistic set theory?

[Peter LeFanu Lumsdaine]

> 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.

If your conception of set includes anything approaching the standard  
separation axiom, then I'd say that your belief in (*) does indeed  
make you a classical mathematician (or at least, classically- 
inclined).  :-)

Arguing informally, a separation axiom typically says "any nice  
logical proposition can be used as a criterion for subset  
membership".  (*) says "membership is decidable for subsets of {0}".   
Putting these together gives "every nice logical proposition is  
decidable", which either makes you pretty classical or else severely  
limits what kind of separation axiom you can accept.

A little more formally: Separation axiom schemes are typically of the  
form
"for any set A, there is a set { x \in A | \phi(x) }"
for some class of formulas \phi(x).  In the usual full separation  
axiom (eg in IZF), all formulas \phi are allowed; in CZF and related  
theories, it's restricted to e.g. bounded formulas, as described at  
the Stanford Encyclopedia entry you link to.

If \phi is any nice proposition, then consider { x \in {0} | \phi }.   
(*) implies that 0 is either in this subset or not in it, and hence  
that \phi is either true or false.  So if you accept (*), then any  
formula with which you can invoke separation must be decidable.

This sounds pretty classical.  It can be made more constructively  
acceptable by turning it on its head: only assert separation for  
formulas which are decidable!  This axiom, "decidable separation", is  
considered (though not at great length) in Moerdijk and Joyal's book  
"Algebraic Set Theory"; I don't know where else, if anywhere, it's  
discussed.  If I recall correctly, it's extremely weak unless one has  
further principles asserting decidability of some class of propositions.

Best,
-Peter.


-- 
Peter LeFanu Lumsdaine
Carnegie Mellon University