Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Impredicativity in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Impredicativity in Coq


chronological Thread 
  • From: Wojciech Moczydlowski <wm174746 AT zodiac.mimuw.edu.pl>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Impredicativity in Coq
  • Date: Fri, 25 Jun 2004 21:12:21 +0200 (CEST)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

  Hello,

I have a question regarding impredicativity in Coq. In System F 
and hence in Calculus of Constructions one can build logical operators and 
equality 
using only universal quantification on Prop. The resulting definitions are 
impredicative. The standard library in Coq defines conjuction, 
disjunction, existence and equality using only inductive definitions, with 
no (apparent) impredicativity present. Moreover, Set is no longer 
impredicative in v8.0. 

Hence the question - can someone point me where the 
impredicativity of Prop is essentially used in the standard library or in 
applications? 
I.e. I would be happy to see a use of Prop which couldn't be done using Set 
and 
Type(i) with sum/prod/sigS instead of or/and/exists. 

Thanks,

Wojtek




Archive powered by MhonArc 2.6.16.

Top of Page