The Coq mailing list

[roconnor AT theorem.ca]

Hi Bruno,

On Thu, 10 Nov 2011, Bruno Barras wrote:

> Hi Russell,
>
> For ZF, you just need excluded-middle and TTCA (a.k.a. statement 
> ChoiceFacts.FunctionalChoice in stdlib). TTCA alone gives you IZF (with 
> replacement, not collection). See my "Sets in Coq, Coq in sets" paper (which 
> is inspired from Benjamin's as the title suggests) at 
> http://jfr.cib.unibo.it/article/view/1695 . Coq sources available at 
> http://www.lix.polytechnique.fr/~barras/proofs/sets/index.html

I don't think this is right.  As you can see from Werner's paper, Theorem 
18 states that "The set theory ZF can be encoded in CCI_2 + EM + TTDA_3"

Further more, in your paper on footnote 5 on page 36 you note that the 
axiom used by Werner is called "Type Theoretical Description Axiom".

P.S.

BTW, it is possible to interpret Zermelo set theory in Coq without 
assuming excluded middle.  One simply needs to use double negated 
existentials (and disjuctions) everywhere.  One also needs to restrict 
separation to predicates that are double negation stable (but this 
restriction isn't problematic because the interpretation of all classical 
propositions are double negation stable).  I've adapted Werner's 
development to do this and it all appears to work; however I haven't taken 
the final step (and neither did Werner) of actually proving this is in 
fact a model of Zermelo's set theory using first order logic.  This 
requires defining what a model for a system in the language of first order 
logic is (which I just happen to have already done to prove the 
consistency of Peano arithmetic in my work on the incompleteness theorem 
:).

I don't recall if I managed to model, via this double negation encoding, 
ZF with TTDA but without excluded middle.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''