29
$\begingroup$

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?

Improve this question
$\endgroup$
9
  • 1
    $\begingroup$ 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? $\endgroup$
    – jbapple
    May 8, 2011 at 18:01
  • $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    May 8, 2011 at 18:15
  • $\begingroup$ 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. $\endgroup$
    – jbapple
    May 8, 2011 at 18:42
  • $\begingroup$ @jbapple: this pretty much looks like the answer, perhaps you should post it as an answer. $\endgroup$
    – Andrej Bauer
    May 8, 2011 at 20:52
  • $\begingroup$ @jbapple Inductive lt : T2 -> T2 -> Prop doesn't look like lexicographical ordering to me. $\endgroup$
    – Russell O'Connor
    May 8, 2011 at 23:02

1 Answer 1

Reset to default
4
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ I don't think this is "natural" in the way specified in the question - see slides 7 and 8. $\endgroup$
    – jbapple
    Jun 6, 2011 at 6:47
  • $\begingroup$ The link doesn't work anymore $\endgroup$
    – Łukasz Lew
    Jun 15, 2018 at 1:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.