[FOM] Hierarchies of truth theories, part 1

[Nik Weaver]

Last month I posted several messages outlining my criticism
of the Feferman-Schutte analysis of predicativism, according
to which Gamma_0 is the smallest predicatively unprovable
ordinal.  In its barest form the critique involves two basic
points: (1) the F-S analysis requires that each instance of
a deduction rule (*) be predicatively acceptable, and this
is not the case; (2) it seems that any reasonable set of
beliefs that would lead someone to accept each instance of
(*) would lead him to accept a corresponding implication
(**) which takes us beyond Gamma_0.  I won't restate this in
any more detail here; it was summarized in the message
http://www.cs.nyu.edu/pipermail/fom/2006-April/010472.html

As I indicated there, it is my impression that although a
number of messages were posted disputing my critique, no one
directly addressed (1), and the responses to (2) tended merely
to establish that there exist situations in which some deduction
rule is acceptable while the corresponding implication is not
(something I've never disputed).  I would like to add here
that my critique is made in much greater detail and with many
additional points in my Gamma_0 paper, where it spans 15 pages.

I am happy to debate this further if there are additional
points to be raised (hopefully responding more directly to
the argument I actually made).  However, I'd now like to
explain how I believe predicativists can get beyond Gamma_0.
I do not want to be merely destructive, tearing down the
accepted analysis of predicativism without offering something
to take its place.  However, an important difference is that
my analysis is open-ended, meaning that I produce several
formal systems of varying strengths which I claim are
predicatively acceptable, but I do not claim to encapsulate
predicative reasoning in any of them.  Indeed, I expect that
my techniques can be extended to prove substantially stronger
well-ordering statements.  This would mean going substantially
beyond the small Veblen ordinal phi_{Omega^omega}(0), which is
the largest ordinal I've explicitly identified as predicatively
provable.  (This is enough to prove Kruskal's theorem.)

I do not know of any basic mathematical principles that are
predicatively acceptable and take one very far up the ladder
to Gamma_0.  If this is to be done I think it has to be by
starting with a relatively weak system and applying reflection
principles, i.e., in some way explicitly incorporating the
fact that the system is accepted as an additional assertion.
By iterating this process we can obtain dramatically stronger
systems.  The vehicle I use to accomplish this is hierarchies
of Tarskian (non self-applicative) truth predicates.

First, here is how a single Tarskian truth predicate works, in
my approach.  I will just sketch this informally; for more
details, see Section 2.6 of "Predicativity beyond Gamma_0".
Let S be a formal theory, in some extension of the language of
second order arithmetic, which includes Peano arithmetic.  We
define Tarski(S) to be the theory in the language of S together
with one additional unary relation symbol T, whose non-logical
axioms are those of S (with the induction schema extended to
the language of Tarski(S)) together with three additional axioms
and one axiom schema asserting

(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).)

where (4) is 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.  In order to formalize Tarsk(S)
we need enumerations of the axioms and deduction rules of S,
etc.  See my paper for more details.

Note that it is easy to formalize Con(S) in terms of the
enumerations of axioms and deduction rules of S, and to show
that Tarski(S) proves the statement Con(S).  More strongly,
Tarski(S) proves every instance of the omega-rule schema
(forall n)[Prov(.A(n).) => A(n)].

I don't want to get into an argument about the meaning of
"truth", but let me note that I am using a truth predicate in
a way that I think is consistent with a very minimal deflationist
concept of truth (expressed well in the first part of the message
http://www.cs.nyu.edu/pipermail/fom/2006-March/010234.html
posted by Arhat Virdi).

In part 2 I'll describe iterated truth theories and explain how
they can be used to get past Gamma_0.

Nik Weaver
Math Dept.
Washington University
St. Louis, MO 63130 USA
nweaver at math.wustl.edu
http://www.math.wustl.edu/~nweaver/