[FOM] Feferman's natural well-ordering problem.
wwtx at earthlink.net
Thu Feb 2 16:15:22 EST 2006
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
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
More information about the FOM