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 &epsilon;0 can be represented by hereditarily finite sorted lists and satisfies these requirements. Define X to be &mu;&alpha;.&nbsp;&mu;&beta;.&nbsp;1&nbsp;+&nbsp;&alpha;&times;&beta;, 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 &epsilon;0 under the usual lexicographical order. 

I conjecture that &mu;&alpha;0.&hellip;&nbsp;&mu;&alpha;n.&nbsp;1&nbsp;+&nbsp;&alpha;0&times;&hellip;&times;&alpha;n can be used to define ordinals less than &phi;n&nbsp;+&nbsp;1(0), where &phi; is the Veblen function, in a similar way.

As you can see I run out of &mu; quantifiers at &phi;&omega;(0). Can I build larger ordinal notations satisfying my requirements?  I was hoping to get as far as &Gamma;0.  Can I get larger ordinals if I drop my decidability requirement on my validity predicate?
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