[FOM] A New Ordinal Notation System

[Dmytro Taranovsky]

I discovered a conjectured ordinal notation system that I conjecture 
reaches full second order arithmetic.  I implemented the system in a 
python module/program:
http://web.mit.edu/dmytro/www/other/OrdinalArithmetic.py
along with ordinal arithmetic operations (addition, multiplication, 
exponentiation, etc.) and other functions.  The ordinal arithmetic 
functionality is useful even if you are only interested in ordinals 
below epsilon_0.

The notation system is simple enough to be defined in full here.

Definition: An ordinal a is 0-built from below from b iff a<=b
a is n+1-built from below from b iff the standard representation of a 
does not use ordinals above a except in the scope of an ordinal n-built 
from below from b.

(Note: "in the scope of" means "as a subterm of".)

The nth (n is a positive integer) ordinal notation system is defined as 
follows.

Syntax: Two constants (0, W_n) and a binary function C.
Comparison: For ordinals in the standard representation written in the 
postfix form, the comparison is done in the lexicographical order where 
'C' < '0' < 'W_n': For example, C(C(0,0),0) < C(W_n, 0) because 0 0 0 C 
C < 0 W_n C.

Standard Form:
0, W_n are standard
"C(a, b)" is standard iff
1. "a" and "b" are standard,
2. b is 0 or W_n or "C(c, d)" with a<=c, and
3. a in n-built from below from b.

I conjecture that the strength of the nth ordinal notation system is 
between Pi^1_{n-1}-CA and Pi^1_n-CA_0, and thus the sum of the order 
types of these ordinal notation systems is the proof-theoretical ordinal 
of second order arithmetic.

The full notation system is obtained by combining these notation systems 
as follows:
Constants 0 and W_i (for every positive integer i), and a binary function C.
W_i = C(W_{i+1}, 0) and the standard form always uses W_i instead of 
C(W_{i+1}, 0).
To check for standard form and compare ordinals use W_i = C(W_{i+1}, 0) 
to convert each W to W_n for a single positive integer n (it does not 
matter which n) and then use the nth ordinal notation system.

To make C a total function for a and b in the notation system (this is 
not required for standard forms), let C(a, b) be the least ordinal (in 
the notation system) of degree >=a above b, where the degree of W_i is 
W_{i+1} and the degree of C(c,d) is c if "C(c,d)" is the standard form.  
A polynomial time computation of C(a, b) (that I believe is correct) is 
included in the program.

To complete ordinal analysis of second order arithmetic, one would need:
* A canonical assignment of notations to formulas that provably in 
second order arithmetic denote an ordinal, and such that for every two 
ordinals/formulas, comparison is provable in second order arithmetic.  
The idea is that the notation system captures not only provably 
recursive ordinals of second order arithmetic but all ordinals that have 
a provable canonical definition in second order arithmetic.  For 
example, W_1 is best assigned to the least admissible ordinal above 
omega. A partial assignment is in my paper.  (It is because of such 
assignment that I believe that the system reaches full second order 
arithmetic.)
* Proof that the system is well-founded and that it has the right 
strength, etc.  (If you do not fully understand the notation system, or 
if you think that it is not well-founded, let me know.)

Historical Note:  In 2005, I discovered the right general form of C, 
defined a notation system at the level of alpha-recursively inaccessible 
ordinals (FOM postings in August 2005), and had an idea for reaching 
second order arithmetic.  In January 2006 (or possibly late 2005), I 
defined the notation system with W_2 and in 2009 (June 29, 2009 FOM 
posting) implemented it is a computer program.  This year I defined the 
key concept -- n-built from below -- that allowed me to complete the 
full notation system.

Details about the ordinal notation system and its initial segments are 
in my paper:
http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm

Sincerely,
Dmytro Taranovsky