The Coq mailing list

[jevgenijs AT dva.lv]

Quoting 
"BruinBear123 AT aol.com"
 
<BruinBear123 AT aol.com>:

> How can you use Coq to show that...
> 
> (forall C: U0). C => (C => C) => C
> 
> can be seen as a representation of the type of natural numbers?
> 
Just remarks of non-expert (possible wrong).
In case you choose definition
 Nat:= forall C: Prop, C -> (C -> C) -> C
you will not be able to prove 0 <> 1 (for Leibniz equality).
For
 Nat:= forall C: Set, C -> (C -> C) -> C
or
 Nat:= forall C: Type, C -> (C -> C) -> C
it looks you can, but still you have no any induction principle for it,
so seems it couldn't be usefull anyway to carry proofs on them
(possible for computations,since connected with lambda-calculus).
There is lot of information on Church numerals on the net, so possible 
you can find some applications there.

Regards,
Jevgenijs Sallinens.
 


-------------------------------------------------
This mail sent through IMP: http://webmail.dva.lv/