1 Introduction
By Gödel’s second incompleteness theorem no consistent extension of
$\mathsf {PA}$
with a computably enumerable axiomatization can prove its own consistency. Thus, whenever we extend a sound arithmetical theory T to a sound theory
$T'$
that proves the consistency of T, it is guaranteed that
$T'$
is stronger than T. The idea of using this phenomenon to attain transfinite sequences of theories of ascending strength goes back to Alan Turing [Reference Turing22]. In modern terms, Turing defined transfinite iterations of local reflection
$\mathsf {Rfn}$
roughly as
$$\begin{align*}\mathsf{Rfn}^0(T)=T\quad\mathsf{Rfn}^{\alpha+1}(T)=T+\mathsf{Rfn}(\mathsf{Rfn}^\alpha(T))\quad \mathsf{Rfn}^\lambda(T)=\bigcup\limits_{\alpha<\lambda}\mathsf{Rfn}^\alpha(T). \end{align*}$$
Here, for a theory T with a fixed c.e. axiomatization,
$\mathsf {Rfn}(T)$
is the collection of all principles
A subtle feature of this definition is that at each step of the inductive definition, one has to pick a c.e. axiomatization of
$\mathsf {Rfn}^\alpha (T)$
. Thus
$\alpha $
has to be a computable ordinal with a fixed computable presentations, hence the theories
$\mathsf {Rfn}^\alpha (T)$
depend not only on the order-type of
$\alpha $
but also on the particular computable presentation. As was proven already by Turing, for any true
$\Pi _1$
-sentence
$\varphi $
there is a computable presentation
$\alpha $
of the ordinal
$\omega +1$
, in fact an ordinal notation in Kleene’s
$\mathcal {O}$
, such that
$\mathsf {Rfn}^\alpha (\mathsf {PA})$
proves
$\varphi $
. Of course, there cannot be a single computable presentation
$\alpha $
such that
$\mathsf {Rfn}^\alpha (\mathsf {PA})$
proves every true
$\Pi _1$
sentence, as this would mean that there is a consistent c.e. extension of
$\mathsf {PA}$
proving all true
$\Pi _1$
statements. Thus, the construction of theories
$\mathsf {Rfn}^\alpha (\mathsf {PA})$
has an intensional character: Their consequences depend not only on the order type of
$\alpha $
but also on the choice of a particular computable presentation.
Turing also conjectured that for every arithmetical theorem
$\varphi $
, there is a computable presentation of an ordinal
$\alpha $
such that
$\mathsf {Rfn}^\alpha (\mathsf {PA})$
proves
$\varphi $
. Later, Feferman [Reference Feferman6] refuted this conjecture. However, he considered a variant of Turing’s progression, where local reflections
$\mathsf {Rfn}(T)$
are replaced with uniform reflections
$\mathsf {RFN}(T)$
:
For this variant, Feferman proved that Turing’s conjecture holds, i.e., any true arithmetical sentence is provable in
$\mathsf {RFN}^\alpha (\mathsf {PA})$
. This result is often referred to as Feferman’s completeness theorem. Feferman’s construction gives
$\omega ^{{\omega }^{\omega +1}}$
as an upper bound on the order type of the ordinal notations along which one needs to iterate reflection to obtain a proof of
$\varphi $
.
The presence of an upper bound in Feferman’s result indicates that it is a negative result: It essentially shows that proof-theoretic strength of an arithmetical sentence
$\varphi $
couldn’t be appropriately measured by the least order-type of ordinal notation, iteration of reflection along which proves
$\varphi $
. However, when restricted to natural ordinal notation systems the length of iterations of reflection necessary to obtain a particular theory does reflect the proof-theoretic strength of the theory. This phenomenon was explored and used for the applications to ordinal analysis [Reference Beklemishev4, Reference Schmerl16]. We furthermore note that as was shown by the first author and James Walsh [Reference Pakhomov and Walsh12], for systems of second-order arithmetic and their
$\Pi ^1_1$
-consequences, the strength of the systems can be appropriately measured in terms of the length of iterations of
$\Pi ^1_1$
-reflection, which is a measure closely connected with the
$\Pi ^1_1$
-proof theoretic ordinals of theories.
Feferman’s original proof of his completeness theorem is not widely known, perhaps because of its considerable technical difficulty. One feature that Feferman’s proof shares with Turing’s (rather simple) proof of the
$\Pi ^0_1$
-completeness of consistency progressions is the employment of non-standard definitions of the axioms of theories. These non-standard definitions are engineered so that we know them to be an axiomatization of a “natural” theory only if we know a certain sentence
$\varphi $
to be true. In Feferman’s proof, they appear in ever more intertwined ways. Very artfully, he applies increasingly more entangled versions of the recursion theorem to generate non-standard definitions of theories (see [Reference Franzén9] for further details). Franzén [Reference Franzén9, p. 387] expressed this as follows:
The completeness theorem [i.e., Feferman’s] can be seen as a dramatic illustration of the role of intensionality in logic.
In this paper, we present three new proofs of Feferman’s completeness theorem. The first is a simple proof of this theorem using results not available to Feferman at the time such as the conservativity of
$\mathsf {ACA_0}$
over
$\mathsf {PA}$
. The second proof is an alternative proof using techniques that Feferman could have had access to, such as Schütte’s completeness theorem for
$\omega $
-logic. At last, we combine our first proof with results of Ash and Knight [Reference Ash and Knight2] in computable structure theory to obtain precise bounds on the order types appearing in Feferman’s theorem.
1.1 Structure of the paper
The paper is structured as follows. First, in Section 2 we give a fully self-contained presentation of our simple proof of Feferman’s completeness theorem. The proof is split into three well-understood steps:
-
(1) For any arithmetical sentence
$\varphi $
there is a computable order
$\mathcal {L}$
such that
$$\begin{align*}\mathsf{ACA}_0\vdash \mathsf{WO}(\mathcal{L})\mathrel{\leftrightarrow} \varphi\;\;\;\text{and}\;\;\; \mathsf{ACA}_0\vdash \mathsf{LO}(\mathcal{L}).\end{align*}$$
-
(2) For any computable linear order
$\mathcal {L}$
such that
$\mathsf {ACA}_0\vdash \mathsf {LO}(\mathcal {L})$
the theories
$\mathsf {ACA}_0+\mathsf {WO}(\mathcal {L})$
and
$\mathsf {PA}+\mathsf {TI}(\mathcal {L})$
prove exactly the same first-order sentences. -
(3) As we prove in Lemma 5
$$\begin{align*}\mathsf{RFN}^{\mathcal{L}+1}(\mathsf{PA})\vdash \mathsf{TI}(\mathcal{L}). \end{align*}$$
The ideas of the proofs of these components are the following:
-
(1) This is a particular case of
$\mathsf {ACA}_0$
-provable
$\Pi ^1_1$
-completeness of well-orders. For the convenience of readers, we give a standard proof of the fact (Lemma 3). -
(2) We prove this in Lemma 19 by showing that the extension of any model of
$\mathsf {PA}+\mathsf {LO}(\mathcal {L})+\mathsf {TI}(\mathcal {L})$
by the second-order universe consisting of first-order definable sets is a model of
$\mathsf {ACA}_0+\mathsf {WO}(\mathcal {L})$
. -
(3) Like most other facts about the iterations of reflection principles, this fact is straightforward to prove using Löb’s Theorem.
We note that neither of these facts is actually new. The first goes back to Kleene and the formalized version can be found in [Reference Simpson18]. The second fact is a triviality, while the third one is folklore.
In Section 3 we give a proof of Feferman’s completeness theorem using techniques available at the time and in Sections 4 and 5 we obtain sharp ordinal bounds for Feferman’s completeness theorem.
Theorem 1. For every true
$\Pi _{2n+1}$
sentence
$\varphi $
there exists a computable
$\mathsf {PA}$
-verifiable linear order
$\mathcal {L}\cong \omega ^n+1$
such that
$$\begin{align*}\mathsf{RFN}^{\mathcal{L}}(\mathsf{PA})\vdash \varphi.\end{align*}$$
To prove Theorem 1 we replace the use of
$\Pi ^1_1$
-completeness of computable well-orders with a sharper theorem of Ash and Knight [Reference Ash and Knight2], who proved that the set of indices of computable orderings of order-type
$\omega ^n$
is
$\Pi ^0_{2n+1}$
-hard.
We complement Theorem 1 with the following result proving that the upper bound on order-types is in fact sharp.
Theorem 2. For every
$n>0$
, there exists a true
$\Pi _{2n}$
-sentence
$\varphi $
such that for any computable
$\mathsf {PA}$
-verifiable linear order
$\mathcal {L}$
of order-type at most
$\omega ^n$
$$\begin{align*}\mathsf{RFN}^{\mathcal{L}}(\mathsf{PA})\nvdash \varphi.\end{align*}$$
The key point in the proof of Theorem 2 is that for any ordinal
$\alpha <\omega ^n$
there is a
$\Sigma _{2n}$
definition of the property of an index of a computable order to be an isomorphic copy of
$\alpha $
.
We remark that in our main results, we are dealing with reflection iterated along arbitrary computable well-orders, while classically Feferman and Turing considered iterations along ordinal notations from Kleene’s
$\mathcal {O}$
. In fact the results are sensitive to this distinction and in Section 6 we establish
$\omega ^{n+1}+1$
as an upper bound on the order types of elements of
$\mathcal {O}$
necessary to attain arbitrary true
$\Pi _{2n+1}$
-sentences as the consequences of iterated full uniform reflection.
2 Feferman’s completeness theorem via Kleene’s normal forms
2.1 Computable orders
Usually, recursive progressions proceed along some ordinal given by some ordinal notation system such as Kleene’s
$\mathcal O$
. We deviate from this since we will work directly with indices for computable orderings.
A linear ordering
$\mathcal {L}$
is a pair consisting of a set L and a binary relation
$\preceq ^{\mathcal {L}}$
satisfying the usual axioms of linear orders.Footnote
1
. Note that L could be recovered from
$\preceq ^{\mathcal {L}}$
as the set of x such that
$x\preceq x$
.
Formally within first-order arithmetic, we represent computable orders
$\mathcal {L}$
as natural numbers coding pairs consisting of an index of a
$\Pi _1$
-set and an index of a
$\Sigma _1$
-set such that they represent the same set
$\preceq ^{\mathcal {L}}$
and this set is a binary relation satisfying the axioms of linear orders. There is a first-order arithmetical formula
$\mathsf {LO}(\mathcal {L})$
expressing that
$\mathcal {L}$
is indeed a computable linear order in the sense above. We say that an order
$\mathcal {L}$
is a
$\mathsf {PA}$
-verifiable computable linear order if
$\mathsf {PA}$
proves
$\mathsf {LO}(\mathcal {L})$
. Over
$\mathsf {ACA}_0$
we formulate the second-order formula
$\mathsf {WO}(\mathcal {L})$
expressing that
$\mathcal {L}$
is a well-order:
$$\begin{align*}\mathsf{LO}(\mathcal{L})\land \forall Y \big(\exists x(x\in Y\cap \mathcal{L}) \to (\exists x\in Y\cap \mathcal{L})(\forall y\in Y\cap \mathcal{L}) (x\preceq^{\mathcal{L}} y)\big).\end{align*}$$
The following theorem gives the first part of our proof of Feferman’s completeness theorem.
Lemma 3. For any arithmetical sentence
$\varphi $
there exists a
$\mathsf {PA}$
-verifiable computable linear order
$\mathcal {L}$
such that
$\mathsf {ACA_0}\vdash \varphi \leftrightarrow \mathsf {WO}(\mathcal {L})$
.
This follows immediately from the fact that it is provable in
$\mathsf {ACA_0}$
that the set of indices of computable well-orders is a complete
$\Pi ^1_1$
-set and that every arithmetical formula is
$\Pi ^1_1$
, see [Reference Simpson18, Lemma V.1.8].
For the convenience of the reader, we give a proof of Lemma 3 using standard techniques.
Proof We claim that there is a formula equivalent to
$\lnot \varphi $
over
$\mathsf {ACA}_0$
that is of the form
$(\exists f: \mathbb {N}\to \mathbb {N})\forall x \psi (f,x)$
, where
$\psi (f,x)$
is a quantifier-free formula whose atomic subformulas are equalities of terms built from f and primitive-recursive formulas.
To prove the claim we consider
$\varphi $
to be a formula built using Boolean connectives and existential quantifiers. Then we consider the expansion of the language of arithmetic by Skolem functions
$f_{\chi }(\vec {y})$
for all the subformulas
$\chi $
of
$\varphi $
of the form
$\exists x \xi (x,\vec {y})$
. Now, by induction on subformulas
$\theta (\vec {x})$
of
$\varphi $
, we define their Skolemized variants
$\theta '(\vec {x})$
that are quantifier-free formulas in the expanded language: the transformation
$(\cdot )'$
commutes with Boolean connectives and
$\chi =(\exists x \xi (x,\vec {y}))'$
is
$\xi (f_{\chi }(\vec y),\vec {y})$
. For each Skolem function
$f_\chi $
where
$\chi =\exists x \xi (x,\vec {y})$
we have the axiom
$\xi (x,\vec {y})\to \xi (f_{\chi }(\vec {y}),\vec {y})$
that expresses that
$f_{\chi }(\vec {y})$
is indeed a Skolem function for
$\exists x \, \xi (x,\vec {y})$
. This allows us to transform
$\lnot \varphi $
over
$\mathsf {ACA}_0$
to a formula of the form
$$\begin{align*}\exists \vec{f}\forall \vec{x}\ \psi(\vec{f},\vec{x}),\end{align*}$$
where the quantifier
$\exists \vec {f}$
quantifies over the candidates for Skolem functions and the following formula is the universal closure of the conjunction of the axioms expressing that the f’s indeed are designated Skolem functions and
$\lnot \varphi '$
. After that, using supplementary primitive-recursive functions, it is easy to merge multiple multi-variant f’s into a single unary f and multiple
$\vec {x}$
into a single x. Which finishes the proof of the claim.
Subsequently we transform
$\varphi $
from the form
$$\begin{align*}(\forall f: \mathbb{N}\to\mathbb{N})\exists x\, \lnot \psi(f,x) \quad \text{to} \quad \forall f\exists x\, \theta(f\upharpoonright x),\end{align*}$$
where
$\theta (y)$
is a quantifier-free formula in the language with primitive-recursive functions that expresses that
-
(1) y is a code of a sequence
$(s_0,\ldots ,s_{k-1})$
that we treat as a pair consisting of
$x=s_0$
and a partial function
$f\colon i\mapsto s_{i+1}$
, -
(2) the domain of f is sufficient to evaluate the validity of the formula
$\psi (f,x)$
, -
(3) and the formula
$\psi (f,x)$
is false.
Hence over
$\mathsf {ACA}_0$
,
$\varphi $
is equivalent to the well-foundedness of the primitive-recursive tree of sequences
$$\begin{align*}T=\{(s_0,\ldots,s_{k-1})\mid(\forall x<k)\neg\theta((x,s_0,\ldots,s_{k-1}))\}.\end{align*}$$
We construct
$\mathcal {L}$
as the Kleene–Brouwer order on T, i.e., the order where each node
$(s_0,\ldots ,s_{k-1})$
is bigger than all its descendants
$(s_0,\ldots ,s_{k-1},u_k,\ldots ,u_{l-1})$
and for all
$u_k<u_k^{\prime }$
all the elements in the subtree of
$(s_0,\ldots ,s_{k-1},u_k)$
are smaller than the elements in the subtree of
$(s_0,\ldots ,s_{k-1},u_k^{\prime })$
.
Every infinite branch through T is an infinite descending chain through
$\mathcal {L}$
. Thus, provably in
$\mathsf {ACA}_0$
, well-orderedness of
$\mathcal {L}$
implies the well-foundedness of T. In the other direction, for every infinite descending chain in
$\mathcal {L}$
using arithmetical comprehension we find the infinite descending sequence
$(),(s_0),(s_0,s_1),\ldots $
in T that is defined to consist of sequences
$(s_0,\ldots ,s_{k-1})$
whose sub-trees contain infinitely many elements of the original descending sequence.
The linearity of this
$\mathcal {L}$
is, of course, trivial to verify in
$\mathsf {ACA}_0$
. And since
$\mathsf {PA}$
is precisely the set of first-order consequences of
$\mathsf {ACA}_0$
, the produced order
$\mathcal {L}$
is
$\mathsf {PA}$
-verifiable.
2.2 Transfinite induction
The statement that a linear order
$\mathcal {L}$
is well-ordered is clearly second-order and thus not expressible in
$\mathsf {PA}$
. However, as we will see, it is closely related to the transfinite induction scheme for
$\mathcal {L}$
.
For
$\mathcal {L}$
a
$\mathsf {PA}$
-verifiable linear order,
$\mathsf {TI}(\mathcal {L})$
, the transfinite induction scheme for
$\mathcal {L}$
consists of the formulas
$$\begin{align*}(\forall x\in \mathcal{L})((\forall y\prec^{\mathcal{L}} x)\varphi(y)\to \varphi(x))\to (\forall x\in \mathcal{L})\; \varphi(x),\end{align*}$$
where
$\varphi $
ranges over arbitrary arithmetical formulas that could contain other free variables.
Lemma 4. Suppose
$\mathcal {L}$
is a
$\mathsf {PA}$
-verifiable computable linear order. Then the theory
$\mathsf {ACA}_0+\mathsf {WO}(\mathcal {L})$
is a conservative extension of
$\mathsf {PA}+\mathsf {TI}(\mathcal {L})$
.
Proof Obviously,
$\mathsf {ACA}_0+\mathsf {WO}(\mathcal {L})\supseteq \mathsf {PA}+\mathsf {TI}(\mathcal {L})$
. Now let us show that every first-order consequence of
$\mathsf {ACA}_0+\mathsf {WO}(\mathcal {L})$
is provable in
$\mathsf {PA}+\mathsf {TI}(\mathcal {L})$
. In order to do this we will show that any model
$\mathfrak {A}$
of
$\mathsf {PA}+\mathsf {TI}(\mathcal {L})$
can be extended to a model of
$\mathsf {ACA}_0+\mathsf {WO}(\mathcal {L})$
. Indeed, we extend
$\mathfrak {A}$
to a model of the language of second-order arithmetic by all the subsets
$A\subseteq \mathfrak {A}$
that are definable in
$\mathfrak {A}$
by an arithmetical formula with parameters from
$\mathfrak {A}$
.
Let X be in the second-order part of
$\mathfrak {A}$
such that
$\varphi (x)$
defines X. Then, since
$\mathfrak {A}$
satisfies induction for
$\varphi (x)$
, it also satisfies induction for X and since X was arbitrary, it satisfies set induction. If
$\varphi $
is an arithmetical formula with parameters
$Y_1,\dots Y_n$
from
$\mathfrak {A}$
, then let
$\theta _i$
be the arithmetical first-order formulas defining
$Y_i$
and
$\psi $
be the formula with every subformula of the form
$t\in Y_i$
replaced by
$\theta _i(t)$
for any term t. Then
$$\begin{align*}\mathfrak A\models \forall x (\psi(x) \leftrightarrow \varphi(x))\end{align*}$$
and thus
$\mathfrak A$
satisfies arithmetical comprehension for
$\varphi $
.
It remains to show that
$\mathfrak {A}$
satisfies
$\mathsf {WO}(\mathcal {L})$
. As
$\mathfrak {A}$
satisfies transfinite induction over
$\mathcal {L}$
for arbitrary
$\varphi (x)$
with side parameters, it satisfies the second-order principle
$$\begin{align*}\forall X\big ((\forall x\in \mathcal{L})((\forall y\prec^{\mathcal{L}} x)y\in X\to x\in X)\to (\forall x\in \mathcal{L})\; x\in X\big).\end{align*}$$
Which is clearly equivalent in
$\mathsf {ACA}_0$
to the well-foundedness of
$\mathcal {L}$
:
$$\begin{align*}\forall X \big(\exists x (x\in X\cap \mathcal{L}) \to (\exists x\in X\cap \mathcal{L})(\forall y\in X\cap \mathcal{L}) (x\preceq^{\mathcal{L}} y)\big).\end{align*}$$
Given that we assume
$\mathcal {L}$
to be
$\mathsf {PA}$
-verifiable computable linear order, we conclude that we have
$\mathfrak {A}\models \mathsf {ACA}_0+\mathsf {WO}(\mathcal {L})$
.
2.3 Uniform reflection and its iterations
For an arithmetical c.e. axiomatizable theory T represented by a
$\Sigma _1$
-formula
$\mathsf {Ax}_T(x)$
expressing that x is a Gödel number of an axiom of T, we have the natural arithmetized provability predicate
$\mathsf {Prv}_T(x)$
. To be precise, the formula
$\mathsf {Prv}_T(x)$
expresses that x is a Gödel number of an arithmetical sentence and there exists a proof in first-order logic of x from some premises y all of which satisfy
$\mathsf {Ax}_T(y)$
.
Full uniform reflection
$\mathsf {RFN}(T)$
for a c.e. axiomatizable theory T as above is the scheme
To simplify our notations we will consider
$\mathsf {RFN}(T)$
to be the extension of T by the schemata above.
For a
$\mathsf {PA}$
-verifiable computable linear order
$\mathcal {L}$
we define the uniformly c.e. axiomatizable family of theories
$(\mathsf {RFN}^{(\mathcal {L},a)}(T))_{a\in \mathcal {L}}$
as
$$\begin{align*}\mathsf{RFN}^{(\mathcal{L}, a)}(T)=T+\bigcup\limits_{b\prec^{\mathcal{L}} a}\mathsf{RFN}(\mathsf{RFN}^{(\mathcal{L}, b)}(T)).\end{align*}$$
Notice that
$\mathsf {RFN}(\mathsf {RFN}^{(\mathcal {L}, b)}(T))$
as a set of theorems might depend on the choice of
$\Sigma _1$
-formula recognizing axioms of
$\mathsf {RFN}^{(\mathcal {L}, b)}(T)$
. Thus, in order to make the definition above formally correct, we, in fact, need to produce a family of formulas defining axioms of theories
$\mathsf {RFN}^{(\mathcal {L}, a)}(T)$
.
We are going to define a
$\Sigma _1$
-formula
$\mathsf {Ax}_T^{\mathcal {L}}(x,y)$
with the intention that when we substitute a numeral
$\underline {a}$
of a instead of x, then the resulting
$\Sigma _1$
-formula
$\mathsf {Ax}_T^{\mathcal {L}}(\underline {a},y)$
should be the formula recognizing the axioms of
$\mathsf {RFN}^{(\mathcal {L}, a)}(T)$
. We construct
$\mathsf {Ax}_T^{\mathcal {L}}(x,y)$
by Gödel’s diagonal lemma so that
$\mathsf {Ax}_T^{\mathcal {L}}(x,y)$
is equivalent to the conjunction of the following conditions:
-
(1)
$x\in \mathcal {L}$
, -
(2) y is an axiom of T or for some
$z\prec ^{\mathcal {L}} x$
, y is an instance of the uniform reflection scheme
$\mathsf {RFN}(\mathsf {RFN}^{(\mathcal {L},z)}(T))$
.
Notice that the instance of
$\mathsf {RFN}(\mathsf {RFN}^{(\mathcal {L},z)}(T))$
formulated as in Eq. (1) employs
$\mathsf {Prv}_{\mathsf {RFN}^{(\mathcal {L},z)}(T)}(x)$
as a subformula, which in turn is fully determined by the formula
$\mathsf {Ax}_{\mathsf {RFN}^{(\mathcal {L},z)}(T)}(x)$
. For the purpose of the fixed point definition of
$\mathsf {Ax}_T^{\mathcal {L}}(x,y)$
, this instance of
$\mathsf {Ax}_{\mathsf {RFN}^{(\mathcal {L},z)}(T)}(x)$
is
$\mathsf {Ax}_{T}^{\mathcal {L}}(\underline z,x)$
. That is, above we define
$\mathsf {Ax}_T^{\mathcal {L}}(x,y)$
in terms of its own Gödel number. Since the conjunction of the items (1) and (2) is clearly
$\Sigma _1$
, the standard proof of the diagonal lemma will produce in this case a
$\Sigma _1$
-formula
$\mathsf {Ax}_T^{\mathcal {L}}(x,y)$
.
Finally, we put
$$\begin{align*}\mathsf{RFN}^{\mathcal{L}}(T)=T+\bigcup\limits_{a\in \mathcal{L}} \mathsf{RFN}(\mathsf{RFN}^{(\mathcal{L},a)}(T)). \end{align*}$$
Lemma 5. For any
$\mathsf {PA}$
-verifiable computable order
$\mathcal {L}$
and
$a,b\in L$
with
$b\prec ^{\mathcal {L}}$
a, the theory
$\mathsf {RFN}^{(\mathcal {L},a)}(\mathsf {PA})$
proves all instances of
$\mathsf {TI}(\mathcal {L}\upharpoonright b)$
.
Proof Recall that Löb’s theorem [Reference Löb10] (in the case of
$\mathsf {PA}$
) states that if for some arithmetical sentence
$\theta $
we have 
, then
$\mathsf {PA}\vdash \theta $
. Note that Löb’s theorem could, in fact, be considered just as a reformulation of the Gödel’s second incompleteness theorem for the theory
$\mathsf {PA}+\lnot \theta $
.
We will pick as the sentence
$\theta $
the natural formalization of the statement of Lemma 5 in the language of arithmetic. In the rest of the proof we reason in
$\mathsf {PA}$
(i.e., by finitistic means) to prove that
$\mathsf {Prv}_{\mathsf {PA}}(\theta )$
implies
$\theta $
, which by Löb’s theorem will imply that
$\theta $
is provable in
$\mathsf {PA}$
and hence by soundness of
$\mathsf {PA}$
we will conclude that
$\theta $
is true which is precisely what we needed to show.
We suppose that we have a proof p of
$\theta $
, a
$\mathsf {PA}$
-verifiable computable order
$\mathcal {L}$
and an element
$a\in \mathcal {L}$
. Our goal is to produce a proof in
$\mathsf {RFN}^{(\mathcal {L},a)}(\mathsf {PA})$
of an instance
$$ \begin{align} (\forall x\prec^{\mathcal{L}} b)((\forall y\prec^{\mathcal{L}} x)\varphi(y)\to \varphi(x))\to (\forall x\prec^{\mathcal{L}} b)\; \varphi(x), \end{align} $$
of transfinite induction
$\mathsf {TI}(\mathcal {L}\upharpoonright b)$
.
Note that the fact that
$\mathcal {L}$
is a
$\mathsf {PA}$
-verifiable linear order implies that
$\mathsf {PA}$
proves that
$\mathcal {L}$
is a
$\mathsf {PA}$
-verifiable linear order. Therefore, since
$\theta $
is provable in
$\mathsf {PA}$
, it is provable in
$\mathsf {PA}$
that,
Henceforth, since
$\mathsf {RFN}^{(\mathcal {L},a)}(\mathsf {PA})$
contains
$\mathsf {RFN}(\mathsf {RFN}^{(\mathcal {L},b)}(\mathsf {PA}))$
we conclude that
$\mathsf {RFN}^{(\mathcal {L},a)}(\mathsf {PA})$
proves
$$ \begin{align} \forall c\prec^{\mathcal{L}} b\big((\forall x\prec^{\mathcal{L}} c)((\forall y\prec^{\mathcal{L}} x)\varphi(y)\to \varphi(x))\to (\forall x\prec^{\mathcal{L}} c)\; \varphi(x)\big). \end{align} $$
Obviously (3) implies (2) even over
$\mathsf {PA}$
, which concludes the proof of our claim and hence the lemma.
Theorem 6 (Feferman’s completeness theorem).
For every true arithmetical sentence
$\varphi $
there exists a well-founded
$\mathsf {PA}$
-verifiable linear order
$\mathcal {L}$
such that
$$\begin{align*}\mathsf{RFN}^{\mathcal{L}}(\mathsf{PA})\vdash \varphi.\end{align*}$$
Proof By Lemma 3 we could pick a
$\mathsf {PA}$
-verifiable computable well-order
$\mathcal {L}_1$
such that
$$\begin{align*}\mathsf{ACA}_0\vdash \varphi\mathrel{\leftrightarrow} \mathsf{WO}(\mathcal{L}_1).\end{align*}$$
By Lemma 4,
$$\begin{align*}\mathsf{PA}+\mathsf{TI}(\mathcal{L}_1)\vdash \varphi.\end{align*}$$
And for the order
$\mathcal {L}$
that is obtained from
$\mathcal {L}_1$
by adding one element a on the very top, by Lemma 5 we get
$$\begin{align*}\mathsf{RFN}(\mathsf{RFN}^{(\mathcal{L},a)}(\mathsf{PA}))\vdash \varphi\end{align*}$$
and hence
$$\begin{align*}\mathsf{RFN}^{\mathcal{L}}(\mathsf{PA})\vdash \varphi.\end{align*}$$
3 Feferman’s completeness theorem via deduction chains
One might wonder whether Feferman could have used a different and technically more transparent approach other than his intricate applications of the recursion theorem. Indeed, the idea we are putting forward here is that two results available at the time could have led to such a proof. The first result, perhaps unsurprisingly, is Löb’s theorem from 1955 [Reference Löb10] while the second is Schütte’s 1956 completeness theorem [Reference Schütte14, Satz 6] for
$\omega $
-logic, which showed that a canonical primitive recursive proof tree (indeed a Kalmár-elementary tree) can be associated with every true arithmetic statement, entailing that
$\omega $
-logic with the primitive recursive
$\omega $
-rule (indeed Kalmár-elementary
$\omega $
-rule) is already complete.Footnote
2
Löb’s theorem, of course, was well known at the time, but even today it remains largely unknown that Schütte was the first mathematician who showed the primitive recursive completeness of
$\omega $
-logicFootnote
3
and introduced canonical search trees.
Definition 7 (The Tait calculus for
$\omega $
-logic).
For classical logic, the so-called Tait calculus is very convenient (see [Reference Tait and Barwise21] and [Reference Schwichtenberg15]). In it, one deduces finite sequences of formulas, called sequents. Sequents are referred to by capital Greek letters
$\Delta ,\Gamma ,\Lambda ,\Xi ,\ldots $
. The result of appending a formula
$\theta $
to a sequent
$\Gamma $
is written
$\Gamma ,\theta $
. Formulas are assumed to be in negation normal form, i.e., negations appear only in front of atomic formulas, whereas negation of more complex formulas is a defined operation, using De Morgan’s laws and dropping double negations. The other logical particles are
$\wedge ,\vee ,\exists ,\forall $
. Literals are either atomic formulas or negated atomic formulas. Working in
$\omega $
-logic means that we can assume that formulas have no free variables. Below we are only concerned with
$\omega $
-logic based on the language of
$\mathsf {PA}$
. As a result, all literals are either true or false, and this can be checked by a primitive recursive algorithm. The axioms of the infinitary calculus are those sequents that contain a true literal. The rules are the usual ones for deducing a conjunction, disjunction, or existential formula, plus the
$\omega $
-rule (for details see [Reference Schwichtenberg15]).
Definition 8. For any non-literal
$\psi $
, a
$\psi $
-deduction chain is a finite string
$$\begin{align*}\Gamma_0,\Gamma_1,\ldots,\Gamma_k\end{align*}$$
of sequents
$\Gamma _i$
constructed according to the following rules:
-
(i)
$\Gamma _0\; = \; \psi $
. -
(ii)
$\Gamma _i$
is not axiomatic for
$i<k$
. -
(iii) If
$i<k$
, then
$\Gamma _i$
is of the form where
$$\begin{align*}\Gamma_i^{\prime},\chi,\Gamma_i^{\prime\prime}\end{align*}$$
$\chi $
is not a literal and
$\Gamma _i^{\prime }$
contains only literals.
$\chi $
is said to be the redex of
$\Gamma _i$
.
Let
$i<k$
and
$\Gamma _i$
be reducible.
$\Gamma _{i+1}$
is obtained from
$\Gamma _i=\Gamma _i^{\prime },\chi ,\Gamma _i^{\prime \prime }$
as follows:
-
(1) If
$\chi \equiv \chi _0\vee \chi _1$
then
$$\begin{align*}\Gamma_{i+1}\;=\; \Gamma_i^{\prime},\chi_0,\chi_1,\Gamma_i^{\prime\prime}.\end{align*}$$
-
(2) If
$\chi \equiv \chi _0\wedge \chi _1 $
then where
$$\begin{align*}\Gamma_{i+1}\;=\; \Gamma_i^{\prime},\chi_j,\Gamma_i^{\prime\prime}\end{align*}$$
$j=0$
or
$j=1$
.
-
(3) If
$\chi \equiv \exists x\,\theta (x)$
then where m is the first number such that
$$\begin{align*}\Gamma_{i+1}\;=\; \Gamma_i^{\prime},\theta(\underline{m}),\Gamma_i^{\prime\prime},\chi\end{align*}$$
$\theta (\underline {m})$
does not occur in
$\Gamma _0,\ldots ,\Gamma _i$
.
-
(4) If
$\chi \equiv \forall x\,\theta (x)$
then for some m.
$$\begin{align*}\Gamma_{i+1}\;=\; \Gamma_i^{\prime},\theta(\underline{m}),\Gamma_i^{\prime\prime}\end{align*}$$
The set of
$\psi $
-deduction chains forms a tree, the Stammbaum
${\mathbb B}_{\psi }$
, labeled with strings of sequents.Footnote
4
We will now consider two possible outcomes.
-
• Case I:
${\mathbb B}_{\psi }$
is well-founded. Then
${\mathbb B}_{\psi }$
yields an elementary recursive
$\omega $
-proof of
$\psi $
. So
$\psi $
is true. -
• Case II:
${\mathbb B}_{\psi }$
is not well-founded. Then one shows that
$\psi $
is false by verifying that an infinite path through this tree contains only false formulas. In more detail, one shows that every formula
$\theta $
occurring on this infinite path is false. The proof proceeds by induction on the syntactic complexity of
$\theta $
, i.e., the length of
$\theta $
as a string of symbols. More details can be found in the proof in [Reference Schütte14] and in [Reference Schwichtenberg15, p. 29], where this is called the Principal semantic lemma.
Kleene’s normal form theorem for arithmetic formulas (Lemma 3) also assigns a linear computable ordering
$\prec _\varphi $
to every sentence
$\varphi $
such that the truth of
$\varphi $
is equivalent to
$\prec _\varphi $
being a wellordering. This result is obtained by a series of syntactic transformations performed on
$\varphi $
, and it seems that it doesn’t yield any new insights as to the truth of
$\varphi $
. Schütte’s completeness theorem, however, associates with
$\varphi $
an ordering coming from a search tree for
$\varphi $
in
$\omega $
-logic and it seems that this result is the more important one.
Definition 9 (Reflexive induction).
There is an immediate consequence of Löb’s theorem, christened reflexive induction. It was singled out by Girard and Schmerl (see [Reference Schmerl16, p. 337]). Here we will use a slight variant due to Beklemishev [Reference Beklemishev, Sommaruga and Strahm5].
A formula
$\theta (u)$
is said to be
$\prec $
-reflexively progressive with respect to T if
$$\begin{align*}T\vdash \forall x[\mathrm{Prv}_{T}(\ulcorner \forall y\prec \dot{x}\,\theta(y)\urcorner)\to \theta(x)]. \end{align*}$$
Lemma 10. If
$\theta (u)$
is
$\prec $
-reflexively progressive with respect to T, then
$$\begin{align*}T\vdash \forall x\,\theta(x).\end{align*}$$
Proof By Löb’s theorem it suffices to show
$$ \begin{align} T\vdash \mathrm{Prv}_{T}(\ulcorner \forall x\,\theta(x)\urcorner)\to \forall x\,\theta(x). \end{align} $$
Reasoning in T, assume
$\mathrm {Prv}_{T}(\ulcorner \forall x\,\theta (x)\urcorner )$
. Then also
$ \forall x[\mathrm {Prv}_{T}(\ulcorner \forall y\prec \dot {x}\,\theta (y)\urcorner )$
, whence, by
$\prec $
-reflexive progressiveness,
$\forall x\,\theta (x)$
, ascertaining (4).
Theorem 11. Let
$\psi $
be an arithmetic sentence and
$\mathcal {L}$
be the Kleene–Brouwer ordering on
$\mathbb {B}_{\psi }$
. Then, for any node
$\sigma \in \mathbb {B}_\psi $
,
$$ \begin{align} \mathsf{RFN}(\mathsf{RFN}^{(\mathcal{L},\sigma)}(\mathsf{PA})) \vdash \Gamma_\sigma, \end{align} $$
where
$\Gamma _\sigma $
is the sequent in the node
$\sigma $
. And in particular for the root node
$\langle \rangle $
:
$$ \begin{align} \mathsf{RFN}(\mathsf{RFN}^{(\mathcal{L},\langle\rangle)}(\mathsf{PA})) \vdash \psi. \end{align} $$
Proof We will prove the
$\mathcal {L}$
-reflexive progressivity of (5), which implies that (5) is provable in
$\mathsf {PA}$
and hence true. For this, we reason in a
$\mathsf {PA}$
-formalizable manner.
Suppose that it is
$\mathsf {PA}$
-provable that for all
$\tau \prec ^{\mathcal {L}}\sigma $
we have
$$ \begin{align} \mathsf{RFN}(\mathsf{RFN}^{(\mathcal{L},\tau)}(\mathsf{PA}))\vdash \Gamma_{\tau}. \end{align} $$
Our goal is to prove (5). The form of
$\Gamma _\sigma $
can be effectively determined. The most interesting case is the one where
$\Gamma _\sigma $
is of the form
$$\begin{align*}\Gamma^{1}_\sigma,\forall x\theta(x),\Gamma^{2}_\sigma \end{align*}$$
with redex
$\forall x\theta (x)$
. Then there are effectively determinable
$\sigma _n\prec ^{\mathcal {L}} \sigma $
such that
$\Gamma _{\sigma _n}$
is of the form
$$\begin{align*}\Gamma^{1}_\sigma,\theta(\underline{n}),\Gamma^{2}_\sigma,\end{align*}$$
and from (7) it follows that it is
$\mathsf {PA}$
-provable that
$$ \begin{align} \forall n\;\big(\mathsf{RFN}(\mathsf{RFN}^{(\mathcal{L},\sigma_x)}(\mathsf{PA}))\vdash \Gamma^{1}_\sigma,\theta(\underline{n}),\Gamma^{2}_\sigma\big). \end{align} $$
And since it is
$\mathsf {PA}$
-provable that all
$\sigma _n$
are smaller than
$\sigma $
, we conclude that
$\mathsf {PA}$
-provably we have
$$ \begin{align} \forall n\;\big(\mathsf{RFN}^{(\mathcal{L},\sigma)}(\mathsf{PA})\vdash \Gamma^{1}_\sigma,\theta(\underline{n}),\Gamma^{2}_\sigma\big). \end{align} $$
Thus, applying reflection for
$\mathsf {RFN}^{(\mathcal {L},\sigma )}(\mathsf {PA})$
to (9) we conclude that we have
$$ \begin{align} \mathsf{RFN}(\mathsf{RFN}^{(\mathcal{L},\sigma)}(\mathsf{PA}))\vdash \forall y \big(\bigvee \Gamma^{1}_\sigma\lor \theta(y)\lor \bigvee\Gamma^{2}_\sigma\big), \end{align} $$
for a fresh new variable y. Given that y is not free in either
$\Gamma ^1_\sigma $
or in
$\Gamma ^2_\sigma $
, we get
$$ \begin{align} \mathsf{RFN}(\mathsf{RFN}^{(\mathcal{L},\sigma)}(\mathsf{PA}))\vdash \Gamma_\sigma. \end{align} $$
3.1 Upper bounds on the size of the Stammbaum
One can show that the ordinal height of the Stammbaum
${\mathbb B}_{\psi }$
of a true sentence
$\psi $
is less than
$\omega ^2$
. More precisely, if the syntactic buildup of C from literals takes k steps, then the height of
${\mathbb B}_{\psi }$
is strictly less than
$\omega \cdot (k+1)$
. This follows by induction on k, by showing the more general result that any sequent containing a true formula of complexity k has a Stammbaum of height strictly less than
$\omega \cdot (k+1)$
.
As a result of the foregoing, we then get that the Kleene–Brouwer ordering
$\prec $
of
${\mathbb B}_{\psi }$
has an order-type strictly less than
$\omega ^{\omega \cdot (k+1)}$
, and thus strictly less than
$\omega ^{\omega ^2}$
. Later in this paper we shall improve this bound by developing progressions of theories staying below
$\omega ^{\omega }$
.
4 A theorem of Ash and Knight in
$\mathsf {ACA_0}$
The goal of this section is to prove a version of a theorem of Ash and Knight [Reference Ash and Knight2, Example 3] from computable structure theory in
$\mathsf {ACA_0}$
. In its original formulation, this theorem connects membership in hyperarithmetical sets to the well-orderedness of certain linear orders.
We are now ready to state the version of Ash and Knight’s theorem we have in mind. In the statement of this theorem and what follows
$\eta $
denotes the order-type of the standard ordering on
$\mathbb Q$
.
Theorem 12. Let
$n\in \omega $
. Then for every
$\Pi _{2n+1}$
formula
$\varphi (x)$
there is a uniformly computable sequence of linear orders
$(\mathcal {L}_i)_{i\in \omega }$
such that
$\mathsf {ACA}_0$
proves that for any i
$$\begin{align*}\mathcal{L}_i \cong \begin{cases} \omega^n & \text{ if }\varphi(i)\\ \omega^n(1+\eta) &\text{ if } \lnot\varphi(i). \end{cases}\end{align*}$$
In order to prove Theorem 12 we will need a few more lemmas. The first is the relativized version of Shoenfield’s classical limit lemma. See [Reference Soare19] for the classical proof of this result and more background on computability theory.
Also to prove Theorem 12 we will need the notions of
$\Delta ^0_n(X)$
linear orders. Our definitions follow Simpson [Reference Simpson18] and can be done in
$\mathsf {ACA}_0$
.
In order to define relative computability, fix for each
$n\in \omega $
a universal
$\Pi ^0_n$
formula
$\pi _n(e,x,X)$
with free number variables e and x, and a free set variable X. Here
$\Pi ^0_n$
universality should be
$\mathsf {ACA}_0$
-verifiable, i.e., for any
$\Pi ^0_n$
formula
$\varphi (e,x,X)$
we should have
$$\begin{align*}\mathsf{ACA}_0\vdash \forall e\exists e'\forall x \forall X (\varphi(e,x,X)\leftrightarrow \pi_n(e',x,X)).\end{align*}$$
This allows us to define some standard notions within
$\mathsf {ACA}_0$
. We say that a set Y is
$\Pi ^0_n(X)$
if there exists e such that
$x\in Y \leftrightarrow \pi _n(e,x,X)$
. We say that a set Y is
$\Sigma ^0_n(X)$
if its complement
$\mathbb {N}\setminus Y$
is
$\Pi ^0_n(X)$
. We say that a set is
$\Delta ^0_n(X)$
if it is simultaneously
$\Pi ^0_n(X)$
and
$\Sigma ^0_n(X)$
. A set Y is X-computable if it is
$\Delta ^0_1(X)$
. A set Y is computable if it is
$\emptyset $
-computable.
A linear order
$\mathcal {L}=(L,\preceq ^{\mathcal {L}})$
is
$\Delta ^0_n(X)$
if
$\preceq ^{\mathcal {L}}$
is
$\Delta ^0_n(X)$
. Notice that this implies that the universe L is also
$\Delta ^0_n(X)$
, since by reflexivity
$x\in L$
iff
$x\preceq ^{\mathcal {L}} x$
. If
$\mathcal {L}$
is
$\Delta ^0_1(X)$
, then we say that
$\mathcal {L}$
is X-computable. We will denote linear orders by calligraphic letters and their universes L by the corresponding capital letters. A sequence
$(\mathcal {A}_i)_{i\in \omega }$
of linear orders is uniformly
$\Delta ^0_n(X)$
if there is a
$\Delta ^0_n(X)$
set S such that its
$i^{\text {th}}$
column is equal to
$\preceq ^{\mathcal {A}_i}$
, i.e.,
$$\begin{align*}S^{[i]}=\{x: \langle i,x\rangle\in S\}=\preceq^{\mathcal{A}_i}. \end{align*}$$
As usual, a sequence of linear orders is uniformly X-computable if it is uniformly
$\Delta ^0_1(X)$
.
In a standard manner, using Ackermann membership, we encode finite sets of naturals by natural numbers, i.e., the elements of a number A with the binary expansion
$a_{n-1}\ldots a_0$
are all
$i<n$
such that
$a_i=1$
. Let
$(A_i)_{i\in \omega }$
be a sequence of finite sets of naturals. We say that a set X is the limit of
$(A_i)_{i\in \omega }$
and write
$X=\lim A_i$
if
$$\begin{align*}\begin{array}{lcl} x\in X & \text{iff } & \exists i (\forall j>i) x\in A_j,\\ x\not\in X & \text{iff } & \exists i(\forall j>i) x\not\in A_j. \end{array} \end{align*}$$
Lemma 13 (
$\mathsf {ACA}_0$
; Limit lemma).
Fix a set X. A set Y is
$\Delta ^0_2(X)$
if and only if there is an X-computable sequence of finite sets
$(A_i)_{i\in \omega }$
such that
$Y=\lim A_i$
.
Proof
$(\Rightarrow )$
. As Y is
$\Delta ^0_2(X)$
there are
$e_0$
,
$e_1$
such that
$$ \begin{align*} y\in Y &\leftrightarrow \pi_2(e_0,y,X)\leftrightarrow \exists u\forall v R(e_0, y,u,v,X)\\ y\not\in Y &\leftrightarrow \pi_2(e_1,y,X)\leftrightarrow \exists u\forall v R(e_1,y,u,v,X) \end{align*} $$
for some formula R containing only bounded quantifiers. First, for fixed i, define sets
$B_i$
and
$C_i$
as follows.
$$ \begin{align*} y\in B_i &\leftrightarrow y<i \land (\exists u<i) (\forall v<i) R(e_0,y,u,v,X)\\ y\in C_i &\leftrightarrow y<i \land (\exists u<i) (\forall v<i) R(e_1,y,u,v,X). \end{align*} $$
The sequences
$(B_i)_{i\in \omega }$
and
$(C_i)_{i\in \omega }$
are clearly X-computable and it is easy to see that
$$ \begin{align*} y\in Y &\leftrightarrow \exists i (\forall j>i) y\in B_i,\\ y\not\in Y &\leftrightarrow \exists i (\forall j>i) y\in C_i. \end{align*} $$
Let
$age_B(i,y)=\min (\{i+1\}\cup \{k\le i: y\not \in B_{i-k}\})$
and
$age_C(i,y)=\min (\{i+1\}\cup \{k\le i\mid y\not \in C_{i-k}\})$
. Clearly both
$age_B$
and
$age_C$
are X-computable functions from
$\mathbb {N}^2$
to
$\mathbb {N}$
. We define
$$\begin{align*}A_i=\{y<i: age_B(i,y)>age_C(i,y)\}.\end{align*}$$
The sequence
$(A_i)_{i\in \omega }$
is clearly uniformly X-computable. To see that Y is its limit notice that if
$y\in Y$
, then there is
$i_0$
such that
$(\forall j>i_0)y\in B_j$
and that for every i with
$y\in C_i$
, there is
$j>i$
such that
$y\not \in C_j$
. Let
$i_1$
be the least such j with
$y\not \in C_j$
greater than
$i_0$
. Then for all
$j>i_1$
,
$age_B(j,y)>age_C(j,y)$
and hence
$y\in A_j$
. That
$y\not \in Y$
if there is i such that for all
$j>i$
$y\not \in A_j$
can be shown in a similar manner.
$(\Leftarrow )$
. Assume
$(A_i)_{i\in \omega }$
is uniformly X-computable and let Y be the limit of
$(A_i)_{i\in \omega }$
. There are
$e_0$
and
$e_1$
such that
$$\begin{align*}x\in A_i \leftrightarrow \pi_1(e_0, \langle i,x\rangle) \quad \text{and} \quad x\not\in A_i \leftrightarrow \pi_1(e_1,\langle i,x\rangle).\end{align*}$$
From this, one can easily extract a pair of
$\Pi ^0_2$
formulas which, given parameter X, define the membership relation of Y, respectively, its negation. Thus Y is
$\Delta ^0_2(X)$
.
From Lemma 13 we will now derive a limit lemma for linear orders.
Definition 14. A sequence
$(\mathcal {A}_i)_{i\in \omega }$
of finite linear orders is locally coherent if
$\preceq ^{\mathcal {A}_i}\upharpoonright (A_i\cap A_{i+1}) =\preceq ^{\mathcal {A}_{i+1}}\upharpoonright (A_i\cap A_{i+1})$
, for each i.
We will be interested in the situation when a linear order
$\mathcal {L}$
is the limit of a locally coherent sequence of finite linear orders
$(\mathcal {A}_i)_{i\in \omega }$
. In this case, we think about
$\mathcal {L}$
as the order obtained by the following procedure. We start with the order
$\mathcal {A}_0$
. At each stage i we switch from
$\mathcal {A}_{i}$
to
$\mathcal {A}_{i+1}$
by removing all the elements
$x\in A_i\setminus A_{i+1}$
and adding all the elements in
$x\in A_{i+1}\setminus A_i$
. The order
$\mathcal {L}$
consists of all the elements x that are present in some
$\mathcal {A}_i$
and aren’t removed in any
$\mathcal {A}_j$
, for
$j>i$
. Whether
$x\preceq ^{\mathcal {L}} y$
can be checked in any
$\mathcal {A}_{i}$
such that both
$x,y$
aren’t removed at any stage
$\ge i$
.
We say that S is a partial successor relation on a linear order
$\mathcal {L}$
if
-
(1)
$\langle x,y\rangle \in S\Rightarrow x\prec ^{\mathcal {L}}y$
, -
(2)
$\langle x,y\rangle \in S\Rightarrow (\forall z\in L) (z\preceq ^{\mathcal {L}} x\lor y\preceq ^{\mathcal {L}} z)$
.
A total successor relation, or just successor relation, is a partial successor relation satisfying (2) with the implication replaced by equivalence. A finite linear order with a partial successor relation
$\mathcal {A}$
is a triple
$(A, \preceq ^{\mathcal {A}},S^{\mathcal {A}})$
, where
$\preceq ^{\mathcal {A}}$
is a finite linear order and
$S^{\mathcal {A}}$
is a finite set of pairs that is a partial successor relation on
$\preceq ^{\mathcal {A}}$
. We say that a sequence of finite linear orders with partial successor relations
$(\mathcal {A}_i)_{i\in \omega }$
is locally coherent if
$\preceq ^{\mathcal {A}_i}\upharpoonright (A_i\cap A_{i+1}) =\preceq ^{\mathcal {A}_{i+1}}\upharpoonright (A_i\cap A_{i+1})$
and
$S_i\upharpoonright (A_i\cap A_{i+1}) \subseteq S_{i+1}\upharpoonright (A_i\cap A_{i+1})$
. As for sequences of finite linear orders we will be interested in the situation when a linear order with the total successor relation
$\mathcal {L}=\langle \preceq ^{\mathcal {L}},S^{\mathcal {L}}\rangle $
is the limit of a locally coherent sequence of finite linear orders with partial successor relations
$(\mathcal {A}_i)_{i\in \omega }$
.
Note that for a linear order without successor relation
$\mathcal {L}=\lim \mathcal {A}_i$
and successive
$x,y\in \mathcal {L}$
, new elements z might appear and disappear between x and y inside
$\mathcal {A}_i$
’s for indefinitely large i. However, for a linear order with successor relation
$\mathcal {L}=\lim \mathcal {A}_i$
and neighboring elements
$x,y\in \mathcal {L}$
, for large enough stages (after the point when both x and y will no longer be removed) we can guarantee that no more new elements will appear in
$\mathcal {A}_i$
’s between x and y.
Using this definition, we get the following corollary of Lemma 13.
Corollary 15 (
$\mathsf {ACA}_0$
).
Fix a set X. A linear order
$\mathcal {L}$
is
$\Delta ^0_2(X)$
if and only if there is an X-computable locally coherent sequence
$(\mathcal {A}_i)_{i\in \omega }$
of finite linear orders with limit
$\mathcal {L}$
, i.e.,
$$ \begin{align*}x\in L &\leftrightarrow \exists i(\forall j>i)\ x\in A_j\\ x\not\in L &\leftrightarrow \exists i (\forall j>i)\ x\not\in A_j\\ x\preceq^{\mathcal{L}} y &\leftrightarrow \exists i (\forall j>i)\ x\preceq^{\mathcal{A}_j} y.\end{align*} $$
Proof
$(\Rightarrow )$
. From Lemma 13 we get a sequence
$(B_i)_{i\in \omega }$
of finite sets with limit
$\preceq ^{\mathcal {L}}$
. We may assume that no
$B_i$
contains elements greater than i. We define a locally coherent sequence
$(\mathcal {A}_i)_{i\in \omega }$
as follows. Let
$\mathcal {A}_0$
be the empty order. Assume we have defined
$\mathcal {A}_i$
. To define
$\mathcal {A}_{i+1}$
first let k be the maximal size of subsets of
$\{ x: \langle x,x\rangle \in B_{i+1}\}$
linearly ordered by
$B_{i+1}$
and among the subsets of size k let
$C_{i+1}$
be the one containing the smallest natural number. Then let
$$\begin{align*}A_{i+1}= C_{i+1} \text{ and } \preceq^{\mathcal{A}_{i+1}}=B_{i+1}\operatorname{\mathrm{\upharpoonright}} A_{i+1}.\end{align*}$$
This sequence is clearly uniformly X-computable. To see that it has limit
$\mathcal {L}$
, first consider
$x,y\in L$
such that
$x\preceq ^{\mathcal {L}} y$
. There exists i such that for all
$j>i$
and
$z,w\le \max (x,y)$
we have
$\langle z,w\rangle \in B_j\iff z\preceq ^{\mathcal {L}} w$
. By definition, we then have that
$x\preceq ^{\mathcal {A}_{j}} y$
. On the other hand, suppose that
$x\not \in L$
, then there is i such that for all
$j>i$
,
$\langle x,x\rangle \not \in B_i$
. So for all
$j>i$
,
$x\not \in A_j$
.
$(\Leftarrow )$
. A locally coherent sequence of finite linear orders
$(\mathcal {A}_i)_{i\in \omega }$
is a special case of a sequence of finite sets. Thus this implication is a direct consequence of Lemma 13.
Using the same ideas as in its proof, we can extend Corollary 15 to work for locally coherent sequences of finite linear orders with partial successor relations.
Corollary 16 (
$\mathsf {ACA}_0$
).
Fix a set X. A linear order
$\mathcal {L}$
with successor relation
$S^{\mathcal {L}}$
is
$\Delta ^0_2(X)$
if and only if there is an X-computable locally coherent sequence
$(\mathcal {A}_i)_{i\in \omega }$
of finite linear orders with successor relation with limit
$\mathcal {L}$
.
We are now ready to prove two lemmas crucial for our proof of Theorem 12. They give a sufficient condition for the existence of computable linear orderings of order-type
$\omega \cdot \mathcal {L}$
for any linear ordering
$\mathcal {L}$
. Variations of these lemmas were first proven by Fellner [Reference Fellner7].
Lemma 17 (
$\mathsf {ACA_0}$
).
Fix X and let
$\mathcal {L}$
be a
$\Delta ^0_2(X)$
linear order with a least element. Then there is an X-computable linear order of order-type
$\omega \cdot \mathcal {L}$
with an X-computable successor relation and
$0$
as its least element.Footnote
5
Proof Assume without loss of generality that
$0$
is the least element in
$\mathcal {L}$
. As
$\mathcal {L}$
is
$\Delta ^0_2(X)$
, by Corollary 15 there is a uniformly X-computable locally coherent sequence
$(\mathcal {A}_i)_{i\in \omega }$
of linear orders with limit
$\mathcal {L}$
. We may furthermore assume that
$\mathcal {A}_i$
does not contain elements greater than i and that each
$\mathcal {A}_i$
has the correct information about
$0$
.
We define
$\mathcal {L}'$
of order-type
$\omega \cdot \mathcal {L}$
as the union
$\bigcup _{s\in \mathbb {N}} \mathcal {L}_s^{\prime }$
of an X-computable sequence of finite linear orders
$\mathcal {L}_0'\subseteq \mathcal {L}_1^{\prime }\subseteq \ldots $
where
$\mathcal {L}_i^{\prime }$
has partial successor relation
$S_i$
. Together with
$\mathcal {L}_s^{\prime }$
we define an X-computable sequence of order-preserving surjections
$f_s\colon \mathcal {L}_s^{\prime }\to \mathcal {A}_s$
with the goal that
$f=\lim f_s: \mathcal {L}' \to \mathcal {L}$
is a surjective order-preserving function labeling the “
$\omega $
-blocks” of
$\mathcal {L}'$
with elements of
$\mathcal {L}$
.
We put
$\mathcal {L}_0'= \mathcal {A}_0$
and let
$f_0$
be the identity function. We will now define
$\mathcal {L}_{s+1}^{\prime }$
and
$S_{s+1}$
as extensions of
$\mathcal {L}_s^{\prime }$
and
$S_s$
, respectively and
$f_{s+1}$
given
$f_s$
as follows. During the construction, we will add fresh elements to
$\mathcal {L}_{s+1}^{\prime }$
where a natural number n is a fresh element if
$n>s+1$
and has not been used in the construction before.
-
(1) If there is a least natural number
$a_0\in A_{s}\setminus A_{s+1}$
, then let
$\mathcal {A}'$
be the suborder of
$\mathcal {A}_{s+1}$
consisting of natural numbers less than
$a_0$
and go to (2). Otherwise, let
$\mathcal {A}'=\mathcal {A}_{s}$
and go directly to (3). -
(2) For all elements
$b\in A_{s}$
such that
$b\geq a_0$
and all
$x\in L_{s}^{\prime }$
with
$f_s(x)=b$
, let
$f_{s+1}(x)$
be the next element to the left of b in
$\mathcal {A}'$
. If there are successive elements
$x,y\in L_{s}^{\prime }$
with
$f_{s+1}(x)=f_{s+1}(y)$
for which
$S_{s}$
is undefined, set
$S_{s+1}(x,y)$
. -
(3) For every
$a\in A'$
, set
$f_{s+1}(a)=f_s(a)$
and for each element
$a\in A_{s+1}\setminus A'$
we add to
$\mathcal {L}_{s+1}^{\prime }$
a fresh element
$x_a$
such that
$f_{s+1}(x_a)=a$
. We compare
$x_a$
with other elements
$y\in \mathcal {L}_{s+1}^{\prime }$
as follows:
$x_a\preceq ^{\mathcal {L}^{\prime }_{s+1}}y$
iff
$a\preceq ^{\mathcal {A}_{s+1}}f_{s+1}(y)$
. -
(4) At last, grow every labeled block by an element to the right. I.e., for every
$a \in L_{s+1}^{\prime }$
such that for all
$b\succeq ^{\mathcal {L}_{s+1}^{\prime }} a$
,
$f_{s+1}(b)\neq f_{s+1}(a)$
, add a fresh element
$x_a$
, set
$f_{s+1}(x_a)=f_{s+1}(a)$
,
$S_{s+1}(a,x_a)$
and define
$\preceq ^{\mathcal {L}_{s+1}^{\prime }}$
accordingly.
This finishes the constructions of
$\mathcal {L}_{s+1}^{\prime }$
,
$S_{s+1}$
and
$f_{s+1}$
. Let
$\mathcal {L}'=\bigcup _{s\in \omega } \mathcal {L}_s^{\prime }$
,
$f=\lim f_{s}$
and
$S=\bigcup _{s\in \omega } S_s$
.
Verification: First, note that
$\mathcal {L}'$
is computable. For any two elements
$x,y\in L'$
with
$m=\max \{x,y\}$
, we have by construction that
$$\begin{align*}x\preceq^{\mathcal{L}'}y \iff x\preceq^{\mathcal{L}^{\prime}_m} y.\end{align*}$$
For the successor relation, the same reasoning applies except that at step (2) of the construction, we define the relation between elements added at previous stages. However, note that if at stage
$s+1$
,
$S_{s+1}(x,y)$
is defined by step (2), then the element x must be the rightmost element of its “labeled block” and thus it was added by step (4) at stage s. Hence, for all
$x,y\in L'$
with
$m=\max \{x,y\}$
$$\begin{align*}S(x,y)\iff S_{m+1}(x,y). \end{align*}$$
Next, note that f is well-defined. Whenever
$f_{s+1}(x)\neq f_{s}(x)$
, by construction
$f_{s+1}(x)<f_{s}(x)$
and hence
$f_s(x)$
stabilizes in the limit for any
$x\in L'$
. To see that
$range(f)=L$
, first suppose that
$a\in L$
. By properties of
$(\mathcal {A}_i)_{i\in \omega }$
, there is a least i such that for all
$j>i$
,
$\mathcal {A}_i\operatorname {\mathrm {\upharpoonright }} a=\mathcal {A}_j\operatorname {\mathrm {\upharpoonright }} a$
. By construction
$f_{i+1}(x)=a$
for some
$x\in L_{i+1}$
and
$f_{j}(x)=a$
for all
$j>i+1$
. On the other hand, suppose that
$a\in range(f)\setminus L$
. Then there is i such that for all
$j>i$
,
$\mathcal {A}_i\operatorname {\mathrm {\upharpoonright }} a=\mathcal {A}_j\operatorname {\mathrm {\upharpoonright }} a$
. Thus, for all
$j>i$
,
$a\not \in range(f_{j})$
, a contradiction. That f is order-preserving follows trivially from the construction. It remains to show that the interval of elements labeled with
$a\in L$
is of order-type
$\omega $
. To see this let i be such that there is
$x\in L_i^{\prime }$
with
$f_j(x)=a$
for all
$j>i$
. After stage i, the interval of elements with
$f(x)=a$
will grow to the right by at least one and at most finitely many elements at each stage, but no elements will be added to the left or in between elements in the interval. Thus the order-type of each labeled interval is
$\omega $
. As f is order-preserving and onto
$\mathcal {L}$
, it follows that
$\mathcal {L}'$
has order-type
$\omega \cdot \mathcal {L}$
as required.
Lemma 18 (
$\mathsf {ACA_0}$
).
Fix X and let
$\mathcal {L}$
be a
$\Delta ^0_2(X)$
linear order of order-type
$\omega \cdot \mathcal {K}$
for some linear order
$\mathcal {K}$
. Further, assume that
$\mathcal {L}$
has
$0$
as its least element and that the successor relation in
$\mathcal {L}$
is
$\Delta ^0_2(X)$
. Then there is an X-computable linear order isomorphic to
$\mathcal {L}$
with
$0$
as its least element.
Proof As
$\mathcal {L}$
is
$\Delta ^0_2(X)$
, by Corollary 16 there is a uniformly X-computable locally coherent sequence of finite linear orders
$(\mathcal {A}_i)_{i\in \omega }$
with partial successor relation and
$\mathcal {L}$
as its limit. Furthermore, we can assume without loss of generality that
$0$
is the least element of all
$\mathcal {A}_i$
.
We build an X-computable linear order
$\mathcal {L}'$
isomorphic to
$\mathcal {L}$
as the union of a sequence of extending finite orders
$\mathcal {L}_s^{\prime }$
. As in the proof of Lemma 17 we also define order-preserving surjections
$f_s: \mathcal {L}^{\prime }_s\rightarrow \mathcal {A}_s$
.
We put
$\mathcal {L}_0'=\mathcal {A}_0$
and let
$f_0$
be the identity function. Assume we have defined
$\mathcal {L}_s^{\prime }$
and
$f_s$
. For elements
$x \in \mathcal {L}_{s}^{\prime }$
we put
$$\begin{align*}f_{s+1}(x)=\max_{\preceq^{A_{s}}}\{a\in A_{s+1}\cap A_s\mid a\preceq^{\mathcal{A}_{s}}f_s(x)\}.\end{align*}$$
The additional elements of
$\mathcal {L}_{s+1}^{\prime }$
are
$x_a$
for
$a\in \mathcal {A}_{s+1}$
such that there are no
$y\in \mathcal {L}_s^{\prime }$
with
$f_{s+1}(y)=a$
. We put
$f_{s+1}(x_a)=a$
and insert
$x_a$
in
$\mathcal {L}_{s+1}^{\prime }$
above all y with
$f_{s+1}(y)\prec ^{\mathcal {A}_{s+1}}a$
and below all y with
$f_{s+1}(y)\succ ^{\mathcal {A}_{s+1}}a$
.
This finishes the construction. Let
$\mathcal {L}'=\lim _s \mathcal {L}_s^{\prime }$
.
Verification: Clearly
$\mathcal {L}'$
is X-computable. It remains to show that
$\mathcal {L}'\cong \mathcal {L}$
. First of all notice that the order
$\mathcal {L}'$
splits into the blocks
$B_a$
, for
$a\in \mathcal {L}$
, where
$B_a=\bigcup \limits _{s\ge s_a}f_s^{-1}(a)$
and
$s_a$
is the first stage such that
$a\in \bigcap \limits _{s\ge s_a} A_s$
. In order to finish the proof it is enough to show that all
$B_a$
are finite and non-empty. For a given
$a\in \mathcal {L}$
consider its successor b. In all the orders
$\mathcal {A}_{s}$
, for
$s\ge \max (s_a,s_b)$
, the element b is the successor of a according to
$S^{\mathcal {A}_s}$
. Thus no elements will appear in between a and b in the orders
$\mathcal {A}_s$
. Therefore, no new elements will be added to
$B_a$
after the stage
$\max (s_a,s_b)$
, and hence
$B_a$
is finite. The block
$B_a$
is non-empty since by construction
$f^{-1}_{s_a}(a)=\{x_a\}$
.
Combining Lemmas 17 and 18 we get a formal version of a special case of a theorem due to Ash [Reference Ash3] as stated in [Reference Ash and Knight1, Theorem 9.11]: If a linear order
$\mathcal {L}$
has an isomorphic copy that is
$\Delta ^0_3$
, then
$\omega \cdot \mathcal {L}$
has a computable copy. The proof of this in two steps, first applying Lemma 17 with
$X=\emptyset '$
and then using Lemma 18, was communicated to us by Andrey Frolov.
Proof of Theorem 12
If X is
$\Pi _{2n+1}$
, then, for some
$\Sigma _{2n}$
set Y
$$\begin{align*}x\in X \leftrightarrow \forall y \langle x,y\rangle \in Y.\end{align*}$$
We can now build a uniformly
$\Delta _{2n+1}$
sequence of linear orders
$(\mathcal {C}_i)_{i\in \omega }$
such that if
$i\in X$
, then
$\mathcal {C}_i$
is the linear order only containing the element
$0$
and if
$i\not \in X$
, then
$\mathcal {C}_i$
has order-type
$1+\eta $
where the first element is
$0$
. The construction is again in stages where
$\mathcal {C}_{i,s}$
contains only one element
$0$
if for all
$y<s$
$\langle i,y\rangle \in Y$
and otherwise we build a copy of
$\eta $
after the
$0$
. The structure
$\mathcal {C}_{i}=\lim _s \mathcal {C}_{i,s}$
clearly is as required.
Having defined
$(\mathcal {C}_i)_{i\in \omega }$
we apply Lemma 17 and then to the resulting sequence Lemma 18 and so on, until, after n repetitions of this process we get a computable sequence of linear orders
$\mathcal {L}_i$
such that
$$\begin{align*}\mathcal{L}_i \cong \begin{cases} \omega^n & \text{ if }i\in X\\ \omega^n(1+\eta) &\text{ if } i\not\in X. \end{cases}\end{align*}$$
Of course, the way Lemma 17 and Lemma 18 are stated, we can not do this right away. We require more uniformity. However, looking at the proof of Lemma 17 the only step that is not uniform is the assumption that the first element is
$0$
. However, in our case, this is no obstacle, as we have defined
$(\mathcal {C}_i)_{i\in \omega }$
so that all
$\mathcal {C}_i$
have
$0$
as its first element.
Corollary 19. For any
$\Pi _{2n+1}$
sentence
$\varphi $
there exists a computable linear order
$\mathcal {L}$
such that
$\mathsf {ACA}_0$
verifies the following:
-
(1)
$\mathcal {L}$
is a linear order; -
(2)
$\mathcal {L}\cong \omega ^n$
if
$\varphi $
; -
(3)
$\mathcal {L}\cong \omega ^n(1+\eta )$
, if
$\lnot \varphi $
; -
(4)
$\varphi \mathrel {\leftrightarrow }\mathsf {WO}(\mathcal {L})$
.
Proof We consider
$\varphi $
as
$\varphi (x)$
, then apply Theorem 12 to it and finally put
$\mathcal {L}=\mathcal {L}_0$
.
Combining Lemma 4 and Corollary 19 we get
Corollary 20. For any
$\Pi _{2n+1}$
sentence
$\varphi $
there exists a computable linear order
$\mathcal {L}$
such that
-
(1)
$\mathsf {PA}$
proves that
$\mathcal {L}$
is a linear order; -
(2)
$\mathcal {L}\cong \omega ^n$
if
$\varphi $
is true; -
(3)
$\mathcal {L}\cong \omega ^n(1+\eta )$
, if
$\varphi $
is false; -
(4)
$\mathsf {PA}+\varphi \equiv \mathsf {PA}+\mathsf {TI}(\mathcal {L})$
.
Now we are ready to prove Theorem 1.
Theorem 1. For every true
$\Pi _{2n+1}$
sentence
$\varphi $
there exists a computable
$\mathsf {PA}$
-verifiable linear order
$\mathcal {L}\cong \omega ^n+1$
such that
$$\begin{align*}\mathsf{RFN}^{\mathcal{L}}(\mathsf{PA})\vdash \varphi.\end{align*}$$
Proof We use Corollary 20 to obtain computable
$\mathsf {PA}$
-verifiable linear order
$\mathcal {L}_1\simeq \omega ^n$
such that
$\mathsf {PA}+\mathsf {TI}(\mathcal {L}_1)\vdash \varphi $
. Next, we consider the order
$\mathcal {L}$
obtained from
$\mathcal {L}_1$
by adding a new greatest element, i.e.,
$\mathcal {L}\simeq \omega ^n +1$
. By Lemma 5 we see that
$\mathsf {RFN}^{\mathcal {L}}(\mathsf {PA})$
proves all instances of
$\mathsf {TI}(\mathcal {L}_1)$
and thus
$\varphi $
, which concludes the proof of Theorem 1.
5 Lower bound for Feferman’s completeness
In order to provide lower bounds for Feferman’s completeness theorem we will use the fact that for any computable linear ordering
$\mathcal {L}$
and
$n\ge 1$
there is a
$\Sigma _{2n}$
formula
$\mathcal {L}{\upharpoonright }_x {\hookrightarrow }_n y$
such that for any
$a\in \mathcal {L}$
and
$\alpha <\omega ^n$
(represented as a Cantor normal form term) the formula
$\mathcal {L}{\upharpoonright }_a {\hookrightarrow }_n \alpha $
expresses that the initial segment of
$\mathcal {L}$
up to a embeds into
$\alpha $
. We will furthermore need the following property being
$\mathsf {PA}$
-verifiable for
$\mathsf {PA}$
-verifiable linear orders
$\mathcal {L}$
:
$$ \begin{align} (\forall \alpha<\omega^n)(\forall a\in \mathcal{L})((\mathcal{L}{\upharpoonright}_a {\hookrightarrow}_n \alpha)\mathrel{\leftrightarrow}(\forall b\prec^{\mathcal{L}} a)(\exists \beta<\alpha) (\mathcal{L}{\upharpoonright}_b {\hookrightarrow}_n \beta)). \end{align} $$
We will do this by defining for
$n\ge 0$
more general
$\Sigma _{2n}$
formulas
$[x,y)^{\mathcal {L}} {\hookrightarrow }_n z$
such that for
$a\preceq ^{\mathcal {L}} b$
and
$\alpha <\omega ^n$
the formula
$\mathcal {L}{\upharpoonright } [a,b) {\hookrightarrow }_n \alpha $
expresses that the interval
$[a,b)^{\mathcal {L}}$
in
$\mathcal {L}$
embeds into
$\alpha $
. Then we put
$\mathcal {L}{\upharpoonright }_x {\hookrightarrow }_n y$
to be
$$\begin{align*}(\exists z\in \mathcal{L})((\forall w\in\mathcal{L})(z\preceq^{\mathcal{L}} w)\land ([z,x){\hookrightarrow}_n y)).\end{align*}$$
We define this formulas by induction on n. For the case of
$n=0$
, the only eligible ordinal
$\alpha $
is
$0$
and thus we simply put
$[x,y)^{\mathcal {L}} {\hookrightarrow }_n z$
to be
$x=y$
. For
$n+1$
, given an ordinal
$\alpha = \omega ^{m_1}+\ldots +\omega ^{m_k}$
, where all
$m_i\le n$
, we express the property
$[a,b)^{\mathcal {L}}{\hookrightarrow }_{n+1} \alpha $
as
$$\begin{align*} & (\exists c_0\preceq^{\mathcal{L}}\ldots\preceq^{\mathcal{L}} c_k)\\ & \big(c_0=a\land c_k=b\land (\forall i<k)(\forall d\in [c_i,c_{i+1})^{\mathcal{L}})(\exists \beta<\omega^{m_i})( [c_i,d){\hookrightarrow}_n \beta)\big),\end{align*}$$
which is a
$\Sigma _{2n+2}$
formula. In a standard manner we go from the above formulas for individual
$\alpha $
to a single
$\Sigma _{2n+2}$
formula
$[x,y)^{\mathcal {L}} {\hookrightarrow }_n z$
. Verification of (12) is also routine.
Let
$\mathcal {C}$
be the standard order of order-type
$\varepsilon _0$
, whose elements are nested Cantor normal form terms. For
$\alpha <\varepsilon _0$
we put
$\mathsf {RFN}^{\alpha }(T)$
to be
$\mathsf {RFN}^{(\mathcal {C},\alpha )}(T)$
.
Lemma 21. For any
$n\ge 1$
and
$\mathsf {PA}$
-verifiable computable linear order
$\mathcal {L}$
it is
$\mathsf {PA}$
-provable that for any
$a\in \mathcal {L}$
and
$\alpha <\omega ^n$
we have
$$ \begin{align} \mathsf{RFN}(\mathsf{RFN}^{\alpha}(T))+(\mathcal{L}{\upharpoonright}_{a} {\hookrightarrow}_n \alpha)\supset \mathsf{RFN}(\mathsf{RFN}^{\mathcal{L},a}(T)). \end{align} $$
Proof We fix n and prove this using Löb’s theorem. We reason in finitistic manner (which here simply means
$\mathsf {PA}$
-formalizable) and assume that it is
$\mathsf {PA}$
-provable that for all
$\mathsf {PA}$
-verifiable computable linear orders
$\mathcal {L}$
, ordinals
$\alpha <\omega ^n$
and
$a\in \mathcal {L}$
we have (13). We consider some
$\mathcal {L}$
,
$\alpha <\omega ^n$
and
$a\in \mathcal {L}$
and claim that (13) holds.
Note that for any c.e. U extending
$\mathsf {PA}$
, we have
$\mathsf {RFN}(U)+\varphi \supseteq \mathsf {RFN}(U+\varphi )$
. And that
$\mathsf {RFN}(U)+(U\supseteq V)\supseteq \mathsf {RFN}(V)$
. Thus in order to prove (13) it is enough to show that
$\mathsf {PA}+(\mathcal {L}{\upharpoonright }_{ a} {\hookrightarrow }_n \alpha ) $
proves that any finite fragment U of
$\mathsf {RFN}^{\mathcal {L},a}(T)$
is contained in
$\mathsf {RFN}^{\alpha }(T)+\varphi $
for some true
$\Sigma _{2n}$
-sentence
$\varphi $
Footnote
6
.
We further reason in
$\mathsf {PA}+(\mathcal {L}{\upharpoonright }_{a} {\hookrightarrow }_n \alpha )$
and consider a finite fragment U of
$\mathsf {RFN}^{\mathcal {L},a}(T)$
. Notice that U is a subtheory of some
$\mathsf {RFN}(\mathsf {RFN}^{\mathcal {L},b}(T))$
, where
$b\prec ^{\mathcal {L}}a$
. By (12) we can deduce from
$\mathcal {L}{\upharpoonright }_{a} {\hookrightarrow }_n \alpha $
that there is
$\beta <\alpha $
such that
$\mathcal {L}{\upharpoonright }_{b} {\hookrightarrow }_n \beta $
. We take
$\mathcal {L}{\upharpoonright }_{b} {\hookrightarrow }_n \beta $
as our
$\varphi $
. By the premise that (13) is already
$\mathsf {PA}$
-provable we see that U is contained in
$\mathsf {RFN}(\mathsf {RFN}^{\beta }(T))+(\mathcal {L}{\upharpoonright }_{b} {\hookrightarrow }_n \beta )$
and hence U is contained in
$\mathsf {RFN}^{\alpha }(T)+(\mathcal {L}{\upharpoonright }_{b} {\hookrightarrow }_n \beta )$
.
Theorem 2. For every
$n>0$
, there exists a true
$\Pi _{2n}$
-sentence
$\varphi $
such that for any computable
$\mathsf {PA}$
-verifiable linear order
$\mathcal {L}$
of order-type at most
$\omega ^n$
$$\begin{align*}\mathsf{RFN}^{\mathcal{L}}(\mathsf{PA})\nvdash \varphi.\end{align*}$$
Proof Indeed, by Lemma 21 the theory
$$\begin{align*}T=\mathsf{RFN}^{\omega^n}(\mathsf{PA})+\text{"all true } \Sigma_{2n}\text{-sentences"} \end{align*}$$
contains
$\mathsf {RFN}^{\mathcal {L}}(\mathsf {PA})$
, for any
$\mathsf {PA}$
-verifiable computable well-ordering
$\mathcal {L}$
of order-type
$\le \omega ^n$
. However, the arithmetically sound theory T has a
$\Sigma _{2n}$
-set of theorems and thus there is a true
$\Pi _{2n}$
sentence
$\varphi $
that is not provable in this theory. Hence
$\varphi $
can not be proved by any
$\mathsf {RFN}^{\mathcal {L}}(\mathsf {PA})$
of the considered form.
6 Reflection iterated along elements of
$\mathcal {O}$
Feferman’s completeness theorem was based on progressions along notations in Kleene’s
$\mathcal O$
, but in Theorem 1 we iterate reflection along a computable well-order. There is a subtle difference in that notations in Kleene’s
$\mathcal {O}$
yield linear orderings with properties that are generally not possessed by computable linear orderings. In particular, the successor relation, the set of limit points, and the end and starting points of such an ordering are computable.
A testament that Theorem 1 cannot be transferred to work with progressions along ordinal notation systems is that it gives for every true
$\Pi _1$
sentence
$\varphi $
a computable well-order
$\mathcal {L}$
of order-type
$1$
such that
$\mathsf {RFN}^{\mathcal {L}}(\mathsf {PA})\vdash \varphi $
. Ordinal notation systems such as Kleene’s
$\mathcal O$
have a unique notation for finite orderings and thus the analogous theorem for ordinal notation systems must fail. However, we can still obtain tight bounds for progressions along ordinal notation systems by using basic properties of computable linear orderings.
For an arbitrary number a and c.e. axiomatizable T extending
$\mathsf {PA}$
we define
$\mathsf {RFN}^a(T)$
to be
-
(1)
$\mathsf {RFN}^{2^a}(T)=\mathsf {RFN}(\mathsf {RFN}^a(T))$
, -
(2)
$\mathsf {RFN}^{3\cdot 5^e}(T)=T+\bigcup \{\mathsf {RFN}(\mathsf {RFN}^a(T))\mid a=\{e\}(n) \text { for some }n\}$
, -
(3)
$\mathsf {RFN}^a(T)=T$
, for a that aren’t of the forms
$3\cdot 5^e$
or
$2^{a'}$
.
We make this definition precise in a manner fully analogous to what we did in Section 2.3
Theorem 22. For every true
$\Pi _{2n+1}$
sentence
$\varphi $
there exists
$a\in \mathcal O$
with
$|a|=\omega ^{n+1}+1$
such that
$$\begin{align*}\mathsf{RFN}^a(\mathsf{PA}) \vdash \varphi. \end{align*}$$
Proof Let
$\varphi $
be a
$\Pi _{2n+1}$
sentence and
$\mathcal {L}$
be the linear ordering obtained in Lemma 19. Then
$\mathsf {ACA}_0$
proves
$\mathsf {WO}(\mathcal L)$
if and only if
$\varphi $
is true. In particular, the ordering
$\mathcal L'=\omega \cdot (1+\mathcal {L})+1$
is a computable ordering such that
$\mathsf {ACA_0}$
proves
$\mathcal L' \cong \omega ^{n+1}+1$
if and only if
$\varphi $
is true. We can also assume that
$\mathcal L'$
comes with other special properties shared with notations in Kleene’s
$\mathcal {O}$
: It has a computable successor relation, a computable set of limit points, and there are algorithms that compute the first and last elements, predecessors, and fundamental sequences for limit points. For example, the ordering defined by
$$\begin{align*}\begin{aligned} L'&=\{\infty,(-1,m),(n,m):n\in L, m\in \omega\}, \\ (n_0,m_0)\preceq^{\mathcal{L}'} (n_1,m_1) &\iff (n_0=n_1 \land m_0\leq m_1)\lor -1 \\ &=n_0\neq n_1\lor n_1\not\preceq^{\mathcal{L}} n_0 , \\ \text{ and for all } x, x\preceq^{\mathcal{L}'} \infty \end{aligned} \end{align*}$$
clearly has these properties. Recall that for
$x\in \mathcal {L}'$
,
$\mathcal {L}'{\operatorname {\mathrm {\upharpoonright }}}_x$
denotes the initial segment of
$\mathcal {L}'$
up to x. It is shown in [Reference Ash and Knight1, Lemma 4.13] that there is a computable function
$g:L'\to \mathbb N$
such that for every
$x\in L'$
, if
$\mathcal {L}'{\operatorname {\mathrm {\upharpoonright }} }_x$
is well-ordered, then
$g(x)\in \mathcal O$
and
$|g(x)|\cong \mathcal {L}'{\operatorname {\mathrm {\upharpoonright }} }_x$
. On the other hand, if
$\mathcal {L}'{\operatorname {\mathrm {\upharpoonright }}}_x$
is not well-ordered, then
$g(x)\not \in \mathcal {O}$
.
Using the same reasoning as in the proof of Theorem 1 we now get that if
$\varphi $
is true, then
$\mathsf {RFN}^{g(\infty )}(\mathsf {PA})\vdash \varphi $
, and
$|g(\infty )|=\omega ^{n+1}+1$
.
Corollary 23 (Feferman’s original completeness theorem with improved bounds).
For any true arithmetical sentence
$\varphi $
, there exists
$a\in \mathcal O$
with
$|a|<\omega ^\omega $
such that
$\mathsf {RFN}^{a}(\mathsf {PA})\vdash \varphi $
. Furthermore, the bound on
$|a|$
is tight, i.e., for every
$\alpha <\omega ^\omega $
, there is a true arithmetical sentence
$\varphi $
such that for no
$a\in \mathcal O$
with
$|a|=\alpha $
,
$\mathsf {RFN}^{a}(\mathsf {PA})\vdash \varphi $
.
A similar result was claimed in [Reference Fenstad8]; however, Savitt found a mistake in this proof [Reference Savitt13].
7 Discussion and open questions
We suspect that it should be easy to adopt the techniques from Theorem 2 to show sharpness of the upper bound from Theorem 22 on the order-types for the iterations of reflection along elements of
$\mathcal {O}$
necessary to attain the completeness of iterations of reflection for
$\Pi _{2n+1}$
-sentences.
In the present paper, we have been focusing on the iterations of full uniform reflection, however, when we want to obtain some true
$\Pi _n$
-sentence in principle it is natural to expect that we need to iterate just partial uniform
$\Pi _n$
reflection
$\mathsf {RFN}_{\Pi _n}$
instead of full uniform reflection
$\mathsf {RFN}$
. For example, the existence of such iterations could be easily proved by combining Feferman’s completeness theorem for full uniform reflection with Schmerl’s formula that allows us to transform short iterations of stronger reflection to longer iterations of weaker
$\Pi _n$
reflection, while preserving the set of
$\Pi _n$
-consequences. We suspect that the methods used in this paper can be adopted to show that for some natural number constant C and every n we can replace
$\mathsf {RFN}$
with
$\mathsf {RFN}_{\Pi _{2n+1+C}}$
in Theorem 1. However, it is not clear to us whether in Theorem 1 full uniform reflection
$\mathsf {RFN}$
can be replaced with just
$\mathsf {RFN}_{\Pi _{2n+1}}$
, while keeping the bound
$\omega ^n+1$
on the order-type.
Acknowledgments
The first author would like to thank Stella Moon whose questions led him to start investigations on Feferman’s theorem. He would also like to thank Nikolay Bazhenov for pointing him to the work of Ash and Knight. We would like to thank Andrey Frolov for sharing with us his neat alternative proof of the theorem of Ash and Knight. Finally, we would like to thank the anonymous referee, as well as Mateusz Łełyk, Patryk Szlufik, and Patrick Lutz for their useful comments on an earlier version of the paper.
Funding
The work of Pakhomov was funded by the FWO grant G0F8421N. The work of Rathjen was supported by the John Templeton Foundation Grant ID 60842 and by the European Union (ERC Advanced Grant, C-FORS: Construction in the Formal Sciences, awarded to Øystein Linnebo, project number 101054836). The work of Rossegger was supported by the European Union’s Horizon 2020 Research and Innovation Programme under the Marie Skłodowska-Curie grant agreement No. 101026834 — ACOSE and the Austrian Science Fund (FWF) 10.55776/P36781
