The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Quoting Jean-Francois Dufourd 
<dufourd AT dpt-info.u-strasbg.fr>:
> I'm trying to (impredicatively) define the type Nat in Coq
> (without the option - impredicative-set, which works well).
>
> Definition Nat:=forall X:Type,(X->X)->X-> X.

Type is not impredicative, so how could you expect the impredicative  
definition of Nat to work?  Perhaps you are asking "why do some basic  
definitions work?" or "what is the limit?"

If you could define exponentiation then you could define a Godel  
numbering scheme and prove consistency of arithmetic, which is  
stronger than predicative type theory.

To see some thinking about this area look at Daniel Leivant's paper  
"Finitely stratified polymorphism" in Information and Computation,  
Volume 93, Issue 1 (July 1991).

Randy
--
> Definition succ(n:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => (f (n X f z)).
>
> Definition add(n m:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => m X f (n X f z).
>
> Definition mult(n m:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => m X (n X f) z.
>
> All that is OK. But, when I write an other version of mult:
>
> Definition mult1(n m:Nat):Nat:=
> n Nat (add m) zero.
>
> Coq answers "Universe inconsistency".
>
> I interprete this mistake as the violation of the typing rules, because
> Nat is probably of higher Type level as the X of its definition.
>
> Is this true ? Does a means exist for circumventing this problem ?
>
> Thank you !
>
> Jean-Franc,ois Dufourd
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club



--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.