[FOM] Goals of Ordinal Analysis

[Dmytro Taranovsky]

It may seem easy to consider ordinal analysis of strong theories as some 
esoteric branch of mathematics.  But in fact, such analysis is of 
fundamental importance.  It is as if the mist shrouding the theory 
disappears, revealing the beauty and the structure.

Here, I will explain what we can expect from an ordinal analysis of a 
strong theory, using ZFC as an example (but the commentary applies 
generally), and a hypothetical future canonical notation system that 
captures it.

Key to the analysis will be a recursive well-ordering, say <_w, that 
corresponds to the theory. Basic properties of <_w will be provable in 
EFA (or an even weaker system).  While <_w can be viewed as a 
well-ordering of N, it is more insightful to treat it as a well-ordering 
of terms, giving a natural structure to the well-ordering. The formal 
rules behind <_w are reasonably simple, and once one reviews enough 
examples, their practical operation is intuitively clear.  There is a 
special term, which we will denote W (or Omega), that satisfies the 
following equivalent (for any reasonable <_w) conditions:
* W is the <_w least term such that every term (equivalently, cofinally 
many terms) is a subterm of a term <_w W.
* W is the supremum of order types of bounded restrictions of <_w. A 
bounded restriction is {t: every subterm of t is <_w s} for some term s.
* W is the proof theoretical ordinal of the theory (ZFC in our case).

But getting the proof theoretical ordinal merely scratches the surface.  
An extension (which only slightly alters the definition of <_w) is to 
define <_w above a generic ordinal kappa, with ordinals <kappa being 
constants and the recursive rules specify comparison of terms given 
comparison of constants. The rules rely only on the ordering of the 
constants in the terms being compared, and not on the specific values.  
We assume that W (denoted W(kappa) for clarity) is a limit of terms that 
do not use constants or that otherwise make sense independent of kappa.

(Future) theorem:
* A Pi-1-1 statement is provable in ZFC iff for some term s <_w W, it is 
provable in a weak base theory + <_w is a well-ordering up to s.  This 
is provable in EFA, or for NBG, in EFA plus tetration is total.
* A Pi-1-2 statement is provable in ZFC iff for some term s <_w W(kappa) 
for the system build above a generic ordinal kappa, the statement is 
provable in RCA_0 plus for every well-ordering kappa, s (built above 
kappa) is a well-ordering.  This is also provable in EFA, or for NBG, 
EFA plus tetration is total.
* Extensions to higher complexity levels.
* Relations between ZFC proofs and ordinals.
* Similar results for provability in theories below ZFC, including 
perhaps for a hierarchy of theories of (in a sense) every natural 
strength below ZFC.

But the most remarkable results are for ordinals above W, which under 
the natural assignment (allowing gaps) is omega_1^CK.  The second 
component of ordinal analysis is to define a canonical assignment 
formula phi:N->Ord mapping terms to ordinals.

To define phi, we first pass to NBG or any other reasonable conservative 
finitely axiomatizable extension of ZFC.  Finite axiomatization will 
allow us to state key results inside NBG as opposed to relying on 
metatheorems.  While each phi(n) will be definable in ZFC, phi itself is 
slightly beyond ZFC-provable definability in (V, in), but is Delta^1_V 
in NBG (but not necessarily a class in NBG).  An extension also defines 
phi for the notation system above an arbitrary ordinal.

The recursive well-ordering <_w and the assignment phi will satisfy the 
following properties:
1. Provably in NBG, phi acts as a partial function N->Ord such that s 
<_w t <==> phi(s) < phi(t) when ordinals phi(s) and phi(t) exist.
2. Provably in NBG, there is a cut I (specifically, I = {n:  Sigma_n 
replacement holds (without proper class parameters)} such that for every 
term s whose length is in I, phi is total on the bounded restriction {t: 
every subterm of t is <_w s} and exists as a set (thus, phi is total on 
terms whose length is in I).  This also applies to the extension above 
an arbitrary ordinal.  Note that the statement goes right to the edge of 
the incompleteness theorem. While NBG cannot prove its own consistency, 
it can prove existence of a cut I (which will thus include all standard 
numbers) such that no inconsistency proof of ZFC (or for cut-free 
proofs, NBG) is in I.  Using I, a substitute statement for the 
well-foundness of the notation system for NBG is provable inside NBG.
3. Every ordinal that has a canonical definition in NBG is in the range 
of phi, and by its nature, phi only gives canonical definitions.  A 
canonical definition is direct and in a sense constructive. A caveat is 
that NBG does not prove (for example) omega_1^L < omega_1, so we cannot 
have different terms for omega^1_L and omega_1, and we have to choose 
which one is canonical.  It appears plausible that there are multiple 
natural phi, but they all agree if V=L, and therefore if an ordinal has 
provably the same definition (for example omega_1) for natural phi_1 and 
phi_2, then it gets assigned the same term by both phi_1 and phi_2.
As for "every ordinal", this can be formalized in a very strong way:
NBG is consistent with "every ordinal is in the range of phi".  The 
relative consistency (and Pi-1-1 soundness) is provable in a weak base 
theory.  We do not require closure of the domain of phi under subterms.

At first, this appears impossible.  After all, <_w is recursive while 
NBG proves existence of many cardinals.  However, NBG only proves that 
<_w is a recursive linear order.  And a theory with a definable 
well-ordering cannot preclude every element from being definable.  
Modulo canonicity, phi can be chosen as follows.  Choose a recursive 
well-ordering <_w that consistently with NBG includes Q (and hence 
Q^<omega) as a suborder, and fix one such suborder. Assign all Sigma^V_1 
definable ordinals to elements of Q (i.e. rationals) in an 
order-preserving way.  Repeat with Sigma^V_2 definable ordinals (the use 
of Q^<omega ensures that there are enough gaps), and so on, for every 
element of I.  As for canonicity, the first step is that the 
well-founded part of <_w below W will be assigned (without gaps) to 
recursive ordinals, nonwellfounded part (if any) <W discarded, and W 
will be set at omega_1^CK.  The general case (including existence of a 
canonical choice) is unclear, but existence of a noncanonical choice 
suggests that a canonical choice exists as well, and let us assume that 
we find it.

Instead of just seeing impredicative comprehension on a mysterious 
totality, one sees the ordinals laid out in a clear recursive order.  It 
is as if all ZFC constructions are now plain as simple operations on the 
ordinals and the notations.  Of course, that is only partially true (and 
many questions will remain unsolved), but ordinals form the core of ZFC 
and its set existence principles.  And large cardinal axioms can be 
handled using stronger ordinal notation systems.

Sincerely,
Dmytro Taranovsky

Personal website:
http://web.mit.edu/dmytro/www/main.htm

Ordinal Notation paper (a promising lead for actually finding such a 
system):
http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm