The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

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, ...".)

Sincerely,
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