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

[Vaughan Pratt]

Florian Rabe wrote:
> [...]
> 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.

Both.

For the former, you seem to be assuming that "powerset" means "power of 
{0,1}", which is the classical meaning and not what IZF defines it to be 
in the SEP article you cite.  You would then be a classical mathematician.

For the latter, there is a wide range of intuitionistic set theories, 
among which are the classical ones based on a Boolean topos, one whose 
subobject classifier Omega = 1+1 = {0,1}.  Classical is a case of 
intuitionistic.

For an intuitionistic set theory in which the object Omega of truth 
values is not Boolean, take the topos Grph of directed multigraphs 
(multiple edges from u to v allowed, as with the labeled edges of 
automata theory).  In this topos, Omega is the clique with vertex set 
{0,1} and an extra self-loop at 1, for a total of five edges.  The 
vertices play the role of classical truth values, which the two 
self-loops at 1 further refine.

An element of Omega is a map from One (to avoid confusion with the 
vertex 1) to Omega, where One is the final graph in the category of 
graphs, consisting of one vertex and one edge, a self-loop.  Instead of 
just two maps from One to Omega as in a Boolean topos there are now 
three: the map sending the vertex of One to 0, and two sending it to 1, 
distinguished according to where they send the edge of One.

One of these two (pick one for definiteness) constitutes the "generic 
subobject" of Grph, aka the improper subobject of One (which exists in 
every topos by definition).  The other constitutes the middle element of 
a three-element Heyting algebra whose bottom element is the 
first-mentioned of these three maps from One to Omega.

The corresponding three graphs, as the three subobjects of One, working 
top-down through Omega, are:

Top t: One itself.

Middle: One less its self-loop, a graph with one vertex and no edges.

Bottom _|_: The empty graph.

If you don't believe in the topos of graphs as a model of intuitionistic 
truth then for consistency you should also not believe in a Kripke 
structure with two possible worlds (Kripke's interpretation of the 
3-element Heyting algebra) as a model serving the same purpose.  (I wish 
I'd thought of that rejoinder when Steve Simpson was explaining 
patiently (somewhat) to Colin McLarty on FOM in 1998 that there was no 
possible way topos theory could have any relevance to mathematical 
truth.  Perhaps Steve was thinking along the same lines as Russell on 
pages 273-274 of Doxiadis and Papadimitriou's Logicomix where Russell is 
pictured as having met Goedel and been challenged by him on the matter 
of truth.)

For more details on how this fits in with the subobject classifier 
machinery of elementary toposes see my Wikipedia subarticle 
http://en.wikipedia.org/wiki/Topos#Explanation .

(It seems to be an unwritten rule of Wikipedia that if you write an 
article or lede or section that no one sees fit to improve on 
significantly after some months then you're entitled to refer to it as 
"yours," the Wikipedia mentality of non-ownership of articles 
notwithstanding.  I wrote this and quite a few other Wikipedia 
articles/ledes/sections during 2006-2008 as a break from writing 
publishable papers, a luxury affordable by retired professors and 
tenured graduate students.)

Vaughan Pratt