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

<p>I also like his book on proof theory, which discusses this system: <a href="http://folk.uio.no/herman/bevisteori.ps" rel="nofollow">http://folk.uio.no/herman/bevisteori.ps</a></p>

CC BY-SA 3.0
2011-06-06T06:47:02.870Z
I don't think this is "natural" in the way specified in the question - see slides 7 and 8.
jbapple
CC BY-SA 4.0
2018-06-15T01:02:48.383Z
The link doesn't work anymore
Łukasz Lew
CC BY-SA 3.0
2011-06-06T05:42:43.430Z
2011-06-06T05:42:43.430Z
solrize
<p>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 <code>deriving Eq</code> in Haskell would produce) and the order should be the usual recursive lexicographical order (the same that <code>deriving Ord</code> in Haskell would produce), and there is a decidable predicate that determines if a member of X is a valid ordinal notation or not.</p>

<p>For example, ordinals less than &epsilon;<sub>0</sub> 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 <code>isValid</code> to check that X is sorted and all members of X are <code>isValid</code>.  The valid members of X are all ordinals less than &epsilon;<sub>0</sub> under the usual lexicographical order. </p>

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

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

CC BY-SA 3.0
2011-05-08T18:01:26.787Z
Have you seen Cantor in the Coq contribs? http://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
CC BY-SA 3.0
2011-05-08T18:15:41.463Z
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
CC BY-SA 3.0
2011-05-08T18:42:41.987Z
The type that encodes the Veblen form has decidable ordering, but I'm not sure if validity is decidable. ordering is `compare` in http://coq.inria.fr/pylons/contribs/files/Cantor/v8.3/Cantor.gamma0.Gamma0.html In that same file, there is a Lemma `nf_intro` which might characterize validity.
jbapple
CC BY-SA 3.0
2011-05-08T20:52:31.483Z
@jbapple: this pretty much looks like the answer, perhaps you should post it as an answer.
Andrej Bauer
CC BY-SA 3.0
2011-05-08T23:02:07.860Z
@jbapple `Inductive lt : T2 -> T2 -> Prop` doesn't look like lexicographical ordering to me.
Russell O'Connor
CC BY-SA 3.0
2011-05-09T01:33:10.293Z
@Russell O'Connor: I agree with you, but I still think it is possible that Veblen notation had a natural `Ord`. I have two reasons: 1. lt is not restricted to well-formed (or `nf` in this Coq development) ordinals. Maybe `nf a -> nf b -> (lt a b <-> lexlt a b)`, for `lexlt` meaning lexicographic ordering. 2. The Wikipedia article on Veblen functions makes Veblen notation seem like Cantor normal form, which is lexicographic. Maybe this subquestion is more suited for mathoverflow.
jbapple
CC BY-SA 3.0
2011-05-09T01:34:33.273Z
@Andrej Bauer: Like Russell, I have some doubts. If it pans out, I'll summarize it in an answer.
jbapple
CC BY-SA 3.0
2011-05-09T04:48:30.267Z
Ok, why do you insist on getting Ord right automatically? You can always define an instance that suits your needs.
Andrej Bauer
CC BY-SA 3.0
2011-05-09T06:49:18.737Z
@Andrej No particular reason. It's just the type for ordinals less than &epsilon;<sub>0</sub> is so nice. I want to know how far we can go with that. Everything else feels like ad-hoc encodings.
Russell O'Connor
<lo.logic><type-theory><proof-theory>
Inductive types for large countable ordinal notations.
Russell O'Connor
# Inductive types for large countable ordinal notations.

(Asked by: username_0 on 2011-05-08)

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?

**Tags:** lo.logic, type-theory, proof-theory

> **Comments:**
> **username_1**: Have you seen Cantor in the Coq contribs? http://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?  
> **username_2**: 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.  
> **username_1**: The type that encodes the Veblen form has decidable ordering, but I'm not sure if validity is decidable. ordering is `compare` in http://coq.inria.fr/pylons/contribs/files/Cantor/v8.3/Cantor.gamma0.Gamma0.html In that same file, there is a Lemma `nf_intro` which might characterize validity.  
> **username_2**: @username_1: this pretty much looks like the answer, perhaps you should post it as an answer.  
> **username_0**: @username_1 `Inductive lt : T2 -> T2 -> Prop` doesn't look like lexicographical ordering to me.  
> **username_1**: @username_0: I agree with you, but I still think it is possible that Veblen notation had a natural `Ord`. I have two reasons: 1. lt is not restricted to well-formed (or `nf` in this Coq development) ordinals. Maybe `nf a -> nf b -> (lt a b <-> lexlt a b)`, for `lexlt` meaning lexicographic ordering. 2. The Wikipedia article on Veblen functions makes Veblen notation seem like Cantor normal form, which is lexicographic. Maybe this subquestion is more suited for mathoverflow.  
> **username_1**: @username_2: Like Russell, I have some doubts. If it pans out, I'll summarize it in an answer.  
> **username_2**: Ok, why do you insist on getting Ord right automatically? You can always define an instance that suits your needs.  
> **username_0**: @Andrej No particular reason. It's just the type for ordinals less than &epsilon;<sub>0</sub> is so nice. I want to know how far we can go with that. Everything else feels like ad-hoc encodings.  

---

## 1 answers

### Answer by username_3 on 2011-06-06. Score: 4

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>

> **Comments:**
> **username_1**: I don't think this is "natural" in the way specified in the question - see slides 7 and 8.  
> **username_4**: The link doesn't work anymore  

---

