The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Arnaud,

Wait a second, this cannot be quite right. I have been looking at Werner’s “Sets in Types, Types in Sets” paper, where he proves that ZF with inaccessible cardinals is equi-consistent with Coq plus a few axioms, including propositional excluded middle (pEM) and the type-theoretic description axiom (TTDA). I have shown that pEM and TTDA imply the existence of a strong sum axiom that you describe. Specifically, I have shown (in Coq) that

pEM -> TTDA_(i+1) -> (exists _:SS_i , True)

where TTDA_i is TTDA at level i and SS_i is strong sums at level i. (I have attached the Coq file below, so you can double-check that I have gotten everything right.) In fact, I have shown the converse as well, i.e., that the consistency of strong sums is equivalent to that of TTDA at one level higher: it turns out that both of these are equivalent to excluded middle for Type at the same level as the strong sums.

Of course, this seems to contradict part of Coquand’s paper, so I looked back over it again and I think maybe I found an issue in his definition of A_0 for strong sums. Specifically, he defines

A_0 = Sigma (C : Prop) (C -> C -> Prop)

which I do not think satisfies his definition of a universal system of notations, at least not in the Coq type system, because C here has to be a Prop, not an arbitrary type. And, of course, if we switch to

A_0 = Sigma (C : Type) (C -> C -> Prop)

for some given type universe i, then his WF well-roundedness relation moves up to the next universe, and so cannot be captured inside of A_0. Does this seem right to you, or am I missing something?

Thanks,

-Eddy

Attachment: strong_sums.v
Description: Binary data

On Apr 28, 2014, at 1:03 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

Coq is believed to be consistent with the axiom [exists x, P x -> { x | P x }].

For the records, assuming I am parsing this correctly as [ (exists x, P x) -> { x | P x } ]. This is known to be inconsistent in general (you can use it to encode system U). It is a very strong property (because of impredicativity). See, Coquand's An Analysis of Girard's Paradox (LICS 1986).

/Arnaud