The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Adam Chlipala wrote:

> Benjamin Werner wrote:
>
> > It is not so much the question of "which types" but rather what you  
> > can do with them. Without inductive types, i.e. in raw CC, you :
>
>
> I think I've below defined True, False, eq, and nat without using 
> inductive definitions or axioms.  I'm able to prove 0 \neq 1, and the 
> induction scheme follows trivially from my definition of nat. 

Oops.  I see that only the non-dependently-typed recursion principle 
follows trivially, which I think is enough for "programming" but not 
"proving" with nats.  It still looks to me like I have a faithful 
encoding of nat in some sense, and I'm able to prove 0 \neq 1 about it.