1 Introduction
In recent studies of reverse mathematics, not only the big five systems, but also other systems are focused on. For example, it is known that the strength of Kruskal’s tree theorem is precisely between
$\mathsf {ATR}_0$
and 
, and the best-known upper bound for Menger’s theorem in graph theory is also between
$\mathsf {ATR}_0$
and 
.
For studying intermediate
$\Pi ^1_2$
statements between
$\mathsf {ATR}_0$
and 
, Towsner introduced new
$\Pi ^1_2$
principles which we call pseudo leftmost path principlesFootnote
1
stating that any ill-founded tree has a pseudo leftmost path [Reference Towsner8]. Here, a pseudo leftmost path is a path which may not be the actual leftmost path, but it behaves like a leftmost path in a restricted range. In [Reference Suzuki and Yokoyama6], the author and Yokoyama generalized Towsner’s work and gave some characterizations of 
. They introduced pseudo hyperjumps and compared them with pseudo leftmost path principles.
The works in [Reference Freund1, Reference Suzuki and Yokoyama6] suggest that a finer analysis of the relationship between the n-th and
$n+1$
-th pseudo hyperjumps is also interesting. Since Towsner’s
$\Sigma ^0_n$
leftmost path principles approximate the single pseudo hyperjump, it seems helpful to study them for a finer analysis between pseudo hyperjumps.
In this article, we give new characterizations of pseudo leftmost path principles. We prove the following equivalences over
$\mathsf {RCA}_0$
. For the detailed definitions, see Definitions 2.2, 3.2, and 3.5.
-
• The transfinite leftmost path principle (written as
$\mathsf {TLPP}$
) and the single pseudo hyperjump with the base (wirtten as ) are equivalent. -
• The arithmetic leftmost path principle (written as
$\mathsf {ALPP}$
), the single pseudo hyperjump (written as
$\beta ^1_0\mathsf {RFN}(1;\top )$
) and the omega-model reflection of (written as ) are mutually equivalent. -
• The n-th pseudo hyperjump with the base
(written as ) and the
$n+1$
-th pseudo hyperjump (written as
$\beta ^1_0\mathsf {RFN}(n+1;\top )$
) are equivalent. -
• The
$\Sigma ^0_n$
leftmost path principle (written as
$\Sigma ^0_n\mathsf {LPP}$
) and the omega-model reflection of (written as ) are equivalent for
$n> 1$
.
(wirtten as 
) are equivalent.
(written as 
) are mutually equivalent.
(written as 
) and the 
(written as 
) are equivalent for 
We note that these results help to reveal the proof-theoretic strength of pseudo leftmost path principles. We also note that the second clause is independently proved by Freund [Reference Freund1].
1.1 Structure of this article
In Section 2, we recall the notion of coded
$\omega $
-models and the
$\omega $
-model reflections. Then, we introduce the notion of realizers for coded
$\omega $
-models, which is used to prove results in Section 3. In Section 3, we prove the main results. In Section 4, we rephrase the results in Section 3 from the point of view of Weihrauch reduction.
2 Coded omega-models
In this section, we see some properties of coded
$\omega $
-models. For the basic definitions, see also Simpson’s textbook [Reference Simpson5].
Definition 2.1 (
$\mathsf {RCA}_0$
).
For a set X, we define the i-th segment
$X_i$
by
$X_i = \{j : \langle i,j \rangle \in X\}$
, where
$\langle i,j \rangle $
denotes the standard pairing function from
$\mathbb {N}^2$
to
$\mathbb {N}$
. Then, a set X can be regarded as a sequence
$\langle X_i \rangle _{i \in \mathbb {N}}$
. In this sense, we say a set A is contained in X (written
$A \in X$
) if
$\exists i(A = X_i)$
holds.
When we identify a set
$\mathcal {M}$
with the structure
$(\mathbb {N},\langle \mathcal {M}_i\rangle _{i \in \mathbb {N}})$
, we call
$\mathcal {M}$
a coded
$\omega $
-model. If it is clear from the context, we sometimes omit the word coded, and simply say
$\mathcal {M}$
is an
$\omega $
-model. One of the important notions related to coded
$\omega $
-models is the principle of
$\omega $
-model reflection. We introduce two kinds of
$\omega $
-model reflections.
Definition 2.2. Let T be a recursively axiomatized theory. We define the
$\omega $
-model reflection of T (written
$\mathsf {RFN}(T)$
) as the assertion that any set X is contained in an
$\omega $
-model of
$T + \mathsf {ACA}_0$
.
It is easy to see that
$\mathsf {RFN}(T)$
implies the consistency of
$\mathsf {ACA}_0 + T$
over
$\mathsf {RCA}_0$
. Therefore, sometimes
$\mathsf {RFN}(T)$
is used for separating two theories.
Proposition 2.3. Let T and
$T'$
be recursive consistent extensions of
$\mathsf {ACA}_0$
such that T proves
$\mathsf {RFN}(T')$
. Then,
$T'$
does not prove T. If T proves
$T'$
in addition, then T is strictly stronger than
$T'$
.
Proof. If
$T'$
proved T, then
$T'$
would prove the consistency of
$T'$
, a contradiction.
Definition 2.4. Let
$\Gamma $
be a class of formulas. We define the
$\Gamma $
-reflection schema (written 
) as the collection of
$$ \begin{align*} \forall X(\varphi(X) \to \exists \mathcal{M} \text{: a coded } \omega\text{-model } (\mathcal{M} \models \mathsf{ACA}_0 + \varphi(X))) \end{align*} $$
for all
$\varphi \in \Gamma $
.
The following characterization of 
is well-known.
Theorem 2.5 (
$\mathsf {ACA}_0$
).
[Reference Jäger and Strahm2] Let
$n \in \omega $
such that
$n>0$
. Then, 
is equivalent to 
.
In the usual definition in the context of formal logics, the truth of a sentence
$\sigma $
over a structure
$\mathcal {M}$
is defined by Tarski’s truth definition. However, it is practically identified with the truth of the relativization
$\sigma ^{\mathcal {M}}$
. We note that when working in a weak system like
$\mathsf {RCA}_0$
, we need to distinguish between these two kinds of truth:
$\sigma ^{\mathcal {M}}$
and
$\mathcal {M} \models \sigma $
. For a detailed definition of
$\mathcal {M} \models \sigma $
, see [Reference Simpson5].
Definition 2.6 (
$\mathsf {RCA}_0$
).
Let
$\mathcal {M} = \langle \mathcal {M}_i \rangle _{i \in \mathbb {N}}$
be a sequence of sets. We say
$\mathcal {M}$
is a jump ideal if
$$ \begin{align*} \forall i ({\mathrm{TJ}}(\mathcal{M}_i) \in \mathcal{M}) \land \forall i,j(\mathcal{M}_i \oplus \mathcal{M}_j \in \mathcal{M}) \land \forall i \forall X \leq_{\mathrm{T}} \mathcal{M}_i (X \in \mathcal{M}). \end{align*} $$
Here,
${\mathrm {TJ}},\oplus $
, and
$\leq _{\mathrm {T}}$
denote the Turing jump, the Turing sum, and the Turing reduction, respectively.
For
$S \subseteq \mathcal {P}(\omega )$
, S is a jump ideal if and only if S is an
$\omega $
-model of
$\mathsf {ACA}_0$
. This fact is provable in
$\mathsf {ACA}_0$
. However, a jump ideal may not be a model of
$\mathsf {ACA}_0$
in
$\mathsf {RCA}_0$
because
$\mathsf {RCA}_0$
does not ensure the existence of a (partial) truth valuation for a coded
$\omega $
-model. We introduce realizers for jump ideals that make a jump ideal an
$\omega $
-model of
$\mathsf {ACA}_0$
within
$\mathsf {RCA}_0$
.
Definition 2.7 (
$\mathsf {RCA}_0$
).
Let
$\mathcal {M}$
be a jump ideal,
$f_{{\mathrm {TJ}}}$
be a function from
$\mathbb {N}$
to
$\mathbb {N}$
and
$f_{\oplus }$
be a function from
$\mathbb {N}^2$
to
$\mathbb {N}$
. We say the pair
$(f_{{\mathrm {TJ}}},f_{\oplus })$
realizes that
$\mathcal {M}$
is a jump ideal (written
$(f_{{\mathrm {TJ}}},f_{\oplus }) \Vdash _{\mathcal {M}} \mathsf {ACA}_0$
) if
$$ \begin{align*} \forall i (\mathcal{M}_{f_{{\mathrm{TJ}}}(i)} = {\mathrm{TJ}}(\mathcal{M}_i)) \land \forall i,j(\mathcal{M}_{f_{\oplus}(i,j)} = \mathcal{M}_i \oplus \mathcal{M}_j). \end{align*} $$
We say a jump ideal
$\mathcal {M}$
is realizable if there is a realizer
$(f_{{\mathrm {TJ}}},f_{\oplus })$
for it.
Remark 2.8. We note that realizable jump ideals are essentially the same as effective
$\omega $
-models of
$\mathsf {ACA}_0$
introduced in [Reference Suzuki and Yokoyama7] in the context of Weihrauch degrees.
Definition 2.9. For each
$n \in \omega $
such that
$n> 0$
, let
$\pi ^0_n$
denote a
$\Pi ^0_n$
-unversal formula. That is, for any
$\Pi ^0_n$
formula
$\theta $
whose Gödel number is
$\ulcorner \theta \urcorner $
, the following holds:
$$ \begin{align*} \mathsf{RCA}_0 \vdash \forall\vec{x},\vec{X} (\theta(\vec{x},\vec{X}) \leftrightarrow \pi^0_n(\ulcorner \theta \urcorner,\vec{x},\vec{X}). \end{align*} $$
Let
$n \in \omega $
such that
$n> 0$
. Then,
$\mathsf {RCA}_0$
proves that any realizable jump ideal has the
$\Pi ^0_n$
truth valuation. More precisely, the following holds.
Proposition 2.10. Let
$n \in \omega $
such that
$n> 0$
. Then,
$\mathsf {RCA}_0$
proves the following. For any jump ideal
$\mathcal {M}$
realized by
$f_{{\mathrm {TJ}}}$
and
$f_{\oplus }$
, there is a
$\{\top ,\bot \}$
-valued function
$f\leq _{\mathrm {T}} \mathcal {M} \oplus f_{{\mathrm {TJ}}} \oplus f_{\oplus }$
such that
$$ \begin{align*} f(e,x,i,j) = \top \leftrightarrow \pi^0_n(e,x,\mathcal{M}_i,\mathcal{M}_j). \end{align*} $$
Proof. We first note that
$\mathsf {RCA}_0$
proves that any
$\Pi ^0_n(X \oplus Y)$
set is many-one reducible to
${\mathrm {TJ}}^n(X \oplus Y)$
where
${\mathrm {TJ}}^n$
denotes the n-times iteration of the jump operator, and
$\Pi ^0_n(X\oplus Y)$
denotes the collection of
$\Pi ^0_n$
-definable sets from an oracle
$X\oplus Y$
. More precisely, there is a primitive recursive function p such that the following holds in
$\mathsf {RCA}_0$
. For any set X and Y such that
${\mathrm {TJ}}^{n}(X \oplus Y)$
exists, we have
$$ \begin{align*} \forall e,x (\pi^0_n(e,x,X,Y) \leftrightarrow p(e,x) \in {\mathrm{TJ}}^n(X\oplus Y)). \end{align*} $$
We work in
$\mathsf {RCA}_0$
and show that any realizable jump ideal has the
$\Pi ^0_n$
truth valuation. Let
$\mathcal {M}$
be a jump ideal realized by
$(f_{{\mathrm {TJ}}},f_{\oplus })$
. Then, for any
$e,x,i,j$
,
$\pi ^0_n(e,x,\mathcal {M}_i,\mathcal {M}_j)$
is equivalent to
$p(e,x) \in \mathcal {M}_{(f_{{\mathrm {TJ}}})^n(f_{\oplus }(i,j))}$
. Therefore, the desired f is
$\Delta ^0_1$
-definable as follows:
$$ \begin{align*} f(e,x) = \top \leftrightarrow p(e,x) \in \mathcal{M}_{(f_{{\mathrm{TJ}}})^nf_{\oplus}(i,j)}. \end{align*} $$
This completes the proof.
For a class of formulas
$\Gamma $
, we define the class
$\exists X \Gamma $
by
$\{\exists X \varphi : \varphi \in \Gamma \}$
. Similarly, we define
$\exists f \Gamma $
by
$\{\exists f \in \mathbb {N}^{\mathbb {N}} \varphi : \varphi \in \Gamma \}$
. Here,
$f \in \mathbb {N}^{\mathbb {N}}$
is the abbreviation of the
$\Pi ^0_2$
formula stating in
$\mathsf {RCA}_0$
that f is a function from
$\mathbb {N}$
to
$\mathbb {N}$
. It is well-known that there exists a primitive recursive function p such that
$$ \begin{align*} \mathsf{RCA}_0 \vdash \exists X \pi^0_2(e,X) \leftrightarrow \exists f \pi^0_1(p(e),f). \end{align*} $$
Therefore, we may say that
$\exists X \Pi ^0_2$
is included in
$\exists f \Pi ^0_1$
. Since
$\exists f \Pi ^0_1$
is a subset of
$\exists X \Pi ^0_2$
, we may think that
$\exists X \Pi ^0_2$
and
$\exists f \Pi ^0_1$
are the same. Similarly, we may say that
$\exists X \Pi ^0_2$
and
$\exists f \Pi ^0_2$
are the same. Henceforth, we identify these three classes.
Remark 2.11. For
$n>0$
,
$\exists X \Pi ^0_n$
is also written as
$\Sigma ^1_1(\Pi ^0_n)$
. Similarly, a formula of the form
$\lnot \varphi $
for some
$\varphi \in \Sigma ^1_1(\Pi ^0_n)$
is said to be
$\Pi ^1_1(\Sigma ^0_n)$
. Formally, we inductively define
$\Pi ^1_{m}(\Gamma )$
and
$\Sigma ^1_{m}(\Gamma )$
for
$\Gamma \in \{\Sigma ^0_n,\Pi ^0_n\}$
as follows:
$$ \begin{align*} \Sigma^1_{m+1}(\Gamma) = \exists X \Pi^1_n(\Gamma), \\ \Pi^1_{m+1}(\Gamma) = \forall X \Sigma^1_{m}(\Gamma). \end{align*} $$
Definition 2.12 (
$\mathsf {RCA}_0$
).
For a set X, we define the hyperjump
$\mathrm {HJ}(X)$
of X by
$\mathrm {HJ}(X) = \{(e,n) : \exists Y \pi ^0_2(e,n,X,Y)\}$
.
Remark 2.13. In the context of computability theory,
$\mathrm {HJ}(X)$
is defined as a certain
$\Pi ^1_1(X)$
-complete set. However, we prefer to define
$\mathrm {HJ}(X)$
as a
$\Sigma ^1_1(\Pi ^0_2)$
-complete set over
$\mathsf {RCA}_0$
for technical reasons. We note that
$\mathsf {RCA}_0$
is not sufficient to prove that
$\mathrm {HJ}(X)$
is
$\Sigma ^1_1$
-complete.
$\mathsf {ACA}_0$
is needed to prove the
$\Sigma ^1_1$
-completeness of hyperjumps.
Definition 2.14 (
$\mathsf {RCA}_0$
).
Let
$\mathcal {M}$
be a coded
$\omega $
-model. We say
$\mathcal {M}$
is a
$\beta $
-model if
$$ \begin{align*} \exists X \pi^0_2(e,x,X,\mathcal{M}_i,\mathcal{M}_j) \leftrightarrow \mathcal{M} \models \exists X \pi^0_2(e,x,X,\mathcal{M}_k,\mathcal{M}_i) \end{align*} $$
holds.
Remark 2.15. In the usual context, a
$\beta $
-model is a
$\Sigma ^1_1$
-elementary submodel of the ground model. Similarly to hyperjumps,
$\mathsf {RCA}_0$
is not enough to prove the
$\Sigma ^1_1$
-elementarity of
$\beta $
-models.
It is well-known that the existence of the hyperjump of X is equivalent to the existence of a coded
$\beta $
-model containing X over
$\mathsf {ACA}_0$
[Reference Simpson5]. If one reads this proof carefully, one can find that the construction of a coded
$\beta $
-model from a hyperjump involves information about
$\Sigma ^1_1$
-truth of the constructed model. To clarify this fact, we introduce a realizer for coded models.
Definition 2.16. Let
$\mathcal {M}$
be a coded
$\omega $
-model. We say a function f is a realizer for
$\exists X \Pi ^0_2$
sentences true in
$\mathcal {M}$
(written
$f \Vdash _{\mathcal {M}} \exists X \Pi ^0_2$
) if
$\exists j \pi ^0_2(e,x,\mathcal {M}_i,\mathcal {M}_j) \to \pi ^0_2(e,x,\mathcal {M}_i,\mathcal {M}_{f(e,x,i)})$
.
As we will see in the proof of Lemma 3.17,
$\mathrm {HJ}(X)$
computes a coded
$\beta $
-model
$\mathcal {M}$
which contains X and has a computable realizer for
$\exists X \Pi ^0_2$
sentences.
In [Reference Suzuki and Yokoyama7], the author and Yokoyama introduced a weaker variant of
$\beta $
-models called
$\Delta ^0_k\beta $
-model to study pseudo leftmost path principles from the point of view of Weihrauch degrees.
Definition 2.17. Let
$n \in \omega $
such that
$n> 0$
. Let
$\mathcal {M}$
be a jump ideal. We say
$\mathcal {M}$
is a
$\Delta ^0_k\beta $
-model if for any
$\Pi ^0_2$
formula
$\varphi $
with parameters from
$\mathcal {M}$
, the following holds.
$$ \begin{align*} \exists X \leq_{\mathrm{T}} {\mathrm{TJ}}^{k-1}(\mathcal{M}) \varphi(X) \to \exists i \varphi(\mathcal{M}_i) \end{align*} $$
In the next section, we show the equivalence of
$\Sigma ^0_k\mathsf {LPP}$
and the existence of
$\Delta ^0_k\beta $
-models with computable realizers.
3 The equivalences
In this section, we show the equivalence of pseudo leftmost path principles and the
$\omega $
-model reflection of transfinite inductions. We first introduce pseudo leftmost path principles.
Definition 3.1. Let
$T \subseteq \mathbb {N}^{<\mathbb {N}}$
be an ill-founded tree.
-
• We say a path f of T is the leftmost path (written
$\mathrm {LP}(T,f)$
) if f is the smallest in
$[T]$
with respect to the lexicographic order. Here,
$[T]$
denotes the set of paths of T. -
• Let
$\alpha $
be a well-order. We say a path f of T is a
$\Sigma ^0_{\alpha }$
-leftmost path if f is the smallest in
$[T] \cap \{g : g \in \Sigma ^{0}_{\alpha }(T \oplus f)\}$
with respect to the lexicographic order.
Definition 3.2. [Reference Suzuki and Yokoyama6, Reference Towsner8] We define
$\Sigma ^0_{n}\mathsf {LPP}$
,
$\mathsf {ALPP}$
, and
$\mathsf {TLPP}$
as follows.
-
•
$\Sigma ^0_{n}\mathsf {LPP}$
is the assertion that any ill-founded tree has a
$\Sigma ^0_n$
-leftmost path, -
•
$\mathsf {ALPP}$
is the assertion that any ill-founded tree has a
$\Sigma ^0_{\omega }$
-leftmost path, -
•
$\mathsf {TLPP}$
is the assertion that for any well-order
$\alpha $
and ill-founded tree T, T has a
$\Sigma ^0_{\alpha }$
leftmost path.
We note that a path of a tree is a total function. Therefore, a path
$g \in [T]$
is
$\Sigma ^0_n$
-definable from
$T \oplus f$
if and only if it is
$\Delta ^0_n$
-definable from
$T \oplus f$
.
Definition 3.3. We say a path
$f \in [T]$
is a
$\Delta ^0_k$
leftmost path if f is the smallest in
$\{g \in [T] : g \leq _{\mathrm {T}} {\mathrm {TJ}}^{k-1}(T \oplus f)\}$
with respect to the lexicographic order. We define
$\Delta ^0_k\mathsf {LPP}$
as the assertion that any ill-founded tree has a
$\Delta ^0_k$
-leftmost path.
Lemma 3.4. Over
$\mathsf {RCA}_0$
,
$\Sigma ^0_k\mathsf {LPP}$
is equivalent to
$\Delta ^0_k\mathsf {LPP}$
for
$k \in \omega $
such that
$k> 0$
.
Proof. As we have mentioned, a path is
$\Sigma ^0_k$
-definable if and only if it is
$\Delta ^0_k$
-definable. Therefore, a path is
$\Sigma ^0_k$
-leftmost if and only if it is
$\Delta ^0_k$
-leftmost.
As it is proved in [Reference Suzuki and Yokoyama7],
$\Delta ^0_k\mathsf {LPP}$
is equivalent to the assertion that any ill-founded tree has a path f that is the smallest in
$\{g \in [T] : g \leq _{\mathrm {T}} {\mathrm {TJ}}^{k-1}(f)\}$
. Thus, we do not distinguish between
$\Sigma ^0_k\mathsf {LPP},\Delta ^0_k\mathsf {LPP}$
and this assertion.
For studying
$\Pi ^1_2$
theorems above
$\mathsf {TLPP}$
, the author and Yokoyama introduced the notion of pseudo hyperjumps in [Reference Suzuki and Yokoyama6].
Definition 3.5. Let
$\sigma $
be a sentence and
$n \in \omega $
. We define the n-th pseudo hyperjump with the base
$\sigma $
as
$$ \begin{align*} \beta^1_0\mathsf{RFN}(n;\sigma) \equiv \forall X \exists \mathcal{M} (X \in \mathcal{M} \land \mathcal{M} \models \mathsf{ACA}_0 + \sigma + \exists \mathrm{HJ}^n(X)). \end{align*} $$
Theorem 3.6 [Reference Suzuki and Yokoyama6].
Over
$\mathsf {ACA}_0$
,
$$ \begin{align*} \beta^1_0\mathsf{RFN}(1;\top) < \mathsf{TLPP} < \beta^1_0\mathsf{RFN}(1;\mathsf{ATR}_0) < \beta^1_0\mathsf{RFN}(2;\top). \end{align*} $$
Here,
$T < T'$
means that
$T'$
proves T and its consistency.
We now provide a new characterization of
$\mathsf {TLPP}$
via a pseudo hyperjump. First, we introduce some properties of
$\mathsf {TLPP}$
.
Lemma 3.7 (
$\mathsf {TLPP}$
) [Reference Towsner8, Theorem 4.6].
For any ill-founded tree T, there exists an
$\omega $
-model of 
which believes that T has a leftmost path.
Lemma 3.8 (
$\mathsf {RCA}_0$
) [Reference Suzuki and Yokoyama6, Lemma 4.23].
$\mathsf {TLPP}$
is equivalent to the assertion that for any well-order
$\alpha $
and set X, there exists an
$\omega $
-model
$\mathcal {M}$
such that
$\alpha ,X \in \mathcal {M}$
and
$\mathcal {M}$
believes
$\mathrm {HJ}(X)$
exists and
$\mathcal {M}$
is closed under
$\alpha $
-times Turing jump.
To connect leftmost paths and hyperjumps, we use the following lemma.
Lemma 3.9. Over
$\mathsf {RCA}_0$
, we may assume that there exists a total Turing functional
$\Phi _T(X)$
such that
-
•
$\Phi _T(X)$
is a tree, -
•
$\Phi _T(X)$
has an infinite path which is uniformly computable from X, -
• each path of
$\Phi _T(X)$
computes X, -
• if
$\mathrm {LP}(\Phi _T(X),f)$
holds, then
$\mathrm {HJ}(X) \leq _{\mathrm {T}} f$
.
For details, see [Reference Suzuki and Yokoyama6, Section 4]. We note that in [Reference Suzuki and Yokoyama6], the above properties are proved in
$\mathsf {ACA}_0$
rather than
$\mathsf {RCA}_0$
. However, if one looks at the proofs carefully, one can find that these properties hold in
$\mathsf {RCA}_0$
.
Theorem 3.10. Over
$\mathsf {RCA}_0$
,
$\mathsf {TLPP}$
is equivalent to 
.
Proof. Since 
is equivalent to 
over
$\mathsf {ACA}_0$
, it is enough to show the equivalence of
$\mathsf {TLPP}$
and 
.
We first show that
$\mathsf {TLPP}$
implies 
. Suppose
$\mathsf {TLPP}$
. Let X be a set. Then, there exists an
$\omega $
-model
$\mathcal {M}$
of 
such that
$\mathcal {M}$
believes
$\Phi _T(X)$
has a leftmost path. Therefore,
$\mathcal {M}$
satisfies 
and there exists the hyperjump of X.
We then show the converse direction by Lemma 3.8. Let
$\alpha $
be a well-order and X be a set. Take an
$\omega $
-model
$\mathcal {M}$
such that
$\alpha ,X \in \mathcal {M}$
and 
. Then,
$\mathcal {M}$
is closed under
$\alpha $
-times Turing jump.
Remark 3.11. We note that 
can be weaken to Montalbán’s Jump Iteration
$\mathsf {JI}$
[Reference Montalbán3] in the above proof.
Corollary 3.12. Over
$\mathsf {RCA}_0$
, 
.
Proof. It is immediate from the equivalence of 
and
$\mathsf {TLPP}$
.
We next show that both
$\mathsf {ALPP}$
and the single pseudo hyperjump
$\beta ^1_0\mathsf {RFN}(1;\top )$
are characterized by the
$\omega $
-model reflection of full transfinite induction. We note that this characterization is independently proved by Freund [Reference Freund1].
Theorem 3.13. Over
$\mathsf {RCA}_0$
, the following assertions are equivalent:
-
1.
$\mathsf {ALPP}$
, -
2.
$\beta ^1_0\mathsf {RFN}(1)$
, -
3.
, -
4.
where is the class built from
$\Pi ^1_1$
with logical connectives and number quantifiers.
,
where 
is the class built from 
Proof. The equivalence of
$(1)$
and
$(2)$
is proved in [Reference Suzuki and Yokoyama6], and the equivalence of
$(2)$
and
$(3)$
is proved in [Reference Freund1]. The implication of
$(3)$
to
$(4)$
is trivial. For the implication of
$(4)$
to
$(2)$
, the same proof of the implication of
$(3)$
to
$(2)$
works. For this implication, see also [Reference Simpson5, Theorem VII.2.18 and Corollary VII.2.21].
The equivalence of
$(2)$
and
$(3)$
in the previous theorem can be extended to the n-th pseudo hyperjump level as follows.
Theorem 3.14. Over
$\mathsf {RCA}_0$
,
$\beta ^1_0\mathsf {RFN}(n+1)$
is equivalent to 
for any
$n \in \omega $
such that
$n> 0$
.
Proof. Since the same proof for the previous theorem works, we give a brief proof. The implication from
$\beta ^1_0\mathsf {RFN}(n+1)$
to 
is trivial. For proving
$\beta ^1_0\mathsf {RFN}(n+1)$
from 
, take an X and an
$\omega $
-model
$\mathcal {M}$
such that 
. Let
$Y \in \mathcal {M}$
such that
$\mathcal {M} \models Y = \mathrm {HJ}^n(X)$
. Let
$\mathcal {M}'$
be the collection of the definable-in-
$\mathcal {M}$
subclasses of
$\mathbb {N}$
. Then,
$\mathcal {M} \subseteq _{\beta } \mathcal {M}'$
. Moreover, there is a set
$Z \in \mathcal {M}'$
such that
$Z = \{n : \mathcal {M} \models \theta _{\mathrm {HJ}}(n,Y)\},$
where
$\theta _{\mathrm {HJ}}$
is the
$\Sigma ^1_1$
formula defining hyperjumps. Then,
$\mathcal {M}' \models Z = \mathrm {HJ}(Y) \land Y = \mathrm {HJ}^n(X)$
, hence
$\mathcal {M}' \models Z = \mathrm {HJ}^{n+1}(X)$
. This completes the proof.
Combining Corollary 3.12 and the previous theorem, we have the following corollary.
Corollary 3.15. Over
$\mathsf {RCA}_0$
,
Proof. We first remark that any of the above statements includes
$\mathsf {ACA}_0$
. We also note that 
is equivalent to
$\beta ^1_0(1;\mathsf {ATR}_0)$
because 
and
$\mathsf {ATR}_0$
are equivalent over
$\Sigma ^1_1$
-induction that is true in any coded
$\omega $
-model. Thus, the inequality 
follows from Theorem 3.6 and Corollary 3.12. The inequality 
follows from Theorems 3.6 and 3.14.
We then show that the equivalence in Theorem 3.13 also holds at the level of
$\Sigma ^0_k\mathsf {LPP}$
. For proving the equivalence of
$\Sigma ^0_k\mathsf {LPP}$
and 
, we use
$\Delta ^0_k\beta $
-models with computable realizers.
Definition 3.16. Let
$n \in \omega $
such that
$n> 0$
. We define 
as the assertion that any set X is contained in a
$\Delta ^0_n\beta $
-model
$\mathcal {M}$
with total computable functions
$f_{{\mathrm {TJ}}},f_{\oplus },f_{\Sigma ^1_1}$
such that
$(f_{{\mathrm {TJ}}},f_{\oplus }) \Vdash _{\mathcal {M}} \mathsf {ACA}_0$
and
$f_{\Sigma ^1_1} \Vdash _{\mathcal {M}} \exists X \Pi ^0_2$
.
Lemma 3.17. For
$k \in \omega $
such that
$k> 0$
,
$\Sigma ^0_{k+1}\mathsf {LPP}$
implies 
over
$\mathsf {RCA}_0$
.
Proof. We first note that
$\Sigma ^0_{k+1}\mathsf {LPP}$
includes
$\mathsf {ACA}_0^+$
. Thus, we may assume that any coded
$\omega $
-model has a total valuation.
Let X be a set. Take a
$\Delta ^0_{k+1}$
-leftmost path f of
$\Phi _T(X)$
. Define an
$\omega $
-model
$\mathcal {M} = \Delta ^0_{k+1}(\Phi _T(X) \oplus f) = \{A : A \leq _{\mathrm {T}} {\mathrm {TJ}}^{k}(\Phi _T(X) \oplus f)\}$
. Then,
$\mathcal {M} \models \mathsf {RCA}_0 + \mathrm {LP}(\Phi _T(X),f)$
. Therefore,
$\mathrm {HJ}^{\mathcal {M}}(X) \leq _{\mathrm {T}} f$
exists.
We perform the construction of [Reference Simpson5, Lemma VII.2.9(19)] within
$\mathcal {M}$
. Then, we have a function
$g \leq _{\mathrm {T}} \mathrm {HJ}^{\mathcal {M}}(X) \leq _{\mathrm {T}} f$
having the following condition.
$$ \begin{align*} \mathcal{M} \models \forall e,m (\exists h \in \mathbb{N}^{\mathbb{N}} \pi^0_1(e,m,(g)_{<\langle e,m \rangle},h) \to \pi^0_1(e,m,(g)_{<\langle e,m \rangle},g_{\langle e,m \rangle})). \end{align*} $$
Here,
$g_n$
denotes the n-th segment of g, that is,
$g_{n}(x) = g(\langle n,x\rangle )$
. Thus, g is identified the sequence
$\langle g_n \rangle _n$
. In addition,
$g_{<n}$
denotes the sequence
$\langle g_0 \ldots , g_{n-1} \rangle $
.
We show that the sequence
$\langle g_n \rangle _n$
is closed under Turing jumps. That is, for any n, there exists m such that
$g_m = {\mathrm {TJ}}(g_n)$
. To see this, take an n. Then,
$g_n \leq _{\mathrm {T}} g \leq _{\mathrm {T}} f$
by definition. Thus,
${\mathrm {TJ}}(g_n) \leq _{\mathrm {T}} {\mathrm {TJ}}(f)$
and hence
${\mathrm {TJ}}(g_n) \in \mathcal {M}$
. Since
$\exists h(h = {\mathrm {TJ}}(g_n))$
is of the form
$\exists h' \in \mathbb {N}^{\mathbb {N}} \Pi ^0_1$
, we have
$g_{m_n} = {\mathrm {TJ}}(g_n)$
for some
$m_n$
. Moreover, the correspondence
$f_{{\mathrm {TJ}}} : n \mapsto m_n$
is clearly computable. By a similar way, we have that there exists a computable correspondence
$f_{\oplus } : (n,n') \mapsto m'(n,n')$
such that
$g_{m'(n,n')} = g_n \oplus g_n'$
. It is also proved by a similar way that
$\langle g_n \rangle _n$
is closed under the Turing reduction. Therefore,
$\langle g_n \rangle _n$
is a jump ideal realized by computable functions
$f_{{\mathrm {TJ}}}$
and
$f_{\oplus }$
. In addition,
$\langle g_n \rangle _n$
and
$\mathcal {M}$
are clearly absolute for
$\exists h \in \mathbb {N}^{\mathbb {N}}\Pi ^0_1$
formulas.
We show that
$\langle g_n \rangle _n$
is a
$\Delta ^0_{k+1}\beta $
-model. Let
$e,x,m \in \mathbb {N}$
and
$h \leq _{\mathrm {T}} {\mathrm {TJ}}^{k}(\langle g_n \rangle _n)$
be such that
$\pi ^0_1(e,x,g_m,h)$
. Then,
$h \leq _{\mathrm {T}} {\mathrm {TJ}}^{k}(\Phi _T(X) \oplus f)$
because
$ \langle g_n\rangle _n \leq _{\mathrm {T}} f$
. Hence,
$h \in \mathcal {M}$
. Thus we have
$\mathcal {M} \models \exists h \pi ^0_1(e,x,g_n,h)$
. By the construction of
$\langle g_n \rangle _n$
,
$\langle g_n \rangle _N \models \pi ^0_1(e,x,g_m,g_{m'})$
for some
$m'$
. Consequently, we have that
$\langle g_n \rangle _n$
is a
$\Delta ^0_{k+1}\beta $
-model.
We then show that
$\langle g_n \rangle _n$
has a computable realizer for
$\exists h \in \mathbb {N}^{\mathbb {N}} \Pi ^0_1$
formulas. We note that
$$ \begin{align*} \langle g_n \rangle_n \models \exists h \pi^0_1(e,m,g_{<\langle e,m \rangle},h) \text{ if and only if } \langle g_n \rangle_n \models \pi^0_1(e,m,g_{<\langle e,m \rangle},g_{\langle e,m \rangle}) \end{align*} $$
holds. Hence, to decide either
$\langle g_n \rangle _n \models \exists h \pi ^0_1(e,m,g_{<\langle e,m \rangle },h)$
or not, it is enough to check either
$\langle g_n \rangle _n \models \pi ^0_1(e,m,g_{<\langle e,m \rangle },g_{\langle e,m \rangle })$
or not. Since
$\langle g_n \rangle _n$
is a realizable jump ideal, it has a computable truth valuation for
$\Pi ^0_1$
formulas. Thus, we have a computable function which decides either
$\langle g_n \rangle _n \models \pi ^0_1(e,m,g_{<\langle e,m \rangle },g_{\langle e,m \rangle })$
or not. This completes the proof.
Lemma 3.18. Let
$\mathcal {M}$
be a
$\Delta ^0_k\beta $
-model and
$f_{{\mathrm {TJ}}},f_{\oplus },f_{\Sigma ^1_1}$
be computable functions such that
$(f_{{\mathrm {TJ}}},f_{\oplus }) \Vdash _{\mathcal {M}} \mathsf {ACA}_0$
and
$f_{\Sigma ^1_1} \Vdash _{\mathcal {M}} \exists X \Pi ^0_2$
. Then, for any arithmetical formula
$\varphi (n,X,Y)$
and
$n,i \in \mathbb {N}$
, the set
$\{n : \mathcal {M} \models \exists Y\varphi (n,\mathcal {M}_i,Y)\}$
is
$\mathcal {M}$
-computable.
Proof. We may assume that
$\varphi $
is
$\Pi ^0_2$
because
$\mathcal {M}$
is a model of
$\mathsf {ACA}_0$
.
Let e be a code of
$\varphi $
. Since
$f_{\Sigma ^1_1} \Vdash _{\mathcal {M}} \exists X \Pi ^0_2$
,
$\{n : \mathcal {M} \models \exists Y \varphi (n,\mathcal {M}_i,Y)\} = \{n : \varphi (n,\mathcal {M}_i,\mathcal {M}_{f_{\Sigma ^1_1}(e,n,i)))}\}$
. Since
$\mathcal {M}$
is a realizable jump ideal, there is a
$(\mathcal {M} \oplus f_{{\mathrm {TJ}}} \oplus f_{\oplus })$
-computable truth valuation for
$\Pi ^0_2$
formulas. Thus,
$\{n: \varphi (n,\mathcal {M}_i,\mathcal {M}_{f_{\Sigma ^1_1}(e,n,i)})\}$
is computable from
$\mathcal {M} \oplus f_{{\mathrm {TJ}}} \oplus f_{\oplus } \oplus f_{\Sigma ^1_1}$
. Since the realizers are computable,
$\{n : \varphi (n,\mathcal {M}_i,\mathcal {M}_{f_{\Sigma ^1_1}(e,n,i)})\}$
is
$\mathcal {M}$
-computable.
Lemma 3.19. Let
$k \in \omega $
such that
$k> 0$
. Let
$\mathcal {M}$
be a
$\Delta ^0_k\beta $
-model having computable realizers
$f_{{\mathrm {TJ}}},f_{\oplus },f_{\Sigma ^1_1}$
. Then, for any
$\Sigma ^1_{k+1}$
formula
$\varphi (n,X)$
, the set
$\{n: \mathcal {M} \models \varphi (n,\mathcal {M}_i)\}$
is
$\Sigma ^0_{k}$
-definable from
$\mathcal {M}$
and
$\{n : \mathcal {M} \models \lnot \varphi (n,\mathcal {M}_i)\}$
is
$\Pi ^0_k$
-definable from
$\mathcal {M}$
.
Proof. It is an easy induction on k.
Lemma 3.20 (
$\mathsf {ACA}_0$
).
Let
$k \in \omega $
such that
$k> 0$
. Let
$\mathcal {M}$
be a
$\Delta ^0_k\beta $
-model,
$f_{{\mathrm {TJ}}}, f_{\oplus }$
$f_{\Sigma ^1_1}$
be computable realizers for
$\mathcal {M}$
. Then, 
.
Proof. Let
$W \in \mathcal {M}$
be such that
$\mathcal {M} \models \mathrm {WO}(W)$
. Let
$\varphi (i)$
be a
$\Pi ^1_{n+1}$
formula such that
$\mathcal {M}$
satisfies the antecedent of transfinite induction along W. That is,
$$ \begin{align*} \mathcal{M} \models \forall i \in |W| ( \forall j <_W i \varphi(j) \to \varphi(i)) \end{align*} $$
where
$|W|$
denotes the field of W.
Assume that
$\mathcal {M} \not \models \forall i \in |W| \varphi (i)$
. Then,
$\{i \in |W| : \lnot \varphi (i)\}$
is nonempty and has no W-minimal element. In addition,
$\{i \in |W| : \lnot \varphi (i)\}$
is
$\Sigma ^0_k$
-definable from
$\mathcal {M}$
. Thus, there exists a W-descending sequence from
$\{i \in |W| : \lnot \varphi (i)\}$
which is
$\Delta ^0_k$
definable from
$\mathcal {M}$
. That is, we have
$$ \begin{align*} \exists A \leq_{\mathrm{T}} {\mathrm{TJ}}^{k-1}(\mathcal{M}) (A \text{ is a descending sequence of } W). \end{align*} $$
Since
$\mathcal {M}$
is a
$\Delta ^0_k\beta $
-model,
$\mathcal {M} \models \lnot \mathrm {WO}(W)$
. However, this is a contradiction.
Now, we have the implication 
. For the converse, we consider a
$\Delta ^0_k$
analogue of the implication 
. The point of this implication is that for a given coded
$\omega $
-model
$\mathcal {M}$
of 
, the set of
$\mathrm {A}\Pi ^1_1$
-definable subclasses
$\{ \{n : \mathcal {M} \models \theta (n)\} : \theta \in \mathrm {A}\Pi ^1_1 \}$
of
$\mathcal {M}$
forms a
$\beta $
-extension of
$\mathcal {M}$
. For considering a
$\Delta ^0_k$
analogue, we begin with introducing the classes
$\Sigma ^0_k(\Pi ^1_1),\Pi ^0_k(\Pi ^1_1)$
and
$\Delta ^0_k(\Pi ^1_1)$
. Intuitively,
$\Sigma ^0_k(\Pi ^1_1)$
is the class of formulas of the form
$\varphi [t \in X/\theta (t)]$
for some
$\Sigma ^0_k$
formula
$\varphi $
and
$\Pi ^1_1$
formula
$\theta (x)$
,
$\Pi ^0_k(\Pi ^1_1)$
is its dual, and
$\Delta ^0_k(\Pi ^1_1)$
is the intersection of
$\Sigma ^0_k(\Pi ^1_1)$
and
$\Pi ^0_k(\Pi ^1_1)$
. Here,
$\varphi [t \in X/\theta (t)]$
is the formula obtained from
$\varphi $
by replacing each occurrence of
$t \in X$
with
$\theta (t)$
. Formally, we define these classes as follows.
Definition 3.21. We say a set
$\varphi $
is
$\Pi ^0_1(\Pi ^1_1)$
if it is of the form
$\forall x \theta (x)$
for some formula
$\theta $
which is built from
$\Pi ^1_1$
using logical connectives
$\lor ,\land ,\lnot $
and bounded quantifiers
$\forall x < y,\exists x < y$
. Similarly, a formula is
$\Sigma ^0_1(\Pi ^1_1)$
if it is of the form
$\exists x \theta (x)$
for some formula
$\theta $
which is built from
$\Pi ^1_1$
using logical connectives
$\lor ,\land ,\lnot $
and bounded quantifiers
$\forall x < y,\exists x < y$
. For the general case, we say a formula is
$\Pi ^0_{k+1}(\Pi ^1_1)$
if it is of the form
$\forall x \theta (x)$
for some formula
$\theta $
which is built from
$\Pi ^0_k(\Pi ^1_1)$
using logical connectives
$\lor ,\land ,\lnot $
and bounded quantifiers
$\forall x < y,\exists x < y$
. We also say a formula is
$\Sigma ^0_{k+1}(\Pi ^1_1)$
if it is of the form
$\exists x \theta (x)$
for some formula
$\theta $
which is built from
$\Pi ^0_k(\Pi ^1_1)$
using logical connectives
$\lor ,\land ,\lnot $
and bounded quantifiers
$\forall x < y,\exists x < y$
.
We say a formula is
$\Delta ^0_n(\Pi ^1_1)$
(in a fixed base theory T) if it belongs to both
$\Pi ^0_n(\Pi ^1_1)$
and
$\Sigma ^0_n(\Pi ^1_1)$
.
In what follows, we show that the class of
$\Delta ^0_n(\Pi ^1_1)$
-definable sets forms a model of
$\mathsf {RCA}_0$
in a sense.
Lemma 3.22 ().
). The class
$\Sigma ^0_n(\Pi ^1_1)$
is closed under
$\lor ,\land $
and bounded quantifications and the existential number quantification. Similarly,
$\Pi ^0_n(\Pi ^1_1)$
is closed under
$\lor ,\land $
and bounded quantifications and the universal number quantification.
Proof. Working in 
, the usual proof for the closure properties of
$\Sigma ^0_n$
and
$\Pi ^0_n$
works.
Lemma 3.23 ().
). The class
$\Pi ^0_n(\Pi ^1_1)$
is a subclass of
$\Pi ^1_{n+1}$
.
Proof. We prove by induction on n. We note that if a formula
$\varphi $
is built from
$\Pi ^1_1$
with
$\land ,\lor ,\lnot ,\forall x < y,\exists x < y$
, then
$\varphi $
is
$\Delta ^1_2$
in 
. Thus, a
$\Pi ^0_1(\Pi ^1_1)$
formula is of the form
$\forall x \Delta ^1_2$
, and hence
$\Pi ^1_2$
.
For the induction step, we can show that a formula built from
$\Pi ^0_n(\Pi ^1_1)$
with
$\land , \lor , \lnot ,\forall x < y,\exists x < y$
is
$\Delta ^1_{n+1}$
. Thus, we have that a
$\Pi ^0_{n+1}(\Pi ^1_1)$
formula is
$\Pi ^1_{n+1}$
formula.
Lemma 3.24 ().
). Let
$\varphi (n)$
be a
$\Sigma ^0_k(\Pi ^1_1)$
formula and
$\psi (n)$
be a
$\Pi ^0_k(\Pi ^1_1)$
formula. If
$X = \{n : \varphi (n)\} = \{n : \psi (n)\}$
and
$Y \leq _{\mathrm {T}} X$
, then Y is
$\Delta ^0_n(\Pi ^1_1)$
-definable.
Proof. It is enough to show that if Y is
$\Sigma ^0_1$
-definable from X then Y is
$\Sigma ^0_k(\Pi ^1_1)$
-definable, and if Y is
$\Pi ^0_1$
-deinable from X then Y is
$\Pi ^0_k(\Pi ^1_1)$
-definable. This is immediate from induction on the construction of
$\Sigma ^0_1/\Pi ^0_1$
formulas.
Lemma 3.25 ().
). Let
$\varphi _X(n),\varphi _Y(n)$
be
$\Sigma ^0_k(\Pi ^1_1)$
formulas and
$\psi _X(n)$
,
$\psi _Y(n)$
be
$\Pi ^0_k(\Pi ^1_1)$
formulas. If
$X = \{n: \varphi _X(n)\} = \{n: \varphi _Y(n)\}$
and
$Y = \{n : \varphi _Y(n)\} = \{n : \varphi _Y(n)\}$
, then
$X \oplus Y$
is
$\Delta ^0_k(\Pi ^1_1)$
-definable.
Proof. Recall that
$X {\kern-1pt}\oplus{\kern-1pt} Y {\kern-1pt}={\kern-1pt} \{2n : n \in X\} \cup \{2n+1 : n \in Y\} {\kern-1pt}={\kern-1pt} \{2n : \varphi _X(n)\} \cup \{2n+1 : \varphi _Y(n)\}$
. Define
$\varphi (n) \equiv \exists m ((m = 2n \land \varphi _X(m)) \lor (m = 2n+1 \land \varphi _Y(m))$
. Since
$\Sigma ^0_k(\Pi ^1_1)$
is closed under logical connectives and existential number quantification,
$\varphi $
is also
$\Sigma ^0_k(\Pi ^1_1)$
. Similarly,
$\psi (n) \equiv \forall m ((m = 2n \to \varphi _X(m)) \lor (m = 2n+1 \to \varphi _Y(m))$
is
$\Pi ^0_k(\Pi ^1_1)$
. Then,
$X \oplus Y$
is defined by both
$\varphi $
and
$\psi $
. This completes the proof.
Lemma 3.26 (
$\mathsf {ACA}_0$
).
Let
$\mathcal {M}$
and
$\mathcal {N}$
be coded
$\omega $
-models such that
$\mathcal {M} \models \mathsf {ACA}_0, \mathcal {N} \models \mathsf {RCA}_0$
and
$\forall X(X \in \mathcal {M} \to X \in \mathcal {N})$
. Assume that for any linear order
$L \in \mathcal {M}$
,
$\mathcal {M} \models \mathrm {WO}(L)$
if and only if
$\mathcal {N} \models \mathrm {WO}(L)$
. Then for any
$\Sigma ^1_1(\Pi ^0_2)$
sentence
$\sigma $
with parameters from
$\mathcal {M}$
,
$\mathcal {M} \models \sigma $
if and only if
$\mathcal {N} \models \sigma $
.
Proof. Write
$\sigma \equiv \exists X \forall x \exists y \theta $
by a
$\Sigma ^0_0$
formula
$\theta $
. It is enough to show that if
$\mathcal {N} \models \sigma $
then
$\mathcal {M} \models \sigma $
.
By Skolemization and Kleene’s normal form, there is a
$\Sigma ^0_0$
formula
$\eta $
such that
$\sigma \leftrightarrow \exists X \exists f \in \mathbb {N}^{\mathbb {N}} \forall x \eta (X[x],x,f[x])$
is provable in
$\mathsf {RCA}_0$
. Assume
$\mathcal {N} \models \exists X \forall x \exists y \theta (X,x,y)$
. Pick an
$X_0$
and
$f_0$
such that
$\mathcal {N} \models \forall x \eta (X_0[x],x,f_0[x])$
. We define a tree
$T \subseteq (2 \times \mathbb {N})^{<\mathbb {N}}$
by
$T = \{(\sigma , \tau ) : \eta (\sigma ,|\sigma |,\tau ) \}$
. Then, T is computable from parameters in
$\sigma $
. Thus, T is in
$\mathcal {M}$
and
$\mathbb {N}$
.
We have
$\mathcal {N} \models (X_0,f_0) \in [T]$
. Thus,
$\mathcal {N} \models \lnot \mathrm {WO}(\mathrm {KB}(T))$
where
$\mathrm {KB}(T)$
denotes the Kleene-Brouwer ordering of T. By assumption,
$\mathcal {M} \models \lnot \mathrm {WO}(\mathrm {KB}(T))$
. Since
$\mathcal {M}$
is a model of
$\mathsf {ACA}_0$
,
$\mathcal {M} \models [T] \neq \varnothing $
. Thus,
$\mathcal {M} \models \sigma $
.
Lemma 3.27 (
$\mathsf {RCA}_0$
).
implies
$\Delta ^0_k\mathsf {LPP}$
.
Proof. Since 
implies
$\mathsf {ACA}_0^ +$
, we may assume
$\mathsf {ACA}_0^+$
.
Let T be an ill-founded tree with a path f. Take an
$\omega $
-model
$\mathcal {M}$
such that 
and
$T,f \in \mathcal {M}$
.
Let
$\langle (\varphi _e(x),\psi _e(x)) \rangle _e$
be an enumeration of 
formulas. That is, each
$\varphi _e$
is
$\Sigma ^0_k(\Pi ^1_1)$
and
$\psi _e$
is
$\Pi ^0_k(\Pi ^1_1)$
having the same parameters from
$\mathcal {M}$
, and
$$ \begin{align*}\mathcal{M} \models \forall x (\varphi_e(x) \leftrightarrow \psi_e(x)).\end{align*} $$
Define
$\mathcal {N}_{e} = \{x: \mathcal {M} \models \varphi _e(x)\}$
and
$\mathcal {N} = \langle \mathcal {N}_e \rangle _e$
. Since
$\mathcal {N}$
is closed under Turing reduction and Turing sum,
$\mathcal {N}$
is an
$\omega $
-model of
$\mathsf {RCA}_0$
.
We show that
$\mathcal {M} \models \mathrm {WO}(L)$
if and only if
$\mathcal {N} \models \mathrm {WO}(L)$
for any linear order
$L \in \mathcal {M}$
. Let
$L \in \mathcal {M}$
be a linear order. Assume
$\mathcal {M} \models \mathrm {WO}(L)$
but
$\mathcal {N} \not \models \mathrm {WO}(L)$
. Then, there exists
$Y \in \mathcal {N}$
such that
$\varnothing \subsetneq Y \subseteq |L|$
and Y has no minimal element. Here,
$|L|$
denotes the field of L. Let
$\varphi _e,\psi _e$
be the defining formulas of Y. That is,
$$ \begin{align*} &\mathcal{M} \models \varphi_e \leftrightarrow \psi_e, \\ &\forall x (x \in Y \leftrightarrow \mathcal{M} \models \varphi_e(x)). \end{align*} $$
We show that
$\mathcal {M} \models \forall i \in |L| (\lnot \varphi _e(i))$
by transfinite induction along L. Let
${i \in |L|}$
such that
$\mathcal {M}$
satisfies
$\forall j <_L i\,\lnot \varphi _e(j)$
. Then,
$\forall j <_L i (j \not \in Y)$
. Since Y has no minimal element,
$i \not \in Y$
and hence
$\mathcal {M}$
satisfies
$\lnot \varphi _e(i)$
. We have
$Y = \varnothing $
, contradiction.
We note that
$\mathcal {M}$
and
$\mathcal {N}$
are
$\exists f \Pi ^0_2$
conservative by Lemma 3.26. Define a tree
$S = \{\sigma : \mathcal {M} \models \exists f \in [T] (\sigma \prec f)\}$
. Then,
$S = \{\sigma : \mathcal {N} \models \exists f \in [T] (\sigma \prec f)\}$
by conservativity. In addition,
$S \in \mathcal {N}$
because S is
$\Sigma ^1_1$
definable over
$\mathcal {M}$
. Let
$\varphi (x)$
be a
$\Sigma ^1_1$
formula defining S. Then, there exists a
$\Delta ^0_{k}(\Pi ^1_1)$
formula
$\psi (x)$
such that
${\mathrm {TJ}}^{k-1}(S) = \{x : \mathcal {M} \models \psi (x)\}$
. Thus,
${\mathrm {TJ}}^{k-1}(S)$
is in
$\mathcal {N}$
.
We note that S is an ill-founded pruned tree by definition. Therefore, S computes its leftmost path g. Then,
${\mathrm {TJ}}^{k-1}(g) \leq _{\mathrm {T}} {\mathrm {TJ}}^{k-1}(S)$
and hence g and
${\mathrm {TJ}}^{k-1}(g) \in \mathcal {N}$
. We claim that g is a
$\Delta ^0_k$
-leftmost path of T. Indeed, if a path
$h \in [T]$
satisfies
$h \leq _{\mathrm {T}} {\mathrm {TJ}}^{k-1}(g)$
, then
$h \in \mathcal {N}$
and hence
$h \in [S]$
. Then, g is lexicographically smaller than h because g is the leftmost path of S.
Theorem 3.28. For
$k \in \omega $
such that
$k> 1$
, the following assertions are equivalent over
$\mathsf {RCA}_0{:}$
-
1.
$\Sigma ^0_k\mathsf {LPP}$
, -
2.
, -
3. the
$\omega $
-model reflection of , -
4. the
$\omega $
-model reflection of .
,
,
.Proof. We note that each assertion includes
$\mathsf {ACA}_0$
. Therefore, we may assume that we work in
$\mathsf {ACA}_0$
.
The implication
$(1) \to (2)$
is Lemma 3.17. The implication
$(2) \to (3)$
is immediate form Lemma 3.20. The implication
$(3) \to (4)$
follows from Lemma 3.23. The implication
$(4) \to (1)$
is Lemma 3.27.
Remark 3.29. We note that the implications
$(2) \to (3) \to (4) \to (1)$
still hold for
$n =1$
. We do not know either
$(1) \to (2)$
holds for
$n=1$
.
Remark 3.30. In [Reference Towsner8], Towsner proved that
-
1.
$\mathsf {RCA}_0 + \Sigma ^0_{k+2}\mathsf {LPP}$
implies the existence of an
$\omega $
-model of (Theorem 4.3), -
2.
proves
$\Sigma ^0_k\mathsf {LPP}$
(Theorem 6.1).
(Theorem 4.3),
proves 
The previous theorem can be seen as a refinement of these results.
At the end of this section, we see some applications of the previous theorem.
Corollary 3.31. Let
$k \in \omega $
such that
$k> 1$
. Then
$\Sigma ^0_{k}\mathsf {LPP}$
is equivalent to 
over
$\mathsf {RCA}_0$
.
Proof. It is immediate from the fact that 
is equivalent to the
$\Pi ^1_{k+2}$
reflection over
$\mathsf {RCA}_0$
.
Corollary 3.32. Let
$n \in \omega $
such that
$n> 0$
. Then,
$\Sigma ^0_{n+1}\mathsf {LPP}$
proves the
$\omega $
-model reflection of
$\Sigma ^0_n\mathsf {LPP}$
over
$\mathsf {RCA}_0$
. Hence,
$\Sigma ^0_{n+1}\mathsf {LPP}$
is strictly stronger than
$\Sigma ^0_n\mathsf {LPP}$
.
Proof. Since 
proves a
$\Pi ^1_{n+2}$
axiomatizable theory 
, it proves the
$\omega $
-model reflection of 
. Hence, we have the following implications:
Remark 3.33. Our
$\mathsf {RFN}(\Pi ^1_{n+2}\mathsf {RFN}_0)$
is the same as Probst’s
$\mathsf {p_1}\mathsf {p_{n+2}}(\mathsf {ACA}_0)$
. He studied the proof theoretic strength of
$\mathsf {p_1}\mathsf {p_{n+2}}(\mathsf {ACA}_0)$
in his habilitation thesis [Reference Probst4].
4 Weihrauch degrees
In [Reference Suzuki and Yokoyama7], the author and Yokoyama introduced a Weihrauch problem corresponding to
$\Sigma ^0_n\mathsf {LPP}$
and studied the computability-theoretic strength of it. In this section, we refine the results in [Reference Suzuki and Yokoyama7]. We prove that
$\Sigma ^0_{n+1}\mathsf {LPP}$
is strictly stronger than
$\Sigma ^0_{n}\mathsf {LPP}$
in the sense of Weihrauch reducibility.
Definition 4.1. A Weihrauch problem is a partial multivalued function on the Cantor space
$2^{\omega }$
.
We sometimes identify a Weihrauch problem
$\mathsf {P}$
and a partial function
$\mathsf {P}'$
from
$2^{\omega }$
to
$\mathcal {P}(2^{\omega })$
defined by
$\mathsf {P}'(X) = \{Y \subseteq \omega : Y \text { is an output of } \mathsf {P} \text { at } X\}$
. In this sense, we write
$Y \in \mathsf {P}(X)$
to mean Y is an output of
$\mathsf {P}$
at X.
Definition 4.2. Let
$\mathsf {P}$
and
$\mathsf {Q}$
be Weihrauch problems. We say
$\mathsf {P}$
is Weihrauch reducible to
$\mathsf {Q}$
(written
$\mathsf {P} \leq _{\mathrm {W}} \mathsf {Q}$
) if there are (partial) Turing functionals
$\Phi $
and
$\Psi $
such that
$$ \begin{align*} \forall X \in \mathrm{dom}(\mathsf{P})(\Phi(X)\mathord{\downarrow} \in \mathrm{dom}(\mathsf{Q}) \land \forall Y \in \mathsf{Q}(\Phi(X)) (\Psi(X,Y)\mathord{\downarrow} \in \mathsf{P}(X)) ). \end{align*} $$
We write
$\mathsf {P} <_{\mathrm {W}} \mathsf {Q}$
to mean
$\mathsf {P} \leq _{\mathrm {W}} \mathsf {Q}$
but
$\mathsf {Q} \not \leq _{\mathrm {W}} \mathsf {P}$
.
We say
$\mathsf {P}$
and
$\mathsf {Q}$
are Weihrauch equivalent (written
$\mathsf {P} \equiv _{\mathrm {W}} \mathsf {Q}$
) if both of
$\mathsf {P} \leq _{\mathrm {W}} \mathsf {Q}$
and
$\mathsf {Q} \leq _{\mathrm {W}} \mathsf {P}$
hold.
Definition 4.3. We define Weihrauch problems
$\Sigma ^0_n\mathsf {LPP},\Delta ^0_n\mathsf {LPP}$
and
$\Delta ^0_n\overline {\mathsf {LPP}}$
as follows. [l]
$\Sigma ^0_n\mathsf {LPP}$
-
$\textsf {Input}$
An ill-founded tree
$T \subseteq \omega ^{<\omega }$
and a path f of T.
-
$\textsf {Output}$
A path g of T such that g is leftmost in
$\Sigma ^0_{n}(T \oplus f \oplus g)$
.
[l]
$\Delta ^0_n\mathsf {LPP}$
-
$\textsf {Input}$
An ill-founded tree
$T \subseteq \omega ^{<\omega }$
and a path f of T.
-
$\textsf {Output}$
A path g of T such that g is leftmost in
$\Delta ^0_{n}(T \oplus f \oplus g)$
.
[l]
$\Delta ^0_n\overline {\mathsf {LPP}}$
-
$\textsf {Input}$
An ill-founded tree
$T \subseteq \omega ^{<\omega }$
and a path f of T.
-
$\textsf {Output}$
A path g of T such that g is leftmost in
$\Delta ^0_{n}(g)$
.
Lemma 4.4.
$\Sigma ^0_n\mathsf {LPP}\equiv _{\mathrm {W}} \Delta ^0_n\mathsf {LPP} \equiv _{\mathrm {W}} \Delta ^0_n\overline {\mathsf {LPP}}$
.
Proof. As a path is
$\Sigma ^0_n$
-definable if and only if it is
$\Delta ^0_n$
-definable,
$\Sigma ^0_n\mathsf {LPP}$
and
$\Delta ^0_n\mathsf {LPP}$
are the same. For the equivalence of
$\Delta ^0_n\mathsf {LPP}$
and
$\Delta ^0_n\overline {\mathsf {LPP}}$
, see [Reference Suzuki and Yokoyama7, Lemma 6.5]
As the same proof of Lemma 3.17, the following problem is Weihrauch reducible to
$\Sigma ^0_n\mathsf {LPP}$
for
$n> 1$
. [l]
$\mathrm {R}\Delta ^0_n\beta \mathsf {RFN}$
-
$\textsf {Input}$
Any set X.
-
$\textsf {Output}$
A
$\Delta ^0_n\beta $
-model
$\mathcal {M}$
and computable functions
$f_{{\mathrm {TJ}}},f_{\oplus },f_{\Sigma ^1_1}$
such that
$$ \begin{align*} X \in \mathcal{M}, && (f_{{\mathrm{TJ}}},f_{\oplus}) \Vdash_{\mathcal{M}} \mathsf{ACA}_0, && f_{\Sigma^1_1} \Vdash_{\mathcal{M}} \exists X \Pi^0_2. \end{align*} $$
We see that the converse reduction also holds.
Theorem 4.5. For
$n> 1$
,
$\Sigma ^0_n\mathsf {LPP} \equiv _{\mathrm {W}} \mathrm {R}\Delta ^0_n\beta \mathsf {RFN}$
.
Proof. It is enough to show that
$\Delta ^0_n\overline {\mathsf {LPP}} \leq _{\mathrm {W}} \mathrm {R}\Delta ^0_n\beta \mathsf {RFN}$
holds. Let T be a tree and f be its path. Let
$\mathcal {M}, f_{{\mathrm {TJ}}},f_{\oplus },f_{\Sigma ^1_1}$
be such that
$$ \begin{align*} T,f \in \mathcal{M}, && (f_{{\mathrm{TJ}}},f_{\oplus}) \Vdash_{\mathcal{M}} \mathsf{ACA}_0, && f_{\Sigma^1_1} \Vdash_{\mathcal{M}} \exists X \Pi^0_2. \end{align*} $$
Define a subtree S of T as the set of
$\sigma $
in T such that
$\mathcal {M}$
believes
$\sigma $
is extended to a path. That is,
$S = \{\sigma \in T : \mathcal {M} \models \exists g \in [T] (\sigma \prec g)\}$
. Then, S is
$\mathcal {M}$
-computable by Lemma 3.18. Moreover, it is easy to see that there is a uniform procedure to make S from
$\mathcal {M},f_{{\mathrm {TJ}}},f_{\oplus },f_{\Sigma ^1_1}$
. We now have
-
• S is ill-founded because
$f \in [S]$
, -
• S is pruned because of the definition, and
-
•
$S = \{\sigma \in T : \exists g \in [T] \cap \Delta ^0_n(\mathcal {M}) (\sigma \prec g)\}$
because
$\mathcal {M}$
is
$\Delta ^0_n\beta $
-model.
Let
$g \leq _{\mathrm {T}} S$
be the leftmost path of S. Then, g is leftmost in
$\Delta ^0_n(\mathcal {M})$
. Since g is
$\mathcal {M}$
-computable, g is leftmost in
$\Delta ^0_n(g)$
. This completes the proof.
We then show the separation of
$\Sigma ^0_{n+1}\mathsf {LPP}$
and
$\Sigma ^0_n\mathsf {LPP}$
. For the separation, we use the
$\omega $
-model reflection of a Weihrauch problem introduced in [Reference Suzuki and Yokoyama7].
Definition 4.6. Let
$\mathsf {P}$
be a Weihrauch problem. We define the
$\omega $
-model reflection of
$\mathsf {P}$
as the following problem.
-
$\textsf {Input}$
Any set X.
-
$\textsf {Output}$
A sequence
$\mathcal {M}$
and functions
$f_{{\mathrm {TJ}}},f_{\oplus }$
such that
$$ \begin{align*} &X \in \mathcal{M} \,\&\, (f_{{\mathrm{TJ}}},f_{\oplus}) \Vdash_{\mathcal{M}} \mathsf{ACA}_0 \,\& \\ &\forall Y \in \mathcal{M} \cap \mathrm{dom}(\mathsf{P}) \exists Z \in \mathcal{M} (Z \in \mathsf{P}(X)) \end{align*} $$
We note that if there are arithmetical formulas
$\theta ,\eta $
such that
$\mathrm {dom}(\mathsf {P}) = \{X: \theta (X)\}$
and
$\mathsf {P}(X) {\kern-1pt}={\kern-1pt} \{Y : \eta (X,Y)\}$
, then the condition
$\forall Y {\kern-1pt}\in{\kern-1pt} \mathcal {M} \cap \mathrm {dom}(\mathsf {P}) \exists Z \in \mathcal {M} (Z \in \mathsf {P}(X))$
is equivalent to
$\mathcal {M} \models \mathsf {P}$
. It is also proved that in that case, the
$\omega $
-model reflection of the problem is strictly stronger than the problem. For details, see [Reference Suzuki and Yokoyama7, Section 4]. We note that the input and output conditions of
$\Sigma ^0_n\mathsf {LPP}$
can be written by arithmetical formulas.
Lemma 4.7 (
$\mathsf {ACA}_0$
).
Let
$\mathcal {M}$
be a
$\Delta ^0_{n+1}\beta $
-model and
$f_{{\mathrm {TJ}}},f_{\oplus },f_{\Sigma ^1_1}$
be computable functions such that
$(f_{{\mathrm {TJ}}},f_{\oplus }) \Vdash _{\mathcal {M}} \mathsf {ACA}_0$
and
$f_{\Sigma ^1_1} \Vdash _{\mathcal {M}} \exists \Pi ^0_2$
. Then,
$\mathcal {M}$
is a model of
$\Sigma ^0_n\mathsf {LPP}$
.
Proof. Let
$T \in \mathcal {M}$
be a tree such that
$\mathcal {M} \models [T] \neq \varnothing $
. Then, as in the proof of Theorem 4.5, there is an
$\mathcal {M}$
-computable function g such that
$\forall f \leq _{\mathrm {T}} {\mathrm {TJ}}^n(g) (f \in [T] \to g \leq _{l} f)$
. In particular, we have
$\forall f \leq _{\mathrm {T}} {\mathrm {TJ}}^{n-1}(g) (f \in [T] \to g \leq _{l} f)$
. Thus, we have
$$ \begin{align*} (\ast) \ \ \exists (g_0 \oplus g_1 \oplus \cdots \oplus g_n) \leq_{\mathrm{T}} {\mathrm{TJ}}^{n}(\mathcal{M}) \Big[&\bigwedge_{i < n} g_i = {\mathrm{TJ}}(g_{i-1}) \\ \land & \forall f \leq_{\mathrm{T}} g_{n-1} (f \in [T] \to g_0 \leq_{\mathrm{T}} f \Big]. \end{align*} $$
by taking
$g_i = {\mathrm {TJ}}^i(g)$
. We note that the condition in the square bracket is
$\Pi ^0_2$
for
$(g_0 \oplus g_1 \oplus \cdots \oplus g_n)$
because
$g_n = {\mathrm {TJ}}(g_{n-1})$
. Therefore, the above
$(\ast )$
is of the form
$\exists X \leq _{\mathrm {T}} {\mathrm {TJ}}^n(\mathcal {M}) \theta (X)$
for a
$\Pi ^0_2$
formula
$\theta $
. Since
$\mathcal {M}$
is a
$\Delta ^0_{n+1}\beta $
-model, we have
$$ \begin{align*} \mathcal{M} \models \exists g_0 \forall f \leq_{\mathrm{T}} {\mathrm{TJ}}^{n-1}(g_0) (f \in [T] \to g_0 \leq_{\mathrm{T}} f). \end{align*} $$
Thus,
$\mathcal {M}$
believes that T has a
$\Delta ^0_n$
leftmost path. This completes the proof.
Theorem 4.8. For
$n> 0$
,
$\Sigma ^0_n\mathsf {LPP} <_{\mathrm {W}} \Sigma ^0_{n+1}\mathsf {LPP}$
.
Acknowledgments
The author would like to thank Keita Yokoyama, Anton Freund, and Koshiro Ichikawa for their useful comments and discussions for this article.
