The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

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