[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hello, Paul Taylor has written about how to formulate ordinals in constructive set theory in his paper "Intuitionistic Sets and Ordinals" [1]. The fixed point theorem Taylor mentions in the introduction to this paper can be proved by the elegant argument of Pataraia (which Pataraia himself never published, but Martin Escardo reproduced the proof in his paper "Joins in the frame of nuclei" [2]). Best, Neel [1] http://www.monad.me.uk/~pt/ordinals/intso.pdf [2] http://www.cs.bham.ac.uk/~mhe/papers/hmj.pdf On 29/01/15 14:59, roux cody wrote:
Dear Vladimir, Coq is more than powerful enough to prove well ordering of epsilon zero, *for a constructive notion of well ordering*. This is usually defined by *accessibility*: if some property about ordinals is closed by successor and limits, then it holds for all ordinals. Sadly, this is not constructively equivalent to the fact that any subset of ordinals has a least element. The n-lab seems to sum the situation up quite nicely: http://ncatlab.org/nlab/show/well-founded+relation Without references I'm afraid. Note that the constructive formulation of well-foundedness is sufficient for most applications! What application did you have in mind? Best, Cody On Thu, Jan 29, 2015 at 7:46 AM, Vladimir Voevodsky <[email protected] <mailto:[email protected]>> wrote: 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.
