[FOM] Gamma_0

[Bill Taylor]

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.
____________________________________

From:    Daryl McCullough 
Date:    Wed, Aug 9 2006 1:44 am
Subject: Characterization of Gamma_0

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.

First of all, some background about what I'm going to call
"reflective closure" of a theory of arithmetic.

Via Godel's theorem, we know that if PA is consistent, then Con(PA) is not
provable by PA. On the other hand, if you believe (as almost everyone does)
that the axioms of PA are a correct formalization of the natural numbers,
then you should also believe Con(PA). A theory that has a model -
the naturals, in this case - must be consistent.

So if someone is trying to characterize as completely as possible what
is true of the naturals, then his characterization should have a certain
closure property:

    If you believe theory T is a correct characterization,
    then you should also believe T + Con(T) is a correct characterization.

Obviously, since T doesn't prove Con(T), this "reflective closure"
principle gives you a more powerful theory than the one you started with.
So what happens if we iterate this process?

Instead of working with PA, let's switch to a weak second-order theory.
In this theory, we have two sorts of objects, naturals and sets of naturals.
The sets of naturals are closed under comprehension. The big advantage
to allowing sets as first-class objects is that you can express the claim

      r is a well-founded primitive recursive binary relation

That can't be expressed in PA (although you can come close, by saying
that it's approximately equivalent to the induction schema for r).

Okay. So let T_0 be this second-order version of PA. Now, if r is
any primitive-recursive relation, we can define an indexed collection
of theories T(r,n), (where r is a primitive recursive relation,
and n is a natural), as follows:

      T(r,n) = that theory whose axioms are defined by:
               1. ach axioms of T_0 is an axiom of T(r,n)
               2. for each m such r(m,n):
                  2.1 each axiom of T(r,m) is an axiom of T(r,n)
                  2.2 Con(T(r,m)) is an axiom of T(r,n)

Finally, let T(r) = the union of all theories of the form T(r,n).

If r is well-founded and T_0 is true (of the naturals) then T(r) will
also be true of the naturals. If T_0 is an r.e. theory, then so is T(r).

Now, let me define the "reflective closure" of a theory T_0
as the theory whose axioms include T_0 plus the axiom

    forallprimitive recursive relations r,
    r is well-founded -> Con(T(r))

If T is the "reflective closure"  of T_0,
then for every primitive recursive binary relation r

       If T proves r is well-founded, then T(r) is a subset of T.

Let's define the ordinal associated with a well-founded relation r:

    Let ord(r,n) = { ord(r,m) | r(m,n) }
    Let ord(r) = union of all ord(r,m)

If r is well-founded, then ord(r) will be a countable von-Neumann ordinal.

Let's also define the ordinal associated with a theory T
in the language of T_0:

   ord(T) = union of all ord(r) such that T proves r is well-founded

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

   Gamma_0 = ord(the reflective closure of T_0)

-- 
Daryl McCullough
Ithaca, NY