Hello. Some developments about ordinals in Coq have been done by Pierre

CastÃ©ran. See his web page http://www.labri.fr/perso/ :

Ordinal notations and rpo

<http://www.labri.fr/%7Ecasteran/Cantor/Kantor.tar.gz>: A contribution

for Coq (8.1) <http://coq.inria.fr>, (joint work with Evelyne Contï¿œjean

<http://www.lri.fr/%7Econtejea> and Florian Hatat). This development

(work in progress !) includes:

* Proof of termination of the rpo with status

* Some results about Hilbert's epsilon operator

* An extension of the Ensembles library : denumerable sets

* Ordinal notations based on Cantor and Veblen normal forms

* Axiomatic definition of countable ordinals (after K. Schï¿œtte)

This development is about termination proofs and ordinal numbers.

It will also serve as a corpus for studying the relationship between Coq

and the mathematical language.

This work is still unfinished, and we hope it will remain so, as the

doamin is very rich.

Table of modules :

prelude/

Some preliminary definitions and results (Pierre Castï¿œran,

Evelyne Contï¿œjean)

hilbert/

Introducing in Coq Hilbert's epsilon operator (Pierre Castï¿œran)

denumerable/

Denumerable sets (Florian Hatat)

rpo/

About the recursive path ordering (Evelyne Contï¿œjean)

epsilon0/

Ordinals in Cantor Normal Form (Pierre Castï¿œran)

gamma0/

Ordinals in Veblen Normal Form (Pierre Castï¿œran)

schutte/

Axiomatic presentation of denumerable ordinals, after K. Schï¿œtte

(Pierre Castï¿œran)

misc/

Computing the length of the Goodstein sequence starting from 4 (in base 2)

(Pierre Castï¿œran)

SCHROEDER/

Slight modification of the contribution by Hugo Herbelin (Florian Hatat)

*Post by Vladimir Voevodsky*If I recall correctly the ordinal numbers smaller than epsilon zero can be represented by finite rooted trees (non planar). It is then not difficult to describe constructively the ordinal partial ordering on them. Gentzen theorem says that if this partial ordering is well-founded then Peano arithmetic is consistent.

What can we prove about this ordering in Coq?

Can it be shown that any decidable subset in the set of trees that is inhabited has a smallest element relative to this ordering?

If not then can the system of Coq me extended *constructively* (i.e. preserving canonicity) so that in the extended system such smallest elements can be found?

Vladimir.