The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

No, afaik, the only proof of consistency of Coq with universes is Werner's reduction to ZFC with inaccessible cardinals (i.e., "types in sets, sets in types").

I am actually working on that problem, and I am in the middle of formalizing a model of Coq inside Coq. The formalization is actually inside Coq with informative excluded middle, which, if successful, would show that informative excluded middle has a high degree of proof-theoretic strength. However, again, I am still in the middle of it. I have an unpublished paper that describes some of my ideas, if you are really interested, but in doing the formalization I have realized that some points that I missed in the paper are actually a little more tricky than I had thought.

Eddy

Sent from my iPhone

On Jan 27, 2016, at 6:49 AM, roux cody <cody.roux AT gmail.com> wrote:

The consistency proof is quite tricky though, even without universes.  Impredicative set is quite brittle, being in particular anti-classical. On a related note, does anyone know of a proof of consistency *with* universes? The only proofs that I know of are Werner's proof of normalization and Altenkirch's Lambda-set model, which afaik haven't been generalized to systems with universes.

Thanks,

Cody

On Wed, Jan 27, 2016 at 4:26 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

It's consistent. Set with --impredicative-set is like that.

On 27 January 2016 at 08:44, Jason Gross <jasongross9 AT gmail.com> wrote:

Is it possible to derive [False] from the assumption that you have [T : Prop] with [a b : T] and [a <> b]?  (On the flip side, is it possible to show that it's consistent to assume this?)

Thanks,

Jason