[FOM] Ordinal Analysis Update

[Dmytro Taranovsky]

Previously, I described a conjectured ordinal notation system that I 
conjectured to correspond to second order arithmetic.  See my FOM posting
https://www.cs.nyu.edu/pipermail/fom/2012-March/016349.html
and my paper (which I updated with the new results)
http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm

Further analysis revealed additional structure in that system that is 
apparently not captured by second order arithmetic, and the full system 
may well exceed ZFC.  However, a key issue has been my inability to 
prove well-foundness, which is not surprising given the expected 
strength involved.  Now, I isolated a variation on a small fragment of 
the main system and proved its well-foundness. Here is the new system 
(its strength is conjectured to be higher than second order arithmetic):

Intuitive set up:  C_i(a,b) will be the least ordinal of reflection 
level i and for that level of degree a above b. The sense of reflection 
level i is that definitions for reflection levels <i have been completed.
C_0(a,b) will be b + omega^a if a is less than the least fix-point of 
x->omega^x above b, and otherwise C_0(a,b) acts as a collapsing function 
to get higher recursive ordinals.
Under the canonical assignment of gaps, reflection level 1 is expected 
to refer to admissible ordinals and their limits. Reflection level i 
(i>1) is expected to refer to ordinals c such that L_c is a Sigma_i 
elementary substructure of L_{omega_1^L}, allowing transfinite i.  
However, I do not have a complete canonical assignment of gaps and my 
proofs of well-foundess use larger gaps.

Syntax: Constant 0 (the least ordinal), and function C with 3 arguments.
Standard form:
C_i(a,b) is standard iff
  - a and b are standard
  - b is 0 or b is C_j(c,d) with (i,a)<=(j,c) (lexicographically). (This 
is needed for uniqueness of representations, but not needed for comparison.)
  - a is built from below from <C_i(a,b) with passthrough for (C_j:j<i), 
that is 'a' does not use ordinals above 'a' except
     -- as a subterm of an ordinal <C_i(a,b) (using standard comparison 
to check) or
     -- as a subterm of C_j(e,f) where j<i that is not in the scope of a 
subterm of C_j(e,f) that is <=f.  In other words, C_j(e,f) is treated as 
as representing the ordinal C_j(e,f) in terms of ordinals <=f, and which 
intermediate ordinals >f are used is irrelevant.
Comparison: Standard where (i,a) is treated as an ordinal ((i,a)<(j,b) 
<==> i<j or (i=j and a<b)).  That is (assuming standard form)
C_i(a,b) <= d ==> C_i(a,b) < C_j(c,d)
b >= C_i(c,d) ==> C_i(a,b) > C_j(c,d)
otherwise C_i(a,b) < C_j(c,d) iff (i,a) < (j,c).

Example:  Let M=C_2(0,0), and for readability allow ordinal addition.
C_1(M+C_1(M*2,0),0) is invalid because M+C_1(M*2,0) uses a higher 
ordinal (M*2).
C_1(C_0(C_3(0,0),M),0) is valid because of the passthrough for C_0.  As 
far as C_1 is concerned, we are not using C_3(0,0) as an ordinal but 
merely as a notational shorthand to define C_0(C_3(0,0),M) in terms of M.
On the other hand, in the first example, M+C_1(M*2,0) = 
C_0(C_1(M*2,0),M) and C_1 "knows" what is C_0(C_1(M*2,0),M) in terms of 
C_1(M*2,0) and M but cannot handle C_1(M*2,0) because M*2 is larger than 
M+C_1(M*2,0).

Theorem:  The C_0,C_1,C_2 system is well-founded.
Note:  The system is conjectured to correspond to Pi^1_2-TR_0.

Theorem:  Assume that there is an inner model with a measurable 
cardinal.  The C_i system is well-founded.
Note:  The system is conjectured to correspond to (canonical countable 
ordinals in) rudimentary set theory plus "for every countable alpha, 
L_{omega_1+alpha} exists".  The proof theoretic ordinal of second order 
arithmetic Z_2 is expected to equal C_0(C_omega(0,0),0).

To simplify exposition and proofs, strong ordinal notation systems are 
often presented using large cardinals, with a striking analogy between 
large cardinals and their recursive counterparts.  Michael Rathjen used 
a version of indescribability for his ordinal notation systems.  In my 
proof (see my paper), I go further by using systems of indiscernibles 
that I extract using a measurable cardinal.

I invite the readers of this posting to explore this notation system and 
my proof of well-foundness, and if they have expertise in proving 
ordinal strengths of theories, try to prove that the notation system has 
the strength indicated.

Good ordinal notation systems give us a qualitatively new understanding 
of infinite ordinals and the theories to which they correspond.   
Instead of vague and general "theory X implies existence of (for 
example) uncountable sets", one gets a precise chart of canonical 
infinite ordinals that capture the theory and its ordinal existence 
principles.

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