# Hierarchies of Tarskian truth predicates

Nik Weaver  Department of Mathematics, Washington University in St. Louis
<EMAIL_ADDRESS>
(Date: January 8, 2022)

###### Abstract.

Hierarchies of non self-applicative truth predicates take us beyond
$\Gamma_{0}$.

##  1\. Introduction

The purpose of this note is to make some earlier work I did on hierarchies of
truth theories [2] more accessible. The immediate prompt for doing this was
the discovery of an error in the proof of an important lemma in [2], which was
pointed out to me by Asger Ipsen [1] (though the statement of the lemma is
still correct). But in hindsight I also see that the whole presentation was,
perhaps, overly technical and probably not very readable. It seemed worthwhile
to summarize the ideas at a more conceptual level, suppressing some of the
coding technicalities which one needs in order to convert the high-level ideas
I will describe here into the machine language of a formal proof. The proofs
have also been simplified a little.

I will be working with number-theoretic formal systems, and the easiest way to
implement a truth predicate for such a system is to introduce a predicate
symbol $T$ which takes a natural number as its argument, with the intended
meaning of $T(n)$ being “the formula with Gödel number $n$ is true”. Gödel
numbers are an example of the sort of coding technicality I intend to pass
over in this paper. In fact, more is needed; for instance, we need to be able
within the system to perform basic syntactic constructions on numerically
encoded strings. E.g., if $\ulcorner A\urcorner$ and $\ulcorner B\urcorner$
are the codes for two formulas $A$ and $B$, and $\ulcorner A\wedge B\urcorner$
is the code for their conjunction, then we require the ability to calculate
$\ulcorner A\wedge B\urcorner$ from $\ulcorner A\urcorner$ and $\ulcorner
B\urcorner$. More precisely, we must be able to express and reason about a
numerical function of two arguments which yields $\ulcorner A\wedge
B\urcorner$ when given the inputs $\ulcorner A\urcorner$ and $\ulcorner
B\urcorner$. Probably primitive recursive arithmetic would suffice for
everything we need to do along these lines. These are the kinds of details I
will either relegate to footnotes or omit entirely from the present account.

The truth predicates I will be discussing are never self-applicative; they
only apply to the sentences of some target language to which they do not
belong. But they are substantial; for instance, within the truth theory of the
target system $\mathcal{S}$ we will be able to prove (a formalization of) the
statement that every theorem provable in $\mathcal{S}$ is true. Since we can
also prove in this truth theory that, say, $0=1$ is not true, we will then be
able to derive that $0=1$ is not a theorem of $\mathcal{S}$. In other words,
the truth theory of $\mathcal{S}$ will always prove that $\mathcal{S}$ is
consistent, which we know that $\mathcal{S}$, if it really is consistent,
cannot do. This shows that truth theories increase deductive strength.

This raises the question of what more can be achieved by iterating the
construction. We would expect to produce a hierarchy of truth theories of
increasing deductive strength, a quality that can be measured by asking what
the provable ordinals of the system are. Here we say that $\alpha$ is a
provable ordinal of a system $\mathcal{S}$ if (1) there is a Turing machine
that outputs (in suitably encoded form) a well-ordering of $\mathbb{N}$ which
is isomorphic to $\alpha$, and (2) we can prove in $\mathcal{S}$ that the
output of this Turing machine is a well-ordering of $\mathbb{N}$. If we are
working with first-order systems that cannot directly express the concept of
well-ordering, we take being able to prove, in $\mathcal{S}$, transfinite
induction up to $\alpha$ (as encoded in $\mathbb{N}$) for all predicates in
its language as a stand-in for well-ordering. The ordinal strength of
$\mathcal{S}$ is the supremum of its provable ordinals.

The subtlety here is that, given a hierarchy of truth theories, there may be a
limit as to how much of the hierarchy we trust. Intuitively, we convince
ourselves that a theory in the hierarchy is sound by a transfinite induction
argument, meaning that before accepting its theorems we would need its index
to be, not just an ordinal, but a provable ordinal. As we work our way up the
hierarchy, we expect to accumulate ever-larger provable ordinals, leading us
to accept ever-higher theories in the hierarchy. But the way it is actually
going to work is more subtle than this.

##  2\. The theory ${\rm Tarski}(\mathcal{S})$

Throughout this paper $\mathcal{S}$ will be a first-order theory which extends
Peano arithmetic. Second-order theories could be analyzed in the same way,
with trivial modifications. Our analysis is indifferent to the use of
classical or intuitionistic logic.

The simplest way to augment $\mathcal{S}$ with a truth predicate would be to
add a predicate symbol $T$, together with, for each sentence $A$ of the
language of $\mathcal{S}$, the axiom $A\leftrightarrow T(\ulcorner
A\urcorner)$. This would implement Tarski’s “T-scheme”, so that it would
qualify as a truth predicate in Tarski’s sense, but it would accomplish almost
nothing. We would have produced a conservative extension of the original
theory, yielding no new theorems expressible in the original, unaugmented
language. Even simple assertions like “for all sentences $A$ and $B$, if $A$
and $B$ are both true then so is $A\wedge B$” could not be proven, as only
finitely many instances of the T-scheme could be used in any proof, which
clearly is not sufficient to draw this conclusion.

We need to be able to reason about truth globally. So I define ${\rm
Tarski}(\mathcal{S})$ to be the formal system system whose language $L_{T}$ is
the language $L$ of $\mathcal{S}$ augmented by a single predicate symbol $T$,
and whose nonlogical axioms are the nonlogical axioms of $\mathcal{S}$
together with

  * •

a single axiom which affirms111Literally, the statement “$(\forall n)T(f(n))$”
for some primitive recursive function $f$ which enumerates the Gödel numbers
of the axioms of $\mathcal{S}$. $T(\ulcorner A\urcorner)$ for all the axioms
$A$ of $\mathcal{S}$

  * •

a single axiom which affirms

$T(\ulcorner A\urcorner)\wedge T(\ulcorner B\urcorner)\to T(\ulcorner
C\urcorner)$

for any $A,B,C\in L$ for which there is a deduction rule that infers $C$ from
$A$ and $B$

  * •

for every formula $A=A(x)$ in $L_{T}$ with free variable $x$ (and possibly
other free variables not shown), the induction axiom

$(A(0)\wedge(\forall n)(A(n)\to A(n+1)))\to(\forall n)A(n)$

  * •

the $\omega$-rule, a single axiom which states that for every predicate $A$ in
$L$ (i.e., every formula in $L$ with exactly one free variable) we have222We
cannot write “$(\forall n)T(\ulcorner A(n)\urcorner)$” here; this expression
is senseless because $\ulcorner A(n)\urcorner$ is a number and does not
contain any variables that could be quantified. We need to talk about the
formula obtained by replacing every occurrence of the variable symbol ‘$n$’ in
$A$ with a constant term that evaluates to the actual number $n$. So something
like $(\forall n)T(g(\ulcorner A\urcorner,n))$, where $g$ is a primitive
recursive function that, given the Gödel number of a predicate, returns the
Gödel number of that predicate with every occurence of its free variable
replaced by $\hat{n}$.

$(\forall n)T(\ulcorner A(\hat{n})\urcorner)\leftrightarrow
T(\ulcorner(\forall n)A(n)\urcorner),$

where $\hat{n}$ represents a canonical constant term that evaluates to $n$

  * •

the T-scheme, which consists of one axiom of the form

$\overline{A}\leftrightarrow T(\ulcorner A\urcorner)$

for each formula $A$ in $L$, where $\overline{A}$ is the universal closure of
$A$.

The intention is to interpret $T(\ulcorner A\urcorner)$ as affirming the truth
of $A$, or of the universal closure of $A$ if it has any free variables.

##  3\. Justifying ${\rm Tarski}(\mathcal{S})$

How do we justify accepting ${\rm Tarksi}(\mathcal{S})$, given that we accept
$\mathcal{S}$?

By “accept” I mean something like: we understand that we have the right,
indeed that we are rationally compelled, to affirm every theorem of
$\mathcal{S}$. Why should we feel the same way about ${\rm
Tarksi}(\mathcal{S})$?

The question seems a little murky because ${\rm Tarski}(\mathcal{S})$ invokes
the notion of “truth”, which is surprisingly subtle, and still the subject of
philosophical debate. I have my own explanation of the nature of truth, which
I have given in detail in [3], but I will not call on it here. Instead, I will
argue that a basic grasp of infinitary reasoning would allow us to accept
${\rm Tarksi}(\mathcal{S})$ without requiring prior familiarity with any
notion of truth.

My particular interest is in “countablist” reasoning which admits countably
infinite, but not uncountable, sets and constructions — and sentences and
derivations. This alone is enough to justify passing from $\mathcal{S}$ to
${\rm Tarski}(\mathcal{S})$, assuming that the language of $\mathcal{S}$ has
only countably many formulas. Because then we could enumerate these formulas
as $A_{1}$, $A_{2}$, $\ldots$ and simply define the desired predicate $T$ by
the infinite conjunction

$(T(\ulcorner
A_{1}\urcorner)\leftrightarrow\overline{A}_{1})\wedge(T(\ulcorner
A_{2}\urcorner)\leftrightarrow\overline{A}_{2})\wedge\cdots.$

No prior ideas about “truth” are needed to do this. I suppose all the material
in this paper could be reworked in terms of countably infinite logic, without
mentioning truth at all — I leave this as a challenge to the reader.

The definition of $T$ I just gave clearly forces us to accept every instance
of the T-scheme. What about the other axioms of ${\rm Tarksi}(\mathcal{S})$?
For instance, how do we infer “$T(\ulcorner A\urcorner)$, for every axiom $A$
of $\mathcal{S}$”? This, of course, demands that we have already accepted all
the axioms of $\mathcal{S}$, and not just schematically — we should have
accepted the single statement
$\overline{B}_{1}\wedge\overline{B}_{2}\wedge\cdots$ where the $B_{n}$’s
enumerate the axioms of $\mathcal{S}$. Granting this, and given the definition
of $T$, we can infer $T(\ulcorner B_{1}\urcorner)\wedge T(\ulcorner
B_{2}\urcorner)\wedge\cdots$, and from there the single statement
“$T(\ulcorner A\urcorner)$, for every axiom $A$ of $\mathcal{S}$”.

A similar justification can be given for the second axiom, which states that
deduction under $T$ is valid. For the induction scheme, which is applied to
the language of ${\rm Tarski}(\mathcal{S})$, not just of $\mathcal{S}$, we do
not need to assume anything about $T$. All we have to do is imagine being
given the premises $A(0)$ and $(\forall n)(A(n)\to A(n+1))$, for some formula
$A$ with exactly one free variable, in the language of ${\rm
Tarski}(\mathcal{S})$. Using countablist reasoning, we can easily see how to
construct a proof from this of $A(1)$, then a proof of $A(2)$, etc., yielding
finally (with one final infinite inference) $(\forall n)A(n)$. Any formula
with more than one free variable can then be handled by the countably long
process of separately applying the preceding reasoning to this formula with
its other free variables replaced by constant terms in every possible way.

Given our definition of $T$, the $\omega$-rule is straightforwardly
justifiable along countablist lines. This completes my sketch of a
justification of ${\rm Tarski}(\mathcal{S})$, given $\mathcal{S}$.

I mentioned in the introduction that it will be a theorem of ${\rm
Tarski}(\mathcal{S})$ that every theorem of $\mathcal{S}$ is true. This is
proven by induction on the number of steps in the derivation of a theorem of
$\mathcal{S}$. The theorems provable in a single step are precisely the axioms
of $\mathcal{S}$, which we know are all true, and the truth of theorems
provable at any subsequent step then follows inductively from the fact that
$T$ respects the deduction rules of $\mathcal{S}$. The assertion that $0=1$ is
not true is an immediate consequence of the forward implication in
‘$T(\ulcorner 0=1\urcorner)\leftrightarrow 0=1$”.

##  4\. The theory ${\rm Tarski}_{\preceq}(\mathcal{S})$

Now let us iterate the ${\rm Tarski}(\mathcal{S})$ construction. Start with a
computable total ordering $\preceq$ of $\mathbb{N}$. The intention is to
iterate along a well-ordering of $\mathbb{N}$, but we do not assume that we
know $\preceq$ is well-ordered. We do need to know that it is a total
ordering, that it has a least element, that every element has an immediate
successor, and so on. There must be operations of addition, multiplication,
and exponentiation which correspond to the usual ordinal operations. One can
prove in Peano arithmetic that any of the standard notation systems for
countable ordinals has all the properties we need.

In the sequel, any notation for sum, product, or exponent will always refer to
these (presumptively) ordinal operations, not to the usual arithmetical
operations on $\mathbb{N}$. Also, from here on, the symbols “$0$”, “$1$”, etc
will always refer to the $\preceq$-minimal element of $\mathbb{N}$, its
immediate $\preceq$-successor, and so on.333I will also write things like
“$A(2)$” to mean “the formula obtained by replacing the free variable in $A$
with a constant term that evaluates to $2$ (as I have already done a few
paragraphs back). It might be more correct to write “$A(\hat{2})$”, but I see
no harm in omitting the hat. Similarly, I will write “$A(\omega)$”, not
“$A(\hat{\omega})$”. But I will keep the hats on variable symbols, as in
“$A(\hat{n})$”, when appropriate. I will write “$\omega$” both for the actual
ordinal $\omega$ and for the $\omega$th element of $\mathbb{N}$ according to
$\preceq$.

The language of ${\rm Tarski}_{\preceq}(\mathcal{S})$, which I denote
$L_{\preceq}$, will be the language of $\mathcal{S}$ augmented by a family of
predicate symbols $T_{a}$, for $a\in\mathbb{N}$, and one additional predicate
symbol ${\rm Acc}$. The idea is that the $T_{a}$’s should be the truth
predicates in the hierarchy and that ${\rm Acc}(a)$ represents our acceptance
of the hierarchy up to $a$ (with respect to the ordering $\preceq$).

For each $a\in\mathbb{N}$ we let $L_{a}$ be the language of $\mathcal{S}$
augmented by only the predicate symbols $T_{b}$ with $b\prec a$. It is the
formulas of $L_{a}$ to which we want to apply $T_{a}$.

We would like a hierarchy of formal systems $\mathcal{S}_{a}$ with
$\mathcal{S}_{a+1}={\rm Tarski}(\mathcal{S}_{a})$ and $\mathcal{S}_{a}={\rm
Tarski}(\bigcup_{b\prec a}\mathcal{S}_{b})$ at limits. This could be achieved
by a recursive construction, but it is simpler (and also a slightly different,
better result) to define them all at once, in the following way.

For each $a\in\mathbb{N}$ let $\mathcal{S}_{a}$ be the formal system whose
language is $L_{a+1}$ (so it includes the predicate $T_{a}$) and whose
nonlogical axioms are the nonlogical axioms of $\mathcal{S}$ and the induction
scheme for every formula in $L_{a+1}$, together with axioms about $T_{a}$:

  * •

the statement “$T_{a}(\ulcorner A\urcorner)$ for all the axioms $A$ of
$\mathcal{S}$”

  * •

the statement “$T_{a}(\ulcorner A\urcorner)\wedge T_{a}(\ulcorner
B\urcorner)\to T_{a}(\ulcorner C\urcorner)$ for all $A,B,C\in L_{a}$ for which
there is a deduction rule that infers $C$ from $A$ and $B$”

  * •

a single axiom which says that $T_{a}$ holds of every instance of the
induction scheme for formulas in $L_{a}$

  * •

a single statement that affirms

$(\forall n)T_{a}(\ulcorner A(\hat{n})\urcorner)\leftrightarrow
T_{a}(\ulcorner(\forall n)A(n)\urcorner)$

for every predicate $A$ in $L_{a}$

  * •

for every formula $A$ in $L_{a}$, the truth definition

$\overline{A}\leftrightarrow T_{a}(\ulcorner A\urcorner)$

and axioms about $T_{b}$ for $b\prec a$:

  * •

the single statement “for all $b\prec a$ and every $A\in L_{b}$ we have
$T_{a}(\ulcorner\overline{A}\leftrightarrow T_{b}(\ulcorner
A\urcorner)\urcorner)$”.

  * •

for each $b\prec a$, the statement “$T_{b}(\ulcorner
A\urcorner)\leftrightarrow T_{a}(\ulcorner A\urcorner)$ for all $A\in L_{b}$”

$\mathcal{S}_{a}$ is the theory whose acceptance is expressed in ${\rm
Tarski}_{\preceq}(\mathcal{S})$ by ${\rm Acc}(a)$. The appropriate axiom for
${\rm Acc}(\cdot)$ is that it should be progressive, i.e.,

$(\forall b\prec a){\rm Acc}(b)\leftrightarrow{\rm Acc}(a).$

I will write “${\rm Prog}({\rm Acc})$” for this condition. (Note that it is
stronger than the usual notion of progressivity, which affirms only the
forward implication. This choice simplifies the analysis given below a
little.) Indeed, $\mathcal{S}_{0}$ is precisely ${\rm Tarksi}(\mathcal{S})$,
and for any $a\succ 0$, although $\mathcal{S}_{a}$ is not exactly the same as
${\rm Tarksi}(\bigcup_{b\prec a}\mathcal{S}_{b})$ (because of the final
“$T_{b}(\ulcorner A\urcorner)\leftrightarrow T_{a}(\ulcorner A\urcorner)$ for
all $A\in L_{b}$” scheme), essentially the same argument can be used to
justify accepting it given that we have accepted $\bigcup_{b\prec
a}\mathcal{S}_{b}$. So there is a straightforward justification of
progressivity of ${\rm Acc}$.

It is easy to see that for every $b\prec a$ it is a theorem of
$\mathcal{S}_{a}$ that all the axioms of $\mathcal{S}_{b}$ are true. Together
with the truth of all deduction rules for formulas in $L_{a}$, this yields the
following fact.

######  Proposition 4.1.

For every $b\prec a$, it is a theorem of $\mathcal{S}_{a}$ that every theorem
of $\mathcal{S}_{b}$ is true.

Now I am ready to describe the axioms of ${\rm
Tarski}_{\preceq}(\mathcal{S})$. Its language was defined earlier; its
nonlogical axioms will consist of

  * •

the nonlogical axioms of $\mathcal{S}$

  * •

the axiom ${\rm Prog}({\rm Acc})$

  * •

the induction scheme for all formulas in the language of $\mathcal{S}$
augmented by ${\rm Acc}$

  * •

for each $a$ and each axiom $A$ of $\mathcal{S}_{a}$ the statement “${\rm
Acc}(\hat{a})\to A$”.

Since the meanings of the $T_{a}$ predicates are not initially specified, I
exclude them from the induction scheme. For the record, I think this
precaution is philosophically unnecessary, but for my purposes there is no
harm in being conservative, as none of the results proven below is affected by
this restriction. We could be even more conservative and forbid any reasoning
about formulas containing $T_{a}$ until ${\rm Acc}(\hat{a})$ has been proven
by, for each $a$ and each axiom $A$ of $\mathcal{S}_{a}$, replacing the “${\rm
Acc}(\hat{a})\to A$” axiom with a deduction rule that infers $A$ from ${\rm
Acc}(\hat{a})$. This also would not affect the validity of anything that
follows in any essential way.

##  5\. The Veblen hierarchy

We can now start to think about the provable ordinals of ${\rm
Tarski}_{\preceq}(\mathcal{S})$. Let us do this in terms of the Veblen
hierarchy.

The Veblen functions $\phi_{\alpha}$ map ordinals into ordinals, and are
defined by induction on the ordinal $\alpha$ by setting
$\phi_{0}(\beta)=\omega^{\beta}$ and, for all $\alpha>0$, letting
$\phi_{\alpha}$ enumerate the common fixed points of
$\\{\phi_{\alpha^{\prime}}:\alpha^{\prime}<\alpha\\}$. At a successor stage
$\alpha+1$ this just means that $\phi_{\alpha+1}$ enumerates the fixed points
of $\phi_{\alpha}$.

We have fixed a computable total ordering $\preceq$ of $\mathbb{N}$. Now fix
an element $c_{0}\in\mathbb{N}$ which is greater than $\omega$ and is stable
under ordinal exponentiation, i.e., if $a,b\prec c_{0}$ then $a^{b}\prec
c_{0}$. Again, we don’t have to know that $\\{c\in\mathbb{N}:c\prec c_{0}\\}$
is well-ordered. Recall that a predicate $A$ is progressive if for all
$a\in\mathbb{N}$

$(\forall b\prec a)A(b)\leftrightarrow A(a);$

I will also say it is progressive up to $c_{0}$ if $(\forall b\prec
a)A(b)\leftrightarrow A(a)$ for all $a\prec c_{0}$.

For each $a,c\prec c_{0}$ define a predicate $B_{a}^{c}$ in the language
$L_{\omega^{a}\cdot c+1}$ by

$B_{a}^{c}(b):=(\forall A\in L_{\omega^{a}\cdot c}^{p})T_{\omega^{a}\cdot
c}(\ulcorner{\rm Prog}(A)\to A(\phi_{a}(b))\urcorner)$

where $L_{a}^{p}$ denotes the set of predicates in $L_{a}$. For fixed $a$, the
predicates $B_{a}^{c}$ say essentially the same thing as $c$ varies: that any
progressive predicate holds of $\phi_{a}(b)$. The only difference is the
languages to which they are applied. This is necessary because we want to
apply some $B_{a}^{c}$’s to others.

Let $C$ be the predicate in the language $L_{c_{0}+1}$

$C(a):=(\forall c\prec c_{0})T_{c_{0}}(\ulcorner{\rm
Prog}(B_{a}^{c})\urcorner)).$

Recalling that $B_{a}^{c}$ and $B_{a}^{c^{\prime}}$ differ only in the
languages to which they are applied, the crude intuition for $C(a)$ is that it
says the assertion that anything progressive holds of $\phi_{a}(b)$ is itself
progressive in $b$. The key theorem we have to prove is that $C$ is itself
progressive!

(The reason the strong version of progressivity defined above helps is that,
under this definition, if $A$ is progressive and $A$ holds of $a$, then the
“shifted” predicate $A^{\to a}(\cdot)=A(a+\cdot)$ is also progressive. Our
version of progressivity ensures that if $A(a)$ fails then $A(a^{\prime})$
also fails for all $a^{\prime}\succ a$, so this shifting can only occur within
the initial, truly progressive part.)

The proof of Theorem 5.4 below is a little long because each $a$ and each $b$
can be zero, a successor, or a limit, leading to nine separate cases which are
nearly all genuinely different. (For limit values of $b$, the argument is
essentially the same regardless of what $a$ is.) For the sake of readability I
have split up the proof into three lemmas. The crucial case appears in Lemma
5.3, when $a$ and $b$ are both successors. (It is only here that the
“$\omega^{a}\cdot c$” expression in $B_{a}^{c}$ becomes important. The point
is that the index $\omega^{a+1}\cdot c$ will always be a limit of indices of
the form $\omega^{a}\cdot c^{\prime}$.)

In the following proofs we will assume ${\rm Acc}(\hat{c}_{0})$, which means
that all the axioms for $T_{c_{0}}$ are available. In particular, we have the
T-scheme for $T_{c_{0}}$. So we can pass freely between $\overline{A}$ and
$T_{c_{0}}(A)$. What we cannot do is to reason under $T_{c_{0}}$ about
predicates such as $C$ which do not belong to $L_{c_{0}}$. Note that in the
definition of $C(a)$ given above we cannot use the $\omega$-rule to import the
quantifier $\forall c\prec c_{0}$ into $T_{c_{0}}$, because $B_{a}^{c}$ is a
distinct predicate for every $a$ and $c$, so an expression like “$(\forall
c\prec c_{0}){\rm Prog}(B_{a}^{c})$” would not be a well-formed formula. But
if we are working under $T_{c_{0}}$, we can simultaneously reason about
$B_{a}^{c}$ for arbitrary values of $c$. Indeed, this is just the sort of
thing truth predicates are good for — allowing us to reason schematically. I
have included some comments about which truth predicate we are reasoning under
at which point, but the essence of the proofs can be understood by ignoring
all references to truth and just accepting that we can reason schematically.

The next three lemmas are proven in ${\rm Tarski}_{\preceq}(\mathcal{S})$.

######  Lemma 5.1.

${\rm Acc}(\hat{c}_{0})$ implies $C(0)$.

###### Proof.

Working in ${\rm Tarski}_{\preceq}(\mathcal{S})$, assume ${\rm
Acc}(\hat{c}_{0})$. Fix $c\prec c_{0}$; reasoning under $T_{c_{0}}$, we must
prove ${\rm Prog}(B_{0}^{c})$, i.e., we must prove progressivity in $b$ of the
statement

(1) $(\forall A\in L_{c}^{p})T_{c}(\ulcorner{\rm Prog}(A)\to
A(\omega^{b})\urcorner).$

For $b=0$ this is trivial; it just says that for any $A\in L_{c}^{p}$ it is
true (according to $T_{c}$) that progressivity of $A$ implies that $A$ holds
of $\omega^{0}=1$. The way we prove this in ${\rm
Tarski}_{\preceq}(\mathcal{S})$ is by first proving in ${\rm
Tarski}_{\preceq}(\mathcal{S})$ — what can actually be done in Peano
arithmetic — a formalization of the statement that for any predicate $A$ in
$L_{c}$ there is a proof in the system $\mathcal{S}_{c}$ from Section 4 of the
sentence “${\rm Prog}(A)\to A(1)$”. We can do this by writing out a proof
template and then verifying its validity for any $A$. Combining this with
Proposition 4.1 (and using ${\rm Acc}(\hat{c}_{0})$), we get $(\forall A\in
L_{c}^{p})T_{c_{0}}(\ulcorner{\rm Prog}(A)\to A(1)\urcorner)$, and then
$(\forall A\in L_{c}^{p})T_{c}(\ulcorner{\rm Prog}(A)\to A(1)\urcorner)$. I
wanted to spell all this out once, but I will omit similar arguments in the
sequel.

For limit values of $b$, assume we are given $(\forall b^{\prime}\prec
b)T_{c}(B_{0}^{c}(b^{\prime}))$; that is, assume

$T_{c}(\ulcorner{\rm Prog}(A)\to A(\omega^{b^{\prime}})\urcorner)$

for all $A\in L_{c}^{p}$ and all $b^{\prime}\prec b$. Using the $\omega$-rule
to bring the quantifier “$\forall b^{\prime}\prec b$” under $T_{c}$, we get
that for every $A\in L_{c}^{p}$ it is true (according to $T_{c}$) that
progressivity of $A$ implies $A(\omega^{b^{\prime}})$ for all $b^{\prime}\prec
b$. Since $\omega^{b}=\sup_{b^{\prime}\prec b}\omega^{b^{\prime}}$, we infer
from this (for arbitrary $A$, under $T_{c}$) that progressivity of $A$ implies
$A(\omega^{b})$.

Finally, if $b=b^{\prime}+1$ is a successor, assume that for every predicate
$A$ in $L_{c}$ it is true (according to $T_{c}$) that progressivity of $A$
implies that $A$ holds of $\omega^{b^{\prime}}$. Since ${\rm Prog}(A)\wedge
A(\omega^{b^{\prime}})$ implies ${\rm Prog}(A^{\to\omega^{b^{\prime}}})$ (as
noted a few paragraphs before this lemma), it is then true that
$A^{\to\omega^{b^{\prime}}}$ holds of $\omega^{b^{\prime}}$, i.e., $A$ holds
of $\omega^{b^{\prime}}+\omega^{b^{\prime}}$. Continuing inductively, we get
the truth for all $n\prec\omega$ of $A(\omega^{b^{\prime}}\cdot n)$, and
progressivity of $A$ then implies that $A$ holds of
$\omega^{b^{\prime}}\cdot\omega=\omega^{b^{\prime}+1}=\omega^{b}$. We have
shown that $B_{0}^{c}(b^{\prime})$ implies $B_{0}^{c}(b^{\prime}+1)$. This
completes the proof that (1) is progressive in $b$ and establishes $C(0)$. ∎

######  Lemma 5.2.

${\rm Acc}(\hat{c}_{0})$ implies that for any limit $a\prec c_{0}$ we have
$(\forall a^{\prime}\prec a)C(a^{\prime})\to C(a)$.

###### Proof.

Working in ${\rm Tarski}_{\preceq}(\mathcal{S})$, assume ${\rm
Acc}(\hat{c}_{0})$. Fix a limit $a\prec c_{0}$ and assume $(\forall
a^{\prime}\prec a)C(a^{\prime})$. This means that we are given the truth,
according to $T_{c_{0}}$, of ${\rm Prog}(B_{a^{\prime}}^{c^{\prime}})$ for
every $a^{\prime}\prec a$ and $c^{\prime}\prec c_{0}$, and we must show that
for every $c\prec c_{0}$ it is true according to $T_{c_{0}}$ that $B_{a}^{c}$
is progressive.

Fix $c\prec c_{0}$. First we check the case $b=0$, where we have to verify
$B_{a}^{c}(0)$. Since we are assuming, for every $c^{\prime}\prec c_{0}$ and
$a^{\prime}\prec a$, that it is true (according to $T_{c_{0}}$) that
$B_{a^{\prime}}^{c^{\prime}}$ is progressive, in particular we have for all
such $c^{\prime}$ and $a^{\prime}$ the truth of
$B_{a^{\prime}}^{c^{\prime}}(0)$. Thus, for every predicate $A$ in some
$L_{\omega^{a^{\prime}}\cdot c^{\prime}}$ with $a^{\prime}\prec a$ and
$c^{\prime}\prec c_{0}$ — which is to say, every predicate $A$ in $L_{c_{0}}$
— we have that progressivity of $A$ implies the truth of
$A(\phi_{a^{\prime}}(0))$ for all $a^{\prime}\prec a$. In particular, for any
predicate $A\in L_{\omega^{a}\cdot c}$ it is true according to $T_{c_{0}}$,
and hence according to $T_{\omega^{a}\cdot c}$, that progressivity of $A$
implies that $A$ holds of $\sup_{a^{\prime}\prec
a}\phi_{a^{\prime}}(0)=\phi_{a}(0)$. This verifies $B_{a}^{c}(0)$. That was
the $b=0$ case.

Next we will show, reasoning under $T_{c_{0}}$, that if $b$ is a limit and we
have $B_{a}^{c}(b^{\prime})$ for all $b^{\prime}\prec b$, then we also have
$B_{a}^{c}(b)$. At this point we have two induction hypotheses going, one for
$a^{\prime}\prec a$ and one for $b^{\prime}\prec b$. To verify $B_{a}^{c}(b)$,
let $A$ be a predicate in $L_{\omega^{a}\cdot c}$. Then
$B_{a}^{c}(b^{\prime})$ for all $b^{\prime}\prec b$ tells us that according to
$T_{\omega^{a}\cdot c}$, progressivity of $A$ implies that $A$ holds of
$\phi_{a}(b^{\prime})$ for all $b^{\prime}\prec b$. So according to
$T_{\omega^{a}\cdot c}$, progressivity of $A$ implies that $A$ holds of
$\sup_{b^{\prime}\prec b}\phi_{a}(b^{\prime})=\phi_{a}(b)$, as desired. We did
not even need the induction hypothesis on $a$ in this part.

The final case is for successor values of $b$. Say $b=b^{\prime}+1$. Reasoning
under $T_{c_{0}}$, we have to verify that $B_{a}^{c}(b^{\prime})$ implies
$B_{a}^{c}(b^{\prime}+1)$. For this we must use both (i) the induction
hypothesis on $a$ (for every $c^{\prime}\prec c_{0}$ and $a^{\prime}\prec a$
the predicate $B_{a^{\prime}}^{c^{\prime}}$ is progressive) and (ii) the
induction hypothesis on $b$ (we have $B_{a}^{c}(b^{\prime})$). Now
$B_{a}^{c}(b^{\prime})$ says that every progressive $A\in L_{\omega^{a}\cdot
c}$ holds of $\phi_{a}(b^{\prime})$, and $\phi_{a}(b^{\prime})$ is a fixed
point of every $\phi_{a^{\prime}}$ with $a^{\prime}\prec a$, so we can also
say that every progressive $A\in L_{\omega^{a}\cdot c}$ holds of
$\phi_{a^{\prime}}(\phi_{a}(b^{\prime}))$ for all $a^{\prime}\prec a$. This
means that $B_{a^{\prime}}^{c^{\prime}}(\phi_{a}(b^{\prime}))$ holds for all
$a^{\prime}\prec a$ and $c^{\prime}\prec c_{0}$ such that
$L_{\omega^{a^{\prime}}\cdot c^{\prime}}\subseteq L_{\omega^{a}\cdot c}$.

But for any $a^{\prime}\prec a$, we can find $a^{\prime\prime}$ such that
$a^{\prime}+a^{\prime\prime}=a$, and then by putting
$c^{\prime}=\omega^{a^{\prime\prime}}\cdot c$, we get
$\omega^{a^{\prime}}\cdot c^{\prime}=\omega^{a}\cdot c$. So by the conclusion
reached in the last paragraph, for any $a^{\prime}\prec a$ there exists
$c^{\prime}\prec c_{0}$ such that $L_{\omega^{a^{\prime}}\cdot
c^{\prime}}=L_{\omega^{a}\cdot c}$ and
$B_{a^{\prime}}^{c^{\prime}}(\phi_{a}(b^{\prime}))$ holds. And since every
such $B_{a^{\prime}}^{c^{\prime}}$ is progressive, by (i), it follows that
$B_{a^{\prime}}^{c^{\prime}}(\phi_{a}(b^{\prime})+1)$ also holds.

We are now in a position to affirm that for every $a^{\prime}\prec a$, every
progressive $A\in L_{\omega^{a}\cdot c}$ lies within the scope of some
$B_{a^{\prime}}^{c^{\prime}}$ which satisfies
$B_{a^{\prime}}^{c^{\prime}}(\phi_{a}(b^{\prime})+1)$, so that $A$ holds of
$\phi_{a^{\prime}}(\phi_{a}(b^{\prime})+1)$. If $a^{\prime}$ is a successor,
$a^{\prime}=a^{\prime\prime}+1$, then this means that $A$ holds of the next
fixed point of $\phi_{a^{\prime\prime}}$ after $\phi_{a}(b^{\prime})$. Thus,
by progressivity, $A$ holds of the supremum of these fixed points over all
$a^{\prime\prime}\prec a$, which equals $\phi_{a}(b^{\prime}+1)=\phi_{a}(b)$.
That verifies $B_{a}^{c}(b)$ and completes the proof of $C(a)$. ∎

######  Lemma 5.3.

${\rm Acc}(\hat{c}_{0})$ implies that for any $a\prec c_{0}$, $C(a)$ implies
$C(a+1)$.

###### Proof.

Working in ${\rm Tarski}_{\preceq}(\mathcal{S})$, assume ${\rm
Acc}(\hat{c}_{0})$. Fix $a\prec c_{0}$ and assume $C(a)$, and on the way to
proving $C(a+1)$, fix $c\prec c_{0}$. Reasoning under $T_{c_{0}}$, we must
prove that $B_{a+1}^{c}$ is progressive, i.e., that for every $b$, if
$B_{a+1}^{c}(b^{\prime})$ holds for all $b^{\prime}\prec b$ then
$B_{a+1}^{c}(b)$ also holds.

If $b=0$ then we simply have to show that $B_{a+1}^{c}(0)$ holds, i.e., that
any progressive $A\in L_{\omega^{a+1}\cdot c}$ holds of $\phi_{a+1}(0)$. Since
we have assumed $C(a)$, we know that for any $c^{\prime}\prec c_{0}$,
according to $T_{c_{0}}$ the predicate $B_{a}^{c^{\prime}}$ is progressive. In
particular, for each $n\prec\omega$ the predicate $B_{a}^{c+n}$ is
progressive. Thus $B_{a}^{c+n}$ holds of $0$, so every progressive predicate
in $L_{\omega^{a}(c+n)}$ holds of $\phi_{a}(0)$, and hence of $\phi_{a}(0)+1$.
In particular, $B_{a}^{c+n-1}$ holds of $\phi_{a}(0)+1$. So every progressive
predicate in $L_{\omega^{a}(c+n-1)}$ holds of $\phi_{a}(\phi_{a}(0)+1)$.
Inductively, every progressive predicate in $L_{\omega^{a}(c+n-k)}$ holds of
$\phi_{a}^{k}(\phi_{a}(0)+1)$, which means (taking $k=n$) that every
progressive predicate in $L_{\omega^{a}\cdot c}$ holds of
$\phi_{a}^{n}(\phi_{a}(0)+1)$. Since $n$ was arbitrary, it follows that every
progressive predicate in $L_{\omega^{a}\cdot c}$ holds of
$\sup_{n\prec\omega}\phi_{a}^{n}(\phi_{a}(0)+1)=\phi_{a+1}(0)$. This finishes
the $b=0$ case.

Next, assuming that for some limit $b$ we have $B_{a+1}^{c}(b^{\prime})$ for
all $b^{\prime}\prec b$, we must verify $B_{a+1}^{c}(b)$. This is easy,
because we are given that any progressive predicate in $L_{\omega^{a+1}\cdot
c}$ holds of $\phi_{a+1}(b^{\prime})$ for all $b^{\prime}\prec b$, and so by
progressivity it holds of $\sup_{b^{\prime}\prec
b}\phi_{a+1}(b^{\prime})=\phi_{a+1}(b)$. The corresponding cases in Lemmas 5.1
and 5.2 were handled in the same way.

Finally, letting $b$ be arbitrary, we must make the inference from
$B_{a+1}^{c}(b)$ to $B_{a+1}^{c}(b+1)$. So assume $B_{a+1}^{c}(b)$ and fix
$A\in L^{p}_{\omega^{a+1}\cdot c}$. We can write $\omega^{a+1}\cdot
c=\omega^{a}\cdot\omega c$, and since $\omega c$ is a limit, this shows that
$A$ must belong to $L_{\omega^{a}\cdot c^{\prime}}$ for some
$c^{\prime}\prec\omega c$. Moreover, since $\omega c$ is a limit, we have
$c^{\prime}+n\prec\omega c$ for all $n\prec\omega$.

Now for each $n\prec\omega$ the predicate $B_{a}^{c^{\prime}+n}$ belongs to
$L_{\omega^{a+1}\cdot c}$, and is progressive since we are assuming $C(a)$, so
the hypothesis of $B_{a+1}^{c}(b)$ yields
$B_{a}^{c^{\prime}+n}(\phi_{a+1}(b))$, and then by progressivity we get
$B_{a}^{c^{\prime}+n}(\phi_{a+1}(b)+1)$. Applying this to
$B_{a}^{c^{\prime}+n-1}$, which lies in
$L_{\omega^{a}(c^{\prime}+n-1)+1}\subseteq L_{\omega^{a}(c+n)}$, then yields
$B_{a}^{c^{\prime}+n-1}(\phi_{a}(\phi_{a+1}(b)+1))$, and inductively we
finally get $B_{a}^{c^{\prime}}(\phi_{a}^{n}(\phi_{a+1}(b)+1))$. Since $A\in
L_{\omega^{a}\cdot c^{\prime}}$, if $A$ is progressive this entails
$A(\phi_{a}^{n+1}(\phi_{a+1}(b)+1))$, and as $n$ was arbitrary
$A(\phi_{a+1}(b+1))$ follows. We have established $B_{a+1}^{c}(b)$, as
desired. ∎

Putting these lemmas together yields the following theorem.

######  Theorem 5.4.

${\rm Tarski}_{\preceq}(\mathcal{S})$ proves that ${\rm Acc}(\hat{c}_{0})$
implies $C$ is progressive up to $c_{0}$.

Define $\gamma_{0}=0$, $\gamma_{1}=\phi_{0}(0)=1$,
$\gamma_{2}=\phi_{1}(0)=\varepsilon_{0}$, etc., with
$\gamma_{n+1}=\phi_{\gamma_{n}}(0)$. The ordinal $\Gamma_{0}$ is defined as
the limit $\Gamma_{0}=\sup_{n}\gamma_{n}$. Just as with $\omega$, I will use
these symbols both for abstract ordinals and their numerical representatives
in $(\mathbb{N},\preceq)$.

In what follows the term “transfinite induction up to $a$ for $\mathcal{S}$”
will refer to the scheme consisting of all sentences of the form “${\rm
Prog}_{\hat{a}}(A)\to(\forall b\prec\hat{a})A(b)$” as $A$ ranges over the
predicates in the language of $\mathcal{S}$, where “${\rm Prog}_{\hat{a}}(A)$”
means “$A$ is progressive up to $\hat{a}$”.

######  Corollary 5.5.

Let $n\geq 2$. Then ${\rm Tarski}_{\preceq}(\mathcal{S}))$ plus transfinite
induction up to $\gamma_{n}$ for ${\rm Tarski}_{\preceq}(\mathcal{S})$ proves
transfinite induction up to $\gamma_{n+1}$ for $\mathcal{S}$.

###### Proof.

Fix $n$. Since ${\rm Acc}$ is progressive, transfinite induction up to
$\gamma_{n}$ for ${\rm Tarski}_{\preceq}(\mathcal{S})$ yields $(\forall
a\prec\gamma_{n}){\rm Acc}(a)$, and then, with one further application of
progressivity, ${\rm Acc}(\gamma_{n})$. Theorem 5.4 then yields, in ${\rm
Tarski}_{\preceq}(\mathcal{S})$ plus ${\rm Acc}(\gamma_{n})$, that $C$ is
progressive up to $\gamma_{n}$, and now the hypothesis on transfinite
induction up to $\gamma_{n}$ yields $(\forall a\prec\gamma_{n})C(a)$. In
particular, we have $(\forall a\prec\gamma_{n})T_{c_{0}}(B_{a}^{0}(0))$.

Thus for any predicate $A$ in $L$, we have

$T_{c_{0}}({\rm Prog}(A)\to(\forall a\prec\gamma_{n})A(\phi_{a}(0))),$

hence

${\rm Prog}(A)\to(\forall a\prec\gamma_{n})A(\phi_{a}(0))$

hence

${\rm Prog}(A)\to(\forall b\prec\gamma_{n+1})A(b)$

since $\sup_{a\prec\gamma_{n}}\phi_{a}(0)=\phi_{\gamma_{n+1}}$. We have proven
transfinite induction up to $\gamma_{n+1}$ for $\mathcal{S}$. ∎

##  6\. Iterating the ${\rm Tarski}_{\preceq}(\mathcal{S})$ construction

Theorem 5.4 doesn’t get us very far by itself, since it requires a strong
assumption about ${\rm Acc}$. What we must do now is to “reflect” on the
legitimacy of the ${\rm Tarski}_{\preceq}$ construction. We have agreed that,
for arbitrary $\mathcal{S}$, if we accept $\mathcal{S}$ then we should accept
${\rm Tarski}_{\preceq}(S)$, and so we should also accept ${\rm
Tarski}^{2}_{\preceq}(\mathcal{S})={\rm Tarski}_{\preceq}({\rm
Tarski}_{\preceq}(\mathcal{S}))$, then ${\rm
Tarski}^{3}_{\preceq}(\mathcal{S})={\rm Tarski}_{\preceq}({\rm
Tarski}^{2}_{\preceq}(\mathcal{S}))$, and so on. We could now formulate a
“higher order” construction that iterates the $\mathcal{S}\mapsto{\rm
Tarski}_{\preceq}(\mathcal{S})$ construction along $\preceq$, which would be
justified by countablist reasoning in the same way we justified ${\rm
Tarski}_{\preceq}(\mathcal{S})$. This was done in [2], and the ordinal
strength that results from doing this can be found there. Here I only want to
consider ${\rm Tarski}^{\omega}_{\preceq}(\mathcal{S})$.

######  Theorem 6.1.

${\rm Tarski}^{\omega}_{\preceq}({\rm PA})=\bigcup_{n\prec\omega}{\rm
Tarski}^{n}_{\preceq}({\rm PA})$ proves ${\rm Prog}(A)\to A(\hat{a})$ for
every $a\prec\Gamma_{0}$ and every predicate $A$ in its language.

###### Proof.

We make the argument for any first-order theory $\mathcal{S}$ that extends
${\rm PA}$. Fix $n\prec\omega$. The main idea is to prove, in ${\rm
Tarski}^{n}_{\preceq}(\mathcal{S})$, transfinite induction up to $\gamma_{2}$
for ${\rm Tarski}^{n-1}_{\preceq}(\mathcal{S})$, and then inductively apply
Corollary 5.5 to get transfinite induction up to $\gamma_{k+1}$ in ${\rm
Tarski}^{n-k}(\mathcal{S})$, for $1\leq k\leq n$, yielding finally transinite
induction up to $\gamma_{n+1}$ for $\mathcal{S}$. At that point the full
statement of the theorem will follow easily.

The base case of transfinite induction up to $\gamma_{2}$ is similar to Lemma
5.1, but different enough to merit being written out. Taking
$\mathcal{S}^{\prime}={\rm Tarski}^{n-1}_{\preceq}(\mathcal{S})$, we want to
prove, in ${\rm Tarski}^{n}_{\preceq}(\mathcal{S})={\rm
Tarski}_{\preceq}(\mathcal{S}^{\prime})$, transfinite induction up to
$\gamma_{2}=\varepsilon_{0}$ for $\mathcal{S}^{\prime}$. To do this we
introduce a jump predicate $J_{A}$, for every predicate $A$ in the language of
$\mathcal{S}^{\prime}$, defined by

$J_{A}(b):=(\forall a)(A(a)\to A(a+\omega^{b})).$

This is a different predicate for each $A$. Now, for any $A$, we start by
proving in $\mathcal{S}^{\prime}$ that progressivity of $A$ implies
progressivity of $J_{A}$. Fix $A$ and assume it is progressive. Then
$J_{A}(0)$ says that $(\forall a)(A(a)\to A(a+1))$, and this is an immediate
consequence of progressivity of $A$. If $b$ is a limit, then
$J_{A}(b^{\prime})$ for all $b^{\prime}\prec b$ says that for any $a$ we have
$A(a)\to A(a+\omega^{b^{\prime}})$ for all $b^{\prime}\prec b$, and this
yields $A(a)\to A(a+\omega^{b})$ for all $a$, by progressivity of $A$ again.
Finally, assuming $J_{A}(b)$, we must prove $J_{A}(b+1)$. Here we use the
reasoning that $J_{A}(b)$ tells us that $A(a)$ implies $A(a+\omega^{b})$, and
also that $A(a+\omega^{b})$ implies $A(a+\omega^{b}+\omega^{b})$, and so on;
that is, an induction argument shows that $J_{A}(b)$ implies $(\forall
a)(A(a)\to A(a+\omega^{b}\cdot n))$ for all $n\prec\omega$. One final appeal
to progressivity of $A$ then yields $J_{A}(b)\to J_{A}(b+1)$.

For a given predicate $A$ in the language of $\mathcal{S}^{\prime}$, we have
shown, in $\mathcal{S}^{\prime}$, that ${\rm Prog}(A)\to{\rm Prog}(J_{A})$.
Now, reasoning in the one-step truth theory ${\rm
Tarski}(\mathcal{S}^{\prime})$, we can see that $T({\rm Prog}(A))$ implies
$T({\rm Prog}(J_{A}))$ implies $T({\rm Prog}(J_{J_{A}}))$ implies $\cdots$,
for any $A$. Thus, if $A$ is progressive then $A(1)$ is true, $J_{A}(1)$ is
true (which implies that $A(\omega)$ is true), $J_{J_{A}}(1)$ is true (which
implies that $J_{A}(\omega)$ is true, which implies that $A(\omega^{\omega})$
is true), and so on. Inductively we get $(\forall
n\prec\omega)T(A(\omega^{(n)}))$, where $\omega^{(1)}=\omega$ and
$\omega^{(n+1)}=\omega^{\omega^{(n)}}$. So $T({\rm Prog}(A))$ implies
$T(A(\varepsilon_{0}))$.

That was in ${\rm Tarski}(\mathcal{S}^{\prime})$. But in ${\rm
Tarksi}_{\preceq}(\mathcal{S}^{\prime})$ we have ${\rm Prog}({\rm Acc})$, so
in particular we have ${\rm Acc}(0)$, which means that we can reason in the
one-step truth theory ${\rm Tarski}(\mathcal{S}^{\prime})$. Thus ${\rm
Tarski}^{n}_{\preceq}(\mathcal{S})$ proves transfinite induction up to
$\gamma_{2}=\varepsilon_{0}$ for ${\rm Tarski}^{n-1}_{\preceq}(\mathcal{S})$.

From this point, we can apply Corollary 5.5 $n-1$ times to obtain transfinite
induction up to $\gamma_{n+1}$ for $\mathcal{S}$, where $n$ was arbitrary. But
${\rm Tarksi}^{\omega}_{\preceq}(\mathcal{S})$ literally equals ${\rm
Tarski}^{\omega}_{\preceq}({\rm Tarski}^{k}_{\preceq}(\mathcal{S}))$ for any
$k$, so this argument actually yields transfinite induction up to
$\gamma_{n+1}$ for ${\rm Tarski}^{k}_{\preceq}(\mathcal{S})$, for any $k$ and
any $n$. We conclude that ${\rm Tarski}^{\omega}_{\preceq}(\mathcal{S})$
proves ${\rm Prog}(A)\to A(\gamma_{n})$ for all $n$ and all predicates $A$ in
its language. ∎

##  7\. Conclusion

So predicativists, or really anyone who accepts countablist reasoning, can
affirm transfinite induction up to anything less than $\Gamma_{0}$ in ${\rm
Tarski}^{\omega}_{\preceq}({\rm PA})$. But then one further step to ${\rm
Tarski}^{\omega+1}_{\preceq}({\rm PA})$ gets us beyond $\Gamma_{0}$, and we
can keep going. Indeed, the “higher order” construction mentioned in Section 6
gets vastly beyond $\Gamma_{0}$.

The celebrated Feferman-Schütte analysis which identified $\Gamma_{0}$ as the
exact limit of predicative reasoning is utter nonsense — I am sorry I have to
say this so plainly, but apparently I do. It was already thoroughly refuted in
[2]; see [4] for a short explanation of the problems. This analysis was based
on the idea from Section 1 about accumulating ever-larger provable ordinals as
we work our way up a hierarchy, leading us to accept ever-higher theories in
the hierarchy. The (well, one) fatal flaw in this approach is that at stage
$n$ we do not prove transfinite induction up to $\gamma_{n}$ for all
predicates in the language, only for predicates of the form “$x\in A$”, i.e.,
we prove induction up to $\gamma_{n}$ for sets. But at stage $n+1$ we require,
not induction up to $\gamma_{n}$ for sets, but recursion up to $\gamma_{n}$.
So we have to make an inference from induction to recursion, which is
something predicativists cannot do. (Or, if they magically somehow could, then
they could use this fact to get beyond $\Gamma_{0}$. The only way to land
exactly on $\Gamma_{0}$ is by postulating that predicativists can always,
somehow, infer recursion from induction, but they are not aware that they have
this general ability and so cannot formulate it as a general principle. The
foundations community is going to have to choose between affirming this
absurdity, which has no rational basis whatever, and admiting that Feferman
and Schütte simply got it wrong.)

The induction/recursion issue doesn’t arise in the analysis of truth theories
presented here, because we actually prove full induction at each stage, not
just induction for sets. But the idea of working up a hierarchy is more subtle
in this approach, because one actually works down a tower of ${\rm
Tarski}_{\preceq}$ theories in order to move up through the $\gamma_{n}$’s.

It would be very interesting to see how much further one can get in a system
that formalizes the idea that whenever we have a construction that converts
any accepted system $\mathcal{S}$ into another, stronger accepted system, we
can accept a system that iterates this construction along $\preceq$. Another
challenge for the reader, one that would get us closer to understanding the
true ordinal strength of predicativism.

## References

  * [1] A. Ipsen, personal communication.
  * [2] N. Weaver, Predicativity beyond $\Gamma_{0}$ (2005), arXiv:math/0509244.
  * [3] ———, Truth & Assertibility, 2015.
  * [4] ———, Predicative well-ordering (2018), arxiv.org/abs/1811.03543.