The Coq mailing list

[Martin Escardo <m.escardo AT cs.bham.ac.uk>]

On 29/01/15 12:46, Vladimir Voevodsky wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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?

In a weak fragment of dependent type theory, it is possible to define 
epslon0 and higher.

Here I did it in Agda, with comments explaining what is (not) needed:

http://www.cs.bham.ac.uk/~mhe/papers/ordinals/ordinals.html

Martin