[FOM] Update on Ordinal Analysis

[Dmytro Taranovsky]

I revised my paper "Ordinal Notation" 
http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm and I am looking 
for feedback.

For readers unfamiliar with the paper, it presents very strong yet 
simple ordinal notation systems -- some stronger than all previously 
known natural systems -- but with an important caveat that strength 
lower bounds are not proved.  Instead, the arguments for the strength 
derive from detailed analysis of the properties of the systems, 
including a detailed (or for weaker levels, a complete formal) mapping 
between terms and canonical ordinals -- if the strengths were weaker, 
some canonical ordinals would be missing from the mapping.  Of course, 
such arguments are not proofs (though they can lead to proofs), and 
conclusions come in varying confidences; I tried to be unbiased (or at 
least accurate) in indicating the degree of confidence.

Given the strength and simplicity of the systems, proving the strengths 
or otherwise working with the systems is a good project for the 
interested reader.

Some of the changes in the paper are:
* Improved organization and exposition.
* Revised discussion of possible strength levels.  A variation on a 
fragment of the main system has conjectured strength beyond second order 
arithmetic Z_2 (and this is unchanged).  However, the main system itself 
does not have certain structure present in the variation, and 
possibilities for its strength were revised accordingly.
* Corrected and completed the canonical ordinal assignment at the level 
of Pi_n reflection and recursive levels of stability.  It is more subtle 
and beautiful than what the structure at KP + Pi_3 reflection would 
suggest.  The definitions of the notation systems in my paper (as 
orderings of standard terms) are unaffected.

As noted in the paper and in my FOM posting "Goals of Ordinal Analysis" 
https://cs.nyu.edu/pipermail/fom/2017-August/020582.html , ordinal 
analysis of an appropriate set theory T gives us a qualitatively 
enhanced understanding of T; it is like having a precise map where only 
vague partial descriptions can be had before.

Modulo a mistake and lack of proof, we now have this map, the canonical 
assignment of ordinals for KP + thereis kappa^+-stable kappa (and 
slightly beyond that, essentially up to Sigma^1_1 reflecting ordinals); 
see "Assignment of Degrees" for Degrees of Reflection in my paper.  
Complex possibilities -- such as (a relatively simple example) the least 
Pi_4 reflecting ordinal that is also Pi_3 reflecting onto Pi_5 
reflecting ordinals and Pi_2 reflecting onto Pi_6 reflecting ordinals -- 
are now points in an intuitive recursive ordering.

Moreover:
* The assignment also works unmodified in weaker theories (extending 
Pi^1_1-CA_0), with the comparison of ordinals agreeing with the 
comparison of terms.  (Comparison of terms (i.e. notations) is 
recursive, and the canonical assignment assigns terms to ordinals.) For 
an appropriate theory T, let S be the set of terms corresponding to T, 
including terms corresponding to nonrecursive ordinals. Typically, S has 
a simple description, such as all terms <alpha that do not have subterms 
<Omega that are >=beta (Omega does not depend on T, and ordinals above 
Omega act solely as reflection configurations), and can often be 
read-off from T 'syntactically'. alpha is often the height of the least 
transitive model of T, and beta can be alpha for limited induction or 
epsilon_{alpha+1} for full transfinite induction, or there can be 
complications with diagonalization.
   Now, I expect that for every term in S, T proves that the term 
denotes an ordinal; and T + "every ordinal is assigned a term in S" is 
Pi^1_1 conservative over T.  (Note the change of ordering between 
provability and quantification, and that we are not restricting to 
recursive ordinals (see 
https://mathoverflow.net/questions/314171/ordinal-analysis-and-nonrecursive-ordinals 
), and that it is in addition to Pi^1_1 conservativity of T over the 
well-foundness schema below its proof ordinal.)  T also works well with 
terms outside of S, acting as an operator: term t --> S(t) (the set of 
terms provably denoting an ordinal in T + "t denotes an ordinal"; a part 
of ordinal analyis is to describe S(t) explicitly).
* The assignment is also defined above a generic ordinal (using lower 
ordinals as constants), thus for appropriate T capturing Pi^1_2 theory 
of T as well.
* The assignment is extensible, and in a sense characterizes ordinals 
below Sigma^1_1 reflecting kappa even in strong theories. The assignment 
is parameterized by a special ordinal notation system used for ordinals 
above Omega.  While Veblen normal form suffices for the above (and for 
iterating kappa^+-stability / Pi^1_1 reflection below Gamma_{kappa^+ + 
1} times), if we plug in an appropriate ordinal notation system for 
(say) the proof ordinal of Z_2 but built above a generic 
ordinal/ordering, we get the canonical assignment of ordinals below the 
least Sigma^1_1 reflecting kappa in Z_2.  It is unclear how much we can 
expect in the future at higher ordinals (such as kappa^{++}-stable kappa).

Designing strong ordinal notation systems is about managing complexity, 
and a key part of the success of my paper is making things as simple as 
possible so that subtle ideas can morph into simple formal definitions.  
This endeavor is not without risks.  For all I know, a system such as 
Degrees of Reflection with Passthrough (one of the most promising 
systems in the paper) might be ill-founded, or it might hit a 
complication even before reaching Z_2, but if we are lucky, it may be 
one of the simplest possible ordinal notation systems for ZFC and some 
large cardinal axioms, eventually bringing the clarity and understanding 
that I alluded to above.

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