[FOM] Hierarchies of truth theories/reply to Davis

Nik Weaver nweaver at math.wustl.edu
Fri May 12 01:05:26 EDT 2006

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

Nik Weaver
Math Dept.
Washington University
St. Louis, MO 63130 USA
nweaver at math.wustl.edu

More information about the FOM mailing list