The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

On Sat, Oct 10, 2009 at 05:07:47PM -0400, Adam Chlipala wrote:
>Â hugo.herbelin AT inria.fr
>  wrote:
> > On the other side, with Nat defined polymorphically in impredicative
> > Set (with option -impredicative-set), you get a full recursor
> > "Nat_rec" and at least the computational expressiveness of system T
> > but you cannot derive 0<>1 (and the recursor has a bad complexity due
> > to the linear complexity of the predecessor).
> >   
> 
> Doesn't the unprovability of [0 <> 1] only arise from doing away with 
> inductive types altogether?  If we just single out [nat] to be defined 
> with impredicative polymorphism, then [0 <> 1] seems to reduce simply to 
> [false <> true], which [discriminate] proves.

Yes, I was assuming defining datatypes impredicatively in
isolation. In the given context of the Calculus of Inductive
Constructions, having "false <> true" for bool in Set indeed
propagates discrimination to the "constructors" of all the
impredicatively defined datatypes.

Hugo