[FOM] Feferman's natural well-ordering problem.

[William Tait]

On Feb 1, 2006, at 10:33 PM, Bill Taylor wrote:
> This was mentioned by Andreas Weierman the other day, and I can  
> find no
> help on Googol for it.
>
> Can someone please explain what it is, for us?

The proof theoretic strength of a formal subsystem of second-order  
number theory is sometimes measured by the LUB of the ordinals alpha  
for which (suitably formulated) transfinite induction up to alpha or  
definition by transfinite recursion up to alpha can be derived in the  
system.

Since the system contains only numerical terms and in particular no  
terms denoting ordinals, the ordinals need to be represented by  
numbers---by a system of ordinal notations. But among these, even  
when the ordering relation is required to be primitive recursive,  we  
could get very different LUB's. In the case of first-order arithmetic  
or even up to Schuette-Feferman predicative analysis, it is obvious  
how to place 'natural' restrictions on the system of notations which  
stabilize the LUB. Its a matter of specifying that certain  
definitions of functions should be provably satisfiable in the system  
But there remains a challenge to give an a priori definition of what  
a natural system of notations should be in general.

Stan Wainer had a (at least preliminary draft of a) paper on this in  
the late 1990's---which I almost understood. His work might be a good  
place to start finding out about the subject.

You might also look at Dmytro Taranovsky's postings to FOM (going  
back to 9/17/05) and his paper to be found at <http://web.mit.edu/ 
dmytro/www/other/OrdinalNotation.htm> for more on the subject. (Due  
to a slow brain and too much on my plate, I haven't yet looked at  
this work.)

Kind regards,

Bill Tait