The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

In fact, for this definition, you need no big ordinals. Iteration up to 
the first infinite ordinal \omega (i.e. on natural numbers) is enough to 
construct the semantics of [le]. But for types having constructors 
taking functions as arguments, it is necessary to use transfinite 
ordinals. For instance, with:

Inductive ord : Type :=
  | Z : ord
  | S : ord -> ord
  | L : (nat -> ord) -> ord.

The term (L f) where f is the injection of nat into ord has size (in the 
models used in size-base termination) \omega+1.

Frédéric.


Le 09/01/2014 00:31, Vladimir Voevodsky a écrit :
> On Jan 8, 2014, at 5:19 PM, Andrej Bauer 
> <andrej.bauer AT andrej.com>
>  wrote:
>
> > It would
> > seem sensible to me to go the same route with inductive definitions,
> > namely, rely on semantic justifications rather than syntactic ones.
> This would certainly be cool. What I do not quite understand however is what ordinals 
> or well-founded relations have with such inductive definition as, for example, the 
> definition of "less or equal" on nat in the Coq standard library?
>
> (It's something like:
>
> Inductive le : forall ( n m : nat ) , Type := le_refl : forall ( n : nat ) , le 
> n n | le_succ : forall ( n m : nat ) , le n m -> le (S n ) ( S m ) .
>
> )
>
> V.