The Coq mailing list

["Robert M. Solovay" <solovay AT Math.Berkeley.EDU>]

The following questions are inspired by question 32 of the Coq FAQ.

        Consider the version of Coq in which the sort Set is
impredicative. Has the consistency of this sytem been proved relative to
one of the usual set-theoretical systems? {For example, can one prove in
ZFC + "There are infinitely many inaccessible cardinals" that this system
is consistent?}

        Now take the variant of Coq where the sort Set is predicative but
we add classical logic + the axiom of choice + proof irrelevance. Can we
prove in ZFC + "There are infinitely many inaccessible cardinals" that
this system is consistent?

        2) My next question concerns this second variant of Coq. Consider
classical type theory where one has infinitely many types [indexed by the
non-negative integers] with the bottom type a model of Peano arithmetic
and type {i+1} corresponding to the power set of type i. [This is the
system considered by Godel in his paper on incompleteness.]

        Call this system TT. I presume that any sentence of TT can b
translated into an assertion in Coq.

        Suppose phi is such a statement of TT and Coq [+ axiom of
choice + excluded middle + proof irrelevance]proves PHI [the
translation of phi into the language of Coq]. Will the obvious
reformulation of phi in the language of set-theory be a theorem of ZFC +
"There are infinitely many inaccessibles"? [A paper of Benjamin Werner
"Sets from types, types from sets" hints at the result I have conjectured,
but he does not [so far as I can see] have the sort Set in the systems he
considers.]

        --Bob Solovay