The Coq mailing list

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

Carlos,

        Thanks for your comments. Some comments of mine are interspersed
below.


On Mon, 13 Sep 2004, Carlos.SIMPSON wrote:

> Hi. Some brief remarks:
> (1) Benjamin Werner also treats the first question (when Set is
> impredicative), in his thesis;
> however he only treats a truncated version of the Type hierarchy,
> i.e. he has sorts Prop, Set and Type_1. Thus, technically speaking this
> doesn't answer the question for the case of
> an arbitrary finite number of sorts Type_i (which is what Coq
> implements).  Also there are some differences between the
> system he considers and the present version of Coq, notably the new
> eqT_rect and false_rect; and on the other hand he
> treats eta-conversion which apparently is not implemented now. And on
> the whole it is already a lot of hard work!

     I'm not clear what result Werner proved here. Does he prove the
consistency of Coq with impredicative Set in some orthodox system of
set-theory [like the system ZFC + "There are infinitely many
inaccessibles" of my prior letter?
 >
   [snip]
>
> (3) for the question about formulae in TT, to make it precise you would
> need to specify what is an allowable ``way of translating formulae into
> Coq''.
>
        My knowledge of Coq is, at the moment, quite rudimentary. But I
would have thought there is an obvious translation:

     (a) There is a development of the natural numbers in Coq.

     (b) Treat subsets of X as just functions from X to 2.

     (c) I forget whether I said logic should be classical when I posed
the question. But certainly this is the case I am interested in. In this
case, the translation of quantifers and propositional connectives seems
unproblematic.

      Are there subtleties I am missing here?


> I would appreciate getting a CC of any emails on this subject which are
> not posted directly to coq_club...Thanks!
> ---Carlos Simpson

     Will do.

     --Bob Solovay