[FOM] Gamma_0

[William Tait]

On Aug 12, 2006, at 12:50 AM, Bill Taylor wrote:


> I'm transferring this article of Daryl McCullough, with his  
> permission,
> from newsgroup sci.logic to this list.  I'm sure people here will have
> some useful remarks to make about it.
>

There begins here Daryl McCullough's posting:


> I've seen definitions of the ordinal Gamma_0, but I have a hard time
> understanding the claim that "Gamma_0 is the smallest impredicative
> ordinal". Let me try to give what I *believe* to be a characterization
> of Gamma_0, to see how it relates to predicativity.
>

The is no problem 'characterizing' Gamma_0. Let {phi_{beta} | beta <
omega_1} be the Veblen hierarchy based on phi_0(x) = 2^x. That is, for
beta > o, phi_{beta} enumerates in order the simultaneous fixed points
of the phi_{\alpha} for alpha< beta. Then Gamma_0 is the least fixed
point of the function  beta |--> phi_{beta}(0).

The interesting issue is the characterization of predicativity, about
which McCullough says nothing.

He defines T_0 to be the 'second-order version of PA.'. This is a bit
imprecise and, in view of what follows, the imprecision makes a
slight difference (in the size of McCulloough's error). If T_0 is RCA  
then its proof-theoretic ordinal is epsilon_0.
If it is ACA, then its pt ordinal is epsilon_{omegax2}

McCullough:

For numbers r and n, T(r,0) = T_0 and for  for n>0, T(r, n) is the
extension of T_0 obtained by adding the consistency statement for T(r,
m) for all m <_r n, where <_r ifs the rth primitive recursive binary
relation with least element 0. T(r) is the union of the T(r,n)'s.

Now he defines the "reflective closure" of a theory T_0 to be the theory
whose axioms include T_0 plus the axiom

     forallprimitive recursive relations r,     r is well-founded ->
Con(T(r))all theories of the form T(r,n).

Finally, we're ready to give my (possibly erroneous)
characterization of Gamma_0:

    Gamma_0 = ord(the reflective closure of T_0)
-------------------------------------------------------------------

Note that, taking r instead to be an ordinal notation in the  
primitive recursive
version of the Church-Kleene constructuve number class O, T(r) is a  
familiar theory
studied by Turing (I think) and Feferman.

But, however conceived, this axiom is expressed by a true Sigma^1_1  
sentence and adding a
true Sigma^1_1 sentence does not increase the proof theoretic ordinal of
T_0. (I think that Kreisel first noted this.) So McCullough's 'possibly
erroneous' characterization of Gamma_0 as the proof theoretic ordinal of
the reflective closure of T_0 is really quite erroneous---
epsilon_{omegax2} = phi_1(omegax2) at most, as compared with the least
fixed point of beta |--> phi_{beta}(0).

In view of the fact that there has been some discussion on FOM about
predicativity and the claim that its proof theoretic ordinal is
Gamma_0,  perhaps it would be worthwhile to outline the argument for
this. I will choose Schütte's analysis in terms of an autonomous
hierarchy  {T_{alpha} | alpha is predicative}, where T_{alpha} is
ramified second-order number theory of order alpha. This is a theory in
the language of second-orderr number theory, except that the set  
variables
have ordinals attached to them to denote their order. A formula is of
order alpha if all of its free set variables are of order <= alpha and
all of its bound set variables are of order < alpha. T_{alpha} admits
only formulas of order <= alpha. The comprehension axiom asserts that  
the
extension {x | A(x)}  of each formula A(x) of order beta is a set of
order beta (possibly depending on free parameters in A(x) other than
x). Mathematical induction of order gamma is in T_{alpha}  for all gamma
<= alpha. It has the form: For all sets X of order gamma, if X contains
0 and is closed under successor,
then X=N. The other axioms are those of PA, except for one
whose formulation is a bit complicated: One needs to introduce set  
variables
with variable order subscripts, so that one can formulate the axiom
that, for limit gamma <=alpha, the statement that $A(X)$ holds for all
sets of order gamma follows from the statement that it holds for all
sets of order beta with beta < gamma.

The hierarchy of systems T_{alpha} is determined when we define what it
means for an ordinal alpha to be predicative. This is inductively
defined to mean that it is <= omega or else that there is a predicative
ordinal beta such that induction up to alpha of order 0 is a theorem of
T_{beta}. Why should this step to T_{alpha} be predicatively justified?
Because predicativity should mean that there are 'no circular
definitions'. One can analyze this to mean that the relation between a
component of a formula and the formula itself---e.g. between A(T) and
exists X A(X), where T is a set term of the same order as X---is well- 
founded. The
formulas of order <= alpha can be assigned ordinal ranks  < omega times
alpha such that the components of a formula A have smaller ordinals than
A. The relation between component and formula is primitive recursive and
so, if A is a formula of order alpha, we are predicatively justified in
introducing it if we can prove in some predicative system T_{beta} that
induction up to omega times alpha holds for sets of order 0. This will
easily follow from induction up to alpha for such sets.

All predicative ordinals are < Gamma_0: If we prove induction up to
alpha for sets of order 0 in T_{beta}, introduce the omega-rule to  
eliminate
induction by means of additional cuts and replace the above awkward  
rule for introducing forall X^{a\beta} A(X), where beta is a limit   
by the infinitary rule that forall X^{beta}A(X) follows from forall X^ 
{alpha}A(X) for all alpha < beta. The height of the resulting deduction
is < omega x 2 and the cut-formulas in it are of rank < omega times  
beta.
Therefore by standard proof theory there is a
cut-free deduction of it using the omega-rule of height
<= phi_{omegaxbeta}(wx2). It fiollows, again by standard proof theory,
that alpha <= phi_{omegaxbeta}(omegax2), which is obviously < Gamma_0  
if beta is.

I will not give details to show that every ordinal < Gamma_0 is  
predicative;
but it is straightforward.

As I see it, the only place at which this analysis of predicativity  
might
be attacked is at the point of understanding 'no circular  
definitions' to
mean that the relation of component formula of a formula to the  
formula itself
should be well-founded.
I think that this understanding is 'correct' (in whatever sense a  
precise
explication of an imprecise notion can be correct), and so I find this
analysis of predicativity convincing.

This, of course, does not imply that I think the arguments for  
restricting
mathematics to predicative mathematics are convincing.

Bill Tait