coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.)
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
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, Kirill Taran, 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
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Altenkirch Thorsten, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Matthieu Sozeau, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Ali Assaf, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/08/2014
Archive powered by MHonArc 2.6.18.