[ 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? Already intuitionisti second order arithmetic does the job and thus so does Coq. Pure MLTT without universes wan't do it unless you have sufficient W-types. But such a pure MLTT cannot even prove not(0 = suc(x)). However, adding a constant for that is possible and we'd arrive at a system of the strength of HA whih can't recognize indutivity of epsilon_0. thomas
