[FOM] On Ordinal Notations Plus Re:A New Ordinal Notation

[Dmytro Taranovsky]

Regarding my ordinal notation system discussed in the previous postings
and in http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm 
Lew Gordeew's corrected Maple script showed that the description of the
comparison relation is apparently consistent and complete.

In ordinal analysis, one frequently encounters assertions that a
particular ordinal representation system is for a particular theory, but
the mathematical claims corresponding to such declarations are not as
well known and are explained in this posting.

A canonical notation system for an ordinal is the simplest one or a
near-simplest one.  The simplicity is measured in part by absence
usability obstacles (excluding lack of human-readability improving
abbreviations).  If beta is a recursive ordinal, then well-foundness of
a canonical notation system for beta (presented in a canonical recursive
form) implies that for alpha if alpha < beta, and otherwise that for the
restriction of the notation system for alpha to the initial segment of
order type beta.

For theories predicting existence of non-recursive ordinals, natural
ordinal notation systems include all ordinals having a canonical
provable representation in that theory, not just the provably recursive
ordinals.

In fact, for theories including induction beyond the set existence
principles, it may be necessary to use ordinals (slightly) larger than
all ordinals predicted by the theory.  They can be called virtual
ordinals and treated internally as special expressions made of ordinals.
For other theories, if present, virtual ordinals are simple (such as a
pair of ordinals with lexicographical comparison) and can be avoided by
rewriting the notation.

An ordinal notation consists of constants and functions and (if it is
not one-to-one) a specification of the unique standard representation. 
The ordinal notation for a strong theory can be given in all three
forms:  
* the explicit polynomial time computable form
* a self-referential definition (which does not specify gaps)
* a canonical interpretation mapping the notation to the ordinals

The recursiveness of the explicit form, and that it denotes a linear
order is provable in polynomial time arithmetic.  The self-referential
definition over a base theory implies the recursive form. The
correctness of the canonical interpretation (that it is well-defined and
implies the self-referential definition) is implied from just the set
existence principles for the ordinals used.   For a strong theory, the
canonical interpretation involves gaps and non-recursive ordinals. The
first gap consists of recursive ordinals that are not provably
recursive.  A clear example of the forms is presented in my paper.

Although the canonical interpretation includes non-recursive ordinals,
for natural theories, for every ordinal alpha in the notation, the set
of ordinals in the notation not invoking ordinals above alpha has a
provably recursive order type, but may be an arbitrarily large provably
recursive ordinal.   This is provable in a base theory given a canonical
algorithm for the notation, interpreting provably recursive as strictly
below a particular "ordinal".  It is also constructively provable in the
theory (being analyzed) for the canonical interpretation. Thus, for
every representation in the notation, the theory proves that it denotes
a unique ordinal (or a virtual ordinal).

(This paragraph applies only to natural theories of sufficient strength
to deal appropriately with Pi-1-1 statements.)  Every Pi-1-1 statement
provable in the theory is provable in a weak base theory from
well-foundness of the ordinal notation up to a particular provably
recursive ordinal.  Every arithmetical statement provable in the theory
is provable from appropriate induction for the ordinal notation up to a
particular provably recursive ordinal.  The theory proves well-foundness
of every restriction of the ordinal notation that is strictly below the
provably recursive ordinal.  The above is provable in a weak base
theory.

For unnatural Pi-1-1 sound theories, there are at least three different
notions of the proof-theoretical ordinal, of which the second one is
standard.  The first one is based on the ability to prove well-foundness
of canonical representations of ordinals.  The second one is the
superior of provably recursive well-orderings ("provably" includes
provability of well-foundness).  The third one is the least ordinal so
that all Pi-1-1 statements provable in the theory are provable from
well-foundness of a canonical ordinal notation strictly below that
ordinal (which may be less than the least ordinal for which the
well-foundness of a canonical representation implies Pi-1-1 soundness of
the theory).   Note that formal definition of the first and third
notions requires a canonical ordinal notation system for appropriate
ordinals, and is thus currently available only for theories that are not
too strong.

Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm