The Coq mailing list

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

Hi,

I haven’t read Benjamin’s paper, so maybe what I am saying is just a summary of what he has done. Let me summarize how to prove consistency of CoC with some extra stuff using omega-sets.

An omega-Set X is a pair |X|:Set and ||- : Nat -> |X| -> Prop s.t. For all x:|X| there exists a “realiser” n : Nat s.t. n ||-X  x. A morphism between omega-sets X,Y s a function X -> Y and a number k : Nat which is viewed as the index of a recursive function tracking f, that is for any m ||-X x we have that {k}m that is the application of the kth Turingmachine to m terminates with a number n and n ||-Y f(x). It is not hard to see that omega-Set is cartesian closed and with a bit more work we can see that we can interpret dependent types and Pi, Sigma etc. 

The interesting observation is that we can model an impredicative universe in omega-Set. This is based on the observation that the partial equivalence relations (that is relations on the natural numbers that are symmetric and transitive but not necessarily symmetric) are equivalent to a the sub model of modest omega-sets. Here a modest omega set is one where a realiser realises at most one element that is n ||- x and n ||- y implies x=y. Given a modest w-set we can construct a PER by saying that mRn iff there exists x:|X| and m ||- x and n ||- x. On the other hand given a PER R, we construct an omega set whose carrier is Nat/R and ||- is just being an element of the equivalence class. This operations constitute an equivalence, i.e. There are inverse unto isomorphism. Now since PER is a set we can define |PROP| = PER and the realiser relation is trivial (everything realises everything). 

Now I don’t think it is difficult to extend this model by universes, because above PROP it is basically set-theoretic. That is we can embed sets using the same technique as with PER, I.e. Use the trivial realisers. Hence inaccessible cardinals in your ambient set-theory give rise to universes in your type theory.

I used ideas from this model to do my normalisation proof in my ’93 PhD [1]. Basically I replaced natural numbers by strongly normalising lambda terms and I required that realizers are closed under candidate-like conditions.

Cheers,

Thorsten

[1] http://www.cs.nott.ac.uk/~psztxa/publ/phd93.pdf

From: roux cody <cody.roux AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Wednesday, 27 January 2016 18:31
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Deriving False from bool : Prop?

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.

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.