[FOM] Hierarchies of truth theories, part 2

[Nik Weaver]

In this message I will say what I mean by a hierarchy of
Tarskian truth predicates and explain how they can be used
to get past Gamma_0.

In part 1 I described what I called the Tarskian truth
theory Tarski(S) of a formal theory S.  The language of S is
assumed to be an extension of the language of second order
arithmetic and S is assumed to include Peano arithmetic.
Tarski(S) has one additional unary relation symbol S and
the same non-logical axioms as S (with the induction schema
extended to the language of Tarski(S)), together with three
additional axioms and one axiom schema:
(1) T(.A.), for every axiom A of S
(2) T(.A.) and T(.B.) => T(.C.), whenever "from A and B derive C"
is a deduction rule of S
(3) (forall k)T(.A(k).) => T(.(forall v)A(v).)
(4) A(v_1, ..., v_j) <=> T(.A(v_1, ..., v_j).)
(a schema with one instance for each formula A in the language
of S with no free set variables and all free number variables
among v_1, ..., v_j).  For a more precise description see
Section 2.6 of "Predicativity beyond Gamma_0".

We can informally assert a general principle

(t) if S is accepted, then Tarski(S) is accepted.

This principle cannot be fully formalized (at least, not
predicatively) in the context of some theory about theories
because of the obvious circularity.  On the other hand, it
should be formalizable as an assertion about a restricted
family of theories which does not include the system in
which the formalization takes place; the following is an
example of this.

Let S be as above and let < be a recursive total order on
omega.  We define the iterated Tarskian truth theory of S
along <, denoted Tarski_<(S), in the following way.  Its
language is the language of S together with one new unary
relation Acc and one new unary relation T_a for each a in
omega.  T_a is supposed to be thought of as a truth predicate
referring to S enriched by all truth predicates T_b for b < a.
Acc is interpreted as asserting that the predicate T_a is
accepted.

The non-logical axioms of Tarski_<(S) are those of S, with
the induction schema extended to the language of Tarski_<(S),
together with one additional axiom

(forall b < a)Acc(b)  =>  Acc(a)

stating progressivity of Acc.  There are also additional
deduction rules, as follows.  Say that a formula is "readable
by T_a" if it is a formula of the language of S enriched by
the symbols T_b for b < a.  Then for each a in omega we have
four deduction rules allowing the inference from Acc(a) of
the formulas

(1') T_a(.A.), for every axiom A of S together with all
logical axioms and the induction schema extended to all
formulas readable by T_a;

(2') T_a(.A.) and T_a(.B.) => T_a(.C.), whenever "from A
and B deduce C" is a deduction rule of S, extended to all
formulas readable by T_a;

(3') (forall k)T(.A(k).) => T(.(forall v)A(v).), for
every formula A readable by T_a;

(4') T_a(.A(v_1, ..., v_j) <=> T_b(.A(v_1, ..., v_j).).),
whenever b < a, A is readable by T_b, and A has no free set
variables and all free number variables among v_1, ..., v_j.

We also have an additional family of deduction rules which
infer from Acc(a) the statements

(5') A(v_1, ..., v_j) <=> T_a(.A(v_1, ..., v_j).)

for all formulas A readable by T_a with no free set variables
and all free number variables among v_1, ..., v_j.  This completes
the definition of Tarski_<(S).  For more details, see Section 2.7
of "Predicativity beyond Gamma_0".

The system Tarski_<(S) should be recognizable as a straightforward
expression of the principle (t) mentioned earlier.  We recognize
that for any a, if T_b is accepted for all b < a then T_a should
be accepted.  Thus, we can assert progressivity of the predicate
Acc and this leads to a higher order principle

(t') if S is accepted then Tarski_<(S) is accepted

(for any recursive total order < on omega).  As with (t), this
can only be informally asserted as a general principle, but it
can be formalized in restricted settings.  I'll have more to
say about that in part 3 of this message.  For now, let S be
as before and recursively define

Tarski^0_<(S) = S

Tarksi^1_<(S) = Tarksi_<(S)

Tarski^2_<(S) = Tarksi_<(Tarksi_<(S))

etc.  Since Tarksi^{n+1}_<(S) extends Tarksi^n_<(S), we can
finally define Tarksi^omega_<(S) to be the union of the
theories Tarksi^n_<(S) for n in omega.

If < is a standard recursive ordering of omega of order type
Gamma_0 then Tarski^omega_<(S) proves the well-ordering of
notations for every ordinal less than Gamma_0.  Going one
step further, Tarksi( Tarski^omega_<(S) ) proves that a
notation for Gamma_0 is well-ordered.  Since the claim is
that predicative acceptability of S implies predicative
acceptability of Tarski( Tarski^omega(S) ), this is supposed
to falsify the received view that predicative provability is
limited by Gamma_0.

The key lemma used to establish this result is the following
("Predicativity beyond Gamma_0", Lemma 2.4).  Let (gamma_n)
be the canonical sequence increasing to Gamma_0, and let a_n
be the notation for gamma_n according to <.

Lemma.  Tarksi_<(S) plus the schema of transfinite induction
up to a_n for all formulas of Tarski_<(S) proves transfinite
induction up to a_{n+1} for all formulas of S.

Applying this lemma with Tarski^n_<(S) in place of S easily
leads to the conclusion that Tarksi^omega_<(S) proves not
only well-ordering up to each a_n but transfinite induction
up to each a_n for all formulas in its language.  Thus,
Tarksi^omega_<(S) proves transfinite induction up to every
ordinal less than Gamma_0 for all formulas in its language.

That's how you can predicatively get past Gamma_0.  I must
emphasize that although the claim that all ordinals less
than Gamma_0 are predicatively provable has been made many
times before, all previous efforts of which I am aware have
crucially involved impredicative reasoning, specifically in
a passage from induction to recursion (see
http://www.cs.nyu.edu/pipermail/fom/2006-April/010472.html
for more about this).

In part 3 I'll explain how to extend the above techniques (in
a way that seems to me to remain predicatively acceptable) so
as to get up to substantially larger ordinals.

Nik