The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

Thorsten: You'd know best, but I don't really have an intuition about how to add inaccessibles to the omega-set model. Certainly, this could look very different from the set theoretic model I know and (somewhat) love. Maybe there's a super topos-theoretic result that makes this all easy, but it seems pretty tricky from down in the type-theoretic weeds.

Eddie: Certainly Impredicative Set with excluded middle is not kosher, because of the Berardi paradox:
https://coq.inria.fr/library/Coq.Logic.Berardi.html

In fact building *any* model of impredicative sets seems to be pretty subtle, so I'm asking about what is currently known about such non-proof irrelevant models. A good reference for omega-sets by Phoa can be found here:
http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ECS-LFCS-92-208.ps.gz

As a side note, I'm sure you're aware of this, but it might be useful to remind others of the Barras formalization of IZF in Coq:

http://www.lix.polytechnique.fr/Labo/Bruno.Barras/proofs/sets/index.html and http://www.lix.polytechnique.fr/Labo/Bruno.Barras/proofs/sets/Ens.html

it's a bit terse, unfortunately.

On Wed, Jan 27, 2016 at 12:47 PM, Eddy Westbrook <westbrook AT kestrel.edu> wrote:

Hi Thorsten,

I would be very interested to know more about this. Could you please share a brief description of, or a pointer to, your definition of omega-sets?

However, as I mentioned in my email, Benjamin Werner did already do a model using inaccessible cardinals in ZFC (see his “Sets in Types, Types in Sets” paper). I, at least, would interested in a model that is formalized in Coq, and that would seem to require it to not use inaccessible cardinals…?

-Eddy

On Jan 27, 2016, at 9:35 AM, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

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.