Parallelizations in Weihrauch Reducibility and Constructive Reverse Mathematics

Abstract

In the framework of finite-type arithmetic, we characterize the notion that an existence statement is primitive recursive Weihrauch reducible to the parallelization of another existence statement by a standard derivability notion in constructive reverse mathematics.

1 Introduction

A large amount of mathematical statements are of the logical form

$$\begin{aligned} \forall f (A(f) \rightarrow \exists g B (f, g)), \end{aligned}$$

(1)

where f and g may be tuples. Such statements are often called existence statements since they argue the existence of some objects. One can see existence statements represented as sentences of the form (1) as problems to be solved. In such a context, any f such that A(f) holds is called an instance of the problem and g is called a solution to the instance. Uniform relationships between existence statements have been investigated extensively in computable analysis and classical reverse mathematics ([4,5,6,7,8, 15] etc.). The investigation usually employs the following reduction: a $\mathrm{\Pi ^1_2}$ sentence $\mathrm{P}$ of the form (1) is reducible to another $\mathrm{\Pi ^1_2}$ sentence $\mathrm{Q}$ of the form (1) if there exist Turing functionals $\varPhi$ and $\varPsi$ such that whenever $f_1$ is an instance of $\mathrm{P}$, then $\varPhi (f_1)$ is an instance of $\mathrm{Q}$, and whenever $g_2$ is a solution to $\varPhi (f_1)$, then $g_1:=\varPsi (f_1, g_2)$ is a solution to $f_1$. This is a particular case of Weihrauch reducibility for $\mathrm{\Pi ^1_2}$ sentences with Baire space as their represented spaces (see [8, Appendix]). For a detailed account of uniformity, the parallelizations:

$$\begin{aligned} \forall {\langle f_{n} \rangle } _{n\in \mathbb {N}} (\forall n^{\mathbb {N}} A(f_{n}) \rightarrow \exists {\langle g_{n} \rangle } _{n\in \mathbb {N}} \forall n^{\mathbb {N}} B (f_{n}, g_{n})), \end{aligned}$$

have been studied in computable analysis ([4, 5]) and also in classical reverse mathematics under the name of sequential versions ([8, 11, 12]). In particular, the weak König lemma $\mathrm {WKL}$, is not Weihrauch reducible to the intermediate value theorem IVT, but is so to the parallelization of IVT (see [4]).

On the other hand, there is another development on the relation between existence statements from constructive mathematics [3], where every existence is shown by giving a construction of the witness entirely in the proofs. Ishihara and others have developed reverse mathematics first informally in Bishop’s constructive mathematics, and later formally in two-sorted intuitionistic arithmetic ([1, 9, 14] etc.). In particular, the intermediate value theorem IVT is known to be equivalent to the weak König lemma $\mathrm {WKL}$ over the constructive base theory containing a countable choice principle (see [1, Section 1]).

Interestingly, there are several corresponding results between constructive reverse mathematics and computability-theoretic investigations on parallelizations or sequential versions, including the above mentioned facts on $\mathrm {WKL}$ and $\mathrm {IVT}$. In particular, it seems to be believed in the community of computable analysis that constructive equivalences of two existence statements in Bishop’s constructive mathematics (which accepts the use of a countable choice principle) correspond to Weihrauch equivalences of their parallelizations (see [6, Footnote c]). In this paper, we verify that this experimental belief is plausible by showing some meta-theorems in the framework of finite-type arithmetic together with observations in some concrete examples. This sheds light on the correspondence between computable analysis and constructive reverse mathematics which have been developed independently until recently. The investigation in this paper is based on the previous work [10] of the author himself.

As a framework for our investigation, we employ an extensional variant $\mathsf {E\text {-}HA^\omega }$ of intuitionistic arithmetic in all finite types and its fragment $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$ from [17, Section 3.3]. Recall that finite types are defined as follows: $\mathbb {N}$ is a type; if $\sigma$ and $\tau$ are types, then so is $\sigma \rightarrow \tau$. Note that $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$ has a recursor only of type $\mathbb {N}$ and its induction schema is restricted to quantifier-free formulas. The $\lambda$-abstraction is officially defined by using the combinators. The set of the closed terms of $\mathsf {E\text {-}HA^\omega }$ and that for $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$ are denoted by $\mathbf{T}$ and $\mathbf{T_{0}}$ respectively. The set-theoretic functionals definable in $\mathbf{T}$ (resp. $\mathbf{T_{0}}$) are called Gödel (resp. Kleene) primitive recursive functionals of finite type. A classical variant $\mathsf {E\text {-}PA^\omega }$ (resp. $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }$) is obtained from $\mathsf {E\text {-}HA^\omega }$ (resp. $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$) by adding the axiom scheme of excluded middle $A \vee \lnot A$. The language of our systems contains a binary predicate symbol $=_{\mathbb {N}}$ for equality between objects of type $\mathbb {N}$ only. Throughout this paper, we employ the same notations as in [10]. Note that the type superscripts (for terms) and subscripts (for equality) are omitted when they are clear from the context. A tuple of terms is denoted with a underline as $\underline{t}$. In addition, $\dot{}-$ denotes the primitive recursive cut-off subtraction, and $\{0,1\}^{m}$ denotes the set of all binary sequences of length m. Recall that an $\exists$-free formula is a formula which does not contain $\vee$ and $\exists$. A countable choice principle $\mathrm {AC}^{0, \omega }$ is the following schema:

$$\begin{aligned} (\mathrm {AC}^{0, \omega }) \forall x^{\mathbb {N}} \exists f^{\tau } A(x,f) \rightarrow \exists F^{\mathbb {N}\rightarrow \tau }\forall x^{\mathbb {N}} A(x,Fx), \end{aligned}$$

where $\tau$ is any type. This principle is crucial for our meta-theorems (see Remark 8). For the other principles in this paper, we refer the reader to [10, Section 1.1].

2 Meta-theorems

In this decade, there are several attempts to reveal the proper relation between constructive reverse mathematics and Weihrauch reducibility in classical reverse mathematics and computable analysis ([10, 12, 13, 18, 20] etc.). In particular, the author formalized in [10, Definition 2.5] the primitive recursive variants of Weihrauch reduction between existence statements $\mathrm{P}$ and $\mathrm{Q}$ formalized as $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$-sentences $\forall \underline{f} (A_{1}(\underline{f}) \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g}))$ and $\forall \underline{f} (A_{2}(\underline{f}) \rightarrow \exists \underline{g} B_{2} (\underline{f}, \underline{g}))$ in the context of finite-type arithmetic as follows:

• For a finite-type arithmetic $\mathsf{S^\omega }$ containing $\mathsf {E\text {-}HA^\omega }$, $\mathrm{P}$ is Gödel-primitive-recursive Weihrauch reducible to $\mathrm{Q}$ in $\mathsf{S^\omega }$ if there exist closed terms $\underline{s}$ and $\underline{t}$ (of suitable types) in $\mathbf{T}$ such that $\mathsf{S^\omega }$ proves

  $$\begin{aligned} \forall \underline{f} ( A_{1}(\underline{f}) \rightarrow A_{2} (\underline{s}\underline{f})) \wedge \forall \underline{f}, \underline{g'} \left( B_{2}( \underline{s}\underline{f}, \underline{g'} ) \wedge A_{1} (\underline{f}) \rightarrow B_{1} (\underline{f}, t\underline{f} \,\, \underline{g'} ) \right) . \end{aligned}$$

  (2)

• For a finite-type arithmetic $\mathsf{S^\omega }$ containing $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$, $\mathrm{P}$ is Kleene-primitive-recursive Weihrauch reducible to $\mathrm{Q}$ in $\mathsf{S^\omega }$ if there exist closed terms $\underline{s}$ and $\underline{t}$ (of suitable types) in $\mathbf{T_{0}}$ such that $\mathsf{S^\omega }$ proves (2).

In addition, $\mathrm{P}$ is normally reducible to $\mathrm{Q}$ in $\mathsf{S^\omega }$ if $\mathsf{S^\omega }$ proves

$$\begin{aligned} \forall \underline{f} \left( A_{1}(\underline{f}) \rightarrow \exists \underline{f'} \left( A_{2}(\underline{f'}) \wedge \forall \underline{g'} \left( B_{2}(\underline{f'}, \underline{g'}) \rightarrow \exists \underline{g} B_{1}(\underline{f}, \underline{g}) \right) \right) \right) . \end{aligned}$$

The notions of Gödel/Kleene-primitive-recursive Weihrauch reducibility is a natural restriction of formalized Weihrauch reducibility e.g. in [8, 18] where Turing functionals for the reduction are replaced by primitive recursive functionals in the sense of Gödel/Kleene. The normal reducibility, which requires a proof of $\mathrm{Q \rightarrow P}$ with a specific form, is a stronger notion than just proving $\mathrm{Q\rightarrow P}$ (see [10, Remark 2.9]). Since intuitionistic finite-type arithmetic with a choice principle roughly corresponds to Bishop’s constructive mathematics, one may regard the normal reducibility in a nearly intuitionistic finite-type arithmetic as a sort of constructive reducibility. In [10, Theorem 2.10], the author showed a meta-theorem stating that the primitive-recursive Weihrauch reducibility verifiably in a fragment of classical finite-type arithmetic is equivalent to the normal reducibility in the corresponding (nearly) intuitionistic finite-type arithmetic for all existence statements formalized with $\exists$-free formulas. Thus constructive reducibility can be captured by the primitive-recursive variant of Weihrauch reducibility with an additional restriction on the verification theory (which has not been taken into account in computable analysis). Of course, the Weihrauch reductions between concrete existence statements are not always primitive recursive (in the sense of Gödel/Kleene). In addition, there are many existence statements which are not formalized with $\exists$-free formulas. Nonetheless, there seem to be plenty of examples to which the meta-theorem is applicable. In fact, the Weihrauch reductions between concrete existence statements can be verified usually in a weak theory (cf. [10, Section 3]). On the other hand, any characterization on parallelizations was still missing.

We call sentences of the form $\forall \underline{f} (A(\underline{f}) \rightarrow \exists \underline{g} B (\underline{f}, \underline{g}))$, where $\underline{f}:\equiv f_{1}^{\sigma _{1}}, \dots , f_{k}^{\sigma _{k}}$ and $\underline{g}:\equiv g_{1}^{\tau _{1}}, \dots , g_{l}^{\tau _{l}}$ are finite tuples of variables, normal existential sentences. In the language of finite-type arithmetic, the parallelization of this sentence is formalized as

$$\begin{aligned} \forall f_{1}^{\mathbb {N}\rightarrow \sigma _{1}}, \dots , f_{k}^{\mathbb {N}\rightarrow \sigma _{k}} \left( \begin{array}{l} \forall n^{\mathbb {N}} A\left( f_{1}n, \dots , f_{k}n\right) \rightarrow \\ \exists g_{1}^{\mathbb {N}\rightarrow \tau _{1}}, \dots , g_{l}^{\mathbb {N}\rightarrow \tau _{l}} \forall n^{\mathbb {N}} B\left( f_{1}n, \dots , f_{k}n, g_{1}n, \dots , g_{l}n\right) \end{array} \right) , \end{aligned}$$

which is again a normal existential sentence. For each normal existential sentence $\mathrm{P}$, we write its parallelization as $\widehat{\mathrm{P}}$. Throughout this paper, we sometimes identify a normal existential sentence with the indicated existence statement. The following proposition is shown straightforwardly by the soundness of modified realizability [17, Theorem 5.8].

Proposition 1

For normal existential sentences $\mathrm{P}$ and $\mathrm{Q}$ with $\exists$-free formulas of $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$ (in the sense of Theorem 6), if $\mathrm{P}$ is normally reducible to $\mathrm{Q}$ in $\mathsf {E\text {-}HA^\omega }+ \mathrm {AC}^{\omega } +{\mathrm {IP}}_{\mathrm {ef}}^{\omega }$, then $\widehat{ \mathrm { P }}$ is normally reducible to $\widehat{ \mathrm { Q }}$ in $\mathsf {E\text {-}HA^\omega }$. The analogous result also holds where $\mathsf {E\text {-}HA^\omega }$ is replaced by $\mathsf {E\text {-}HA^\omega }+ \mathrm {QF\text {-}AC}^{0,0} + \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}, \, \mathsf {E\text {-}HA^\omega }+ \mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0} + \mathrm {\Sigma _{2}^{0}\text {-}\mathrm{DNS}^{0}}, \, \mathsf {E\text {-}HA^\omega }+ \mathrm {AC}^{\omega } + \mathrm { mr \text {-} DNS^{\omega }}, \, \mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }, \mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+ \mathrm {QF\text {-}AC}^{0,0} + \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}, \, \mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+ \mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0} + \mathrm {\Sigma _{2}^{0}\text {-}\mathrm{DNS}^{0}}$, or $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+ \mathrm {AC}^{\omega } + \mathrm { mr \text {-} DNS^{\omega }}$.

The following corollary is obtained immediately from [10, Theorem 2.10] and Proposition 1 together with the general fact that $\mathrm{P}$ is normally reducible to $\widehat{ \mathrm { P }}$.

Corollary 2

Let $\mathsf{S}^{\omega }$ be one of the systems $\mathsf {E\text {-}PA^\omega }, \, \mathsf {E\text {-}PA^\omega }+\mathrm {QF\text {-}AC}^{0,0}, \, \mathsf {E\text {-}PA^\omega }+\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}, \, \mathsf {E\text {-}PA^\omega }+\mathrm {AC}^{\omega }, \mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }, \, \mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0}, \, \mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}$, and $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {AC}^{\omega }$. For $\mathrm{P}$ and $\mathrm{Q}$ as in Proposition 1, if $\mathrm{P}$ is Gödel/Kleene-primitive-recursive Weihrauch reducible to $\mathrm{Q}$ in $\mathsf{S}^{\omega }$, then $\mathrm{P}$ is so to $\widehat{ \mathrm { Q }}$ in $\mathsf{S}^{\omega }$.

Remark 3

The relation between $\mathrm {WKL}$ and $\mathrm {IVT}$ in computable analysis, which is mentioned in Sect. 1, shows that the converse of Corollary 2 does not hold.

From the perspective of Corollary 2 and Remark 3, it is worthwhile to characterize the property that $\mathrm{P}$ is Gödel/Kleene-primitive-recursive Weihrauch reducible to $\widehat{ \mathrm { Q }}$ in $\mathsf{S}^{\omega }$ in some natural context of constructive reverse mathematics. For this purpose, we introduce the following notions:

Definition 4

Let $\mathrm{P}$ and $\mathrm{Q}$ be existence statements formalized as normal existential sentences $\forall \underline{f} (A_{1}(\underline{f}) \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g}))$ and $\forall f_{1} ,\dots ,f_{k} (A_{2}(f_{1} ,\dots , f_{k} ) \rightarrow \exists \underline{g} B_{2} (f_{1} ,\dots ,f_{k}, \underline{g})$ of $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$ respectively. For a finite-type arithmetic $\mathsf{S^\omega }$ containing $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$, $\mathrm{P}$ is normally $\mathbf{T}$-derivable from $\mathrm{Q}$ in $\mathsf{S^\omega }$ if there exist closed terms $s_{1}, \dots , s_{k}$ (of suitable types) in $\mathbf{T}$ such that $\mathsf{S^\omega }$ proves

$$\begin{aligned} \forall \underline{f} \left( A_{1}(\underline{f}) \rightarrow \forall m^{\mathbb {N}} A_{2} (s_{1}m\underline{f} , \dots , s_{k}m\underline{f} )\right) \end{aligned}$$

(3)

and

$$\begin{aligned} \forall \underline{f} \left( \begin{array}{l} A_{1}(\underline{f}) \, \wedge \forall m \left( A_{2} (s_{1}m\underline{f} , \dots , s_{k}m\underline{f} ) \rightarrow \exists \underline{g'} B_{2} \left( s_{1}m\underline{f} , \dots , s_{k}m\underline{f}, \underline{g'} \right) \right) \\[5pt] \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g}) \end{array} \right) . \end{aligned}$$

(4)

The notion that $\mathrm{P}$ is normally $\mathbf{T_{0}}$-derivable from $\mathrm{Q}$ in $\mathsf{S^\omega }$ is defined in the same manner with using $\mathbf{T_{0}}$ instead of $\mathbf{T}$. In fact, “$A_2(s_1 m \underline{f},..., s_k m \underline{f}) \rightarrow$” in (4) is redundant in the presence of (3).

Remark 5

For existence statements $\mathrm{P}:\, \forall \underline{f} (A_{1}(\underline{f}) \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g}))$ and $\mathrm{Q}$, the fact that $\mathrm{P}$ is normally derivable from $\mathrm{Q}$ demands some proof of $\mathrm{Q \rightarrow P}$ with the following structure:

• 1. Fix $\underline{f}$ such that $A_{1}(\underline{f})$;

• 2. Assuming $A_{1}(\underline{f})$, derive $\exists \underline{g} B_{1} (\underline{f}, \underline{g})$ by using $\mathrm{Q}$ for the countably many instances which are given primitive recursively in $\underline{f}$.

For existence statements $\mathrm{P}$ and $\mathrm{Q}$, it is quite common in practical mathematics (not only in constructive mathematics) to show $\mathrm{Q \rightarrow P}$ in this manner.

On the other hand, the normal derivability is properly weaker than the normal reducibility in the context of (nearly) intuitionistic systems. Note also that the normal derivability relation is reflexive and transitive.

Theorem 6

Let $\mathrm{P}$ and $\mathrm{Q}$ be existence statements formalized as normal existential sentences $\forall \underline{f} (A_{1}(\underline{f}) \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g}))$ and $\forall f_{1} ,\dots ,f_{k} (A_{2}(f_{1} ,\dots , f_{k} ) \rightarrow \exists \underline{g'} B_{2} (f_{1} ,\dots ,f_{k}, \underline{g'})$ of $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$ respectively with $\exists$-free formulas $A_{1}, A_{2}, B_{1}$, and $B_{2}$. Then the following hold:

• 1. $\mathrm{P}$ is Gödel-primitive-recursive Weihrauch reducible to $\widehat{ \mathrm { Q }}$ in $\mathsf {E\text {-}PA^\omega }$ if and only if $\mathrm{P}$ is normally $\mathbf{T}$-derivable from $\mathrm{Q}$ in $\mathsf {E\text {-}HA^\omega }+ \mathrm {AC}^{0, \omega }$.

• 2. $\mathrm{P}$ is Kleene-primitive-recursive Weihrauch reducible to $\widehat{ \mathrm { Q }}$ in $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }$ if and only if $\mathrm{P}$ is normally $\mathbf{T_{0}}$-derivable from $\mathrm{Q}$ in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+ \mathrm {AC}^{0, \omega }$.

Proof

(1) Assume that $\mathrm{P}$ is Gödel-primitive-recursive Weihrauch reducible to $\widehat{ \mathrm { Q }}$ in $\mathsf {E\text {-}PA^\omega }$. As in the proof of [10, Theorem 2.10], by the negative translation (see [17, Section 10.1]), we have that $\mathsf {E\text {-}HA^\omega }$ proves $\forall \underline{f} ( A_{1}(\underline{f}) \rightarrow \forall n^{\mathbb {N}} A_{2} (s_{1}\underline{f}n,\dots , s_{k}\underline{f}n))$ and $\forall \underline{f}, \underline{G'} ( \forall n^{\mathbb {N}}B_{2}( s_{1}\underline{f}n, \dots , s_{k}\underline{f}n, \underline{G'}n ) \wedge A_{1} (\underline{f}) \rightarrow B_{1} (\underline{f}, \underline{t}\underline{f}\underline{G'} ) )$ for some closed terms $s_{1}, \dots , s_{k}$ and $\underline{t}$ in $\mathbf{T}$. Put a closed term $\tilde{s}_{i}$ as $\lambda n, \underline{f}. \, s_{i} \underline{f} n$ for each $i\in \{ 1, \dots , k\}$. Then we have that $\mathsf {E\text {-}HA^\omega }$ proves

$$\begin{aligned} \forall \underline{f} ( A_{1}(\underline{f}) \rightarrow \forall n^{\mathbb {N}} A_{2} (\tilde{s}_{1}n\underline{f},\dots , \tilde{s}_{k}n\underline{f})) \end{aligned}$$

(5)

and

$$\begin{aligned} \forall \underline{f}, \underline{G'} \left( \forall n^{\mathbb {N}}B_{2}( \tilde{s}_{1}n\underline{f},\dots , \tilde{s}_{k}n\underline{f}), \underline{G'}n ) \wedge A_{1} (\underline{f}) \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g} ) \right) . \end{aligned}$$

(6)

Applying $\mathrm {AC}^{0, \omega }$ to (6), we have

$$\begin{aligned} \forall \underline{f} \left( \forall n^{\mathbb {N}} \exists \underline{g'}B_{2}( \tilde{s}_{1}n\underline{f},\dots , \tilde{s}_{k}n\underline{f}), \underline{g'}) \wedge A_{1} (\underline{f}) \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g} ) \right) . \end{aligned}$$

(7)

Then it follows from (5) and (7) that

$$\begin{aligned} \forall \underline{f} \left( \begin{array}{l} A_{1}(\underline{f}) \, \wedge \forall n^{\mathbb {N}} \left( A_{2} (\tilde{s}_{1}n\underline{f},\dots , \tilde{s}_{k}n\underline{f}) \rightarrow \exists \underline{g'} B_{2} \left( \tilde{s}_{1}n\underline{f},\dots , \tilde{s}_{k}n\underline{f}, \underline{g'} \right) \right) \\[5pt] \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g}) \end{array} \right) . \end{aligned}$$

(8)

Thus $\mathrm{P}$ is normally $\mathbf{T}$-derivable from $\mathrm{Q}$ in $\mathsf {E\text {-}HA^\omega }+ \mathrm {AC}^{0, \omega }$.

For the converse direction, assume that $\mathsf {E\text {-}HA^\omega }+ \mathrm {AC}^{0, \omega }$ proves (5) and (8) for some closed terms $\tilde{s}_{1}, \dots , \tilde{s}_{k}$ in $\mathbf{T}$. By (8), we have that $\mathsf {E\text {-}HA^\omega }+ \mathrm {AC}^{0, \omega }$ proves (7), and hence, (6).

As in the proof of [10, Theorem 2.10], by the soundness of modified realizability [17, Theorem 5.8], there exist closed terms $\underline{t}$ in $\mathbf{T}$ such that $\mathsf {E\text {-}HA^\omega }$ proves

$$\begin{aligned} \forall \underline{f} , \underline{G'} \left( A_{1}(\underline{f}) \, \wedge \forall n^{\mathbb {N}} B_{2} \left( \tilde{s}_{1}n\underline{f},\dots , \tilde{s}_{k}n\underline{f}, \underline{G'}n \right) \rightarrow B_{1} (\underline{f}, \underline{t} \underline{f} \, \underline{G'}) \right) . \end{aligned}$$

(9)

Put a closed term $s_{i}$ as $\lambda \underline{f},n. \, \tilde{s}_{i} n\underline{f}$ for each $i\in \{ 1, \dots , k\}$. Then, by (5) and (9), we have that $\mathrm{P}$ is Gödel-primitive-recursive Weihrauch reducible to $\widehat{ \mathrm { Q }}$ in $\mathsf {E\text {-}HA^\omega }$ (and hence, so is in $\mathsf {E\text {-}PA^\omega }$) with $s_{1}, \dots , s_{k}$ and $\underline{t}$ as the witnesses.

The same proof works also for (2).    $\square$

Combining the proof of Theorem 6 with [10, Lemma 2.1] and [10, Lemma 2.2] as in [10, Theorem 2.10], we have the following:

Theorem 7

Let $\mathrm{P}$ and $\mathrm{Q}$ be existence statements formalized as normal existential sentences $\forall \underline{f} (A_{1}(\underline{f}) \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g}))$ and $\forall \underline{f'} (A_{2}(\underline{f'} ) \rightarrow \exists \underline{g'} B_{2} (\underline{f'}, \underline{g'})$ of $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$ respectively with $\exists$-free formulas $A_{1}, A_{2}, B_{1}$, and $B_{2}$. Then

• 1. $\mathrm{P}$ is Gödel-primitive-recursive Weihrauch reducible to $\widehat{ \mathrm { Q }}$ in $\mathsf {E\text {-}PA^\omega }+\mathrm {QF\text {-}AC}^{0,0}$ (resp. $\mathsf {E\text {-}PA^\omega }+\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}, \, \mathsf {E\text {-}PA^\omega }+\mathrm {AC}^{\omega }$) if and only if $\mathrm{P}$ is normally $\mathbf{T}$-derivable from $\mathrm{Q}$ in $\mathsf {E\text {-}HA^\omega }+ \mathrm {AC}^{0, \omega } + \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}$ (resp. $\mathsf {E\text {-}HA^\omega }+ \mathrm {AC}^{0, \omega } + \mathrm {\Sigma _{2}^{0}\text {-}\mathrm{DNS}^{0}}, \, \mathsf {E\text {-}HA^\omega }+\mathrm {AC}^{\omega }+\mathrm { mr \text {-} DNS^{\omega }}$).

• 2. $\mathrm{P}$ is Kleene-primitive-recursive Weihrauch reducible to $\widehat{ \mathrm { Q }}$ in $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0}$ (resp. $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0},\, \mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {AC}^{\omega }$) if and only if $\mathrm{P}$ is normally $\mathbf{T_{0}}$-derivable from $\mathrm{Q}$ in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+ \mathrm {AC}^{0, \omega } + \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}$ (resp. $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+ \mathrm {AC}^{0, \omega } + \mathrm {\Sigma _{2}^{0}\text {-}\mathrm{DNS}^{0}}, \, \mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+\mathrm {AC}^{\omega }+\mathrm { mr \text {-} DNS^{\omega }}$).

Remark 8

The meta-theorem where $\mathrm {AC}^{0, \omega }$ is replaced by $\mathrm {QF\text {-}AC}^{0,0}$ in Theorem 7.(2) does not hold: If it holds, by Proposition 10 below, we have that $\mathrm {WKL}$ is normally $\mathbf{T_{0}}$-derivable from $\mathrm{LLPO}$ in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+ \mathrm {QF\text {-}AC}^{0,0} + \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}$, and hence, $\mathrm {WKL}$ is provable in $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+ \mathrm {QF\text {-}AC}^{0,0}$ (cf. Remark 5). This is a contradiction (see [16]). The same argument holds also for Theorem 7.(1).

3 Application

There seem to be many results (proofs) in computable analysis and constructive reverse mathematics to which our meta-theorems are applicable. For the purpose of demonstrating the availability of our meta-theorems, we inspect the existing proofs in both of the contexts on the relation between the weak König lemma $\mathrm {WKL}$ and the lesser limited principle of omniscience LLPO. This is the core for the relation between the intermediate value theorem $\mathrm {IVT}$ and $\mathrm {WKL}$ which is mentioned in Sect. 1.

Recall that $\mathrm {WKL}$ states that for any infinite binary tree, there exists an infinite path through the tree (see [10, Section 3.1] for the formal definition) and LLPO is formalized as

$$\forall f_{0}^{\mathbb {N}\rightarrow \mathbb {N}}, f_{1}^{\mathbb {N}\rightarrow \mathbb {N}} \left( \begin{array}{l} \lnot \left( \exists x^{\mathbb {N}} f_{0}(x)=0 \wedge \exists y^{\mathbb {N}} f_{1}(y)=0 \right) \\ \rightarrow \exists k^{\mathbb {N}}((k=0 \rightarrow \lnot \exists x \, f_{0}(x)= 0 ) \wedge (k\ne 0 \rightarrow \lnot \exists y\, f_{1}(y)= 0 ) ) \end{array} \right) $$

in the language of $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$. Both of them are normal existential sentences of the form to which our meta-theorems are applicable. We also recall the following disjunctive variant of $\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}$ from [2, 14]:

$$\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}_{\vee }: \begin{array}{l} \forall n^{\mathbb {N}} \left( \forall x^{\mathbb {N}} {A}_{\mathrm {qf}}(n,x)\vee \forall y^{\mathbb {N}} {B}_{\mathrm {qf}}(n,y) \right) \\ \rightarrow \exists h \forall n \left( \left( h(n)=0 \rightarrow \forall x\, {A}_{\mathrm {qf}}(n,x) \right) \wedge \left( h(n)\ne 0 \rightarrow \forall y \, {B}_{\mathrm {qf}}(n,y) \right) \right) , \end{array} $$

where ${A}_{\mathrm {qf}}$ and ${B}_{\mathrm {qf}}$ are quantifier-free. In the context of constructive reverse mathematics, Ishihara [14, Section 5] first showed that $\mathrm {WKL}$ is equivalent to $\mathrm {LLPO}$ plus $\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}_{\vee }$ over a weak intuitionistic arithmetic. More recently, Berger, Ishihara, and Schuster [2, Section 6] provided a simpler proof of the fact. On the other hand, in the context of computable analysis, Brattka and Gherardi [5, Theorem 8.2] showed that $\mathrm {WKL}$ is Weihrauch equivalent to the parallelization of $\mathrm {LLPO}$ while it is not so to $\mathrm {LLPO}$.

Proposition 9

$\mathrm {WKL}$ is normally $\mathbf{T_{0}}$-derivable from $\mathrm {LLPO}$ in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+ \mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}_{\vee } + \mathrm {QF\text {-}AC}^{0,0} + \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}$.

Proof

The proof is basically the same as that for [2, Theorem 27]. We reason informally in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}_{\vee } + \mathrm {QF\text {-}AC}^{0,0} + \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}$ and let $T^{\mathbb {N}\rightarrow \mathbb {N}}$ be an infinite binary tree (officially given by its characteristic function as in [10, Section 3.1]).

For each $i\in \{0, 1\}$ and each code $u^{\mathbb {N}}$ of a finite sequence of natural numbers, define $C_{i}(u, T)$ as $\exists m^{\mathbb {N}} \left( \lnot D(m, u * {\langle i \rangle } ) \wedge D(m, u * {\langle 1-i \rangle } ) \right)$, where D(m, u) expresses that there exists a finite binary sequence $v^{\mathbb {N}}$ of length m such that $u * v$ is contained in T. Then we have $\forall u^{\mathbb {N}}\lnot \left( C_{0}(u, T) \wedge C_{1}(u, T) \right)$. Notice that there exist closed terms $s_{0}$ and $s_{1}$ of type $\mathbb {N}\rightarrow ((\mathbb {N}\rightarrow \mathbb {N}) \rightarrow (\mathbb {N}\rightarrow \mathbb {N}))$ in $\mathbf{T_{0}}$ such that

$$\exists m^{\mathbb {N}}\, s_{i}uTm=0 \, \leftrightarrow \, C_{i}(u, T)$$

for each $i\in \{ 0,1\}$. Thus we have $\forall u^{\mathbb {N}} \lnot ( \exists m^{\mathbb {N}}\, s_{0}uTm=0 \wedge \exists m^{\mathbb {N}}\, s_{1}uTm=0)$. This validates the first condition of normal derivability in Definition 4.

For the second condition, assume also that for each $u^{\mathbb {N}}$, there exists $k^{\mathbb {N}}$ such that $k=0 \rightarrow \lnot \exists m^{\mathbb {N}}\, s_{0}uTm=0$ and $k\ne 0 \rightarrow \lnot \exists m^{\mathbb {N}}\, s_{1}uTm=0$. Using a dependence choice principle which is derived from $\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}_{\vee }$ (see [2, Corollary 5]), we have a function $h^{\mathbb {N}\rightarrow \mathbb {N}}$ such that $\forall u^{\mathbb {N}} \lnot \exists m^{\mathbb {N}}\, s_{h(u)} \left( \overline{h}u \right) Tm=0$, equivalently, $\forall u^{\mathbb {N}} \lnot C_{h(u)}\left( \overline{h}u, T\right)$. As in the proof of [2, Theorem 27], one can show that $\forall n^\mathbb {N}, m^\mathbb {N}D(m, \overline{h}n)$ by using $\mathrm{\Pi ^{0}_{1}}$ induction which is provable in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0} + \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}$ (see [9, Lemma 20]). Then it follows that h is an infinite path through T.    $\square$

Applying Theorem 7.(2) to Proposition 9, as a corollary, we obtain the following result in the context of computable analysis:

Proposition 10

$\mathrm {WKL}$ is Kleene-primitive-recursive Weihrauch reducible to $\widehat{ \mathrm { LLPO }}$ in $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0}$.

On the other hand, by refining the proof of [5, Theorem 8.2] (where $\mathrm {WKL}$ itself is used for the verification as it is mentioned there), we can also have a direct proof of Proposition 10:

Proof

Recall that $\widehat{ \mathrm { LLPO }}$ states that for all $f_{0}$ and $f_{1}$ of type $\mathbb {N}\rightarrow (\mathbb {N}\rightarrow \mathbb {N})$, if $\forall n^{\mathbb {N}} \lnot \left( \exists x^{\mathbb {N}} f_{0}nx=0 \wedge \exists x^{\mathbb {N}} f_{1}nx=0 \right)$, then there exists $h^{\mathbb {N}\rightarrow \mathbb {N}}$ such that

$$\begin{aligned} \forall n^{\mathbb {N}} \left( \left( hn=0 \rightarrow \lnot \exists x^{\mathbb {N}} f_{0}nx=0 \right) \wedge \left( hn\ne 0 \rightarrow \lnot \exists x^{\mathbb {N}} f_{1}nx=0\right) \right) . \end{aligned}$$

(10)

We reason informally in $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+ \mathrm {QF\text {-}AC}^{0,0}$ and let $T^{\mathbb {N}\rightarrow \mathbb {N}}$ be an infinite binary tree (officially given by its characteristic function).

As in the proof of [5, Theorem 8.2], for each $i \in \{ 0,1\}$, let $P^{T}_{k,i}$ denote the set of finite binary sequences u such that $u * {\langle i \rangle }$ is incomparable with all branches in T of length k. We define $f_{0}$ and $f_{1}$ of type $\mathbb {N}\rightarrow (\mathbb {N}\rightarrow \mathbb {N})$ primitive recursively (in the sense of Kleene) in the given tree T as

$$ f_{i}ux =\left\{ \begin{array}{ll} 0&{}\text { if } x \text { is the least}~k~\text {such that } u \in P^{T}_{k, i} \setminus P^{T}_{k, 1-i},\\ 1&{}\text { otherwise}, \end{array} \right. $$

for $i \in \{ 0,1\}$. For each $u^{\mathbb {N}}$, we have $\lnot \left( \exists x^{\mathbb {N}} f_{0}ux=0 \wedge \exists x^{\mathbb {N}} f_{1}ux=0 \right)$ straightforwardly by definition.

For the second condition, let h satisfy (10) for $f_{0}$ and $f_{1}$ defined above. Define $p^{\mathbb {N}\rightarrow \mathbb {N}}$ primitive recursively in h as

$$ p(k)= \left\{ \begin{array}{ll} 0&{}\text { if } h\left( \overline{p}k \right) =0 ,\\ 1&{}\text { otherwise}, \end{array} \right. $$

For verifying that p is an infinite path through T, it suffices to show that for all $n^{\mathbb {N}}$ and $m^{\mathbb {N}}$, there exists $u\in \{ 0,1\}^{m}$ such that $\overline{p}n * u$ is in T. In the following, we show this assertion by $\mathrm{\Pi ^{0}_{1}}$ induction (which is provable in $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0}$) on $n^{\mathbb {N}}$. When $n=0$, we are done since T is infinite. Assume that for all $m^{\mathbb {N}}$, there exists $u\in \{ 0,1\}^{m}$ such that $\overline{p}n * u$ is in T. Our goal is to show the corresponding assertion for $n+1$. Based on classical logic, we consider the following 4 cases:

• 1. There exists $k^{\mathbb {N}}$ such that $\overline{p}n \in P^{T}_{k,1}\setminus P^{T}_{k,0}$;

• 2. There exists $k^{\mathbb {N}}$ such that $\overline{p}n \in P^{T}_{k,0}\setminus P^{T}_{k,1}$;

• 3. There is no $k^{\mathbb {N}}$ such that $\overline{p}n \in P^{T}_{k,0}\cup P^{T}_{k,1}$;

• 4. There exists $k^{\mathbb {N}}$ such that $\overline{p}n \in P^{T}_{k,0}\cap P^{T}_{k,1}$.

We first work in the first case. Using classical logic, it follows from our induction hypothesis that at least one of the following holds:

• For all $m^{\mathbb {N}}$, there exists $u\in \{ 0,1\}^{m}$ such that $\overline{p}n * {\langle 0 \rangle } * u$ is in T;

• For all $m^{\mathbb {N}}$, there exists $u\in \{ 0,1\}^{m}$ such that $\overline{p}n * {\langle 1 \rangle } * u$ is in T.

If the latter holds, then for $m_{0}:= k {\dot{}-}(n+1)$, there exists $u\in \{ 0,1\}^{m_{0}}$ such that $\overline{p}n\,*\,{\langle 1 \rangle } \,*\,u$ is in T, which contradicts $\overline{p}n\in P^{T}_{k,1}$. Thus the former holds. Since p(n) must be 0 by definition, we have our goal. In the second case, by mimicking the above argument, we have our goal as well. Next, we work in the third case. Fix $m_{1}^{\mathbb {N}}$ and assume that for all $u\in \{ 0,1\}^{m_{1}}$, $\overline{p}(n+1) * u$ is not in T. Then all branches in T of length $n+1+m_{1}$ (note that there is at least one branch of this length by induction hypothesis) are incomparable with $\overline{p}(n+1)$, and hence, $\overline{p}n \in P^{T}_{n+1+m_{1}, p(n)}$, which is a contradiction. Thus there exists $u\in \{ 0,1\}^{m_{1}}$ such that $\overline{p}(n+1) * u$ is in T. Finally, we show that the fourth case does not occur. If $\overline{p}n \in P^{T}_{k,0} \cap P^{T}_{k,1}$, then for any $s\in \{ 0,1\}^{k}$ in T, s is incomparable with both of $\overline{p}n\,*\,{\langle 0 \rangle }$ and $\overline{p}n\,*\,{\langle 1 \rangle }$. Note that k must be greater than n. By induction hypothesis, there exists $u\in \{ 0,1\}^{k- n}$ such that $\overline{p}n\,*\,u$ is in T. This is a contradiction.    $\square$

Remark 11

We obtain Proposition 9 by applying Theorem 7.(2) to Proposition 10 with the following observation: In particular cases where $\mathrm{Q}$ is $\mathrm{LLPO}$ in Theorem 7.(2), the proof shows that only $\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}_{\vee }$ rather than $\mathrm {AC}^{0, \omega }$ is enough for the corresponding argument. On the other hand, one needs $\mathrm {QF\text {-}AC}^{0,0}$ and $\mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}$ for deriving the negative translation of $\mathrm {QF\text {-}AC}^{0,0}$ (see [10, Lemma 2.1.(3)]).

Remark 12

One can notice that the proof of Proposition 9 and the proof of Proposition 10 are somewhat similar. Nevertheless, the primitive recursive witnesses for the latter is not obvious from the proof of Proposition 9. On the other hand, the proof of Proposition 10 heavily uses classical logic for the verification, and hence, the former is also not an immediate consequence from the latter. This observation illustrates that our meta-theorems should give rise to new results in one of the contexts from the results or the proofs in the other context.

At the end of this section, we briefly deal with the relation between the intermediate value theorem $\mathrm {IVT}$ (see [10, Section 3.2] for the formal definition) and $\mathrm {WKL}$ which is mentioned in Sect. 1.

Proposition 13

• 1. $\mathrm {DICH_{\mathbb {R}}}$ is normally reducible to $\mathrm {IVT}$ in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+ \mathrm {QF\text {-}AC}^{0,0}$, where

  $$\mathrm {DICH_{\mathbb {R}}}:\, \forall f^{\mathbb {N}\rightarrow \mathbb {N}} \exists k^{\mathbb {N}} \left( \left( k=0 \rightarrow f\ge _{\mathbb {R}} 0 \right) \wedge \left( k\ne 0 \rightarrow f\le _{\mathbb {R}} 0\right) \right) .$$

• 2. $\mathrm {LLPO}$ is normally reducible to $\mathrm {DICH_{\mathbb {R}}}$ in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0}$.

• 3. $\widehat{ \mathrm { \mathrm {WKL} }}$ is normally reducible to $\mathrm {WKL}$ in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0}$.

Proof

(1): Inspect the argument in [19, 6.1.2]. (2): Inspect the argument in [19, 5.2.12]. (3): Inspect the proof of $(1) \rightarrow (3)$ of [11, Lemma 5].    $\square$

By Propositions 1, 9, 10, and 13, together with [10, Proposition 3.8], we have the following:

Corollary 14

$\mathrm {WKL}$ is Kleene-primitive-recursive Weihrauch reducible to $\widehat{ \mathrm { \mathrm {IVT} }}$ and vice versa in $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0}$.

Corollary 15

$\mathrm {WKL}$ is normally $\mathbf{T_{0}}$-derivable from $\mathrm {IVT}$ and vice versa in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}_{\vee }+\mathrm {QF\text {-}AC}^{0,0}+ \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}$.

4 Another Possible Consequence from Constructive Reverse Mathematics

A lot of existing proofs in constructive reverse mathematics show not only provability but rather normal derivability (see Remark 5). However, this is not always the case. For example, in the proof of deriving the convex weak König lemma $\mathrm {WKL}^{c}$ from $\mathrm {IVT}$ [1, Theorem 3], for a given infinite convex tree T, $\mathrm {IVT}$ is first used to construct an infinite convex subtree $T'$ having at most 2 branches for each height, and then it is used again for taking an infinite path through $T'$. Thus, while the first instance to which one applies $\mathrm {IVT}$ is provided primitive recursively in a given infinite convex tree T, the second instance is not so. In this section, we characterize this kind of proofs by the notion of Weihrauch reducibility to the consecutive composition of the finitely many copies of an existence statement, which has been studied recently in computable analysis (e.g. [7, 15, 18]).

Definition 16

Let $\mathrm{P}$ and $\mathrm{Q}$ be existence statements formalized as normal existential sentences $\forall \underline{f} (A_{1}(\underline{f}) \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g}))$ and $\forall \underline{f'} (A_{2}(\underline{f'}) \rightarrow \exists \underline{g'} B_{2} (\underline{f'}, \underline{g'}))$ of $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$ respectively.

• For a finite-type arithmetic $\mathsf{S^\omega }$ containing $\mathsf {E\text {-}HA^\omega }$, $\mathrm{P}$ is Gödel-primitive-recursive Weihrauch reducible to the 2-copies of $\mathrm{Q}$ in $\mathsf{S^\omega }$ if there exist closed terms $\underline{s}$, $\underline{t}$, and $\underline{u}$ (of suitable types) in $\mathbf{T}$ such that $\mathsf{S^\omega }$ proves

  $$\begin{aligned} \begin{array}{l} \forall \underline{f} ( A_{1}(\underline{f}) \rightarrow A_{2} (\underline{s}\underline{f})) \wedge \\ \forall \underline{f}, \underline{g'} \left( B_{2}(\underline{s} \underline{f}, \underline{g'}) \wedge A_{1}(\underline{f}) \rightarrow A_{2}(\underline{t} \underline{f} \,\, \underline{g'}) \right) \wedge \\ \forall \underline{f}, \underline{g'} , \underline{g''} \left( B_{2}(\underline{t} \underline{f} \,\, \underline{g'}, \underline{g''} ) \wedge B_{2}(\underline{s} \underline{f}, \underline{g'}) \wedge A_{1}(\underline{f}) \rightarrow B_{1}(\underline{f}, \underline{u}\underline{f} \,\, \underline{g'} \, \underline{g''} ) \right) . \end{array} \end{aligned}$$

  (11)

• For a finite-type arithmetic $\mathsf{S^\omega }$ containing $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$, $\mathrm{P}$ is Kleene-primitive-recursive Weihrauch reducible to the 2-copies of $\mathrm{Q}$ in $\mathsf{S^\omega }$ if there exist closed terms $\underline{s}$, $\underline{t}$, and $\underline{u}$ (of suitable types) in $\mathbf{T_{0}}$ such that $\mathsf{S^\omega }$ proves (11).

• For a finite-type arithmetic $\mathsf{S^\omega }$ containing $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$, $\mathrm{P}$ is normally reducible to the 2-copies of $\mathrm{Q}$ in $\mathsf{S^\omega }$ if $\mathsf{S^\omega }$ proves

  $$\begin{aligned} \forall \underline{f} \left( \begin{array}{l} A_{1}(\underline{f})\rightarrow \\ \exists \underline{f'} \left( A_{2}(\underline{f'}) \wedge \forall \underline{g'} \left( \begin{array}{l}B_{2}(\underline{f'}, \underline{g'}) \rightarrow \\ \exists \underline{f''} \left( A_{2}(\underline{f''}) \wedge \forall \underline{g''} \left( \begin{array}{l} B_{2}(\underline{f''}, \underline{g''} )\rightarrow \\ \exists \underline{g} B_{1} (\underline{f}, \underline{g}) \end{array} \right) \right) \end{array} \right) \right) \end{array} \right) . \end{aligned}$$

The versions for k-copies $(k= 3,4,5,\dots )$ are also defined in the same manner. Note that [10, Definition 2.5] is the case of $k=1$.

The proof of [10, Theorem 2.10] allows us to generalize it as follows:

Theorem 17

Let k be a fixed natural number. Let $\mathrm{P}$ and $\mathrm{Q}$ be existence statements formalized as normal existential sentences $\forall \underline{f} (A_{1}(\underline{f}) \rightarrow \exists \underline{g} B_{1} (\underline{f}, \underline{g}))$ and $\forall \underline{f'} (A_{2}(\underline{f'} ) \rightarrow \exists \underline{g'} B_{2} (\underline{f'}, \underline{g'})$ of $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$ respectively with $\exists$-free formulas $A_{1}, A_{2}, B_{1}$, and $B_{2}$. Then the following hold:

• 1. $\mathrm{P}$ is Gödel-primitive-recursive Weihrauch reducible to the k-copies of $\mathrm{Q}$ in $\mathsf {E\text {-}PA^\omega }$ (resp. $\mathsf {E\text {-}PA^\omega }+\mathrm {QF\text {-}AC}^{0,0}, \, \mathsf {E\text {-}PA^\omega }+\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}, \, \mathsf {E\text {-}PA^\omega }+ \mathrm {AC}^{\omega }$) if and only if $\mathrm{P}$ is normally reducible to the k-copies of $\mathrm{Q}$ in $\mathsf {E\text {-}HA^\omega }$ (resp. $\mathsf {E\text {-}HA^\omega }+\mathrm {QF\text {-}AC}^{0,0} + \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}, \, \mathsf {E\text {-}HA^\omega }+\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0} + \mathrm {\Sigma _{2}^{0}\text {-}\mathrm{DNS}^{0}}, \, \mathsf {E\text {-}HA^\omega }+\mathrm {AC}^{\omega }+\mathrm { mr \text {-} DNS^{\omega }}$).

• 2. $\mathrm{P}$ is Kleene-primitive-recursive Weihrauch reducible to the k-copies of $\mathrm{Q}$ in $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }$ (resp. $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0}, \, \mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0}, \, \mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+ \mathrm {AC}^{\omega }$) if and only if $\mathrm{P}$ is normally reducible to the k-copies of $\mathrm{Q}$ in $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }$ (resp. $\mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0} + \mathrm {\Sigma _{1}^{0}\text {-}\mathrm{DNS}^{0}}, \, \mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+\mathrm {\Pi ^{0}_{1}\text {-}AC}^{0,0} + \mathrm {\Sigma _{2}^{0}\text {-}\mathrm{DNS}^{0}}, \, \mathsf {\widehat{E\text {-}HA}^\omega \upharpoonright }+\mathrm {AC}^{\omega }+\mathrm { mr \text {-} DNS^{\omega }}$).

Applying Theorem 17.(2) for $k=2$ to the proof of deriving $\mathrm {WKL}^{c}$ from $\mathrm {IVT}$ in [1, Theorem 3], one can obtain a non-trivial result in computable analysis:

Proposition 18

$\mathrm {WKL}^{c}$ is Kleene-primitive-recursive Weihrauch reducible to the 2-copies of $\mathrm {IVT}$ in $\mathsf {\widehat{E\text {-}PA}^\omega \upharpoonright }+\mathrm {QF\text {-}AC}^{0,0}$.

Remark 19

The notion of normal derivability does not imply the notion of normal reducibility to k-copies (verifiably even in a nearly intuitionistic system containing a choice principle) for any natural number k: if so, by Corollary 15, we have that $\mathrm {WKL}$ is normally reducible to the k-copies of $\mathrm {IVT}$, and hence, $\mathrm {WKL}$ is Kleene-primitive-recursive Weihrauch reducible to the k-copies of $\mathrm {IVT}$ by Theorem 17. However, this is not the case because any computable instance of $\mathrm {IVT}$ has a computable solution while $\mathrm {WKL}$ is not so.