[TYPES] Gentzen proof and Kantor ordering

[Martin Escardo]

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