The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

In Coq the stratification constraints are implicit in Type and solved
under the hood in the Coq kernel.

So there's no such thing as Type_i, it only exists as a phantom inside
the internal solver, which enforces that there is a assignment of
levels that makes everything work out.

The difference between first and higher order logic is as simple as
being able to quantify over functions in Set, e.g.,

    Coq < Print nat_ind.
    nat_ind =
    fun P : nat -> Prop => nat_rect P
         : forall P : nat -> Prop,
          P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

Even a simple induction principle is higher order.  It takes a
predicate on nats (`nat -> Prop`).

I actually haven't heard the term `quantor` before, but I think it's
the level that goes on a hierarchy of universes for constraints.  Is
that correct?

I apologize if I'm wasting your time, I should probably go learn about
Agda's universes to answer this question more correctly..

Kris


On Sat, Feb 8, 2014 at 5:28 AM, Kirill Taran 
<kirill.t256 AT gmail.com>
 wrote:
> 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
>
>