coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Kirill Taran <kirill.t256 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] impredicativity of Prop
- Date: Sat, 8 Feb 2014 14:28:27 +0400
Kristopher,
You are right about Set/Prop/Type model in Coq.
Because in Agda universes are Set 0/Set 1/Set 2/etc., it seems that we can write all programs we can write in Coq, but I am not really sure about pitfalls.
The question actually was about difference between 1-order and higher-order logic.
Is only difference in presence of quantors on all predicates? If yes, we see that in 1-order logic we can express all the same things we can in higher-order with just specification of "level".
(Like in Agda we do "forall l : level, forall P : Set l, ...".)
You are right about Set/Prop/Type model in Coq.
Because in Agda universes are Set 0/Set 1/Set 2/etc., it seems that we can write all programs we can write in Coq, but I am not really sure about pitfalls.
The question actually was about difference between 1-order and higher-order logic.
Is only difference in presence of quantors on all predicates? If yes, we see that in 1-order logic we can express all the same things we can in higher-order with just specification of "level".
(Like in Agda we do "forall l : level, forall P : Set l, ...".)
Sincerely,
Kirill Taran
Kirill Taran
On Sat, Feb 8, 2014 at 6:08 AM, Kristopher Micinski <krismicinski AT gmail.com> wrote:
disclaimer: I don't know much about Agda
Prop is impredicative in Coq, while Set is predicative. Type is
actually a special collection of universes that is indexed by naturals
(in a way to make a "nested" set of universes) to enforce
stratification constraints. The basic idea is this:
...
|
Type_n
|
Type_{n-1}
|
Type_1
/ \
Set Prop
There's an elimination restriction for Prop so that you can't do bad
things that would lead to inconsistencies. The best description of
them is probably this (in my view, which is pragmatic in nature..)
http://adam.chlipala.net/cpdt/html/Universes.html
I don't know much about Agda, but I am almost certain that it does not
model only first order logic, otherwise why would people use it?
Predicativity vs., impredicativity is simply about whether you define
an object in reference to itself. This causes sticky paradoxes that
you have to be careful to avoid.
Kris
On Fri, Feb 7, 2014 at 9:27 AM, Kirill Taran <kirill.t256 AT gmail.com> wrote:
> Hello,
>
> Why we need impredicativity of Prop?
> Also, is there difference in expressivity between Coq and Agda due
> difference in predicativity of Prop (in Agda everything is predicative)?
>
> Also, is it right assertion that "Coq models higher-order logic while Agda
> models first-order logic"? If yes, are first-order and higher-order logic
> essentialy "the same"?
> (My assumption about that is that *-order logics have a lot of sorts and
> logics modelled by type theories are in some sense "equal" due to essense of
> TT.)
>
> Sincerely,
> Kirill Taran
- [Coq-Club] impredicativity of Prop, Kirill Taran, 02/07/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/08/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/08/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/08/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/08/2014
- Re: [Coq-Club] impredicativity of Prop, Jonas Oberhauser, 02/09/2014
- Re: [Coq-Club] impredicativity of Prop, Ali Assaf, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Matthieu Sozeau, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Altenkirch Thorsten, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Altenkirch Thorsten, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Matthieu Sozeau, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Ali Assaf, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/08/2014
Archive powered by MHonArc 2.6.18.