[FOM] powerset {0} = {0,{0}} in intuitionistic set theory?
Vaughan Pratt
pratt at cs.stanford.edu
Mon Oct 19 22:56:34 EDT 2009
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
More information about the FOM
mailing list