1 Introduction
1.1 Background and results
Let Heyting arithmetic (
$\mathbf {HA}$
) be the standard formalization of intuitionistic number theory. Throughout, we work in intuitionistic logic. Classical Peano arithmetic (
$\mathbf {PA}$
) may be viewed as
$\mathbf {HA} + \mathbf {LEM}$
, where
$\mathbf {LEM}$
comprises all instances of the law of excluded middle.
Let T be a recursively enumerable theory in the language of first-order arithmetic. Informally, one wishes to iterate reflection across the ordinals by setting
$$\begin{align*}T_{0}= T, \qquad T_{\alpha+1}= (T_\alpha)', \qquad T_{\lambda} = \bigcup_{\alpha\, <\, \lambda} T_\alpha \ \text{ for } \lambda \text{ limit}, \end{align*}$$
where
$T'$
is obtained from T by adjoining either the consistency statement
$\mathbf {Con}(T)$
, the local reflection scheme
$\mathbf {Rfn}(T)$
, or the uniform reflection scheme
$\mathbf {RFN}(T)$
, each intended to formalize a stronger form of soundness for T:
-
(1) (consistency) T does not prove
$\bot $
; -
(2) (local) if T proves
$\varphi $
, then
$\varphi $
is true; -
(3) (uniform) if T proves
$\varphi (\bar n)$
for every natural number n, then
$\forall x\, \varphi (x)$
is true.Footnote
1
Full details of the formalization are given in §2. In general, such iterations are possible as long as the ordinals are effectively presented. We follow Feferman [Reference Feferman5] and consider sequences of recursively enumerable theories
$(T_d)_{d \in \mathcal {O}}$
indexed by ordinal notations in Kleene’s
$\mathcal {O}$
—what Feferman calls transfinite recursive progressions. We will simply call these theories
$T_d$
(for
$d\in \mathcal {O}$
) iterations.
Theorem 1.1 (Feferman’s completeness Theorem; [Reference Feferman5, Theorem 5.13]).
All true sentences of arithmetic are provable in iterations of uniform reflection over
$\mathbf {PA}$
.
Theorem 1.2 (Feferman [Reference Feferman5, Theorems 4.1 and 4.5]).
The sentences provable in iterations of either consistency or local reflection over
$\mathbf {PA}$
coincide with those provable in
$\mathbf {PA} +$
all true
$\Pi _1$
sentences.
The idea of iterating consistency and the fact that such iterations capture all true
$\Pi _1$
sentences goes back to Turing [Reference Turing24, p. 210]. Turing, however, believed that local reflection would be stronger (cf. [Reference Feferman5, p. 260]), a conjecture that is refuted by Theorem 1.2.
In this note, we consider iterations of reflection along Kleene’s
$\mathcal {O}$
and prove the following results.
Theorem 1.3 (Dragalin’s theorem [Reference Dragalin3, Theorem 1]; see Theorem 4.3).
The sentences provable in iterations of uniform reflection over
$\mathbf {HA}$
are precisely those provable in
$\mathbf {HA}$
extended by the recursive
$\omega $
-rule. This holds for every recursively enumerable extension of
$\mathbf {HA}$
.
The situation for consistency and local reflection mirrors the classical case.
Theorem 1.4 (see Theorem 3.1).
The sentences provable in iterations of either consistency or local reflection over
$\mathbf {HA}$
coincide with those provable in
$\mathbf {HA}\, +$
all true
$\Pi _1$
sentences. In fact, this holds for every recursively enumerable extension of
$\mathbf {HA}$
.
We will establish these results for
$\mathbf {HA}$
itself, as the proofs carry over mutatis mutandis to all recursively enumerable extensions.
1.2 Discussion
The result for consistency and local reflection is fairly straightforward, yet it does not seem to have been noted before. At the same time, the result about uniform reflection should come as no great surprise since the true core of Feferman’s completeness theorem—indeed, of Feferman’s own proof—is the following.
Theorem 1.5 (cf. [Reference Feferman5, Theorem 5.10]).
Every sentence provable in
$\mathbf {PA}$
extended by the recursive
$\omega $
-rule can be proved in some iteration of uniform reflection over
$\mathbf {PA}$
.
In fact, Feferman relies on Shoenfield [Reference Kreisel, Shoenfield and Wang9, Reference Shoenfield19], who showed that every true sentence of arithmetic is provable in
$\mathbf {PA}$
augmented by the recursive
$\omega $
-rule. Note that Theorem 1.5 is a special case of Theorem 1.3, and therefore, in light of Shoenfield’s result, Dragalin’s theorem can be seen as an extension of Feferman’s completeness theorem. Dragalin’s proof of Theorem 1.3 is merely a sketch, while another proof is outlined in Sundholm [Reference Sundholm21, Chap. 7]. Both aim to show how classical reasoning can be eliminated from Feferman’s argument. As noted by both Dragalin and Sundholm, the main obstacle in extending Theorem 1.5 to
$\mathbf {HA}$
is that Feferman’s [Reference Feferman5, Theorem 4.9] depends crucially on classical logic. A closer look reveals the use of
$\Sigma _1$
-
$\mathbf {LEM}$
, the law of excluded middle for
$\Sigma _1$
formulas. Dragalin claims that a weakening of [Reference Feferman5, Theorem 4.9] suffices. Sundholm points out that Derevyankina’s approach [Reference Derevyankina2] to iterated reflection, which is based on a more flexible notation system for constructive ordinals, goes through in intuitionistic logic. In any case, both Dragalin’s proof and Sundholm’s account presuppose familiarity with Feferman [Reference Feferman5], a notoriously long and technical paper, known more for its results than for its proofs.
In this note, we retain Feferman’s framework—considering iterations along Kleene’s
$\mathcal {O}$
and following his formalization of iterated reflection—and present an entirely new proof of Dragalin’s theorem that does not follow Feferman’s route, but instead is inspired by Rathjen’s proof of Feferman’s completeness theorem. Rathjen’s proposal (first announced in [Reference Rathjen14, Reference Rathjen15] and later expounded in [Reference Pakhomov, Rathjen and Rossegger12]) is to employ Schütte’s canonical search trees (also known as deduction chains; see [Reference Schütte18]) and combine in one stroke Theorem 1.5 and the aforementioned Shoenfield’s result. For any sentence
$\varphi $
, the construction of its canonical tree
$S(\varphi )$
(the Stammbaum of
$\varphi $
) is primitive recursive and returns a classical
$\omega $
-proof of
$\varphi $
if and only if
$\varphi $
is true. In the intuitionistic case, we cannot replicate a similar scenario; nonetheless—and here lies our key idea—we can construct a primitive recursive tree
$S(a)$
for any natural number a such that
$S(a)$
is an intuitionistic
$\omega $
-proof of
$\varphi $
(possibly with repetitions) if and only if a codes an intuitionistic recursive
$\omega $
-proof of
$\varphi $
. An elaboration of this idea will lead to Theorem 4.3. A further insight, due to Rathjen, is the use of Löb’s theorem to formalize certain arguments within
$\mathbf {PA}$
. Although Löb’s theorem does not hold wholesale for
$\mathbf {HA}$
, its restriction to
$\Pi _2$
formulas does, and this will allow us to prove—within
$\mathbf {HA}$
itself—several facts that prima facie require induction on Kleene’s
$\mathcal {O}$
.
All our proofs rely squarely on intuitionistic logic: see the implications (2)
$\Rightarrow $
(3) of Theorem 3.1 on local reflection and (1)
$\Rightarrow $
(2) of Theorem 4.3 on uniform reflection. It is therefore natural to ask the following question.
Question. Do any of these results hold for minimal logic, that is, intuitionistic logic without the principle of explosion (ex falso quodlibet)?
We emphasize that our attention is restricted to iterations of reflection along Kleene’s
$\mathcal {O}$
(as in Feferman [Reference Feferman5]). In this paper, we do not compute ordinal bounds relating the height
$\alpha $
of an intuitionistic recursive
$\omega $
-proof of a sentence
$\varphi $
to the ordinal
$|d|$
of a notation
$d\in \mathcal {O}$
such that
$T_d\vdash \varphi $
, where
$T_d$
is the d-th iteration based on uniform reflection. Such bounds can certainly be obtained from our proof of Dragalin’s theorem. In the classical case, there exists a uniform ordinal bound
$\beta <\omega _1^{\text {CK}}$
such that every true sentence is provable in
$T_d$
for some
$d\in \mathcal {O}$
with
$|d|<\beta $
. Recall that the so-called Church–Kleene ordinal
$\omega _1^{\text {CK}}$
is defined as the least non-recursive ordinal. Feferman [Reference Feferman5] gives
$\beta =\omega ^{\omega ^\omega }$
. A proof that
$\omega ^\omega $
is a sharp bound for iterations of uniform reflection over
$\mathbf {PA}$
is provided in [Reference Pakhomov, Rathjen and Rossegger12], where tight bounds are determined based on the complexity of a true sentence. We do not know whether a recursive ordinal bound even exists in the case of
$\mathbf {HA}$
; equivalently, whether there is an ordinal
$\beta <\omega _1^{\text {CK}}$
such that every sentence
$\varphi $
with an intuitionistic recursive
$\omega $
-proof admits one of height
$<\beta $
.Footnote
2
We expect the answer to be positive. Moreover, we do not, in this paper, deal with autonomous progressions in the sense of Feferman [Reference Feferman6], nor with progressions over fixed (primitive recursive) ordinal notation systems in the sense of Schmerl [Reference Schmerl, Boffa, Dalen and Mcaloon16]. In particular, as concerns progressions à la Schmerl, we do not investigate the relationship between (fragments of) iterated uniform reflection, transfinite induction and the
$\omega $
-rule (see [Reference Schmerl, Boffa, Dalen and Mcaloon16, Reference Schmerl17] for the classical case). Note that a formalization in
$\mathbf {HA}$
of the intuitionistic
$\omega $
-rule and of cut elimination for intuitionistic
$\omega $
-proofs is carried out in [Reference López-Escobar11]: this is then used to show that, over
$\mathbf {HA}$
, the scheme
$\mathbf {RFN}(\mathbf {HA})$
is equivalent to the scheme of transfinite induction up to
$\varepsilon _0$
, a result due to Kreisel in the case of
$\mathbf {PA}$
. Finally, the approach introduced in [Reference Schmerl, Boffa, Dalen and Mcaloon16] has proved to be a valuable tool in the proof theory of first-order classical arithmetic (e.g., [Reference Beklemishev1]) and, more recently, of second-order arithmetic (e.g., [Reference Pakhomov and Walsh13]). It would be interesting to pursue this line of research for
$\mathbf {HA}$
and potentially for intuitionistic second-order arithmetic (a standard formalization of the latter is
$\mathbf {HAS}$
; cf. [Reference Troelstra22, Chap. 1, Sec. 9]).
1.3 Motivation, related work, and open questions
Our interest in Dragalin’s theorem, and more generally in the topic of iterated reflection over
$\mathbf {HA}$
, is driven by the quest for a simple characterization of the intuitionistic recursive
$\omega $
-rule. Since the recursive
$\omega $
-rule over
$\mathbf {PA}$
is complete for true sentences of arithmetic, it is natural to ask how it fares against the unrestricted
$\omega $
-rule when the underlying logic is intuitionistic. It is well known that:
-
(1) every true arithmetical sentence has an intuitionistic
$\omega $
-proof—albeit one that is far from constructive, as it is computable only relative to the set of all true sentences; -
(2) any sentence with an intuitionistic recursive
$\omega $
-proof is realizable (cf. [Reference López-Escobar11, p. 91].
Since there exist true sentences that are not realizable, it follows that, in the intuitionistic setting, the recursive
$\omega $
-rule is strictly weaker than the full
$\omega $
-rule. A natural question then arises as follows.
Question. Does every realizable true sentence admit an intuitionistic recursive
$\omega $
-proof? Equivalently, is any such sentence provable in an iteration of uniform reflection over
$\mathbf {HA}$
?
Let
$\mathbf {MP}$
be Markov’s principle, that is, the scheme
$$\begin{align*}\neg\neg \varphi\rightarrow \varphi \end{align*}$$
for
$\varphi \in \Sigma _1$
. We claim that
$\mathbf {MP}$
is not provable in iterations of uniform reflection over
$\mathbf {HA}$
. This gives a counterexample—a realizable, true sentence not provable in that way. Consequently, the answer is negative. The following broader question thus remains open.
Question. Is there a notion of intuitionistic truth that renders such iterations complete?
Kreisel (unpublished; see [Reference Feferman7] and [Reference Sundholm21, Sec. 7:17]) observed that the closure of
$\mathbf {HA}$
under Markov’s rule extends to every iteration of uniform reflection
$\mathbf {HA}_d$
for
$d\in \mathcal {O}$
, and thus to
$\mathbf {HA}$
equipped with the recursive
$\omega $
-rule. This suggests that any notion of truth that seeks to achieve the desired completeness with respect to recursive
$\omega $
-provability over
$\mathbf {HA}$
cannot be compositional. Specifically, the following Tarski clause for implication
$$\begin{align*}T(\varphi)\rightarrow T(\psi) \text{ implies } T(\varphi\rightarrow\psi)\end{align*}$$
must be dropped.
We conclude by highlighting a handful of lesser-known results that are directly relevant to our quest. These are found in Dragalin [Reference Dragalin3] and in Kurata [Reference Kurata10].
Definition 1.6. A formula is negative if it has no occurrences of
$\lor $
or
$\exists $
. It is quasi negative if it consists of a block of quantifiers followed by a negative matrix.
Theorem 1.7 [Reference Dragalin3, Theorem 3].
If a quasi negative formula
$\varphi $
is realizable in the sense of Kleene’s recursive realizability, then
$\varphi $
has an intuitionistic recursive
$\omega $
-proof.
The proof of this theorem is based on a primitive recursive bottom-up search for an
$\omega $
-proof of
$\varphi $
within an intuitionistic, cut-free
$\omega $
-calculus with two infinitary
$\omega $
-rules: one for introducing
$\exists $
in the antecedent and the other for introducing
$\forall $
in the succedent. Now, for negative
$\varphi $
, a systematic proof search can be arranged so that the resulting tree is an
$\omega $
-proof if and only if
$\varphi $
is true; notice that a negative formula is true if and only if it is realizable (cf. [Reference Troelstra22, Lemma 3.2.11]). For quasi negative
$\varphi $
, a given realizer allows one to deal effectively with the leading quantifiers. In particular, the following holds.
Corollary 1.8 (Completeness for the negative fragment).
All true negative sentences are provable in iterations of uniform reflection over
$\mathbf {HA}$
. In particular, the Gödel–Gentzen negative translation of every true sentence is likewise provable in such an iteration.
This corollary also follows from the fact that negative translation extends to both
$\mathbf {PA}$
and
$\mathbf {HA}$
equipped with the recursive
$\omega $
-rule, and a negative formula is provably equivalent to its own translation within
$\mathbf {HA}$
.
The next result gives a characterization of realizability in terms of iterated uniform reflection. Let
$\mathbf {ECT}_0$
be the extended Church’s thesis scheme
$$\begin{align*}\forall x\, (\chi\rightarrow \exists y\, \varphi(x,y))\rightarrow \exists e\, \forall x\, (\chi\rightarrow \exists y\, (\{e\}(x)\simeq y\land \varphi(x,y))) \end{align*}$$
for
$\chi $
almost negative.Footnote
3
Theorem 1.9 [Reference Dragalin3, Theorem 4].
A sentence is realizable if and only if it is provable in
$\mathbf {HA}+\mathbf {ECT}_0+\mathbf {MP}$
augmented by the recursive
$\omega $
-rule.Footnote
4
Kurata [Reference Kurata10] appears to be the first to study iterated reflection over
$\mathbf {HA}$
. While he does not discuss
$\omega $
-provability, he investigates iterations of uniform reflection over both
$\mathbf {HA}$
and
$\mathbf {HA}+\mathbf {MP}$
. The following results from [Reference Kurata10] are relevant here.Footnote
5
Theorem 1.10 [Reference Kurata10, Theorem 1, p. 149, Proposition 5.5, p. 160, Theorem 3, p. 161].
Let
$T_d$
denote the d-th iteration of uniform reflection over T. The following hold:
-
(1) if
$\varphi $
is provable in
$\mathbf {HA}_d$
for some
$d\in \mathcal {O}$
, then
$\varphi $
is realizable; -
(2) if
$\varphi $
is provable in
$(\mathbf {HA}+\mathbf {MP})_d$
for some
$d\in \mathcal {O}$
, then Gödel’s Dialectica interpretation
$\varphi ^D$
of
$\varphi $
is true in Kreisel’s model
$\mathbf {HRO}$
of the hereditarily recursive operations; -
(3) if
$\varphi $
is in prenex form, then
$\varphi $
is provable in
$(\mathbf {HA}+\mathbf {MP})_d$
for some
$d\in \mathcal {O}$
if and only if
$\varphi $
is recursively true.
A prenex sentence
$\varphi $
is recursively true if
$\mathbf {HRO}\models \varphi ^S$
, where
$\varphi ^S$
is the normal Skolem form of
$\varphi $
(cf. [Reference Kleene8, Chap. XV, Sec. 79, p. 465]). Note that a sentence in prenex form is recursively true if and only if it is realizable (see [Reference Kleene8, Chap. XV, Sec. 82, p. 516]). It is not difficult to see that any such sentence has an intuitionistic recursive
$\omega $
-proof. By Dragalin’s theorem, one obtains the following interesting corollary.
Theorem 1.11. Iterations of uniform reflection over
$\mathbf {HA}$
and over
$\mathbf {HA}+\mathbf {MP}$
prove the same prenex sentences.
Question. Is there a notion of intuitionistic truth that makes iterations of uniform reflection over
$\mathbf {HA}+\mathbf {MP}$
complete?
2 Preliminaries
Let
$\mathbf {HA}$
be a standard axiomatization of
$\mathbf {HA}$
with only one relation symbol
$=$
for equality and function symbols for all (definitions of) primitive recursive functions (cf. Troelstra [Reference Troelstra22, Chap. 1, Sec. 3]. Negation
$\neg \varphi $
is defined as
$\varphi \rightarrow \bot $
.
2.1 Arithmetization of reflection
If
$F\colon \mathbb {N}^k\to \mathbb {N}$
is a primitive recursive function, we denote by
$F^\circ $
the corresponding function symbol.Footnote
6
In particular,
$$\begin{align*}\mathbf{HA}\vdash F^\circ(\bar n_1,\ldots,\bar n_k)=\overline{F(n_1,\ldots,n_k)}. \end{align*}$$
Moreover, if
$R\subseteq \mathbb {N}^k$
is a primitive recursive relation, we denote by
$R^\circ (x_1,\ldots ,x_k)$
the formula
$F^\circ (x_1,\ldots ,x_k)=0$
, where F is the representing function of R.Footnote
7
In particular,
$$ \begin{align*} & (n_1,\ldots,n_k)\in R \quad\text{iff} \quad \mathbf{HA}\vdash R^\circ(\bar n_1,\ldots,\bar n_k), \\& (n_1,\ldots,n_k)\notin R \quad \text{iff}\quad \mathbf{HA}\vdash \neg R^\circ(\bar n_1,\ldots,\bar n_k). \end{align*} $$
In other words, primitive recursive functions and relations are representableFootnote
8
in
$\mathbf {HA}$
.
Convention 2.1. We typically drop the
$\circ $
notation when the context makes it clear whether we are talking about the primitive recursive function (relation) or its corresponding symbol.
We can define
$x<y$
by 
, where 
is the primitive recursive cutoff subtraction. Bounded quantifiers are then defined as usual.
Definition 2.2 (cf. [Reference Visser25]).
The
$\Delta _0$
formulas are defined by the following clauses:
-
• atomic formulas (including
$\bot $
) are
$\Delta _0$
; -
• if
$\varphi $
and
$\psi $
are
$\Delta _0$
, then
$\varphi \land \psi $
,
$\varphi \lor \psi $
and
$\varphi \rightarrow \psi $
are
$\Delta _0$
; -
• if
$\varphi $
is
$\Delta _0$
and
$t$
is a term not containing x, then
$\forall x<t\, \varphi (x)$
and
$\exists x<t\, \varphi (x)$
are
$\Delta _0$
.
Let
$$ \begin{align*} \Sigma_1&=\{\exists x\, \varphi(x)\mid \varphi\in\Delta_0\}, & \Pi_1&=\{\forall x\, \varphi(x)\mid \varphi\in\Delta_0\}, & \Pi_2 &=\{\forall x\, \varphi(x)\mid \varphi\in \Sigma_1\}. \end{align*} $$
The
$\Sigma $
formulas are defined by the following clauses:
-
•
$\Delta _0$
formulas are
$\Sigma $
; -
• if
$\varphi $
and
$\psi $
are
$\Sigma $
, then
$\varphi \land \psi $
and
$\varphi \lor \psi $
are
$\Sigma $
; -
• if
$\varphi $
is
$\Delta _0$
and
$\psi $
is
$\Sigma $
, then
$\varphi \rightarrow \psi $
is
$\Sigma $
; -
• if
$\varphi $
is
$\Sigma $
and
$t $
is a term not containing x, then
$\forall x<t\, \varphi (x)$
is
$\Sigma $
; -
• if
$\varphi $
is
$\Sigma $
, then
$\exists x\, \varphi (x)$
is
$\Sigma $
.
The
$\Pi $
formulas are defined dually by switching
$\exists $
and
$\forall $
in last two clauses.
By a routine induction on the build-up of a formula one can prove the following.
Proposition 2.3 (Normal form).
For every
$\Delta _0$
formula
$\varphi (x_1,\ldots ,x_k)$
there is a (definition of a) primitive recursive function F such that
$$\begin{align*}\mathbf{HA}\vdash \varphi(x_1,\ldots,x_k) \leftrightarrow F^\circ(x_1\,\ldots,x_k)=0. \end{align*}$$
For every
$\Sigma $
formula
$\varphi (x_1,\ldots ,x_k)$
there is a (definition of a) primitive recursive function F such that
$$\begin{align*}\mathbf{HA}\vdash \varphi(x_1,\ldots,x_k) \leftrightarrow \exists x\, F^\circ(x_1\,\ldots,x_k,x)=0. \end{align*}$$
For every
$\Pi $
formula
$\varphi (x_1,\ldots ,x_k)$
there is a (definition of a) primitive recursive function F such that
$$\begin{align*}\mathbf{HA}\vdash \varphi(x_1,\ldots,x_k) \leftrightarrow \forall x\, F^\circ(x_1\,\ldots,x_k,x)=0. \end{align*}$$
In particular,
$\Delta _0$
formulas are decidable in
$\mathbf {HA}$
, namely,
$\mathbf {HA}\vdash \varphi \lor \neg \varphi $
, for every
$\Delta _0$
formula
$\varphi $
.
Definition 2.4. A formula
$\varphi $
is
$\Sigma $
in
$\mathbf {HA}$
if it is equivalent in
$\mathbf {HA}$
to a
$\Sigma $
formula. Similarly for other classes of formulas.
We assume a primitive recursive coding of finite sequences. As in Feferman [Reference Feferman4, Reference Feferman5], we make no distinction between expressions (terms or formulas) and their Gödel numbers. For example,
$\bot $
will be a given natural number (based on the coding), and
$\bar \bot $
will be the numeral for that number. The logical symbols
$\land , \lor ,\rightarrow , \forall , \exists $
can be treated as (primitive recursive) operations on the natural numbers. For example, we have a primitive recursive function
$F_\rightarrow $
such that
$F_\rightarrow (\varphi ,\psi )=\varphi \rightarrow \psi $
. We abuse notation an write
$x \rightarrow ^\circ y$
for
$F_\rightarrow ^\circ (x,y)$
. We fix a Hilbert-style system for intuitionistic first-order logic with equality. We may safely assume a primitive recursive presentation of the logical axioms and rules.
Notation 2.5. We make use of the following primitive recursive functions and relations. The predicate
${Seq}(x)$
indicates that
$x$
is sequence,
${lh}(x)$
is the length of
$x$
,
$x_i$
is the
$i$
-th element of
$x$
and
$x\restriction i$
is the initial segment of
$x$
of length
$i$
. Let
${Snt}(x)$
and
${Fml}(x)$
express that
$x$
is a sentence and
$x$
is a formula, respectively. The predicate
${Ax}(v)$
means that
$v$
is a logical axiom and
${Rule}(x,y)$
means that the formula
$x$
can be obtained from formulas in the sequence
$y$
by means of a logical rule.
Definition 2.6 (Provability predicate).
Let
$\chi (v)$
be a formula with free variable
$v$
. The formula
${Pr}_\chi (x)$
is defined as
$\exists y\, {Prf}(x,y)$
, where
$$\begin{align*}{Prf}(x,y) \, =_{\text{def}} \ {Seq}(y)\land x\kern1.4pt{=}\kern1.4pt y_{{lh}(y)-1}\land \forall i\kern1.4pt{<}\kern1.4pt{lh}(y)\, \big({Ax}(y_i)\lor \chi(y_i)\lor {Rule}(y_i,y\restriction i)\big). \end{align*}$$
The consistency formula
${Con}_\chi $
is defined by
$\neg {Pr}_\chi (\bar \bot )$
.
Remark 2.7. If
$\chi (v)$
is
$\Sigma $
(in
$\mathbf {HA}$
), then
${Pr}_\chi (x)$
is
$\Sigma $
(in
$\mathbf {HA}$
) and
${Con}_\chi $
is
$\Pi $
in
$\mathbf {HA}$
.
Note that the formula
$\chi (v)$
may contain additional free variables aside from
$v$
.
Remark 2.8. Let
$\chi (z,v)$
be any formula with displayed free variables, and let
${Pr}(z,x)$
denote the corresponding provability predicate. Then
$$\begin{align*}\mathbf{HA}\vdash \forall v\, (\chi(z_0,v)\rightarrow {Pr}(z_1,v))\rightarrow {Pr}(z_0,x)\rightarrow {Pr}(z_1,x).\end{align*}$$
Definition 2.9 (Syntactic operations).
There are primitive recursive functions
${Nm}$
,
${Sb}$
,
${Pr}$
and
${Con}$
such that:
-
•
${Nm}(n)$
is the n-th numeral
$\bar n$
for every natural number n; -
•
${Sb}(e,x,t)$
is the result of replacing
$x$
with
$t$
in
$e$
. In general, the simultaneous substitution
${Sb}(e,x_1,\ldots ,x_k,t_1,\ldots ,t_k)$
is obtained by replacing all
$x_i$
in
$e$
by
$t_i$
; -
•
${Pr}_\chi $
and
${Con}_\chi $
are the provability predicate and the consistency formula for
$\chi $
, respectively, whenever
$\chi (v)$
is a formula and
$v $
is a variable.
Strictly speaking,
${Pr}$
is a function of both
$\chi $
and the variable
$v$
, not just
$\chi $
. We rely on context and omit
$v$
. We can assume that this operation is always well defined and returns a formula whose free variables are those of
$\chi $
except for
$v$
and a fresh new variable x. The same goes for
${Con}$
. We will not bother with such details in the future, but the reader should be aware of them.
Remark 2.10. For a formula
$\varphi (u)$
and a term
$t$
, we have
$$\begin{align*}{Sb}(\varphi,u,t)=\varphi(t) \ \text{ and }\ \mathbf{HA}\vdash {Sb}^\circ(\bar\varphi,\bar u,\bar t)=\overline{\varphi(t)}. \end{align*}$$
Remark 2.11. To the functions
${Pr}$
and
${Con}$
correspond unary function symbols
${Pr}^\circ $
and
${Con}^\circ $
. Let T be a theory defined by a formula
$\chi (v)$
with a single free variable
$v$
. Then:
-
•
${Pr}_\chi (\bar \varphi )$
is true iff
$T\vdash \varphi $
; -
•
$\mathbf {HA}\vdash {Pr}^\circ _{\bar \chi }=\overline {{Pr}_{\chi }}$
; -
•
${Con}_\chi $
is true iff T is consistent; -
•
$\mathbf {HA}\vdash {Con}^\circ _{\bar \chi }=\overline {{Con}_\chi }$
.
Definition 2.12 (Syntactic operations one level down).
There are primitive recursive functions
${N}$
and
${S}$
such that:
-
•
${N}(t)$
is the term
${Nm}^\circ (t)$
, whenever
$t$
is a term; -
•
${S}(r,s,t)$
is the term
${Sb}^\circ (r,s,t)$
, whenever
$r,s$
, and
$t $
are terms.
Let
${N}^\circ $
and
${S}^\circ $
be the corresponding function symbols.
Notation 2.13. We use
$\dot x$
to denote
${Nm}^\circ (x)$
and abbreviate
${Sb}^\circ (\bar \varphi ,\bar u,\dot x)$
by
$\bar \varphi (\dot x)$
.
Remark 2.14. For a formula
$\varphi (u)$
and a natural number
$n$
, we have
$$\begin{align*}\mathbf{HA} \vdash \bar \varphi (\dot{\bar n})=\overline{\varphi(\bar n)}. \end{align*}$$
Note that
$\bar \varphi (\dot {\bar n})$
stands for
${Sb}^\circ (\bar \varphi ,\bar u,\dot {\bar n})$
.
Definition 2.15 (Reflection principles).
Let T be a theory defined by a formula
$\chi (v)$
with a single free variable
$v$
.
-
(a) The axiom
$\mathbf {Con}(T)$
is expressed by the sentence
${Con}_\chi $
, which stands for
$\neg {Pr}_\chi (\bar \bot )$
. -
(b) The scheme
$\mathbf {Rfn}(T)$
of local reflection consists of all sentences of the form
$$\begin{align*}{Pr}_\chi(\bar \varphi)\rightarrow \varphi. \end{align*}$$
-
(c) The scheme
$\mathbf {RFN}(T)$
of uniform reflection consists of all sentences of the form where
$$\begin{align*}\forall x\, ({Pr}_\chi(\bar \varphi(\dot x)) \rightarrow \varphi(x)), \end{align*}$$
$\varphi (u)$
is a formula containing only
$u$
as free variable.Footnote
9
Remark 2.16. If
$\chi (v)$
is
$\Sigma $
, then
$T'$
is also
$\Sigma $
definable.
Remark 2.17. The scheme
$\mathbf {RFN}(T)$
should consist of sentences of the form
$$\begin{align*}\forall x\, {Pr}_\chi(\bar \varphi(\dot x)) \rightarrow \forall x\, \varphi(x). \end{align*}$$
This seemingly weaker scheme is known to be equivalent in the case of
$\mathbf {PA}$
(see [Reference Feferman5, Lemma 2.18, Theorem 2.19]), and the very same proof goes through in
$\mathbf {HA}$
.
Definition 2.15 describes one step in the iteration of reflection: the transition from a theory T to any of the following:
$$\begin{align*}T+\mathbf{Con}(T),\qquad T+\mathbf{Rfn}(T),\qquad T+\mathbf{RFN}(T). \end{align*}$$
This process is uniform and effective. In fact, there is a formula, say
$\rho (x,y)$
, corresponding to a primitive recursive relation, such that
$\rho (\bar \chi ,\bar \vartheta )$
holds iff
$\vartheta $
is the consistency statement for the theory T defined by
$\chi $
. Likewise, there are formulas defining
$\mathbf {Rfn}(T)$
and
$\mathbf {RFN}(T)$
. We now show how to construct these formulas: the parameterized version is used in the formalization of iterated reflection (see Definition 2.45). Note that for the proof of Theorem 4.3, the mere existence of these formulas does not suffice.
Notation 2.18. We use
$\ddot {x}$
to denote
${N}^\circ (x)$
and write
$\dot \varphi (\ddot {x})$
for
${S}^{\circ }(\dot \varphi ,\dot u,\ddot {x})$
.
Definition 2.19 (Defining reflection).
Let T be a theory defined by a formula
$\chi (v)$
with a single free variable
$v$
.
-
(a) The theory
$T+\mathbf {Con}(T)$
is defined by
$\chi (v)\lor v={Con}^\circ _{\bar \chi }$
. -
(b) The theory
$T+\mathbf {Rfn}(T)$
is defined by
$\chi (v)\lor \vartheta (v)$
, where
$$\begin{align*}\vartheta(v) \ =_{\text{def}}\ \exists \varphi\, ({Snt}(\varphi)\land v={Pr}^\circ_{\bar\chi}( \dot \varphi)\rightarrow^\circ \varphi).\end{align*}$$
-
(c) The theory
$T+\mathbf {RFN}(T)$
is defined by
$\chi (v)\lor \vartheta (v)$
, where
$$\begin{align*}\vartheta(v) \ =_{\text{def}} \ \exists \varphi\, \exists u\, \exists x\, ({Snt}(\forall^\circ u\, \varphi) \land v=\forall^\circ x\, ({Pr}^\circ_{\bar\chi}(\dot \varphi(\ddot x))\rightarrow^\circ \varphi(x))). \end{align*}$$
Remark 2.20. If
$\varphi (u)$
is a formula containing solely the free variable
$u$
, then
$$\begin{align*}\mathbf{HA}\vdash \forall^\circ \bar x\, ({Pr}^\circ_{\bar\chi}(\dot{\bar \varphi}(\ddot {\bar x}))\to^\circ \bar{\varphi}(\bar x)))=\overline{\forall x\, ({Pr}_\chi(\bar \varphi(\dot x)) \to \varphi(x))}. \end{align*}$$
In particular,
$$\begin{align*}\mathbf{HA}\vdash \dot{\bar \varphi}(\ddot{\bar x}) = \overline{\bar\varphi(\dot x)}.\end{align*}$$
Note that
$\dot {\bar \varphi }(\ddot {\bar x})$
stands for
${S}^{\circ }(\dot {\bar \varphi },\dot {\bar u},\ddot {\bar x})$
.
2.2 Self-reference
Theorem 2.21 (Diagonal lemma).
Let
$\varphi (u,x_1,\ldots ,x_n)$
be any formula. Then there is a formula
$\nu (x_1,\ldots ,x_n)$
such that
$$\begin{align*}\mathbf{HA}\vdash \nu(x_1,\ldots,x_n)\leftrightarrow \varphi(\bar\nu, x_1,\ldots,x_n).\end{align*}$$
Proof. For ease of notation, let
$n=1$
. Fix a variable u, and take the primitive recursive function
$D\colon \mathbb {N}\to \mathbb {N}$
defined by
$$\begin{align*}D(\psi)={Sb}(\psi, u, \bar \psi). \end{align*}$$
Let
$g \ =_{\text {def}}\ \varphi (D^{\circ }(u),x)$
and let
$\nu (x)\ =_{\text {def}}\ \varphi (D^{\circ }(\bar g),x)$
.
Remark 2.22. If
$\varphi $
is
$\Sigma $
(in
$\mathbf {HA}$
), so is
$\nu $
.
Let
$T(e,x,z)$
be Kleene T-predicate with output function
$U(z)$
. Write
$\{e\}(x)\simeq y$
for
$\exists z\, (T(e,x,z)\land U(z)=y)$
and
$\{e\}_z(x)\simeq y$
for
$T(e,x,z)\land U(z)=y$
. Further abbreviations are
$\{e\}(x)\downarrow $
for
$\exists y\, (\{e\}(x)\simeq y)$
and
$\{e\}_z(x)\downarrow $
for
$T(e,x,z)$
.
Theorem 2.23 (s-m-n and recursion theorem; cf. Troelstra [Reference Troelstra22, Chap. 1, Sec. 3.10]).
Let
$m,n\geq 1$
. There are primitive recursive functions
$S^m_n$
and
$F_n$
such that
$$ \begin{align*} \mathbf{HA}& \vdash \{S^m_n(e,z_1,\ldots,z_m)\}(x_1,\ldots,x_n)\simeq \{e\}(z_1,\ldots,z_m,x_1,\ldots,x_n) \\ \mathbf{HA}& \vdash \{F_n(e)\}(x_1,\ldots,x_n)\simeq \{e\}(F_n(e),x_1,\ldots,x_n). \end{align*} $$
Remark 2.24. The s-m-n theorem is all we need to prove the recursion theorem.
Remark 2.25. We use the recursion theorem mainly to compute indices
$e$
of total recursive functions satisfying
$$\begin{align*}\mathbf{HA} \vdash \{\bar e\}(x_1,\ldots,x_n)\simeq G(\bar e,x_1\ldots,x_n),\end{align*}$$
where G is some primitive recursive function. Moreover, we repeatedly use the
$S^m_n$
functions to primitive recursively construct indices from indices.
Recall that Robinson’s
$\mathbf {Q}$
is a finite theory in the language
$0,S,+,\cdot $
. In keeping with our formulation of
$\mathbf {HA}$
, we extend
$\mathbf {Q}$
to include all primitive recursive functions. We may safely assume that
$$\begin{align*}\mathbf{HA} \vdash {Pr}_{\mathbf{Q}}(x)\rightarrow {Pr}_{\mathbf{HA}}(x), \end{align*}$$
where
${Pr}_T(x)$
denotes
${Pr}_\chi (x)$
for a standard primitive recursive presentation
$\chi (v)$
of T.
Theorem 2.26 (
$\Sigma $
completeness; cf. [Reference Visser25, Theorem 2.9]).
For every
$\Sigma $
formula
$\varphi (x_1,\ldots ,x_k)$
:
-
• if
$\varphi (\bar n_1,\ldots ,\bar n_k)$
is true, then
$\mathbf {Q}\vdash \varphi (\bar n_1,\ldots ,\bar n_k)$
; -
•
$\mathbf {HA} \vdash \varphi (x_1,\ldots ,x_k)\rightarrow {Pr}_{\mathbf {Q}}(\bar \varphi (\dot x_1,\ldots ,\dot x_k))$
.
In particular, if
$\varphi (x_1,\ldots ,x_k)$
is
$\Sigma $
in
$\mathbf {HA}$
, then
-
•
$\mathbf {HA}\vdash \varphi (x_1,\ldots ,x_k)\rightarrow {Pr}_{\mathbf {HA}}(\bar \varphi (\dot x_1,\ldots ,\dot x_k))$
.
The next theorem (its restriction to
$\Sigma $
formulas) is needed to prove the existence of transfinite recursive progressions in the sense of Theorem 2.40 (see however Remark 2.44).
Theorem 2.27 (Soundness of
$\mathbf {Q}$
; cf. Troelstra [Reference Troelstra22, Chap. 1, Sec. 5.9]).
For every formula
$\varphi (x_1,\ldots ,x_k)$
,
$$\begin{align*}\mathbf{HA} \vdash {Pr}_{\mathbf{Q}}(\bar\varphi(\dot x_1,\ldots,\dot x_k))\rightarrow \varphi(x_1,\ldots,x_k).\end{align*}$$
Convention 2.28. For our purposes, we are interested in formulas
$\chi (z,v)$
having only
$z,v$
as free variables, which can be seen as a uniform definition of theories
$T_d$
, for
$d\in \mathbb {N}$
, consisting of all sentences
$\varphi $
such that
$\chi (\bar d,\bar \varphi )$
holds. When a formula
$\chi (z,v)$
is given, we abuse notation and write
$$ \begin{align*}{Pr}(z,x) \ \text{ and } \ {Con}(z)\end{align*} $$
to denote
${Pr}_\chi (z,x)$
and
$\neg {Pr}_\chi (z,\bar \bot )$
, respectively. Similarly, we may write
${Pr}^\circ $
and
${Con}^\circ $
and omit
$\bar \chi $
.
Theorem 2.29 (I am not provable; cf. [Reference Feferman5, Theorem 2.11, p. 272]).
Let
$\chi (z,v)$
be a
$\Sigma $
formula in
$\mathbf {HA}$
having only
$z,v$
as free variables such that
$$ \begin{align} \mathbf{HA}\vdash {Pr}_{\mathbf{HA}}(x)\rightarrow {Pr}(z,x). \end{align} $$
Then there is a formula
$\nu (z)$
such that
$$ \begin{align*} \mathbf{HA} \vdash {Con}(z)\leftrightarrow \nu(z) \leftrightarrow \neg{Pr}(z,\bar \nu(\dot z)). \end{align*} $$
In particular,
$\nu (z)$
is
$\Pi _1$
in
$\mathbf {HA}$
.
Proof. By the diagonal lemma, there is a fixed point
$\nu (z)$
of the formula
$\varphi (u,z)\ =_{\text {def}}\ \neg {Pr}(z,{Sb}^\circ (u,\bar z,\dot z))$
. Then
$\mathbf {HA}\vdash \nu (z)\leftrightarrow \neg {Pr}(z,\bar \nu (\dot z))$
. In particular,
$\nu (z)$
is
$\Pi _1$
in
$\mathbf {HA}$
. Clearly,
$\mathbf {HA}\vdash \nu (z)\rightarrow {Con}(z)$
. The converse direction
$\mathbf {HA}\vdash {Con}(z)\rightarrow \nu (z)$
relies on the fact that
$$ \begin{align} \mathbf{HA}\vdash \nu(z)\leftrightarrow \forall y\, \vartheta(z,y) \end{align} $$
for some
$\Delta _0$
formula
$\vartheta $
.Footnote
10
Therefore,
$$ \begin{align}\kern-10pt \mathbf{HA}& \vdash \neg\vartheta(z,y)\rightarrow {Pr}_{\mathbf{HA}}(\overline{\neg \vartheta}(\dot z,\dot y)) & \Sigma \text{ completeness (indeed}\ \Delta_0),\end{align} $$
$$ \begin{align} \mathbf{HA}& \vdash \neg\vartheta(z,y) \rightarrow {Pr}_{\mathbf{HA}}(\overline{\neg \forall y\, \vartheta}(\dot z)) & \text{ (1),} \end{align} $$
$$ \begin{align} \mathbf{HA}&\vdash \neg\vartheta(z,y)\rightarrow {Pr}(z, \overline{\neg \forall y\, \vartheta}(\dot z)) & \text{ (2) and } (\ast), \end{align} $$
$$ \begin{align} \mathbf{HA}& \vdash {Pr}(z, \overline{\forall z\, (\nu(z) \leftrightarrow \forall y\, \vartheta(z,y)}) & \Sigma \text{ completeness from (0) and } (\ast), \end{align} $$
$$ \begin{align} \mathbf{HA}& \vdash \neg\vartheta(z,y)\rightarrow {Pr}(z, \neg^\circ\, \bar\nu(\dot z )) & \text{ (3) and (4),} \end{align} $$
$$ \begin{align} \mathbf{HA}& \vdash {Con}(z)\rightarrow \neg\vartheta(z,y)\rightarrow \neg {Pr}(z, \overline \nu(\dot z)) & \text{ (5),} \end{align} $$
$$ \begin{align} \mathbf{HA}&\vdash {Con}(z)\rightarrow \neg\vartheta(z,y)\rightarrow \nu(z) & \text{ (6) and the fixed point property,} \end{align} $$
$$ \begin{align} \mathbf{HA}&\vdash \neg\vartheta(z,y)\rightarrow \neg\nu(z) & \text{ pure logic from (0),} \end{align} $$
$$ \begin{align} \mathbf{HA}&\vdash {Con}(z)\rightarrow \forall y\, \neg\neg \vartheta(z,y) & \text{ (7) and (8) (in minimal logic),} \end{align} $$
$$ \begin{align} \mathbf{HA}&\vdash {Con}(z)\rightarrow \forall y\, \vartheta(z,y) & \text{ (9) and decidability of}\ \Delta_0 \text{ formulas}. \end{align} $$
Hence
$\mathbf {HA}\vdash {Con}(z)\rightarrow \nu (z)$
, as desired.
Theorem 2.30 (Second incompleteness).
Let
$\chi (z,v)$
be as in Theorem 2.29. Then
$$\begin{align*}\mathbf{HA}\vdash {Con}(z)\rightarrow \neg{Pr}(z, {Con}^\circ(\dot z)). \end{align*}$$
Proof.
$$ \begin{align} \mathbf{HA} &\vdash {Con}(z)\rightarrow \neg {Pr}(z,\bar \nu(\dot z)) & \text{ Theorem}\ 2.29, \end{align} $$
$$ \begin{align} \mathbf{HA}& \vdash {Con}(z)\rightarrow \nu(z) & \text{ Theorem}\ 2.29, \end{align} $$
$$ \begin{align} \mathbf{HA} & \vdash {Pr}_{\mathbf{HA}}(\overline{\forall z\, ({Con}(z)\rightarrow \nu(z))}) & \Sigma \text{ completeness from (2),} \end{align} $$
$$ \begin{align} \mathbf{HA}&\vdash {Pr}_{\mathbf{HA}}({Con}^\circ(\dot z)\rightarrow^\circ \bar\nu(\dot z)) & \text{ (3),} \end{align} $$
$$ \begin{align} \mathbf{HA}&\vdash {Pr}(z,{Con}^\circ(\dot z)\rightarrow^\circ \bar\nu(\dot z)) & \text{ (4) and} (\ast), \end{align} $$
$$ \begin{align} \mathbf{HA}& \vdash {Pr}(z,{Con}^\circ(\dot z))\rightarrow {Pr}(z,\bar\nu(\dot z)) & \text{ (5),} \end{align} $$
$$ \begin{align} \mathbf{HA}&\vdash {Con}(z)\rightarrow \neg{Pr}(z, {Con}^\circ(\dot z)) & \text{ (1) and (6).} \end{align} $$
Remark 2.31. The two results above could be transferred from
$\mathbf {PA}$
to
$\mathbf {HA}$
, owing to the fact that they prove the same
$\Pi _2$
statements. In fact,
$$\begin{align*}{Con}(z)\rightarrow \nu(z) \quad \text{ and } \quad {Con}(z)\rightarrow \neg{Pr}(z, {Con}^\circ(\dot z)) \end{align*}$$
are both equivalent in
$\mathbf {HA}$
to a statement of the form
$$ \begin{align} \forall x\, \varphi(x)\rightarrow \forall x\, \psi(x), \end{align} $$
which is classically equivalent to
$$ \begin{align} \forall x\, \exists y\, (\varphi(y)\rightarrow \psi(x)). \end{align} $$
On the other hand, the implication from
$(\ast \ast )$
to
$(\ast )$
holds intuitionistically.
Theorem 2.32 (Löb’s theorem for
$\Pi _2$
formulas).
Let
$\varphi $
be
$\Pi _2$
in
$\mathbf {HA}$
. Then
$$ \begin{align*} &\mathbf{HA}\vdash {Pr}_{\mathbf{HA}}(\bar\varphi)\rightarrow \varphi \quad\text{iff} \quad \mathbf{HA}\vdash \varphi. \end{align*} $$
Proof. Notice that this holds for any formula in the case of
$\mathbf {PA}$
. On the other hand,
$\mathbf {PA}$
is
$\Pi _2$
-conservative over
$\mathbf {HA}$
and the proof of this fact via negative translation coupled with Friedman A-translation formalizes in
$\mathbf {HA}$
. The theorem thus follows from Löb’s theorem for
$\mathbf {PA}$
.
2.3 Kleene’s
$\mathcal {O}$
Let us recall Kleene’s notation system
$(\mathcal {O},<_{\mathcal {O}})$
for constructive ordinals. The set
$\mathcal {O}$
consists of natural numbers which are notations for all recursive ordinals. Moreover,
$<_{\mathcal {O}}$
is a well-founded partial order on
$\mathcal {O}$
such that
$a<_{\mathcal {O}} b$
implies
$|a|<|b|$
, where
$|a|$
is the recursive ordinal denoted by a.
Definition 2.33. The sets
$\mathcal {O}$
and
$<_{\mathcal {O}}$
are defined inductively by:
-
•
$0\in \mathcal {O}$
; -
• if
$d\in \mathcal {O}$
, then
$2^d\in \mathcal {O}$
and
$d<_{\mathcal {O}} 2^d$
; -
• if e is the index of a total recursive function and
$\{e\}(n)<_{\mathcal {O}} \{e\}(n+1)$
for every n, then
$3\cdot 5^e\in \mathcal {O}$
and
$\{e\}(n)<_{\mathcal {O}} 3\cdot 5^e$
for every n; -
• if
$a<_{\mathcal {O}} b<_{\mathcal {O}} c$
then
$a<_{\mathcal {O}} c$
.
We write
$a\leq _{\mathcal {O}} b$
for
$a<_{\mathcal {O}} b \lor a=b$
.
Proposition 2.34 (Properties of
$<_{\mathcal {O}}$
).
The following properties hold:
-
• if
$a<_{\mathcal {O}} b$
then
$a,b\in \mathcal {O}$
; -
• if
$a\in \mathcal {O}$
then
$0\leq _{\mathcal {O}} a$
; -
• if
$a<_{\mathcal {O}} b$
then
$b\notin \{0,a\}$
; -
• if
$a<_{\mathcal {O}} 2^b$
then
$a\leq _{\mathcal {O}} b$
; -
• if
$a<_{\mathcal {O}} b$
then
$2^a\leq _{\mathcal {O}} b$
; -
• if
$a<_{\mathcal {O}} 3\cdot 5^e$
then
$a<_{\mathcal {O}} \{e\}(n)$
for some n.
For technical reasons (see Lemma 4.4), it will be convenient to define addition as follows.Footnote 11
Proposition 2.35. There is a total recursive function
${+}_{\mathcal {O}}$
such that:
$$\begin{align*}a+_{\mathcal{O}} b\simeq \begin{cases} a & b=0 \\ 2^{a+_{\mathcal{O}} c} & b=2^c\\ 3\cdot 5^{H(a,e)} & b=3\cdot 5^e, \text{where } \{H(a,e)\}(n)\simeq a+_{\mathcal{O}} 2^{\{e\}(n)} \\ 7 & \text{otherwise}. \end{cases} \end{align*}$$
Proof. By the recursion theorem.
Remark 2.36. The function F such that
$F(a,b)=a+_{\mathcal {O}} b$
is primitive recursive.
Proposition 2.37 (Properties of
$+_\mathcal {O}$
).
The following properties hold:
-
•
$a,b\in \mathcal {O}$
iff
$a+_\mathcal {O} b\in \mathcal {O}$
; -
• if
$a,b\in \mathcal {O}$
and
$b\neq 0$
then
$a<_{\mathcal {O}} a+_{\mathcal {O}} b$
; -
•
$a\in \mathcal {O}$
and
$b<_{\mathcal {O}} c$
iff
$a+_{\mathcal {O}} b<_{\mathcal {O}} a+_{\mathcal {O}} c$
;
Definition 2.38. Let
$0_{\mathcal {O}}=0$
and
$(n+1)_{\mathcal {O}}= 2^{n_{\mathcal {O}}}$
. Note that
$a+_{\mathcal {O}} n_{\mathcal {O}}<_{\mathcal {O}} a+_{\mathcal {O}} m_{\mathcal {O}}$
for every
$a\in \mathcal {O}$
and for all
$n<m$
.
We use association to the left and thus write
$a+_{\mathcal {O}} b+_{\mathcal {O}} c$
for
$(a+_{\mathcal {O}} b)+_{\mathcal {O}} c$
.
2.4 Transfinite recursive progressions
Let us fix a standard primitive recursive presentation
$\chi _0(v)$
of
$\mathbf {HA}$
. Let
${Pr}_{\mathbf {HA}}(x)$
be the corresponding provability predicate.
Definition 2.39 (Progression and succession formulas).
Let
$\chi (z,v)$
and
$\rho (u,z,v)$
be
$\Sigma $
formulas. We say that
$\chi (z,v)$
is a progression formula based on
$\rho (u,z,v)$
if
$$ \begin{align*} \mathbf{HA} \vdash& \ \chi_0(v)\rightarrow \chi(z,v), \\ \mathbf{HA} \vdash & \ \chi(0,v) \leftrightarrow \chi_0(v), \\ \mathbf{HA} \vdash & \ \chi(2^d,v) \leftrightarrow \chi(d,v)\lor \rho(\bar\chi,d,v), \\ \mathbf{HA} \vdash & \ \chi(3\cdot 5^e,v) \leftrightarrow \chi_0(v)\lor \exists n\, \exists d\, \big(\{e\}(n)\simeq d\land \chi(d,v))\big). \end{align*} $$
In this context,
$\rho (u,z,v)$
is called a succession formula.
Theorem 2.40 (Existence).
Let
$\rho (u,z,v)$
be
$\Sigma $
. Then there is a
$\Sigma $
progression formula
$\chi (z,v)$
based on
$\rho (u,z,v)$
.
Proof. By the diagonal lemma (Theorem 2.21), there is a fixed point
$\chi (z,v)$
of the formula
$\varphi (u,z,v)$
so that
$\mathbf {HA}\vdash \chi (z,v)\leftrightarrow \varphi (\bar \chi ,z,v)$
, where
$$ \begin{align*} \varphi(u,z,v)\ =_{\text{def}}\ (\varphi_0(z)\land \chi_0(v)) \lor \exists d\, (z=2^d\land \varphi_1(u,d,v))\lor \exists e\, (z=3\cdot 5^e\land \varphi_2(u,e,v)), \end{align*} $$
and
$$ \begin{align*} \varphi_0(z)\ &=_{\text{def}} \ z=0\lor \forall w<z\, (z\neq 2^w\land z\neq 3\cdot 5^w), \\ \varphi_1(u,d,v)\ &=_{\text{def}} \ \xi(u,d,v)\lor \rho(u,d,v),\\ \varphi_2(u,e,v)\ &=_{\text{def}} \ \chi_0(v)\lor \exists n\, \exists d\, (\{e\}(n)\simeq d\land \xi(u,d,v)) \end{align*} $$
with
$\xi (u,d,v)\ =_{\text {def}}\ {Pr}_{\mathbf {Q}}(u(\dot d,\dot v))$
. Since
$\varphi (u,z,v)$
is
$\Sigma $
, so is
$\chi (z,v)$
. The first item in the definition of progression formula is proved by ordinary induction on z. The rest follows by completeness (Theorem 2.26) and soundness (Theorem 2.27).
Lemma 2.41. Let
$\chi (z,v)$
be a progression formula based on
$\rho (u,z,v)$
. Then
$$ \begin{align*} \mathbf{HA} &\vdash \ {Pr}_{\mathbf{HA}}(x)\rightarrow {Pr}(z,x), \\ \mathbf{HA} &\vdash \ {Pr}(z,x)\rightarrow {Pr}(2^z,x), \\ \mathbf{HA} &\vdash \ \{e\}(n)\simeq z\rightarrow \chi(z,v)\rightarrow \chi(3\cdot 5^e,v), \\ \mathbf{HA} & \vdash \ \{e\}(n)\simeq z\rightarrow {Pr}(z,x)\rightarrow {Pr}(3\cdot 5^e,x). \end{align*} $$
Definition 2.42 (Progression).
Let
$\chi (z,v)$
be a progression formula based on
$\rho (u,z,v)$
. For
$d\in \mathbb {N}$
, let
$T_{d}=\{\varphi \mid \chi (\bar d,\bar \varphi ) \text { is true}\}$
. We call
$(T_d)_{d\in \mathbb {N}}$
a progression over
$\mathbf {HA}$
based on
$\rho (u,z,v)$
.
Theorem 2.43. Let
$(T_d)_{d\in \mathbb {N}}$
be a progression over
$\mathbf {HA}$
based on the
$\Sigma $
formula
$\rho (u,z,v)$
. Then
$(T_{d})_{d\in \mathbb {N}}$
is a recursively enumerable sequence of theories such that:
-
•
$\mathbf {HA}=T_0\subseteq T_d$
for every
$d$
; -
•
$a<_{\mathcal {O}} b$
implies
$T_a\subseteq T_b$
; -
•
$T_{3\cdot 5^e}=\bigcup _{d<_{\mathcal {O}} 3\cdot 5^e} T_d$
whenever
$3\cdot 5^e\in \mathcal {O}$
.
Proof. The second item is proved by induction on
$<_{\mathcal {O}}$
.
Remark 2.44. A close inspection reveals that we could do without Theorem 2.27. In fact, if
$\rho (u,z,v)$
is
$\Sigma $
in
$\mathbf {HA}$
, by the diagonal lemma we can obtain a formula
$\chi (z,v)$
such that
$\chi (z,v)$
is
$\Sigma $
in
$\mathbf {HA}$
and
$$ \begin{align*} \mathbf{HA} \vdash& \ \chi_0(v)\rightarrow \chi(z,v), \\ \mathbf{HA} \vdash & \ \chi(0,v) \leftrightarrow \chi_0(v), \\ \mathbf{HA} \vdash & \ \chi(2^z,v) \leftrightarrow {Pr}_{\mathbf{HA}}(\bar \chi(\dot z,\dot v))\lor \rho(\bar\chi,z,v), \\ \mathbf{HA} \vdash & \ \chi(3\cdot 5^e,v) \leftrightarrow \chi_0(v)\lor \exists n\, \exists z\, \big(\{e\}(n)\simeq z\land {Pr}_{\mathbf{HA}}(\bar \chi(\dot z,\dot v))\big). \end{align*} $$
The formula
$\chi (z,v)$
would still satisfy Lemma 2.41 and Theorem 2.43.
Definition 2.45 (Succession formulas for reflection).
Let
$$\begin{align*}\rho(\chi,z,v)\ =_{\text{def}}\ \ v={Con}^\circ_\chi(\dot z)\end{align*}$$
be the succession formula for consistency.
Let
$$\begin{align*}\rho(\chi,z,v)\ =_{\text{def}}\ v= \exists \varphi\, ({Snt}(\varphi) \land v= {Pr}^{\circ}_\chi(\dot z, \dot \varphi)\rightarrow^\circ \varphi)\end{align*}$$
be the succession formula for local reflection.
Let
$$\begin{align*}\rho(\chi,z,v)\ =_{\text{def}}\ \exists \varphi\, \exists u\, \exists x\, \big({Snt}(\forall^\circ u\, \varphi) \land v=\forall^\circ x\, ({Pr}^\circ_\chi(\dot z, \dot \varphi(\ddot x))\rightarrow^\circ \varphi(x))\big) \end{align*}$$
be the succession formula for uniform reflection.
Remark 2.46. Let
$(T_d)_{d\in \mathbb {N}}$
be a progression based on the succession formula for consistency. Then
$T_{2^d}=T_d+\mathbf {Con}(T_d)$
for every
$d$
. Notice that
$d$
need not be in Kleene’s
$\mathcal {O}$
. Similarly for local and uniform reflection.
Definition 2.47. We say that a formula
$\varphi $
is provable in an iteration of consistency over
$\mathbf {HA}$
if there exists a
$d\in \mathcal {O}$
such that
$T_d\vdash \varphi $
, for some fixed progression
$(T_d)_{d\in \mathbb {N}}$
based on the succession formula for consistency. Similarly for local and uniform reflection.
3 Iterating consistency or local reflection
Theorem 3.1 (Local reflection).
Let
$\varphi $
be a formula. The following are equivalent:
-
(1)
$\varphi $
is provable in an iteration of consistency over
$\mathbf {HA}$
; -
(2)
$\varphi $
is provable in an iteration of local reflection over
$\mathbf {HA}$
; -
(3)
$\varphi $
is provable in
$\mathbf {HA} +$
all true
$\Pi _1$
sentences.
Proof. Clearly (1)
$\Rightarrow $
(2). Let T be the extension of
$\mathbf {HA}$
with all true
$\Pi _1$
sentences.
(2)
$\Rightarrow $
(3) is proved exactly as in [Reference Feferman5, Theorem 4.5, p. 289]. One proves that
$T_d\subseteq \{\varphi \mid T\vdash \varphi \}$
by induction on
$d\in \mathcal {O}$
, where
$(T_d)_{d\in \mathbb {N}}$
is a progression over
$\mathbf {HA}$
based on local reflection. The cases
$d=0$
and
$d=3\cdot 5^e$
are immediate. For the successor case it suffices to show that
$T\vdash {Pr}(\bar d,\bar \varphi )\rightarrow \varphi $
for every sentence
$\varphi $
assuming that T proves all theorems of
$T_d$
. Denote
${Pr}(\bar d,\bar \varphi )$
by
$\zeta $
. The sentence
$\neg \zeta $
is
$\Pi _1$
in
$\mathbf {HA}$
. We now have two cases. Case (i)
$T_d\vdash \varphi $
. Then by induction,
$T\vdash \varphi $
and hence
$T\vdash \zeta \rightarrow \varphi $
. Case (ii)
$T_d\nvdash \varphi $
. Then
$\neg \zeta $
is true and hence
$T\vdash \neg \zeta $
. Also in this case we have
$T\vdash \zeta \rightarrow \varphi $
. Notice that:
-
• in case (ii) we use explosion (ex falso) and hence such proof does not extend to, for example, minimal logic;
-
• the case distinction between (i) and (ii), although classical, takes place at the meta level.
(3)
$\Rightarrow $
(1) is a verbatim copy of [Reference Feferman5, Theorem 4.1, p. 287] once we have Theorem 2.30. We reproduce the argument for the sake of the reader. Let
$(T_d)_{d\in \mathbb {N}}$
be a progression over
$\mathbf {HA}$
based on consistency. Let
$\forall x\, \vartheta (x)$
be a
$\Pi _1$
sentence, where
$\vartheta (x)$
is
$\Delta _0$
. By the recursion theorem we can find e such that
$$\begin{align*}\{e\}(n)\simeq \begin{cases} n_{\mathcal{O}} & \text{ if } \forall x\leq n\, \vartheta(x);\\ 2^{3\cdot 5^e} & \text{ otherwise.} \end{cases} \end{align*}$$
We observe that if
$\forall x\, \vartheta (x)$
is true, then
$d=3\cdot 5^e\in \mathcal {O}$
and so
$2^d\in \mathcal {O}$
. We aim to prove that
$T_{2^d}\vdash \forall x\, \vartheta (x)$
, whenever
$\forall x\, \vartheta (x)$
is true. Actually, we will show that
$T_{2^d}\vdash \forall x\, \vartheta (x)$
in any case. This means that if
$\forall x\, \vartheta (x)$
is false, then
$2^d\notin \mathcal {O}$
and
$T_{2^d}$
proves a false
$\Pi _1$
statement.
Claim. If
$\exists x\, \neg \vartheta (x)$
is true, then
$T_d\vdash {Con}(\bar d)$
.
Proof of claim.
If
$\exists x\ \neg \vartheta (x)$
is true, then
$T_{2^d}=T_d$
. By construction,
$T_{2^d}\vdash {Con}(\bar d)$
.
The claim is provable in
$\mathbf {HA}$
.
Claim.
.
Proof of claim.
By the recursion theorem in
$\mathbf {HA}$
, the definition of e carries over to
$\mathbf {HA}$
. In particular,
$$ \begin{align} \ \mathbf{HA} &\vdash \{\bar e\}(n)\simeq 2^{\bar d} \leftrightarrow \exists x\leq n\, \neg\vartheta(x). \end{align} $$
Hence:
$$ \begin{align} &\mathbf{HA} \vdash \{\bar e\}(n)\simeq z \rightarrow {Pr}(z,x)\rightarrow {Pr}(3\cdot 5^{\bar e},x) & \text{ Lemma}\ 2.41, \end{align} $$
$$ \begin{align} &\mathbf{HA} \vdash \exists x\, \neg \vartheta(x) \rightarrow {Pr}( 2^{\bar d},x)\rightarrow {Pr}(\bar d,x) & \text{ (0) and (1)}, \end{align} $$
By Lemma 2.41,
$\chi (z,v)$
satisfies the requirements of Theorem 2.30. This means that
$\mathbf {HA}\vdash {Con}(z)\rightarrow \neg {Pr}(z, {Con}^\circ (\dot z))$
. Thus 
. Since
$\mathbf {HA}\subseteq T_{2^d}$
and
$T_{2^d}\vdash {Con}(\bar d)$
, we then obtain 
, and so by (4) it follows that
$T_{2^d}\vdash \forall x\, \vartheta (x)$
, as desired.
4 Iterating uniform reflection
We start by defining codes of recursive
$\omega $
-proofs.
Definition 4.1. For a natural number
$a$
, let
$$\begin{align*}\varphi_a= \begin{cases} \varphi & \text{ if } a=2^\varphi\cdot b, \text{ where } \varphi \text{ is a formula and } 2 \text{ does not divide } b; \\ \bot & \text{ otherwise.} \end{cases} \end{align*}$$
Let
$$\begin{align*}Q_{axiom}(n)=2^n, \qquad Q_\omega(n,e)=2^n\cdot 3\cdot 5^e,\qquad Q_{rule}(n,b)=2^n\cdot 3^2\cdot 5^b. \end{align*}$$
Let
$$\begin{align*}Q_{rep}(n,e,m,z)= 2^n\cdot 3^3\cdot 5^e\cdot 7^m\cdot 11^z.\end{align*}$$
The role of
$Q_{rep}$
(repetition) will become clear in the proof of Theorem 4.3.
Definition 4.2 (Recursive
$\omega $
-rule).
Let
$p_n$
be the
$n$
-th prime number. The set
$\mathcal {P}$
is defined inductively by the following clauses:
-
• (axioms) if
$\varphi $
is a logical axiom or an axiom of
$\mathbf {HA}$
, then
$Q_{axiom}(\varphi )\in \mathcal {P}$
; -
• (
$\omega $
-rule) if
$e$
is the index of a total recursive function,
$\{e\}(n)\in \mathcal {P}$
and
$\varphi _{\{e\}(n)}\simeq \varphi (\bar n)$
for every
$n$
, then
$Q_\omega (\forall x\, \varphi (x), e) \in \mathcal {P}$
; -
• (logical rules) if
$\varphi $
follows from
$\varphi _0,\ldots ,\varphi _k$
by means of a logical rule and
$a_0,\ldots ,a_k\in \mathcal {P}$
with
$\varphi _{a_i}=\varphi _i$
for all
$i\leq k$
, then
$Q_{rule}(\varphi , b)\in \mathcal {P}$
, where
$b= p_0^{a_0}\ldots p_k^{a_k}$
.Footnote
12
We say that
$\varphi $
has a proof in
$\mathcal {P}$
if there is some
$a\in \mathcal {P}$
with
$\varphi _a=\varphi $
.
We can now state Dragalin’s theorem.
Theorem 4.3 (Uniform reflection).
Let
$\varphi $
be a formula. The following are equivalent:
-
(1)
$\varphi $
is provable in an iteration of uniform reflection over
$\mathbf {HA}$
; -
(2)
$\varphi $
has a proof in
$\mathcal {P}$
.
The rest of the section is devoted to proving Theorem 4.3. From now on, we fix a progression
$(T_d)_{d\in \mathbb {N}}$
over
$\mathbf {HA}$
based on uniform reflection.
4.1 Forth
We start with the easy implication.
Proof of
$(1) \Rightarrow (2)$
of Theorem 4.3.
We claim that there is an index g of a partial recursive function such that if d is in Kleene’s
$\mathcal {O}$
and
$T_d\vdash \varphi $
, then
$\{g\}(d,\varphi )$
is defined and
$\{g\}(d,\varphi )$
is a proof of
$\varphi $
in
$\mathcal {P}$
. The index g can be found with the aid of the recursion theorem. We only indicate how to look effectively for a proof of
$$\begin{align*}\forall x\, ({Pr}(\bar d,\bar \varphi(\dot x))\rightarrow\varphi(x)) \end{align*}$$
uniformly in d and
$\varphi (x)$
. The search will succeed if
$d\in \mathcal {O}$
. Let
$\zeta (x)$
be
${Pr}(\bar d,\bar \varphi (\dot x))\rightarrow \varphi (x)$
. One can find a
$\Delta _0$
formula
$\vartheta (x,y)$
such that
$$\begin{align*}\mathbf{HA} \vdash \exists y\, \vartheta(x,y)\leftrightarrow {Pr}(\bar d,\bar \varphi(\dot x)). \end{align*}$$
One can therefore construct, effectively in n, a proof in
$\mathbf {HA}$
and so a proof
$c_n$
in
$\mathcal {P}$
of
$$\begin{align*}\forall y\, (\vartheta(\bar n,y)\rightarrow \varphi(\bar n)) \rightarrow \zeta(\bar n). \end{align*}$$
Effectively in m, one can decide whether
$\vartheta (\bar n, \bar m)$
is true. If it is true, then
$T_d\vdash \varphi (\bar n)$
. In this case one computes
$\{g\}(d,\varphi (\bar n))$
. If it is not true, then there is a proof in
$\mathbf {HA}$
and so a proof
$d_{nm}$
in
$\mathcal {P}$
of
$\vartheta (\bar n,\bar m)\rightarrow \varphi (\bar n)$
. So let
$$\begin{align*}\{g\}(d,\forall x\, \zeta(x))\simeq Q_\omega(\forall x\, \zeta(x),e),\end{align*}$$
where
$$\begin{align*}\{e\}(n)\simeq Q_{rule}(\zeta(\bar n),a_n), \ \ \ a_n = 2^{b_n} \cdot 3^{c_n}, \ \ \ b_n= Q_\omega(\forall y\, (\vartheta(\bar n,y)\rightarrow \varphi(\bar n)), h_n) \end{align*}$$
and
$$\begin{align*}\{h_n\}(m)\simeq \begin{cases} H_{nm}(\{g\}(d,\varphi(\bar n))) & \text{ if } \vartheta(\bar n,\bar m); \\ d_{nm} & \text{ otherwise.} \end{cases} \end{align*}$$
Here,
$H_{nm}$
is a total recursive function such that if a is a proof of
$\varphi (\bar n)$
in
$\mathcal {P}$
then
$H_{nm}(a)$
is a proof of
$\vartheta (\bar n,\bar m)\rightarrow \varphi (\bar n)$
in
$\mathcal {P}$
.
4.2 Back
The hard part is
$(2)\Rightarrow (1)$
. We could try to define a partial recursive function g and then prove by induction on
$\mathcal {P}$
that
$g(a)$
is defined,
$g(a)\in \mathcal {O}$
and
$T_{g(a)}\vdash \varphi $
whenever
$a\in \mathcal {P}$
is a proof of
$\varphi $
. This is exactly how we handled
$(1)\Rightarrow (2)$
. Let’s see where this approach breaks down. The cases
$a=Q_{axiom}(\varphi )$
and
$a=Q_{rule}(\varphi ,b)$
can be easily dealt with, by letting
$g(a)\simeq 0$
in the first case and
$$\begin{align*}g(a)\simeq g(b_0)+_{\mathcal{O}}\dots +_{\mathcal{O}} g(b_k)\end{align*}$$
in the second case, where
$b=p_0^{b_0}\ldots p_k^{b_k}$
. Suppose that
$a=Q_\omega (\forall x\, \varphi (x),e)$
. By induction on
$\mathcal {P}$
, we could assume that, for every n,
$\{s\}(n)\in \mathcal {O}$
and
$T_{\{s\}(n)}\vdash \varphi (\bar n)$
, where
$$\begin{align*}\{s\}(n)\simeq 2^{g(\{e\}(0))}+_{\mathcal{O}}\dots +_{\mathcal{O}} 2^{g(\{e\}(n))}.\end{align*}$$
This would imply that
$d=3\cdot 5^{s}\in \mathcal {O}$
and
$T_{d}\vdash \varphi (\bar n)$
, for every n. In that case, uniform reflection would give
$T_{2^d}\vdash \forall x\, \varphi (x)$
if there were a proof in
$T_{2^d}$
of
$\forall x\, {Pr}(\bar d,\bar \varphi (\dot x))$
. We could then let
$g(a)\simeq 2^d$
. However, the induction hypothesis is too weak and does not grant us that much.
How do we fix this? Simply put, we avoid induction on
$\mathcal {O}$
and prove everything inside
$\mathbf {HA}$
. Indeed, we are able to define a total recursive function g within
$\mathbf {HA}$
(cf. Definition 4.8) such that
$$\begin{align*}\mathbf{HA}\vdash \forall a\, {Pr}(g(a),\varphi_a). \end{align*}$$
The idea, in a nutshell, is that every natural number a can be regarded as (the code of) a locally correct primitive recursive
$\omega $
-proof with repetitions of the formula
$\varphi _a$
. A repetition is an inference of the form “
$\varphi $
follows from
$\varphi $
.” More in detail, given any natural number a, we can build a primitive recursive tree S (cf. Definition 4.7) such that the root has label a and
$T_{g(b)}\vdash \varphi _b$
for every node in S with label b. The tree S encodes a possibly ill-founded
$\omega $
-proof with repetitions. We use repetitions to handle, in particular, applications of the
$\omega $
-rule. If a node carries a label of the form
$$ \begin{align*}Q_\omega(\forall x\, \varphi(x),e),\end{align*} $$
then for every
$n\in \mathbb {N}$
we branch above by adding nodes labeled
$$ \begin{align*}Q_{rep}(\varphi(\bar n),e,n,s)\end{align*} $$
and wait to see whether
$\{e\}(n)$
converges within s steps. If
$\{e\}_s(n)$
does not converge, we add another node with label
$Q_{rep}(\varphi (\bar n),e,n,s+1)$
. If
$\{e\}_s(n)$
does converge but not to something that looks like (the code of) a recursive
$\omega $
-proof of
$\varphi (\bar n)$
, we iterate that node upward ad infinitum.
Our plan is define the index g of a total recursive function such that:
-
(1.1) if
$a\in \mathcal {P}$
is a proof of
$\varphi $
then
$\{g\}(a)\in \mathcal {O}$
and
$\varphi _a=\varphi $
; -
(1.2)
$T_{\{g\}(a)}\vdash \varphi _a$
for every a (a need not be in
$\mathcal {P}$
).
To prove (1.2), we ensure that g is the index of a total recursive function within
$\mathbf {HA}$
:
$$ \begin{align*}\mathbf{HA}\vdash \forall a\, \exists d\, (\{\bar g\}(a)\simeq d),\end{align*} $$
and that
$\mathbf {HA}$
proves the formalized version of (1.2):
$$ \begin{align} \mathbf{HA} \vdash \forall a\, {Pr}(\{\bar g\}(a),\varphi_a). \end{align} $$
We use Löb’s theorem in
$\mathbf {HA}$
for
$\Pi _2$
sentences (Theorem 2.32) to prove (
$\ast $
). Namely, we show
$$ \begin{align} \mathbf{HA}\vdash {Pr}_{\mathbf{HA}}(\bar k)\rightarrow k, \ \text{ where }\ k \ = _{\text{def}}\ \forall a\, {Pr}(\{\bar g\}(a),\varphi_a). \end{align} $$
In the rest of this section we carry out the plan just outlined.
Although we can define
$+_\mathcal {O}$
in
$\mathbf {HA}$
, most of its properties can only be verified by induction on
$\mathcal {O}$
, and so are not available in
$\mathbf {HA}$
. Crucially, we can establish the following by applying Löb’s theorem.
Lemma 4.4.
$\mathbf {HA}\vdash {Pr}(b,x)\rightarrow {Pr}(a+_{\mathcal {O}} b,x)$
.
Proof. Note that by induction on
$\mathcal {O}$
one can easily prove that
$T_b\subseteq T_{a+_{\mathcal {O}} b}$
, whenever
$a+_{\mathcal {O}} b\in \mathcal {O}$
. Moreover, this is true of any recursive progression in the sense of Theorem 2.43. For this lemma, local reflection is indeed sufficient. The sentence we are trying to prove is
$\Pi _2$
in
$\mathbf {HA}$
. We can then use Löb’s theorem 2.32. Let
$\zeta (c,a,b)$
be the
$\Sigma $
formula
$c=a+_{\mathcal {O}} b$
.
We now reason in
$\mathbf {HA}$
and proceed by ordinary induction on b. The cases
$b=0$
and
$b=2^c$
are straightforward: they immediately follow from the induction hypothesis and the definition of
$+_\mathcal {O}$
. Suppose
$b=3\cdot 5^e$
and
${Pr}(b,x)$
. We aim to show
${Pr}(c,x)$
, where
$c=a+_{\mathcal {O}} b$
. By Remark 2.8, it suffices to treat the case
$\chi (b,x)$
, since provability is (provably) closed under logic.
Recall that
$c=3\cdot 5^l$
, where
$\{l\}(n)\simeq a+_{\mathcal {O}} 2^{\{e\}(n)}$
. We are going to use the hypothesis
$$ \begin{align} {Pr}_{\mathbf{HA}}(\bar h ), \ \text{ where }\ h\ =_{\text{def}}\ \forall a\, \forall b\, \forall c\, \forall x\, ({Pr}(b,x)\land \zeta(c,a,b) \rightarrow {Pr}(c,x)). \end{align} $$
By construction, if
$\chi (b,x)$
then
$\{e\}(n)\simeq z$
and
$\chi (z,x)$
for some n and z. In particular,
${Pr}(z,x)$
. Let
$d=a+_{\mathcal {O}} z$
. By
$\Sigma $
completeness,
${Pr}_{\mathbf {HA}}({Pr}^\circ (\dot z,\dot x)\land \bar \zeta (\dot d,\dot a,\dot z))$
. It follows by (
$\ast $
) that
${Pr}_{\mathbf {HA}}({Pr}^\circ (\dot d,\dot x))$
. By Lemma 2.41,
${Pr}(2^d,{Pr}^\circ (\dot d,\dot x))$
, and hence by (local) reflection
${Pr}(2^d, x)$
. By definition,
$\{l\}(n)\simeq a+_{\mathcal {O}} 2^z= 2^{a+_{\mathcal {O}} z}=2^d$
. Thus
${Pr}(\{l\}(n), x)$
. By Lemma 2.41, we finally obtain
${Pr}(c,x)$
, as desired.
Definition 4.5. There is a primitive recursive function L such that
$$ \begin{align*} \{L(e)\}(n) &\simeq 2^{\{e\}(0)}+_{\mathcal{O}}\dots +_{\mathcal{O}} 2^{\{e\}(n)}. \end{align*} $$
Let
$G(e)=3\cdot 5^{L(e)}$
. Note that the definition of G carries over to
$\mathbf {HA}$
.
Lemma 4.6. Let G be as above. Then the following hold:
-
(i) if
$\{e\}(n)\in \mathcal {O}$
for every n, then
$G(e)\in \mathcal {O}$
; -
(ii)
$\mathbf {HA}\vdash (\forall n\, \{e\}(n)\downarrow ) \rightarrow (\{e\}(n)\simeq z \land {Pr}(z,x))\rightarrow {Pr}(G(e),x)$
.
Definition 4.7 (The unfolding of a proof).
Let S be the primitive recursive function defined by
$$\begin{align*}S(a,n) = \begin{cases} 0 & \text{if } a=Q_{axiom}(\varphi) \text{ and } \varphi \text{ is a logical axiom or an axiom of } \mathbf{HA} \\
& (a \text{ is axiomatic);} \\
%Q_{rep}(\varphi(\bar n),e,n,0) & \text{if } a=Q_{\omega}(\forall x \varphi(x),e) (a \text{ is universal);} \\
%Q_{rep}(\varphi,e,m,z+1) & \text{if } a= Q_{rep}(\varphi,e,m,z) \text{ with } \varphi_{a}=\varphi \text{ and } \{e\}_{z}(m) \text{ is undefined;} \\
%b & \text{if } a= Q_{rep}(\varphi,e,m,z) \text{ and } \{e\}_{z}(m)\simeq b \text{ and } \varphi_{b}= \varphi;\\
%2^{\varphi} & \text{if } a= Q_{rep}(\varphi,e,m,z) \text{ with } \varphi_{a}=\varphi \text{ and } \{e\}_{z}(m)\simeq b \\
%& \text{ with }\varphi_{b}\neq \varphi; \\
%a_{n} & \text{if } a=Q_{rule}(\varphi,a) \text{ and } a=p_{0}^{a_{0}}\ldots p_{k}^{a_{k}} \text{ with } \\
%& \quad \varphi_{a_{i}}=\varphi_{i} \text{ for every } i\leq k \text{ and } \varphi \text{ follows from } \\
%& \varphi_{0},\ldots,\varphi_{k} \text{ by means of a logical rule and } n\leq k \\
%& (a \text{ is an inference of arity } k); \\
2^{\varphi_{a}} & \text{if none of the above holds.} \end{cases} \end{align*}$$
We say that
$a$
is a repetition if
$a$
is neither axiomatic nor universal nor an inference.
Definition 4.8. By the recursion theorem we can find
$g$
such that
$$\begin{align*}\{g\}(a) \simeq \begin{cases} 0 & a \text{ is axiomatic;} \\ 2^{G(H(g,a))} & a \text{ is universal;} \\ 2^{G(I(g,a))} & a \text{ is an inference of arity k;} \\ 2^{3\cdot 5^{J(g,a)}} & a \text{ is a repetition.} \end{cases} \end{align*}$$
Here,
$$ \begin{align*} \{H(g,a)\}(n) &\simeq \{g\}(S(a,n)), \\ \{I(g,a)\}(n) & \simeq \begin{cases} \{g\}(S(a,n)) & \text{if } n\leq k;\\ 0 & \text{otherwise,} \end{cases} \\ \{J(g,a)\}(n)& \simeq \{g\}(S(a,0))+_{\mathcal{O}} n_{\mathcal{O}}. \end{align*} $$
Notice that g is the index of a total recursive function.
Lemma 4.9. Let
$g$
be as above. If
$a\in \mathcal {P}$
, then
$\{g\}(a)\in \mathcal {O}$
.
Proof. The proof is by induction on
$\mathcal {P}$
. We first observe that if
$a\in \mathcal {P}$
, then a is either axiomatic, universal or an inference. The cases where a is axiomatic or an inference are straightforward. Suppose a is universal, say
$a= Q_\omega (\forall x\, \varphi (x),e)$
. By Lemma 4.6 part (i) and the definition of g, it suffices to show that
$\{g\}(S(a,n))\in \mathcal {O}$
for every n. Fix n and let
$a_{z}= Q_{rep}(\varphi (\bar n),e,n,z)$
. Since
$a\in \mathcal {P}$
, we have that
$\{e\}(n)\simeq b$
for some
$b\in \mathcal {P}$
. By induction on
$\mathcal {P}$
, we can assume
$\{g\}(b)\in \mathcal {O}$
. Now let
$\hat z$
be least (indeed the unique z) such that
$\{e\}_{z}(n)\simeq b$
. Then, for any given m,
$S(a_{\hat z},m)\simeq b$
and
$S(a_{z},m)=a_{z+1}$
for
$z<\hat z$
. By definition,
$$\begin{align*}\{g\}(a_{\hat z})\simeq 2^{3\cdot 5^{J(g,a_{\hat z})}}, \text{ where } \{J(g,a_{\hat z})\}(m) \simeq \{g\}(b)+_{\mathcal{O}} m_{\mathcal{O}} \end{align*}$$
and for
$z<\hat z$
,
$$\begin{align*}\{g\}(a_{z})\simeq 2^{3\cdot 5^{J(g,a_{z})}}, \text{ where } \{J(g,a_{z})\}(m) \simeq \{g\}(a_{z+1})+_{\mathcal{O}} m_{\mathcal{O}}. \end{align*}$$
By an ordinary induction (on
$\hat z-z$
),Footnote
13
we can then prove that
$\{g\}(a_{z})\in \mathcal {O}$
for every
$z\leq \hat z$
. But
$S(a,n)=a_{0}$
. Hence
$\{g\}(S(a,n))\in \mathcal {O}$
. This concludes the proof.
Finally, we can deliver on our promise.
Proof of
$(2)\Rightarrow (1)$
of Theorem 4.3.
We aim to show that if
$a\in \mathcal {P}$
then
$\varphi _a$
is provable in an iteration of uniform reflection over
$\mathbf {HA}$
, that is, there exists
$d\in \mathcal {O}$
such that
$T_d\vdash \varphi _a$
. By Lemma 4.9, we have
-
(1.1) if
$a\in \mathcal {P}$
then
$\{g\}(a)\in \mathcal {O}$
.
According to our plan, it remains to show:
-
(1.2)
$T_{\{g\}(a)}\vdash \varphi _a$
for every a.
The index g can be defined by the recursion theorem and proved total within
$\mathbf {HA}$
. As planned, it suffices to prove in
$\mathbf {HA}$
the formalized version of the following claim:
-
(1.3) if
$\mathbf {HA}\vdash \forall a\, {Pr}(\{\bar g\}(a),\varphi _a)$
, then
$T_{\{g\}(a)}\vdash \varphi _a$
for every a.
We will prove the claim and leave the formalization as an exercise for the reader.Footnote 14
Proof of claim
$(1.3)$
.
Assume
$\mathbf {HA}\vdash \forall a\, {Pr}(\{\bar g\}(a),\varphi _a)$
and let a be given. We proceed by cases.
Case 1.
$a=Q_{axiom}(\varphi )$
is axiomatic. Then
$\varphi _a=\varphi $
is a logical axiom or an axiom of
$\mathbf {HA}$
and
$\{g\}(a)\simeq 0$
. We can directly conclude that
$T_{\{g\}(a)}\vdash \varphi _a$
since
$T_{\{g\}(a)}=T_0=\mathbf {HA}$
and
$\mathbf {HA}\vdash \varphi $
.
Case 2. a is universal. Say
$a=Q_\omega (\forall x\, \varphi (x),e)$
. In this case,
$\varphi _a=\forall x\, \varphi (x)$
and
$\varphi _{S(a,n)}=\varphi (\bar n)$
for all n. Moreover,
$\{g\}(a)\simeq 2^{G(H(g,a))}$
, where
$\{H(g,a)\}(n) \simeq \{g\}(S(a,n))$
. All this formalizes in
$\mathbf {HA}$
. In particular,
$$ \begin{align*} \mathbf{HA} &\vdash \forall x\, (\varphi_{S(\bar a,x)}=\bar \varphi(\dot x)), \\ \mathbf{HA} &\vdash \forall x\, \exists z\, (\{\bar g\}(S(\bar a,x))\simeq z\land {Pr}(z,\varphi_{S(\bar a,x)})), \\ \mathbf{HA} & \vdash \forall x\, (\{H(\bar g,\bar a)\}(x) \simeq \{\bar g\}(S(\bar a,x))), \end{align*} $$
where the second item follows from the assumption. Then by Lemma 4.6 part (ii)
$$\begin{align*}\mathbf{HA}\vdash \forall x\, {Pr}(G(H(\bar g,\bar a)),\bar \varphi(\dot x)). \end{align*}$$
Let
$d=G(H(g,a))$
so that
$\{g\}(a)\simeq 2^d$
. Since
$\mathbf {HA}\subseteq T_{2^d}$
and
$\mathbf {HA}\vdash G(H(\bar g,\bar a))=\bar d$
, we obtain
$$ \begin{align} T_{2^d}\vdash \forall x\, {Pr}(\bar d,\bar \varphi(\dot x)). \end{align} $$
On the other hand, by definition,
$$\begin{align*}T_{2^d}\vdash \forall x\, ({Pr}(\bar d,\bar \varphi(\dot x)) \rightarrow \varphi(x)). \end{align*}$$
Hence
$T_{2^d}\vdash \forall x\, \varphi (x)$
, as desired. If there are free variable in
$\forall x\, \varphi (x)$
, say
$z_1,\ldots ,z_m$
, take the universal closure
$\psi (x)\ =_{\text {def}}\ \forall z_1\ldots \forall z_m\, \varphi (x,z_1,\ldots ,z_m)$
. Now, from (1) we can infer
$T_{2^d}\vdash \forall x\, {Pr}(\bar d,\bar \psi (\dot x))$
, and then conclude
$T_{2^d}\vdash \forall x\, \psi (x)$
by applying uniform reflection with respect to
$\psi (x)$
. In particular,
$T_{2^d}\vdash \forall x\, \varphi (x)$
.
Case 3. a is an inference of arity k. Say
$a=Q_{rule}(\varphi ,b)$
and
$b= p_0^{a_0}\ldots p_k^{a_k}$
with
$\varphi _{a_i}=\varphi _i$
for
$i\leq k$
. In this case,
$\varphi _a=\varphi $
and
$\varphi _{S(a,n)}=\varphi _n$
for every
$n\leq k$
. Moreover,
$\{g\}(a)\simeq 2^{G(I(g,a))}$
, where
$\{I(g,a)\}(n) \simeq \{g\}(S(a,n))$
for all
$n\leq k$
. As before, everything formalizes in
$\mathbf {HA}$
. In particular, for all
$n\leq k$
,
$$ \begin{align*} \mathbf{HA} &\vdash \varphi_{S(\bar a,\bar n)}=\overline{\varphi_n}, \\ \mathbf{HA} &\vdash \exists z\, (\{\bar g\}(S(\bar a,\bar n))\simeq z\land {Pr}(z,\varphi_{S(\bar a,\bar n)})), \\ \mathbf{HA} &\vdash \{I(\bar g,\bar a)\}(\bar n) \simeq \{\bar g\}(S(\bar a,\bar n)). \end{align*} $$
Then by Lemma 4.6 part (ii), for all
$n\leq k$
,
$$\begin{align*}\mathbf{HA} \vdash {Pr}(G(I(\bar g,\bar a)),\overline{\varphi_n}). \end{align*}$$
Let
$d=G(I(g,a))$
so that
$\{g\}(a)\simeq 2^d$
. As before, we obtain
$$\begin{align*}T_{2^d}\vdash {Pr}(\bar d,\overline{\varphi_n}) \end{align*}$$
for all
$n\leq k$
. Since uniform reflection implies local reflection, we thus have
$$\begin{align*}T_{2^d}\vdash \varphi_n \end{align*}$$
for all
$n\leq k$
. Finally, since
$\varphi $
follows from
$\varphi _0,\ldots ,\varphi _k$
by means of a logical rule, we get
$T_{2^d}\vdash \varphi $
, as desired.
Case 4. a is a repetition. Then
$\varphi _a=\varphi _{S(a,0)}=\varphi $
for some formula
$\varphi $
. This includes the case
$\varphi =\bot $
. Moreover,
$\{g\}(a)\simeq 2^{3\cdot 5^{J(g,a)}}$
, where
$\{J(g,a)\}(n)\simeq \{g\}(S(a,0))+_{\mathcal {O}} n_{\mathcal {O}}$
. Then
$$ \begin{align*} \mathbf{HA} &\vdash \varphi_{S(\bar a,0)}=\bar{\varphi}, \\ \mathbf{HA} &\vdash \exists z\, (\{\bar g\}(S(\bar a,0))\simeq z\land {Pr}(z,\varphi_{S(\bar a,0)})), \\ \mathbf{HA} &\vdash \{J(\bar g,\bar a)\}(\bar n) \simeq \{\bar g\}(S(\bar a,0))+_{\mathcal{O}} n_{\mathcal{O}}. \end{align*} $$
In particular,
$$\begin{align*}\mathbf{HA}\vdash {Pr}(\{J(\bar g,\bar a)\}(0),\bar \varphi) \end{align*}$$
and therefore by Lemma 2.41,
$$\begin{align*}\mathbf{HA}\vdash {Pr}(3\cdot 5^{J(\bar g,\bar a)},\bar \varphi). \end{align*}$$
Let
$d=3\cdot 5^{J(g,a)}$
so that
$\{g\}(a)\simeq 2^d$
. Then
$$\begin{align*}T_{2^d}\vdash {Pr}(\bar d, \bar \varphi). \end{align*}$$
Again, since uniform reflection implies local reflection, we have
$T_{2^d}\vdash \varphi $
, as desired.
