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?