# Inductive types for large countable ordinal notations.

I'm looking to build notations for large countable ordinals in a "natural way". By "natural way" I mean that given an inductive data type X, that equality should be the usual recursive equality (the same that deriving Eq in Haskell would produce) and the order should be the usual recursive lexicographical order (the same that deriving Ord in Haskell would produce), and there is a decidable predicate that determines if a member of X is a valid ordinal notation or not.

For example, ordinals less than ε0 can be represented by hereditarily finite sorted lists and satisfies these requirements. Define X to be μα. μβ. 1 + α×β, a.k.a. hereditarily finite lists. Define isValid to check that X is sorted and all members of X are isValid. The valid members of X are all ordinals less than ε0 under the usual lexicographical order.

I conjecture that μα0.… μαn. 1 + α0×…×αn can be used to define ordinals less than φn + 1(0), where φ is the Veblen function, in a similar way.

As you can see I run out of μ quantifiers at φω(0). Can I build larger ordinal notations satisfying my requirements? I was hoping to get as far as Γ0. Can I get larger ordinals if I drop my decidability requirement on my validity predicate?

• Have you seen Cantor in the Coq contribs? coq.inria.fr/pylons/pylons/contribs/view/Cantor/v8.3 It seems intuitive to me that Veblen normal form is "natural" in the way you specify. Is that not the case? – jbapple May 8 '11 at 18:01
• What does the theory say, how far can you go with having decidable equality? At some point you have to give up decidability and be satisfies with semidecidability. – Andrej Bauer May 8 '11 at 18:15
• The type that encodes the Veblen form has decidable ordering, but I'm not sure if validity is decidable. ordering is compare in coq.inria.fr/pylons/contribs/files/Cantor/v8.3/… In that same file, there is a Lemma nf_intro which might characterize validity. – jbapple May 8 '11 at 18:42
• @jbapple: this pretty much looks like the answer, perhaps you should post it as an answer. – Andrej Bauer May 8 '11 at 20:52
• @jbapple Inductive lt : T2 -> T2 -> Prop doesn't look like lexicographical ordering to me. – Russell O'Connor May 8 '11 at 23:02

Hermann Ruge Jervel has a nice system that goes all the way to the Bachmann-Howard ordinal based on labelled trees. See: http://folk.uio.no/herman/logsem.pdf

I also like his book on proof theory, which discusses this system: http://folk.uio.no/herman/bevisteori.ps

• I don't think this is "natural" in the way specified in the question - see slides 7 and 8. – jbapple Jun 6 '11 at 6:47
• The link doesn't work anymore – Łukasz Lew Jun 15 '18 at 1:02