Ordinal notation systems

Rough notes.

An ordinal notation system is, unsurprisingly enough, a way of writing down an initial segment of the ordinals. But what is an ordinal, and what does it mean to "write them down"?

A quick definition. An ordinal notation system (in the weakest, least controversial sense) is a coalgebra g : S -> B(S) for the functor B(X) = 1 + X + X^w in which all elements are accessible, ie. satisfy every progressive predicate over S. So each element of S belongs to one of three categories, and a sequency of predecessors which is either empty, a singleton or countably infinite, depending on its category. I use the notation 0, a+1, as to indicate the different forms of expression. A predicate P : S -> Set is progressive if it satisfies P' subset P where

         P'(s) = CASE g(s) OF 0   |-> {}
                              a+1 |-> P(a)
                              as  |-> all i P(as[i])
In other words, a progressive predicate is one which holds of a notation provided that it holds for all predecessors of that notation; the accessible notations are those `built up from below', from which all chains of successive predecessors eventually stop. Each element in an ordinal notation system (of course) denotes a countable ordinal, ie. an element of the initial algebra for B in the obvious way.

According to this analysis, a notation is necessarily for a countable ordinal. Only for these can be hope to write down all their predecessors; part of the notion of a notation system, and of writing down an ordinal is that if we can write something down, then we should be able to write down all its predecessors.

A different approach is taken by Anton Setzer, who has developed a highly interesting notion of `ordinal system' to analyse various systems of ordinal notations.

As originally conceived (by Cantor, in the 1880's, set out first in a work whose title begins "Grundlagen ..": -- I have not checked the history) an ordinal is an order type, ie. an isomorphism class of well-founded linear orders. Such an order is a pair (S,<) where S is a set and < is a binary relation on S which is transitive ( a < b /\ b < c => a < c ), linear (aka. total, connected, trichotomous, ...) ( a < b \/ a = b \/ b < a ), and such that any nonempty subset of S contains a least element. A morphism between two such orders is the obvious thing: a function between the underlying sets which preserves the relation < . An isomorphism class is an equivalence class of orders with respect the equivalence relation defined by the existence of a pair of inverse morphisms. When set-theory had developed sufficiently (about half a century later), von Neumman was able to propose the identification of these equivalence classes by certain `canonical' representative orders (in which the underlying set is the set of proper predecessors, and the order relation is set membership).

More than a century later, the concept of well-foundedness identified by Cantor has turned out to be among the most subtle of mathematical concepts. One subtlety relates to the fundamental incompleteness of formal systems. Not only is first order arithmetic incomplete, but we can in a meaningful way put a number on how incomplete it is - the least proper bound on the ordinals which can be recognised as wellfounded with proofs of accessibility within the system. In the case of first order arithmetic, this degree of incompleteness can be identified with a certain transfinite number, with the unexciting name $\epsilon_0$. This number was first identified by Cantor, on arithmetical grounds, about half a century before the relevance of transfinite arithmetic to the incompleteness of formal systems was contemplated. It is as if the "limits of language", or at any rate of a particular circumscribed formal system are in some sense susceptible of quantitative analysis. What is astounding isn't that there is a countable ordinal (which is obvious, given that there can be at most countably many proofs of accessibility) but that the ordinal should have a natural arithmetic description.

Ordinal analysis is the program of analysing the strength of formal fragments of mathematics, where strength can be thought of as capacity to recognise or capture wellfoundedness. A number of different connections between ordinals and systems have been studied. It is infamous that ordinal analysis stands in need of a clear notion of `natural well-ordering'; that this need has been recognised for about half a century; but that no attempt to capture this notion mathematically has succeeded. Some explanation and discussion of this situation can be found in survey papers by the proof theorist Michael Rathjen.

What is an ordinal?

Many questions present themselves first in the heroic (ontological) form "What is .. ?", and seem to demand a heroic answer. We can ask instead more practically oriented questions, whose content comes to the same thing. What are ordinals for? Why do we need them? It is one thing to characterise them by their structure, but what is so important about that structure? How do we know that a formal definition has hit the nail on the head?

The central thing here is well-foundedness. (However, something else is connected with the ordinals being canonical - they should be `perfect' sets, where perfection includes transitivity, and perhaps other things.)

There are two "sides" to the concept of well-foundedness. I call these synthetic, and analytic. On the synthetic side, we think of building something "up", or "forwards in time"; on the analytic side, we think of digging "down" into its structure, going "backwards in time".

What we have here is the same thing looked at from two different sides, or pictures which are complementary rather than competing. It is impossible to slide a cigarette-paper between the idea of producing something "completely", and the idea of the satisfactory conclusion of any investigation into its structure. They are different sides of the same coin.

[ Or rather, one corresponds to the physics of the coin, and the other to its monetary value. It is the physical shape and appearance, and metallic construction of a coin that makes it work in a coin-operated ticket-machine -- but however sophisticated the technology with which you study the metallurgy of a coin, or the physical makeup of a bank note, you will not find its monetary value. ]

The following are some ways in which one can formulate the notion of well foundedness.

What is it to write down an ordinal?


To write down an ordinal is surely to give a notation, and that is something finite, a concrete data structure, with decidable relations of syntactic equality and inclusion.

If we can write down an ordinal, then surely we can write down `any' of its predecessors - but perhaps in a subtle sense, something like `as many as you like', and in a delicate sense of `predecessor'.

A notation system such as (based on) Cantor's (normal form) is actually a calculus, in which there is a notion of bringing expressions to normal form, and an algorithm for comparing expressions in normal form.

Part of what is meant by `normal' form is that a (syntactical) difference in normal form should imply a difference in value.

The calculus here lets us compute a specified predecessor of a given expression in normal form. There are as it were 3 types here : Zero, Successor, and Limit, and for each a computation rule.

We then set up computation rules (or an `operational semantics') for non-normal expressions involving the predecessor operator a[...] .

representation in Haskell

Gamma0 in haskell

Peter Hancock
Last modified: Wed Aug 4 11:47:26 BST 1999