The Coq mailing list

[casteran AT labri.fr]

Selon Benjamin Werner 
<werner AT lix.polytechnique.fr>:

>
> In general it depends of what ordinals you want to deal with. You can get
> a subset of the set-theoretical ordinals with the well-known example (but
> Pierre is certainly aware of that) :
>
> Inductive Ord : Type :=
>     O_Ord : Ord
>   | S_ord : Ord -> Ord
>   | lim_Ord : (nat->Ord) -> Ord.
>
> Which is a form of ordinal notation.
>
> When considering ordinals like in set-theory, the problem is that the
> usual definition is fundamentally classical (ordinals are sets which,
> among other things, have the property that their elements are totaly
> ordered wrt. membership).
>
> Paul Taylor has a big paper where he develops ordinals constructively. On
> the other hand, he heavily relies on impredicativity. A few years back, I
> adapted his developement into Coq (on top of the Ens type) and it works
> quite well. I did not know what to do with this and have not advertized
> this work. If you think you have a use for it, I would be happy to talk
> about it.
>

 Hello Benjamin,

 Thank you for your answer,

 My goal is to write in Coq (just for fun:-)) the proof of convergence
of the Goodstein sequence. I wanted to be sure that the inductive
definition you cite above is enough for that purpose.

Amitiés,

Pierre


>
> Amities,
>
>
> Benjamin
>




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.