The Coq mailing list

[Benjamin Werner <werner AT lix.polytechnique.fr>]

         Dear Bob,

I am sorry I was only able to answer so late.

> 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?}

This system has, to my knowledge, not been proven consisten in its whole. 
As Carlos mentionned, some people, including myself, have studied type 
theories corresponding to impredicative Coq but without full universe 
hierarchy. One could think that the same techniques could be applied to 
the full, impredicative, Coq TT, but without new tools, the proof would be 
very complex in its details and thus not very reliable.

The main difficulty is, in short, that impredicative Set cannot be modeled 
in a simple set-theoretic way (I admit there is irony here). The 
argument is Reynold's "polymorphism is not set-theoretic". And it is not 
easy to combine a model of polymorphism (for Set) with a model of the 
Type_i hierarchy.

>         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?

Yes. I am not 100% sure about the rule stating that Prop is a sub-type of 
Type and some variants of the guard condition for (structural) recursive 
functions have shown to be bugged, but the general answer is yes and the 
corresponding model construction is simple.

Note however that there are various axioms that can be called "axiom of 
choice" in this setting.


>         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.]

As Carlos mentionned, when Set is predicative, it is basicaly an alias for 
Type_0. We decided to not get rid of the keyword "Set" in predicative 
version of Coq essentially for compatibility reasons.

To come back to your question, there are indeed two translations of phi. 
One directly into Coq [PHI], one into ZFC. The translation into ZFC can be
stated in Coq using an encoding of set theory into Coq's theory; this 
gives another Coq statement [PHI'].

It is true that PHI and PHI' are not identical, but they would simillar 
enough so that their equivalence should be reasonably obvious.

What is more interesting is that when proving PHI in Coq, you might follow 
a path different from an arithmetical set-theoretical proof of phi or 
PHI'. Indeed, the proof of PHI may very well include intermediate 
statements whose counterparts in set theory have no obvious use.

This is typically the case when you use computations in Coq as short-cuts 
for reasonning. For instance when proving the primality of 1783 in Coq, 
you can build a function test : nat -> bool and prove that for any x, if 
(test x)=true, then x is prime; that is prove :

test_cor : forall x:nat, (test x)=true -> (prime x)

The primality of 1783 is then proved by the term:

(test_cor 1783 [the canonical proof that true=true]) : (prime 1783)

verifying this proof however requires computing (test 1783).

When translating this proof is set-theory, this computation is unwinded 
and its steps now appear as steps of reasonning in ZFC.

As a result,  the set-theoretical (or TT) proof is much larger. This can 
be a crucial practical issue in proofs that rely on computation. like the 
4-color theorem or Hales' work on Kepler's conjecture.


I hope this helps. Best wishes,


Benjamin