coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] impredicativity of Prop

From: Kirill Taran <kirill.t256 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] impredicativity of Prop
Date: Fri, 7 Feb 2014 18:27:16 +0400

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