[FOM] Hierarchies of truth theories/reply to Davis

[Nik Weaver]

The goal is to use hierarchies of truth predicates to substantially
strengthen a given base system.  This is the last message in a series
of three on this topic.

In message #010501 I described a way to enrich a formal system S
with a Tarskian (not self-applicative) truth predicate T, resulting
in a stronger system Tarski(S).  Then in message #010509 I described
a way of enriching S with a totally ordered family of truth predicates
T_a, such that T_b falls under the scope of T_a if b < a.  We do not
initially accept these truth predicates as legitimate, but we regard
their legitimacy as progressive, meaning that if T_b is accepted for
all b < a then T_a is also accepted.  This is formalized using an
additional predicate Acc, together with deduction rules that implement
axioms for T_a once Acc(a) has been established.  I called this system
Tarski_<(S), where < is the order relation being used.

If we accept S then we should accept Tarski(S).  Recognizing this, if
we accept S we should accept Tarksi_<(S).  Thus, starting with a base
system S that has the strength of Peano arithmetic, we produce a sequence
of theories S, Tarski_<(S), Tarksi_<(Tarski_<(S)), ..., a process that
can be extended into the transfinite.  Proof-theoretic strength passes
Gamma_0 as the iteration index passes omega.

The basic step of the preceding construction involves a family of truth
predicates whose use is governed by a single acceptability predicate.
This step is then iterated "by hand".  We can now take a step back and
systematize this iteration in the same way that the Tarski_<(S)
construction systematizes the iteration of the Tarski(S) construction.
This means we have a totally ordered family of truth predicates and a
totally ordered family of acceptability predicates and we additionally
have a global acceptability predicate which governs the use of all other
predicates.  I refer the reader to Sections 2.9 and 2.10 of "Predicativity
beyond Gamma_0" for details.

Using this type of construction I was able to get to systems with
proof-theoretic ordinal larger than the small Veblen ordinal
phi_{Omega^omega}(0).  It should be possible to design related
systems which get substantially further.  I even suspect this would
be rather easy for an expert in proof theory to do.

There is a question whether theories of this type are predicatively
legitimate.  I would not assert this with complete confidence because
it is not always easy to recognize vicious circles embedded in formal
systems; indeed, one of my claims is that every previously proposed
system for predicative reasoning that got up to Gamma_0 did in fact
have some impredicative aspect.  All I can say is that I have tried
to think through rather carefully just what the informal concept of
predicativism entails as acceptable (see pages 17-23 of the Gamma_0
paper) and it seemed to me that the systems discussed above are
indeed fully predicatively legitimate.

----------

The moderator has denied my request to respond to his recent criticism
of me ("Weaver's `reply' to Friedman"); however, he permits me to add
a postscript to this message suggesting that those interested see my
web site (in particular: the last paragraph on page 2 of "Predicativity
beyond Gamma_0") or contact me directly.  The URL is
http://www.math.wustl.edu/~nweaver/conceptualism.html

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