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

[Peter Schuster]

The statement (*) P(1) = 2 cannot hold in any set theory based on 
intuitionistic logic, for (*) is equivalent (over a fragment of CZF, say, 
with Delta0-separation) to the law of excluded middle for Delta0-formulas. 
Or, to put it in a pithier way, the intuitionistic truth values coincide 
with the classical truth values precisely when classical logic is adopted.

To see this equivalence one can invoke the natural correspondence between 
Delta0-formulas F and subsets S of 1: given F, set S = {x in 1: x = 0 and 
F}; given S, set F = "0 in S". To do so P(1) need not be a set a priori.

Most of this should be present in Aczel and Rathjen's 
Mittag-Leffler Institute preprint 40 (2001/2002):

http://www.ml.kva.se/preprints/archive/2000-2001/2000-2001-40.pdf

Peter Schuster
Pure Mathematics
University of Leeds




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
>