Skip to Content.
Sympa Menu

coq-club - [Coq-Club] impredicativity of Prop

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] impredicativity of Prop


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page