The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Why can’t we just use omega-Sets? They are certainly a model for pure CoC and it seems to me that it shouldn’t be too hard to add universes on top by just using inaccessible cardinals.

Cheers,

Thorsten

From: Eddy Westbrook <westbrook AT kestrel.edu>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Wednesday, 27 January 2016 17:19
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Deriving False from bool : Prop?

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.