The Coq mailing list

[Bob Atkey <bob.atkey AT gmail.com>]

Hello all,

I believe the model sketched by Thorsten below is essentially the same 
as the one described for ECC by Zhaohui Luo [1] (Chapter 7), which has 
an impredicative universe Prop at the bottom of an otherwise predicative 
hierarchy of universes. Inaccessible cardinals are used to interpret the 
Type_i universes (see page 146 of the PDF).

[1] 
http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-118/ECS-LFCS-90-118.pdf

Bob

On 28/01/16 13:29, Thorsten Altenkirch wrote:
> 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
>  
> <mailto:cody.roux AT gmail.com>>
> Reply-To: 
> "coq-club AT inria.fr
>  
> <mailto:coq-club AT inria.fr>"
> <coq-club AT inria.fr
>  
> <mailto:coq-club AT inria.fr>>
> Date: Wednesday, 27 January 2016 18:31
> To: 
> "coq-club AT inria.fr
>  
> <mailto:coq-club AT inria.fr>"
>  
> <coq-club AT inria.fr
> <mailto: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
> <mailto: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
>     
> <mailto: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
> >     
> > <mailto:westbrook AT kestrel.edu>>
> >     Reply-To: 
> > "coq-club AT inria.fr
> >  
> > <mailto:coq-club AT inria.fr>"
> >     
> > <coq-club AT inria.fr
> >  
> > <mailto:coq-club AT inria.fr>>
> >     Date: Wednesday, 27 January 2016 17:19
> >     To: 
> > "coq-club AT inria.fr
> >  
> > <mailto:coq-club AT inria.fr>"
> >     
> > <coq-club AT inria.fr
> >  
> > <mailto: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
> >     
> > <mailto: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
> > >     
> > > <mailto: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
> > > >     
> > > > <mailto: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.