[FOM] Goals of Ordinal Analysis
Dmytro Taranovsky
dmytro at mit.edu
Sat Aug 12 13:00:41 EDT 2017
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
More information about the FOM
mailing list