I was able to prove well-foundedness of an ordinal notation system that
I conjecture corresponds to the proof ordinal of Pi^1_2-CA_0. The proof
works in a weak base theory plus Pi^1_1 soundness of Pi^1_2-CA_0.
http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm
Previously, the proofs I gave were for systems that I now suspect are
weaker, and even there, the proofs used large cardinals. While Pi^1_2
comprehension may not sound much, it advances the state of the art in
reasonable notation systems, and there are also (what I expect are) much
stronger systems in the paper. Moreover, with all reals in the
constructible universe L being Delta^1_2 in a countable ordinal, it
might be a key milestone towards ordinal analysis of L and weak large
cardinal axioms. I will leave full definitions to the paper, while
discussing key themes here, including the strength of the system.
Ordinal analysis of natural strong theories is important because under
canonical assignment of gaps, the notation systems apparently capture
all ordinals with a canonical definition in the theory, and not just the
recursive ordinals, and thus give a qualitatively enhanced understanding
of the theory.
While I do not have the complete canonical assignment of gaps (between
representable ordinals) beyond the least Sigma^1_1 reflecting ordinal,
we have a reasonable picture on how the terms in the system correspond
with ordinals in Pi^1_2-CA_0, and how structures in the system mirror
structures in Pi^1_2-CA_0. If the system did not reach Pi^1_2-CA_0,
then something would be missing, and given the conceptual simplicity of
the system, it is not likely to stay hidden.
The three ingredients of the notation system are the right form,
layering/passthrough, and symmetry (with reflection configurations).
First, key to ordinal notations (and technology in general) is managing
complexity. And the general framework in the paper leads to simple
powerful systems, with simple basic structure and comparison, and
customizable conditions for standardness. The particular system uses 0
and C, with C_i(a,b) being the least ordinal above b with degree >=(i,a)
(i is a numeral below n in the nth system; (i,a)<(j,b) iff i<j or (i=j
and a<b)). The standard form of c=C_i(a,b) always uses the maximal
degree and the minimum b. Despite not being told what degree is, the
reader can already compare terms that are promised to be standard (even
without the minimal b requirement).
Second, as is typical in ordinal notation systems, we can collapse
built-from-below terms while preserving monotonicity (bigger ordinal ->
bigger collapse; this is necessary for us). C_i(a,b) is the least
collapse of an ordinal >=a above b, with passthrough for i'<i (in
defining the collapse), and with C_0(a,b) = b+omega^a for a < C_0(a,b).
However, for a collapse of alpha leading to an admissible or limit of
admissibles beta (roughly beta = C_1(alpha,b) but see below), we can use
well-behaved Delta^1_1 definitions freely (even for ordinals >beta) even
when the definitions are represented in the notation system using
ordinals >alpha. The passthrough condition (in the paper) captures this
dynamic, with each layer C_n permitting passthrough for lower layers.
It may seem that C_n should correspond with Delta^1_{n+1}^L -- and I
indeed suspect that the strength quickly rises once we get to extensions
where C_i(a,b) can be below i. However, Pi^1_2-CA_0 already has this
structure for finite n. Consider the minimal Sigma_1 elementary chain
(in terms of levels of L) kappa_1 < kappa_2 < ... < omega_1^L. There is
a recursive order-invariant linear order f on Q^<omega such that for
cofinally many alpha<kappa_1, the initial well-founded portion of f
restricted to alpha^<omega has length alpha^{+CK}. (By order
invariance, it does not matter how alpha is embedded (preserving order)
into Q.) However, for alpha>=kappa_i, such an f would need an oracle
outside of L_{kappa_i}, and in a sense existence of i levels of oracles
once we cross kappa_i makes alpha^{+CK} >= C_{i+1}(0,alpha).
Third, even (or perhaps, especially) with passthrough, a limitation of
ordinary built-from-below is that if we want to collapse alpha to get c,
with a subterm d of alpha with c<d<alpha, then what alpha is to d might
be smaller than what alpha is to c, which cuts off the permitted degree
of diagonalization above d (except for instances of d inside an ordinal
<c). We address this using a fundamental symmetry of the notation
system -- a symmetry that may qualitatively enhance our understanding of
the ordinals. For every e and f in the system, we can express e as a
reflection configuration above f, and then change f to any ordinal f'>f,
getting e' with the same relationship to f' as e is to f. The
translation is notation system dependent, and if e<f, then e'=e, but we
get the right structure of e' above f' in the system. The
built-from-below condition can then use comparison with e' rather than e.
The well-foundedness proof gives further insight into the strength, and
Pi^1_2-CA_0 is used as follows. We build the system above every
countable ordinal (using lower ordinals as constants), and then trim the
first layer C_0 to the portion that is well-founded even when translated
above every ordinal. We then repeat this with the second layer (C_1),
and so on, and using the symmetry and well-foundedness of the final
trim, we can identify the least point (if there were any) -- that we
should not have trimmed. Doing so depends on no new ill-foundedness
appearing above a certain ordinal (so that well-foundedness can be
translated to higher ordinals), which uses Pi^1_2 comprehension, with
each trim using a Pi^1_2 comprehension instance with the previous trims
as parameters.
Paradoxically at first sight, for the omega-th system, in Pi^1_2-CA_0,
there is likely a natural way to partially assign ordinals to terms such
that every term of standard length is assigned an ordinal, and in some
(nonstandard) model of Pi^1_2-CA_0 (satisfying all true Sigma^1_1
statements), every ordinal is assigned a term. Such an assignment may
confirm the intuition that (with the right gaps) every ordinal with a
canonical definition in the theory is assigned a term, and also act as a
model-theoretic proof of the strength of the system.
Finally, I should mention that Michael Rathjen has once claimed an
ordinal analysis of Pi^1_2-CA_0. However, his system was unreasonably
complex (and my guess it would correspond to a large portion of the
C_0,C_1,C_2 subsystem here) -- to the point that it stayed essentially
untouched for years until Rathjen published an account of a weaker
version (meant for KPi + parameter free Pi^1_2-CA). Later, Jan-Carl
Stegert identified a flaw in that weaker version, and completed a
portion of the system (KP + for every alpha there is alpha-stable beta,
which is much lower than Pi^1_2-CA_0). In any case, because of the
complexity, the systems there effectively failed at what should be the
primary mission: To tell the story of the ordinals of the theory.
I am looking for feedback on this posting and the paper (
http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm ).
Sincerely,
Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm