The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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.

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail