Parallelizations in Weihrauch Reducibility and Constructive Reverse Mathematics
 65 Downloads
Abstract
In the framework of finitetype 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.
Keywords
Weihrauch reducibility Parallelization Constructive reverse mathematics1 Introduction
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 twosorted 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 computabilitytheoretic 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 metatheorems in the framework of finitetype 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.
2 Metatheorems
 For a finitetype arithmetic \(\mathsf{S^\omega }\) containing \(\mathsf {E\text {}HA^\omega }\), \(\mathrm{P}\) is Gödelprimitiverecursive 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 finitetype arithmetic \(\mathsf{S^\omega }\) containing \(\mathsf {\widehat{E\text {}HA}^\omega \upharpoonright }\), \(\mathrm{P}\) is Kleeneprimitiverecursive 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).
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/Kleeneprimitiverecursive 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/Kleeneprimitiverecursive 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
Remark 5
 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
 1.
\(\mathrm{P}\) is Gödelprimitiverecursive 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 Kleeneprimitiverecursive 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
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).
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
 1.
\(\mathrm{P}\) is Gödelprimitiverecursive 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 Kleeneprimitiverecursive 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 metatheorem 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 metatheorems are applicable. For the purpose of demonstrating the availability of our metatheorems, 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.
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 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 Kleeneprimitiverecursive 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
 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}\).
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 metatheorems 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 Kleeneprimitiverecursive 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 finitetype arithmetic \(\mathsf{S^\omega }\) containing \(\mathsf {E\text {}HA^\omega }\), \(\mathrm{P}\) is Gödelprimitiverecursive Weihrauch reducible to the 2copies 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 finitetype arithmetic \(\mathsf{S^\omega }\) containing \(\mathsf {\widehat{E\text {}HA}^\omega \upharpoonright }\), \(\mathrm{P}\) is Kleeneprimitiverecursive Weihrauch reducible to the 2copies 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 finitetype arithmetic \(\mathsf{S^\omega }\) containing \(\mathsf {\widehat{E\text {}HA}^\omega \upharpoonright }\), \(\mathrm{P}\) is normally reducible to the 2copies 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 kcopies \((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
 1.
\(\mathrm{P}\) is Gödelprimitiverecursive Weihrauch reducible to the kcopies 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 kcopies 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 Kleeneprimitiverecursive Weihrauch reducible to the kcopies 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 kcopies 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 nontrivial result in computable analysis:
Proposition 18
\(\mathrm {WKL}^{c}\) is Kleeneprimitiverecursive Weihrauch reducible to the 2copies 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 kcopies (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 kcopies of \(\mathrm {IVT}\), and hence, \(\mathrm {WKL}\) is Kleeneprimitiverecursive Weihrauch reducible to the kcopies 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.
Notes
Acknowledgement
The author thanks Vasco Brattka and Kenshi Miyabe for their suggestions which motivate this work and also for their valuable comments. He also thanks one of the anonymous referees, who provides the author with valuable information on the literature. This work is supported by JSPS KAKENHI Grant Numbers JP18K13450 and JP19J01239.
References
 1.Berger, J., Ishihara, H., Kihara, T., Nemoto, T.: The binary expansion and the intermediate value theorem in constructive reverse mathematics. Arch. Math. Logic 58, 203–217 (2018). https://doi.org/10.1007/s0015301806272MathSciNetzbMATHGoogle Scholar
 2.Berger, J., Ishihara, H., Schuster, P.: The weak König lemma, Brouwer’s fan theorem, de Morgan’s law, and dependent choice. Rep. Math. Logic 47, 63 (2012)zbMATHGoogle Scholar
 3.Bishop, E.: Foundations of Constructive Analysis. McGrawHill Book Co., New York (1967)zbMATHGoogle Scholar
 4.Brattka, V., Gherardi, G.: Effective choice and boundedness principles in computable analysis. Bull. Symb. Logic 17(1), 73–117 (2011)MathSciNetzbMATHGoogle Scholar
 5.Brattka, V., Gherardi, G.: Weihrauch degrees, omniscience principles and weak computability. J. Symb. Logic 76(1), 143–176 (2011)MathSciNetzbMATHGoogle Scholar
 6.Brattka, V., Le Roux, S., Miller, J.S., Pauly, A.: Connected choice and the Brouwer fixed point theorem. J. Math. Logic 19(01), 1950004 (2019)Google Scholar
 7.Brattka, V., Pauly, A.: On the algebraic structure of Weihrauch degrees. Log. Methods Comput. Sci. 14(4), 1–36 (2018) MathSciNetzbMATHGoogle Scholar
 8.Dorais, F.G., Dzhafarov, D.D., Hirst, J.L., Mileti, J.R., Shafer, P.: On uniform relationships between combinatorial problems. Trans. Am. Math. Soc. 368(2), 1321–1359 (2016)MathSciNetzbMATHGoogle Scholar
 9.Fujiwara, M.: Bar induction and restricted classical logic. In: Iemhoff, R., Moortgat, M., de Queiroz, R. (eds.) WoLLIC 2019. LNCS, vol. 11541, pp. 236–247. Springer, Heidelberg (2019). https://doi.org/10.1007/9783662595336_15zbMATHGoogle Scholar
 10.Fujiwara, M.: Weihrauch and constructive reducibility between existence statements. Computability (2020, to appear)Google Scholar
 11.Hirst, J.L.: Representations of reals in reverse mathematics. Bull. Pol. Acad. Sci. Math. 55(4), 303–316 (2007)MathSciNetzbMATHGoogle Scholar
 12.Hirst, J.L., Mummert, C.: Reverse mathematics and uniformity in proofs without excluded middle. Notre Dame J. Form. Log. 52(2), 149–162 (2011)MathSciNetzbMATHGoogle Scholar
 13.Hirst, J.L., Mummert, C.: Using Ramsey’s theorem once. Arch. Math. Logic 58(7), 857–866 (2019). https://doi.org/10.1007/s0015301900664zMathSciNetzbMATHGoogle Scholar
 14.Ishihara, H.: Constructive reverse mathematics: compactness properties. In: From Sets and Types to Topology and Analysis. Oxford Logic Guides, vol. 48, pp. 245–267. Oxford University Press, Oxford (2005)Google Scholar
 15.Kihara, T., Pauly, A.: Finite choice, convex choice and sorting. In: Gopal, T.V., Watada, J. (eds.) TAMC 2019. LNCS, vol. 11436, pp. 378–393. Springer, Cham (2019). https://doi.org/10.1007/9783030148126_23zbMATHGoogle Scholar
 16.Kohlenbach, U.: Higher order reverse mathematics. In: Reverse Mathematics 2001, pp. 281–295. Lecture Notes in Logic, Cambridge University Press (2005)Google Scholar
 17.Kohlenbach, U.: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer Monographs in Mathematics. Springer, Berlin (2008). https://doi.org/10.1007/9783540775331zbMATHGoogle Scholar
 18.Kuyper, R.: On Weihrauch reducibility and intuitionistic reverse mathematics. J. Symb. Log. 82(4), 1438–1458 (2017)MathSciNetzbMATHGoogle Scholar
 19.Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, An Introduction, Vol. I, Studies in Logic and the Foundations of Mathematics, vol. 121. North Holland, Amsterdam (1988)Google Scholar
 20.Uftring, P.: The characterization of Weihrauch reducibility in systems containing \({\sf E}\text{}{\sf PA}^{\omega }+{\rm QF}\text{ }{\rm AC}^{0,0}\). Preprint arXiv:2003.13331 (2020)