Weihrauch and constructive reducibility between existence statements

Abstract

We formalize the primitive recursive variants of Weihrauch reduction between existence statements in finite-type arithmetic and show a meta-theorem stating that the primitive recursive Weihrauch reducibility verifiably in a classical finite-type arithmetic is identical to some formal reducibility in the corresponding (nearly) intuitionistic finite-type arithmetic for all existence statements formalized with existential free formulas. In addition, we demonstrate that our meta-theorem is applicable in some concrete examples from classical and constructive reverse mathematics.

Keywords

Foundations of mathematics Weihrauch reducibility reverse mathematics constructive mathematics finite-type arithmetic existence statements

1. Introduction

A large amount of mathematical statements are of the logical form $\begin{matrix} (1) & \forall f (A (f) \to \exists g B (f, g)), \end{matrix}$ 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, f is called an instance of the problem and g is called a solution to the instance. In computable mathematics [10] and reverse mathematics [24], the complexity of the procedure to obtain a solution g to an arbitrary given instance f of the problem has been extensively studied for many mathematical statements. In more recent years, uniform relationship between existence statements has been investigated for a fine-grained analysis both in computable analysis (e.g. [3–5,26]) and reverse mathematics (e.g. [7,9]). The investigation of uniform relationship employs the following reduction: a $Π_{2}^{1}$ sentence P of the form (1) is reducible to another $Π_{2}^{1}$ sentence Q of the form (1) if there exist Turing reductions Φ and Ψ such that whenever $f_{1}$ is an instance of P, then $Φ (f_{1})$ is an instance of Q, and whenever $g_{2}$ is a solution to $Φ (f_{1})$ , then $g_{1} : = Ψ (f_{1}, g_{2})$ is a solution to $f_{1}$ . This reduction is called Weihrauch reduction as it corresponds to Weihrauch reduction for partial multi-valued functions (see [7, Appendix]). For a detailed account of uniformity, the parallelizations have been studied in the context of computable analysis [3,4], and the sequential and uniform versions have been studied in reverse mathematics [8,13,18,21].

On the other hand, there is another development from constructive mathematics [2], where 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 (see [1,20]).

These developments have been mostly disjoint until recently. Interestingly, however, there are several corresponding results between constructive reverse mathematics and classical reverse mathematics of sequential versions. For instance, the principle of trichotomy for reals is intuitionistically equivalent to the limited principle of omniscience LPO whereas its sequential version is classically equivalent to the arithmetical comprehension axiom $ACA$ [8]. On the other hand, the principle of dichotomy for reals is intuitionistically equivalent to the lesser limited principle of omniscience LLPO whereas its sequential version is classically equivalent to the weak König lemma $WKL$ [8]. In fact, $ACA$ and $WKL$ are intuitionistically equivalent to LPO and LLPO respectively in the presence of weak choice principle [20]. A lot of statements seemingly not to be of the form (1) at first glance can be also formalized as equivalent (over a very weak theory of arithmetic) sentences of this form. For instance, LLPO can be represented as $\begin{matrix} \forall f^{{0, 1}^{N}} (\begin{matrix} \neg (\exists x^{N} f (2 x) = 0 \land \exists x^{N} f (2 x + 1) = 0) \\ \to \exists k^{N} ((k = 0 \to \neg \exists x^{N} f (2 x) = 0) \land (k \neq 0 \to \neg \exists x^{N} f (2 x + 1) = 0)) \end{matrix}) . \end{matrix}$ The equivalence between $WKL$ and the parallelization of LLPO has been also found in the early age of reverse mathematics via Weihrauch reducibility [3].

Based on the situation, several meta-theorems have been established on the relation between intuitionistic and classical uniform provability for existence statements [6,11–13,19,23]. In particular, the author [11] showed that for any existence statements P formalized as a $Π_{2}^{1}$ sentence of the form (1) with syntactically simple A and B, P is provable in intuitionistic analysis $EL$ if and only if there exists a Turing functional Φ such that $RCA$ ( $= EL + LEM$ ) proves that Φ provides a solution to any instance of P. As the author knows, this is a first meta-theorem which states not only the derivability of classical uniform provability from intuitionistic provability but also the converse. In the current paper, we extend the formalization of uniform provability in [11] to the (primitive recursive) uniform reduction between existence statements and also introduce the formalized notion of constructive reducibility in terms of finite-type arithmetic. Then we show a meta-theorem which characterizes the former by the latter. In fact, the equivalence between intuitionistic and classical uniform provability in the sense of [11,12] is a special case of the established equivalence between corresponding reductions in the current paper (see Remark 2.12).

1.1. Framework

As a framework for our investigation, we employ an extensional variant $E - {HA}^{ω}$ of intuitionistic arithmetic in all finite types from [22, Section 3.3]. Recall that finite (simple) types are defined as follows: $N$ is a type; if σ, τ are types, then so is $σ \to τ$ (denoted also by $τ^{σ}$ ). Types are denoted by the lower-case Greek letters ρ, σ, τ etc. The degree $\deg (τ)$ of a type τ is defined by $\deg (N) = 0$ and $\deg (σ \to τ) = max {\deg (σ) + 1, \deg (τ)}$ . Terms and formulas of $E - {HA}^{ω}$ are defined as usual. If t is a term of type σ, we write $t^{σ}$ . An application term $s^{σ \to τ} (t^{σ})$ is often abbreviated as $s^{σ \to τ} t^{σ}$ if there is no confusion. The λ-abstraction is officially defined by using the combinators. The language of the systems contains only a binary predicate symbol $=_{N}$ for equality between objects of type $N$ . The type superscripts (for terms) and subscripts (for equality) are omitted when they are clear from the context or the exact information of type is not needed. In addition, a tuple of terms is denoted with an underline as $\underline{t}$ . Recall that an ∃-free formula is a formula which does not contain ∨ and ∃ (see [22, Definition 5.2]). We use the notations $A_{ef}$ and $A_{qf}$ for ∃-free formulas and quantifier-free formulas respectively.

A subsystem ${\hat{E - HA}}^{ω} ↾$ is an important fragment of $E - {HA}^{ω}$ . ${\hat{E - HA}}^{ω} ↾$ has a recursor only of type $N$ and its induction schema is restricted to quantifier-free formulas only. The set of the closed terms of $E - {HA}^{ω}$ is denoted by T and that for ${\hat{E - HA}}^{ω} ↾$ is denoted by $T_{0}$ . The set-theoretic functionals defined by closed terms in T are called Gödel primitive recursive functionals of finite type and those for $T_{0}$ are called Kleene primitive recursive functionals of finite type. A classical variant $E - {PA}^{ω}$ (resp. ${\hat{E - PA}}^{ω} ↾$ ) is obtained from $E - {HA}^{ω}$ (resp. ${\hat{E - HA}}^{ω} ↾$ ) by adding the axiom scheme of excluded middle $A \lor \neg A$ . We refer the reader to [22, Section 3.3] for more details of these systems.

We recall the following choice principles:

$({AC}^{n, m})$	$\forall X^{σ} \exists Y^{τ} A (X, Y) \to \exists F^{σ \to τ} \forall X^{σ} A (X, F (X))$ , where $n = \deg (σ)$ and $m = \deg (τ)$ .
$({AC}^{ω})$	${AC}^{n, m}$ for all n and m.
$({AC}_{ef}^{n, m})$	${AC}^{n, m}$ where A is restricted to ∃-free formulas.
$({AC}_{ef}^{ω})$	${AC}_{ef}^{n, m}$ for all n and m.
$(Π_{1}^{0} - {AC}^{0, 0})$	${AC}^{0, 0}$ where A is restricted to formulas of form $\forall x^{N} A_{qf}$ .
$(QF - {AC}^{0, 0})$	${AC}^{0, 0}$ where A is restricted to quantifier-free formulas.

In addition, we recall the following principles called independence of premise (IP) and double negation shift (DNS):

$({IP}_{ef}^{n})$	$(A_{ef} \to \exists X^{ρ} B (X)) \to \exists X^{ρ} (A_{ef} \to B (X))$ ,
	where $A_{ef}$ does not contain X as its free variable and $n = \deg (ρ)$ .
$({IP}_{ef}^{ω})$	${IP}_{ef}^{n}$ for all n.
$({DNS}^{n})$	$\forall X^{ρ} \neg \neg A (X) \to \neg \neg \forall X^{ρ} A (X)$ where $n = \deg (ρ)$ .
$({DNS}^{ω})$	${DNS}^{n}$ for all n.
$(mr - {DNS}^{n})$	${DNS}^{n}$ where A is restricted to formulas of form $\exists Y A_{ef}$ (Y is of any type).
$(mr - {DNS}^{ω})$	$mr - {DNS}^{n}$ for all n.
$(Σ_{2}^{0} - {DNS}^{0})$	${DNS}^{0}$ where A is restricted to formulas of form $\exists y^{N} \forall z^{N} A_{qf}$ .
$(Σ_{1}^{0} - {DNS}^{0})$	${DNS}^{0}$ where A is restricted to formulas of form $\exists y^{N} A_{qf}$ .

Note that these principles are to be interpreted in the language of the system in question (

E - {HA}^{ω}

{\hat{E - HA}}^{ω} ↾

), and they may contain free variables of any types as parameters. Note also that finite tuples of variables of different types can be coded together into a single variable in

{\hat{E - HA}}^{ω} ↾

(see [25, 1.6.16]).

Notation 1.
We use the following convention: The letters x, y, z, k, l, c etc. range over objects of type $N$ (a type for natural numbers), the letters f, g, h, ω etc. range over objects of type $N \to N$ , and the capital letters range over higher-type objects. Let j be a bijective pairing function over natural numbers, which is defined as a closed term of ${\hat{E - HA}}^{ω} ↾$ . We assume a fixed bijective coding of finite sequences of objects of type $N$ defined by the bijective parting function (see e.g. [25, 1.3.9]), and identify finite sequences with their codes. In particular, the empty sequence $⟨ ⟩$ is coded by 0. The letters u, v, r etc. range over (the codes of) finite sequences of objects of type $N$ . A singleton sequence is denoted by $⟨ x ⟩$ . The concatenation of finite sequences u and v is denoted by $u * v$ . The length of a finite sequence u is denoted by $| u |$ , and if $x < | u |$ , then $u_{x}$ denotes the xth entry of u. We write $u ⪯ v$ if u is an initial segment of v. For g of type $N \to N$ , $\overline{g} n$ denotes the initial segment of g of length n, especially, $\overline{g} 0 = ⟨ ⟩$ . In addition, we make use of the notation $\underline{Y} \underline{X} : = Y_{1} \underline{X}, \dots, Y_{m} \underline{X}$ , where $\underline{Y} = Y_{1}, \dots, Y_{m}$ and $\underline{X} = X_{1}, \dots, X_{n}$ are tuples of functionals of suitable types and $Y_{i} \underline{X} = Y_{i} X_{1} \dots X_{n}$ for $i \in {1, \dots, m}$ .

1.2. Outline

Throughout this paper, we call sentences of the form (1) normal existential sentences. In Section 2, we introduce the formalized notions of primitive recursive Weihrauch reducibility and constructive reducibility between normal existential sentences in terms of finite-type arithmetic. Then we show a meta-theorem which states that the primitive recursive Weihrauch reducibility is characterized by the formalized constructive reducibility for existence statements formalized as a normal existential sentence with ∃-free (namely, not containing ∃ and ∨) premise and conclusion in finite-type arithmetic. In Section 3, we demonstrate that our meta-theorem is applicable in some concrete examples from classical and constructive reverse mathematics. In Section 4, we verify that the syntactical restrictions in our meta-theorem is crucial.

2. Meta-theorems

2.1. Lemmas

The main tools for our investigation are the negative translation (see [25, Section 1.10]) and the modified realizability (see [22, Chapter 5]). The former is used for obtaining constructive reducibility from primitive recursive Weihrauch reducibility as in [11], and the latter is used for the converse direction. In fact, the modified realizability is already used in [19, Lemma 3.5] as well as [13, Proposition 3.4] to show a particular case (in the sense of Remark 2.12) of the converse direction. For a formula A, we call the formula $\exists \underline{Φ} (\underline{Φ} m r A)$ defined by [22, Definition 5.1] the modified realizability interpretation of A. Note that the negative translation and the modified realizability interpretation of A contain exactly those variables which are contained in A.

Lemma 2.1.

The negative translation of an instance of ${AC}^{ω}$ is provable in ${\hat{E - HA}}^{ω} ↾ + {AC}_{ef}^{ω} + mr - {DNS}^{ω}$ .

The negative translation of an instance of $Π_{1}^{0} - {AC}^{0, 0}$ is provable in ${\hat{E - HA}}^{ω} ↾ + Π_{1}^{0} - {AC}^{0, 0} + Σ_{2}^{0} - {DNS}^{0}$ .

The negative translation of an instance of $QF - {AC}^{0, 0}$ is provable in ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0} + Σ_{1}^{0} - {DNS}^{0}$ .

Proof.
We write the negative translation (due to Gentzen [25, Definition 1.10.2]) of a formula A by $A^{N}$ .

(1) The negative translation of an instance of ${AC}^{ω}$ is (equivalent over ${\hat{E - HA}}^{ω} ↾$ to) $\begin{matrix} \forall X^{σ} \neg \neg \exists Y^{τ} A^{N} (X, Y) \to \neg \neg \exists F^{σ \to τ} \forall X^{σ} A^{N} (X, F (X)), \end{matrix}$ which is derived from ${AC}_{ef}^{ω}$ and $mr - {DNS}^{ω}$ since $A^{N}$ is ∃-free by definition.

(2) The negative translation of an instance of $Π_{1}^{0} - {AC}^{0, 0}$ is (equivalent over ${\hat{E - HA}}^{ω} ↾$ to) $\begin{matrix} \forall x^{N} \neg \neg \exists y^{N} \forall z^{N} A_{qf}^{N} (x, y, z) \to \neg \neg \exists f^{N \to N} \forall x^{N}, z^{N} A_{qf}^{N} (x, f (x), z), \end{matrix}$ which is derived from $Π_{1}^{0} - {AC}^{0, 0}$ and $Σ_{2}^{0} - {DNS}^{0}$ .

(3) The negative translation of an instance of $QF - {AC}^{0, 0}$ is (equivalent over ${\hat{E - HA}}^{ω} ↾$ to) $\begin{matrix} \forall x^{N} \neg \neg \exists y^{N} A_{qf}^{N} (x, y) \to \neg \neg \exists f^{N \to N} \forall x^{N} A_{qf}^{N} (x, f (x)), \end{matrix}$ which is derived from $QF - {AC}^{0, 0}$ and $Σ_{1}^{0} - {DNS}^{0}$ . □
Lemma 2.2.

The modified realizability interpretation of an instance of ${DNS}^{ω}$ is provable in ${\hat{E - HA}}^{ω} ↾ + {AC}_{ef}^{ω} + mr - {DNS}^{ω}$ .

The modified realizability interpretation of an instance of $Σ_{2}^{0} - {DNS}^{0}$ is provable in ${\hat{E - HA}}^{ω} ↾ + Π_{1}^{0} - {AC}^{0, 0} + Σ_{2}^{0} - {DNS}^{0}$ .

The modified realizability interpretation of an instance of $Σ_{1}^{0} - {DNS}^{0}$ is provable in ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0} + Σ_{1}^{0} - {DNS}^{0}$ .

Proof.
(1) Let $\exists \underline{Φ} (\underline{Φ} m r A (X))$ be the modified realizability interpretation of $A (X)$ . Then it is straightforward to see that the modified realizability interpretations of $\forall X \neg \neg A (X)$ and $\neg \neg \forall X A (X)$ are intuitionistically equivalent to $\forall X \neg \neg \exists \underline{Φ} (\underline{Φ} m r A (X))$ and $\neg \neg \exists \underline{Ψ} \forall X (\underline{Ψ} X m r A (X))$ respectively. Since $(\underline{Φ} m r A (X))$ is ∃-free (see [22, Remark 5,4]), the modified realizability interpretation of an instance of ${DNS}^{ω}$ is derivable from $mr - {DNS}^{ω}$ and ${AC}_{ef}^{ω}$ .

(2) The modified realizability interpretations of $\forall x^{N} \neg \neg \exists y^{N} \forall z^{N} A_{qf} (x, y, z)$ and $\neg \neg \forall x^{N} \exists y^{N} \forall z^{N} A_{qf} (x, y, z)$ are intuitionistically equivalent to $\forall x^{N} \neg \neg \exists y^{N} \forall z^{N} A_{qf} (x, y, z)$ and $\neg \neg \exists Y^{N \to N} \forall x^{N} \forall z^{N} A_{qf} (x, Y (x), z)$ respectively. Then the modified realizability interpretation of an instance of $Σ_{2}^{0} - {DNS}^{0}$ is derivable from $Σ_{2}^{0} - {DNS}^{0}$ and $Π_{1}^{0} - {AC}^{0, 0}$ .

(3) The modified realizability interpretations of $\forall x^{N} \neg \neg \exists y^{N} A_{qf} (x, y)$ and $\neg \neg \forall x^{N} \exists y^{N} A_{qf} (x, y)$ are intuitionistically equivalent to $\forall x^{N} \neg \neg \exists y^{N} A_{qf} (x, y)$ and $\neg \neg \exists Y^{N \to N} \forall x^{N} A_{qf} (x, Y (x))$ respectively. Then the modified realizability interpretation of an instance of $Σ_{1}^{0} - {DNS}^{0}$ is derivable from $Σ_{1}^{0} - {DNS}^{0}$ and $QF - {AC}^{0, 0}$ . □
Remark 2.3.
Any term of a suitable type plays a role as a realizer for an instance of a double negation shift principle. Lemma 2.2, however, shows that the double negation shift principle itself (as well as some choice principle) is used for the verification.
Remark 2.4.
The proofs of Lemma 2.1 and 2.2 show that the analogous results also hold for $E - {HA}^{ω}$ instead of ${\hat{E - HA}}^{ω} ↾$ (in the language of $E - {HA}^{ω}$ ).

2.2. Formalizations of primitive recursive Weihrauch reducibility and constructive reducibility

Definition 2.5.
Let P and Q be existence statements formalized as sentences $\forall \underline{f} (A_{1} (\underline{f}) \to \exists \underline{g} B_{1} (\underline{f}, \underline{g}))$ and $\forall \underline{f} (A_{2} (\underline{f}) \to \exists \underline{g} B_{2} (\underline{f}, \underline{g}))$ of ${\hat{E - HA}}^{ω} ↾$ respectively.
For a finite-type arithmetic $S^{ω}$ containing $E - {HA}^{ω}$ , P is Gödel-primitive-recursive Weihrauch reducible to Q in $S^{ω}$ if there exist closed terms $\underline{s}$ and $\underline{t}$ (of suitable types) in T such that $S^{ω}$ proves $\begin{matrix} (2) & \forall \underline{f} (A_{1} (\underline{f}) \to A_{2} (\underline{s} \underline{f})) \land \forall \underline{f}, \underline{g^{'}} (B_{2} (\underline{s} \underline{f}, \underline{g^{'}}) \land A_{1} (\underline{f}) \to B_{1} (\underline{f}, t \underline{f} \underline{g^{'}})) . \end{matrix}$

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

For a finite-type arithmetic $S^{ω}$ containing ${\hat{E - HA}}^{ω} ↾$ , P is normally reducible to Q in $S^{ω}$ if $S^{ω}$ proves $\begin{matrix} (3) & \forall \underline{f} (A_{1} (\underline{f}) \to \exists \underline{f^{'}} (A_{2} (\underline{f^{'}}) \land \forall \underline{g^{'}} (B_{2} (\underline{f^{'}}, \underline{g^{'}}) \to \exists \underline{g} B_{1} (\underline{f}, \underline{g})))) . \end{matrix}$

We say that P is Gödel-primitive-recursive Weihrauch/Kleene-primitive-recursive Weihrauch/normally equivalent to Q in $S^{ω}$ if P is Gödel-primitive-recursive Weihrauch/Kleene-primitive-recursive Weihrauch/normally reducible to Q in $S^{ω}$ and vice versa.

Remark 2.6.
The notions of Gödel-primitive-recursive Weihrauch reducibility and Kleene-primitive-recursive Weihrauch reducibility are natural restrictions of formalized Weihrauch reducibility e.g. in [7,23] where Turing functionals for the reduction are replaced by primitive recursive functionals in the sense of Gödel and Kleene respectively. The normal reducibility, which requires a specific form of a proof of that Q implies P, is a stronger notion than just proving $Q \to P$ (cf. Remark 2.9 and Proposition 2.8). 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.
Remark 2.7.
One can straightforwardly verify that the notions of reducibility for existence statements in Definition 2.5 are reflexive and transitive.

Notice that the normal reducibility in the context of a classical system is identical with provability in the system (we provide a proof of this for P and Q with single quantifiers for simplicity): Proposition 2.8.
Let P and Q be existence statements formalized as sentences $\forall f (A_{1} (f) \to \exists g B_{1} (f, g))$ and $\forall f (A_{2} (f) \to \exists g B_{2} (f, g))$ of ${\hat{E - HA}}^{ω} ↾$ respectively, and $S^{ω}$ be a classical finite-type arithmetic such that $S^{ω} ⊢ \exists f^{'} A_{2} (f^{'})$ (note that if $S^{ω} ⊢ \forall f^{'} \neg A_{2} (f^{'})$ , then $S^{ω} ⊢ Q \to P$ just means $S^{ω} ⊢ P$ ). If $S^{ω} ⊢ Q \to P$ , then P is normally reducible to Q in $S^{ω}$ .
Proof.
Assume that $S^{ω}$ proves $\begin{matrix} Q \to P : \forall f^{'} (A_{2} (f^{'}) \to \exists g^{'} B_{2} (f^{'}, g^{'})) \to \forall f (A_{1} (f) \to \exists g B_{1} (f, g)) . \end{matrix}$ Using classical logic, we have that $S^{ω}$ proves $\begin{matrix} (4) & \forall f \exists f^{'} \forall g^{'} ((A_{2} (f^{'}) \to B_{2} (f^{'}, g^{'})) \land A_{1} (f) \to \exists g B_{1} (f, g)) \end{matrix}$

In what follows, we informally reason in $S^{ω}$ to show that P is normally reducible to Q. Fix a functional f such that $A_{1} (f)$ . Take a functional $f^{'}$ from (4). Now we have $A_{2} (f^{'}) \lor \neg A_{2} (f^{'})$ by classical logic.

We first consider in the former case, i.e., $A_{2} (f^{'})$ . Fix a functional $g^{'}$ such that $B_{2} (f^{'}, g^{'})$ . Then we have $(A_{2} (f^{'}) \to B_{2} (f^{'}, g^{'}))$ and $A_{1} (f)$ , and hence, $\exists g B_{1} (f, g)$ by (4). Thus we have $\forall g^{'} (B_{2} (f^{'}, g^{'}) \to \exists g B_{1} (f, g))$ . This proves that P is normally reducible to Q.

Next, we consider in the later case, i.e., $\neg A_{2} (f^{'})$ . Taking one $g_{0}^{'}$ , we have $(A_{2} (f^{'}) \to B_{2} (f^{'}, g_{0}^{'}))$ and $A_{1} (f)$ , and hence, $\exists g B_{1} (f, g)$ by (4). Thus we have $\forall g^{'} (B_{2} (f^{″}, g^{'}) \to \exists g B_{1} (f, g))$ for any $f^{″}$ . On the other hand, there exists $f^{″}$ such that $A_{2} (f^{″})$ by our assumption. Thus we have that P is normally reducible to Q. □
Remark 2.9.
Proposition 2.8 does not hold for an (nearly) intuitionistic finite-type arithmetic containing a choice principle as $E - {HA}^{ω} + {AC}^{ω} + mr - {DNS}^{ω}$ : Since the lesser limited principle of omniscience LLPO intuitionistically derives the weak König lemma $WKL$ in the presence of weak choice principle (see [20, Section 5]), if Proposition 2.8 holds for such an intuitionistic system, Theorem 2.10 implies that $WKL$ is Weihrauch reducible to LLPO, which is a contradiction (see [4, Theorem 2.7]).

Thus, in an intuitionistic context, the notion of normal reducibility is a strictly stronger notion than provability for existence statements. On the other hand, for a (even intuitionistic) finite-type arithmetic $S^{ω}$ which satisfies the deduction theorem and proves the existence of an instance of Q, $S^{ω}$ proves $Q \to P$ if and only if P is normally reducible to Q in $S^{ω} + Q$ (namely, Q is also used for the verification).

2.3. Main results

Now we are ready to state our meta-theorem.

Theorem 2.10.
Let P and Q be existence statements formalized as normal existential sentences $\forall \underline{f} (A_{1} (\underline{f}) \to \exists \underline{g} B_{1} (\underline{f}, \underline{g}))$ and $\forall \underline{f} (A_{2} (\underline{f}) \to \exists \underline{g} B_{2} (\underline{f}, \underline{g}))$ of ${\hat{E - HA}}^{ω} ↾$ respectively with ∃-free formulas $A_{1}$ , $A_{2}$ , $B_{1}$ , and $B_{2}$ . Then the following hold:
P is Gödel-primitive-recursive Weihrauch reducible to Q in $E - {PA}^{ω} + {AC}^{ω}$ if and only if P is normally reducible to Q in $E - {HA}^{ω} + {AC}^{ω} + mr - {DNS}^{ω}$ .

P is Gödel-primitive-recursive Weihrauch reducible to Q in $E - {PA}^{ω} + Π_{1}^{0} - {AC}^{0, 0}$ if and only if P is normally reducible to Q in $E - {HA}^{ω} + Π_{1}^{0} - {AC}^{0, 0} + Σ_{2}^{0} - {DNS}^{0}$ .

P is Gödel-primitive-recursive Weihrauch reducible to Q in $E - {PA}^{ω} + QF - {AC}^{0, 0}$ if and only if P is normally reducible to Q in $E - {HA}^{ω} + QF - {AC}^{0, 0} + Σ_{1}^{0} - {DNS}^{0}$ .

P is Kleene-primitive-recursive Weihrauch reducible to Q in ${\hat{E - PA}}^{ω} ↾ + {AC}^{ω}$ if and only if P is normally reducible to Q in ${\hat{E - HA}}^{ω} ↾ + {AC}^{ω} + mr - {DNS}^{ω}$ .

P is Kleene-primitive-recursive Weihrauch reducible to Q in ${\hat{E - PA}}^{ω} ↾ + Π_{1}^{0} - {AC}^{0, 0}$ if and only if P is normally reducible to Q in ${\hat{E - HA}}^{ω} ↾ + Π_{1}^{0} - {AC}^{0, 0} + Σ_{2}^{0} - {DNS}^{0}$ .

P is Kleene-primitive-recursive Weihrauch reducible to Q in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ if and only if P is normally reducible to Q in ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0} + Σ_{1}^{0} - {DNS}^{0}$ .

Proof.
(1) Assume that P is Gödel-primitive-recursive Weihrauch reducible to Q in $E - {PA}^{ω} + {AC}^{ω}$ . Then there exist terms $\underline{s}$ and $\underline{t}$ in T such that $E - {PA}^{ω} + {AC}^{ω}$ proves $\begin{matrix} (5) & \forall \underline{f} (A_{1} (\underline{f}) \to (A_{2} (\underline{s} \underline{f}) \land \forall \underline{g^{'}} (B_{2} (\underline{s} \underline{f}, \underline{g^{'}}) \to B_{1} (\underline{f}, \underline{t} \underline{f} \underline{g^{'}})))) . \end{matrix}$ By negative translation (see [25, Section 1.10]) with using Lemma 2.1(1), we have that $E - {HA}^{ω} + {AC}_{ef}^{ω} + mr - {DNS}^{ω}$ proves (5) (note that the negative translation of a ∃-free formula is equivalent to the ∃-free formula itself over the system in question), and hence, $\begin{matrix} \forall \underline{f} (A_{1} (\underline{f}) \to \exists \underline{f^{'}} (A_{2} (\underline{f^{'}}) \land \forall \underline{g^{'}} (B_{2} (\underline{f^{'}}, \underline{g^{'}}) \to \exists \underline{g} B_{1} (\underline{f}, \underline{g})))) . \end{matrix}$ Then P is normally reducible to Q in $E - {HA}^{ω} + {AC}^{ω} + mr - {DNS}^{ω}$ .

For the converse direction, assume (3) in Definition 2.5. Since $A_{1}$ , $A_{2}$ and $B_{2}$ are ∃-free, we straightforwardly have that $E - {HA}^{ω} + {AC}^{ω} + mr - {DNS}^{ω} + {IP}_{ef}^{ω}$ proves $\begin{matrix} (6) & \exists \underline{G}, \underline{F^{'}} \forall \underline{f}, \underline{g^{'}} (A_{1} (\underline{f}) \to (A_{2} (\underline{F^{'}} \underline{f}) \land (B_{2} (\underline{F^{'}} \underline{f}, \underline{g^{'}}) \to B_{1} (\underline{f}, \underline{G} \underline{f} \underline{g^{'}})))) . \end{matrix}$ By the soundness of modified realizability ([22, Theorem 5.8]) with using Lemma 2.2(1) and Remark 2.3, there exist closed terms in T which witness $\underline{G}$ and $\underline{F^{'}}$ in (6), verifiably in $E - {HA}^{ω} + {AC}_{ef}^{ω} + mr - {DNS}^{ω}$ . Then it follows that P is Gödel-primitive-recursive Weihrauch reducible to Q in $E - {PA}^{ω} + {AC}^{ω}$ .

(2) The proof is same as that for (1) but using Lemma 2.1(2) and Lemma 2.2(2) instead of Lemma 2.1(1) and Lemma 2.2(1) respectively.

(3) The proof is same as that for (1) but using Lemma 2.1(3) and Lemma 2.2(3) instead of Lemma 2.1(1) and Lemma 2.2(1) respectively.

The same proofs work for the analogous results for Kleene-primitive-recursive Weihrauch reducibility. □
Remark 2.11.
The intuitionistic system $E - {HA}^{ω} + {AC}^{ω}$ roughly corresponds to Bishop’s constructive mathematics [2] while the classical system $E - {PA}^{ω} + {AC}^{ω}$ corresponds to ordinary mathematics. Form this perspective, Theorem 2.10(1) suggests some connection between computable analysis and constructive mathematics (see [11, Remark 6]). On the other hand, Kohlenbach shows that ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{1, 0}$ is a conservative extension of the most typical base system ${RCA}_{0}$ in Friedman-Simpson reverse mathematics [24], and suggests to use it as a base theory for reverse mathematics (see [21]). Theorem 2.10(5) and Theorem 2.10(6) are meta-theorems for the finite-type extensions of ${ACA}_{0}$ and ${RCA}_{0}$ respectively in reverse mathematics (see [14] for more details).
Remark 2.12.
Consider a particular case that P is a normal existential $Π_{2}^{1}$ sentence $\forall f^{N \to N} (A (f) \to \exists g^{N \to N} B (f, g))$ with ∃-free A and B, and Q is $\forall f^{N \to N} (A (f) \to \exists g^{N \to N} A (f))$ with the same A. Then P is normally reducible to Q in an intuitionistic finite-type arithmetic $S^{ω}$ if and only if $S^{ω}$ proves P. On the other hand, P is Gödel-primitive-recursive Weihrauch reducible to Q in $S^{ω} + LEM$ if and only if P is uniformly provable in $S^{ω} + LEM$ in the sense of [11, p. 189, item 2]. Thus it follow from Theorem 2.10 that $S^{ω}$ proves P if and only if P is uniformly provable in $S^{ω} + LEM$ . This is a meta-theorem in the taste of [11,12].

The following result is an interesting consequence from our meta-theorem with respect to the study of Weihrauch complexity in computable analysis (we only show the case for P and Q with single quantifiers for simplicity): Corollary 2.13.
Let P and Q be existence statements formalized as normal existential sentences with ∃-free formulas. If P is Gödel-primitive-recursive Weihrauch reducible to Q in $E - {PA}^{ω} + {AC}^{ω}$ , then there exists a Gödel-primitive-recursive functional Φ (verifiably in $E - {HA}^{ω} + {AC}_{ef}^{ω} + mr - {DNS}^{ω}$ ) which transforms a functional providing a solution to an instance of Q to a functional providing a solution to an instance of P. This also holds for the Kleene-primitive-recursive counterparts where “Gödel-primitive-recursive”, $E - {PA}^{ω}$ , and $E - {HA}^{ω}$ are replaced by “Kleene-primitive-recursive”, ${\hat{E - PA}}^{ω} ↾$ , and ${\hat{E - HA}}^{ω} ↾$ respectively.
Proof.
Let P and Q be $\forall f (A_{1} (f) \to \exists g B_{1} (f, g))$ and $\forall f (A_{2} (f) \to \exists g B_{2} (f, g))$ respectively with ∃-free formulas $A_{1}$ , $A_{2}$ , $B_{1}$ , and $B_{2}$ , and assume that P is Gödel-primitive-recursive Weihrauch reducible to Q in $E - {PA}^{ω} + {AC}^{ω}$ . By Theorem 2.10(1), we have that $E - {HA}^{ω} + {AC}^{ω} + mr - {DNS}^{ω}$ proves $\begin{matrix} \forall f (A_{1} (f) \to \exists f^{'} (A_{2} (f^{'}) \land \forall g^{'} (B_{2} (f^{'}, g^{'}) \to \exists g B_{1} (f, g)))), \end{matrix}$ and hence, $\begin{matrix} Q \to P : \forall f^{'} (A_{2} (f^{'}) \to \exists g^{'} B_{2} (f^{'}, g^{'})) \to \forall f (A_{1} (f) \to \exists g B_{1} (f, g)) . \end{matrix}$ Then it follows straightforwardly that $E - {HA}^{ω} + {AC}^{ω} + mr - {DNS}^{ω} + {IP}_{ef}^{ω}$ proves $\begin{matrix} (7) & \exists Φ \forall G^{'} (\forall f^{'} (A_{2} (f^{'}) \to B_{2} (f^{'}, G^{'} f^{'})) \to \forall f (A_{1} (f) \to B_{1} (f, Φ G^{'} f))) . \end{matrix}$ By the soundness of modified realizability ([22, Theorem 5.8]) with using Lemma 2.2(1) (note that all of $A_{1}$ , $A_{2}$ , $B_{1}$ , and $B_{2}$ are ∃-free), there exists a closed term in T which witnesses Φ in (7), verifiably in $E - {HA}^{ω} + {AC}_{ef}^{ω} + mr - {DNS}^{ω}$ .

The same proof works for the analogous result for the Kleene-primitive-recursive counterparts. □
Remark 2.14.
In computable analysis (see e.g. [3–5]) and reverse mathematics (see e.g. [7,9]), a notion of so-called strong Weihrauch reducibility which is a more resource-sensitive variant of Weihrauch reducibility between existence statements, has also been introduced and used for their analysis. The formalized primitive recursive variant of strong Weihrauch reducibility is also defined naively in finite-type arithmetics as in Definition 2.5. In fact, as in the proof of Theorem 2.10, one can straightforwardly show that the formalized primitive recursive strong Weihrauch reducibility is characterized by intuitionistic provability of the two sentences $\forall \underline{f} (A_{1} (\underline{f}) \to \exists \underline{f^{'}} A_{2} (\underline{f^{'}}))$ and $\forall \underline{g^{'}} \exists \underline{g} \forall \underline{f}$ , $\underline{f^{'}} (A_{1} (\underline{f}) \land A_{2} (\underline{f^{'}}) \land B_{2} (\underline{f^{'}}, \underline{g^{'}}) \to B_{1} (\underline{f}, \underline{g}))$ . In the practical context of constructive mathematics, however, such a proof is quite curious as a proof of that $\forall \underline{f} (A_{2} (\underline{f}) \to \exists \underline{g} B_{2} (\underline{f}, \underline{g}))$ implies $\forall \underline{f} (A_{1} (\underline{f}) \to \exists \underline{g} B_{1} (\underline{f}, \underline{g}))$ . For this reason, we do not spell out the artificial characterization of the primitive recursive variant of strong Weihrauch reducibility.
Remark 2.15.
Kuyper [23] recently showed a similar meta-theorem in the context of second-order (two-sorted) arithmetic. In particular, his meta-theorem states that for all normal existential $Π_{2}^{1}$ sentences P and Q, P is Weihrauch reducible to Q in ${RCA}_{0}$ if and only if the affine refinement of the nearly intuitionistic system ${EL}_{0} + MP$ (Markov’s principle) proves $Q^{'} \to P^{'}$ where normal existential $Π_{2}^{1}$ sentences $P^{'}$ and $Q^{'}$ are obtained from P and Q by applying the negative translation to the premises and the conclusions respectively (see [23, Theorem 7.1]). The merit of our meta-theorem relative to Kuyper’s is that there are much more mathematical statements, including existence statements on discontinuous functions (see [21]), to which the meta-theorem is applicable since our meta-theorem is formulated in the context of finite-type arithmetic. In addition, our meta-theorem is more flexible for the application to concrete mathematical statements since the codings of continuous functions on real numbers and Polish spaces etc. in finite-type arithmetic are much more naive than those in second-order (two-sorted) arithmetic (see [22, Chapter 4]). Another merit is that our meta-theorem does not require any curious restrictions in the systems for constructive reducibility, whereas Kuyper’s requires some restrictions on the contraction and weakening rules (see [23, Definition 2.8]). On the other hand, there are also some price to be paid in our meta-theorem. One price is the restriction of Weihrauch reducibility to its primitive recursive variants. In the practice of computable analysis (e.g. [3–5]), Turing functionals which are not primitive recursive, are often used to show results on Weihrauch reducibility between existence statements. Nonetheless, there seems to be still many examples from computable analysis to which our meta-theorem is applicable as we demonstrate in Section 3. Another obvious price in our meta-theorem relative to Kuyper’s one is the syntactical restriction. From the practical viewpoint, however, Kuyper’s meta-theorem also contains some syntactical restriction implicitly in the sense that it is meaningful for the existence statements formalized as sentences of the form $\begin{matrix} \forall f (A (f) \to \exists g B (f, g)) \end{matrix}$ where $A (f)$ and $B (f, g)$ are equivalent to their negative translations. In fact, ∃-free formulas, which are from our syntactical restriction, satisfy this property. On the other hand, the restriction to “number-negative” formulas is enough for obtaining Weihrauch reducibility from constructive reducibility in Kuyper’s meta-theorem (see [23, Theorem 5.2]).

3. Application

The author believes that our meta-theorem (Theorem 2.10) is useful for the interaction between reverse mathematics via Weihrauch reducibility in computable analysis (e.g. [3–5]) and constructive reverse mathematics (e.g. [1,20]). These two fashions of reverse mathematics have been developed independently with the distinguished techniques respectively. While there are a lot of similarities between them, there are still crucial distinctions.

A notable feature of computable analysis is in the use of classical logic for the verifications, which is entirely rejected in constructive mathematics. Since it is sometimes difficult for computability theorists to recast the proofs without using any classical principle as $A \lor \neg A$ , the direction from constructive reducibility to obtain Weihrauch reducibility should be meaningful.

On the other hand, in constructive reverse mathematics, the form of the proof of $Q \to P$ seems to have never been taken into account. If one carefully inspects the existing proofs of $Q \to P$ in constructive reverse mathematics, one notices that some of them show exactly that P is normally reducible to Q but some are not so (see Remark 3.10). Therefore, one cannot (at least directly) apply our meta-theorem to almost all the equivalences between normal existential sentences with ∃-free formulas in constructive reverse mathematics. Nevertheless, there seem to be plenty of existing proofs in constructive reverse mathematics to which our meta-theorem is directly applicable. Moreover, even if an existing constructive proof of $Q \to P$ shows that P is normally reducible to Q, the witnessing functionals for the corresponding Gödel/Kleene-primitive-recursive Weihrauch reducibility are often non-trivial since such a proof contains a lot of arguments in the intermediate steps. Then the direction from constructive reducibility to obtain Weihrauch reducibility should be also meaningful.

In what follows, we demonstrate the use of Theorem 2.10 for both directions in some concrete examples.

3.1. Obtaining constructive reducibility from Weihrauch reducibility

As a sample, we deal with the equivalence between the weak König lemma, the bounded weak König lemma, and the bounded marriage theorem.

First, we recall that the weak König lemma states that for any infinite binary tree on natural numbers, there exists an infinite path through the tree, and it is formalized as $\begin{matrix} WKL : \forall f^{N \to N} (T (f, λ k^{N} .2) \land \forall x^{N} \exists u^{N} (| u | = x \land f (u) = 0) \to \exists g^{N \to N} \forall x^{N} f (\overline{g} x) = 0) \end{matrix}$ where $T (f, h)$ denotes $\begin{matrix} \forall u^{N}, v^{N} (f (u * v) = 0 \to f (u) = 0) \land \forall u^{N} (f (u) = 0 \to \forall k < | u | u_{k} < h (k)) \end{matrix}$ in the language of ${\hat{E - HA}}^{ω} ↾$ (cf. [22, Section 9.3]). Note that a tree is dealt with as its characteristic function in finite-type arithmetic. Since the existential quantifier on $u^{N}$ can be bounded by $max {v ∣ v \in {0, 1}^{x}} + 1$ , the part of $\exists u^{N} (| u | = x \land f (u) = 0)$ is in fact equivalent to some quantifier-free formula in ${\hat{E - HA}}^{ω} ↾$ .

Note also that $WKL$ is a particular instance of the bounded König lemma $\begin{matrix} BKL : \forall f^{N \to N}, h^{N \to N} (T (f, h) \land \forall x^{N} \exists u^{N} (| u | = x \land f (u) = 0) \to \exists g^{N \to N} \forall x^{N} f (\overline{g} x) = 0) \end{matrix}$ Recall that h in BKL is called a bounding function for the tree f in BKL.

Next, we recall that the bounded marriage theorem states that for any bounded marriage problem satisfying Hall’s condition, there exists a perfect matching (called a solution), and it is formalized as $\begin{matrix} BMT : \forall f^{N \to N}, h^{N \to N} (\begin{matrix} \forall x^{N}, y^{N} (f (j (x, y)) = 0 \to y ⩽ h (x)) \land \\ \forall u^{N} (D (u) \to \exists v^{N} (D (v) \land \forall l < | v | \exists k < | u | f (j (u_{k}, v_{l})) = 0 \land | u | ⩽ | v |)) \\ \to \exists g^{N \to N} (\forall x^{N} f (j (x, g (x)) = 0) \land \forall x, x^{'} (x \neq x^{'} \to g (x) \neq g (x^{'}))) \end{matrix}), \end{matrix}$ where $D (u)$ denotes $\begin{matrix} \forall k, k^{'} < | u | (k \neq k^{'} \to u_{k} \neq u_{k^{'}}), \end{matrix}$ in the language of ${\hat{E - HA}}^{ω} ↾$ . Recall that f in BMT is called a marriage problem and h in BMT is called a bounding function for the marriage problem f. Since the existential quantifier on $v^{N}$ can be bounded with the aid of the bounding function $h^{N \to N}$ , the part of $\exists v^{N} (D (v) \land \forall l < | v | \exists k < | u | f (u_{k}, v_{l}) = 0 \land | u | ⩽ | v |)$ is in fact equivalent to some quantifier-free formula in ${\hat{E - HA}}^{ω} ↾$ .

That is to say, all of $WKL$ , $BKL$ , $BMT$ are of the form to which Theorem 2.10 is applicable.

Proposition 3.1.
$BMT$ is Kleene-primitive-recursive Weihrauch reducible to $BKL$ in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ .
Proof.
By an inspection of the proof of BMT from BKL inside ${RCA}_{0}$ in [17, Theorem 2.3]. Notice that a primitive recursive (in the sense of Kleene) transformation from a marriage problem to an infinite tree is given there. Moreover, in the proof inside ${RCA}_{0}$ , a bounding function for a marriage problem works as a bounding function for the constructed infinite tree, and an infinite path through the constructed infinite tree is itself a solution to the given marriage problem. Thus the proof shows that BMT is Kleene-primitive-recursive Weihrauch reducible to BKL in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ (which contains ${RCA}_{0}$ as mentioned in [21]). □
Proposition 3.2.
$BKL$ is Kleene-primitive-recursive Weihrauch reducible to $WKL$ in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ .
Proof.
By an inspection of the proof of BKL from $WKL$ inside ${RCA}_{0}$ in [24, Lemma IV.1.4]. Note that both of the given transformation from an infinite bounded tree to an infinite binary tree and that from an infinite path through the constructed binary tree to an infinite path through the given bounded tree are primitive recursive in the sense of Kleene. □
Proposition 3.3.
$WKL$ is Kleene-primitive-recursive Weihrauch reducible to $BMT$ in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ .
Proof.
We show our proposition again by inspecting the proof of WKL from BMT inside ${RCA}_{0}$ in [17, Theorem 2.3]. Let f be an arbitrary given infinite binary tree. Construct an infinite marriage problem $f^{'}$ from f as a pair $(u, v)$ is contained in $f^{'}$ if and only if $u = v \neq ⟨ ⟩$ or v is a successor of u in the binary tree f. Then a function $h^{'}$ defined as $h^{'} (u) : = max {u, u * ⟨ 0 ⟩, u * ⟨ 1 ⟩}$ is a bounding function for $f^{'}$ . Note that $f^{'}$ and $h^{'}$ are defined primitive recursively in f. In addition, if $g^{'}$ is a solution to $f^{'}$ , then a function g defined as $g (k) : = {⟨ g^{'} (\overline{g} k) ⟩}_{k}$ is an infinite path through f. Note that $\overline{g} (k + 1)$ consists of $g (0)$ , $g (1), \dots, g (k)$ , and then g is defined primitive recursively in $g^{'}$ . Since all of them are verified inside ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ as in the proof of [17, Theorem 2.3], $WKL$ is Kleene-primitive-recursive Weihrauch reducible to $BMT$ in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ . □
Theorem 3.4.
$BMT$ is Kleene-primitive-recursive Weihrauch equivalent to $WKL$ in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ .
Proof.
Immediate form Propositions 3.1, 3.2, and 3.3 by transitivity (see Remark 2.7). □

Applying Theorem 2.10(6) to Theorem 3.4, we have the following: Corollary 3.5.
$BMT$ is normally equivalent to $WKL$ in ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0} + Σ_{1}^{0} - {DNS}^{0}$ .
Remark 3.6.
In fact, it is possible to show Corollary 3.5 directly without using Theorem 2.10(6) by inspecting the classical proofs in Theorem 3.4 carefully. For the verifications of the proof of Proposition 3.1 described in [16,17], however, some classical reasoning is used (especially in the proof of the finite marriage theorem) at first glance, and recasting the classical proof inside the intuitionistic system requires some more effort.

3.2. Obtaining Weihrauch reducibility from constructive reducibility

We deal with some derivability results in constructive reverse mathematics [1] on the intermediate value theorem, the convex weak König lemma, and the weak König lemma for trees having exactly 2 branches for each non-0-height.

The convex weak König lemma is the weakening of the weak König lemma where a given infinite binary tree is convex in the sense that for each k, if two branches u and v of height k are contained in the tree, then all branches r of height k such that r is between u and v in the graphic tree representation are contained in the tree. The assertion that a (characteristic function of) binary tree f is convex is formalized as $\begin{matrix} C (f) : \equiv \forall k^{N}, u^{N}, v^{N}, r^{N} (f (u) = f (v) = 0 \land | u | = | r | = | v | = k \land u ⊏ r ⊏ v \to f (r) = 0), \end{matrix}$ where $u ⊏ v$ denotes $\exists r^{'} ⪯ u (r^{'} * ⟨ 0 ⟩ ⪯ u \land r^{'} * ⟨ 1 ⟩ ⪯ v)$ . On the other hand, the assertion that f has exactly 2 branches for each non-0-height is formalized as $B_{2} (f) : \equiv \begin{matrix} \forall k^{N} > 0 (\exists u^{N}, v^{N} (u \neq v \land | u | = | v | = k \land f (u) = f (v) = 0) \land \\ \forall u^{N}, v^{N}, r^{N} (| u | = | v | = | r | = k \land f (u) = f (v) = f (r) = 0 \to u = v \lor v = r \lor r = u)) . \end{matrix}$ Since all the existential number quantifiers in the above can be bounded, both of $C (f)$ and $B_{2} (f)$ (for binary tree f) are equivalent to some formulas of form $\forall x^{N} A_{qf} (f, x)$ in ${\hat{E - HA}}^{ω} ↾$ . Thus the convex weak König lemma and the weak König lemma for trees having exactly 2 branches for each non-0-height are formalized as $\begin{matrix} {WKL}^{c} : \forall f^{N \to N} (T (f, λ k^{N} .2) \land \forall x^{N} \exists u^{N} (| u | = x \land f (u) = 0) \land C (f) \to \exists g^{N \to N} \forall x^{N} f (\overline{g} x) = 0) \end{matrix}$ and $\begin{matrix} {WKL}_{2} : \forall f^{N \to N} (T (f, λ k^{N} .2) \land \forall x^{N} \exists u^{N} (| u | = x \land f (u) = 0) \land B_{2} (f) \to \exists g^{N \to N} \forall x^{N} f (\overline{g} x) = 0) \end{matrix}$ respectively, which are both sentences of the applicable form for Theorem 2.10.

The intermediate value theorem (in constructive mathematics) states that for any uniformly continuous function Φ from the unit interval $[0, 1]$ to $R$ such that $Φ (0) ⩽ 0 ⩽ Φ (1)$ , there exists $x \in [0, 1]$ such that $Φ (x) = 0$ . In contrast to the previous examples, if one deals with the intermediate value theorem in two-sorted arithmetic (as ${RCA}_{0}$ or $EL$ ), it is necessary to encode a uniformly continuous function from the unit interval $[0, 1]$ to $R$ as a function on natural numbers. One of the benefits of the use of finite-type arithmetic is to be able to avoid such a cumbersome encoding and formalize the statement naively. In particular, Kohlenbach’s representation of real numbers [22, Section 4.1] allow us to deal with all functions of type $N \to N$ as (codes of) real numbers, and also to use usual arithmetical operations $+_{R}$ , $-_{R}$ , $\cdot_{R}$ , $| \cdot |$ etc. on real numbers as closed terms (of ${\hat{E - HA}}^{ω} ↾$ ). In addition, the equality $=_{R}$ and the inequality $⩽_{R}$ on real numbers are defined as (characteristic functions of) binary relations on functions of type $N \to N$ . For the details of this representation, the reader is referred to [22, Section 4.1]. Under this representation, the intermediate value theorem is naively formalized as $\begin{matrix} {IVT}^{+} : \forall Φ^{N^{N} \to N^{N}} (\forall x^{N} \exists y^{N} U_{[0, 1]} (Φ, x, y) \land Φ (0) ⩽_{R} 0 ⩽_{R} Φ (1) \to \exists h^{N^{N}} (Φ (h) =_{R} 0 \land 0 ⩽_{R} h ⩽_{R} 1)), \end{matrix}$ where $\begin{matrix} U_{[0, 1]} (Φ, x, y) : \equiv \forall f^{N^{N}}, g^{N^{N}} (0 ⩽_{R} f, g ⩽_{R} 1 \land | f -_{R} g | ⩽_{R} 2^{- y} \to | Φ (f) -_{R} Φ (g) | ⩽_{R} 2^{- x}), \end{matrix}$ in the language of ${\hat{E - HA}}^{ω} ↾$ . Since $f =_{R} g$ and $f ⩽_{R} g$ are represented as formulas of form $\forall x^{N} A_{qf} (f, g, x)$ , $\begin{matrix} IVT : \forall Φ^{N^{N} \to N^{N}}, \forall ω^{N \to N} (\begin{matrix} \forall x^{N} U_{[0, 1]} (Φ, x, ω (x)) \land Φ (0) ⩽_{R} 0 ⩽_{R} Φ (1) \\ \to \exists h^{N^{N}} (Φ (h) =_{R} 0 \land 0 ⩽_{R} h ⩽_{R} 1) \end{matrix}), \end{matrix}$ which is equivalent to ${IVT}^{+}$ in the presence of ${AC}_{ef}^{ω}$ , is a sentence of the applicable form in Theorem 2.10 while ${IVT}^{+}$ is not.

Recently, Berger et al. [1] showed inside ${EL}_{0}$ , which is a intuitionistic variant of ${RCA}_{0}$ , that the intermediate value theorem (in a slightly different formulation than ours) is equivalent to the convex weak König lemma and it implies the weak König lemma for trees having exactly 2 branches for each non-0-height. Note that one can easily recast the proofs inside finite-type arithmetic ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0}$ .

Proposition 3.7.
${WKL}_{2}$ is normally reducible to $IVT$ in ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0}$ .
Proof.
By mimicking the proof of $IVT \to {WKL}_{2}$ in [1, Proposition 4] inside ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0}$ , we have that ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0}$ proves $\begin{matrix} \forall f^{N \to N} (\begin{matrix} T (f, λ k^{N} .2) \land \forall x^{N} \exists u^{N} (| u | = x \land f (u) = 0) \land B_{2} (f) \\ \to \exists Φ^{N^{N} \to N^{N}}, ω^{N \to N} (\begin{matrix} \forall x^{N} U_{[0, 1]} (Φ, x, ω (x)) \land Φ (0) ⩽_{R} 0 ⩽_{R} Φ (1) \land \\ \forall h^{N^{N} \to N^{N}} (Φ (h) =_{R} 0 \land 0 ⩽_{R} h ⩽_{R} 1 \to \exists g^{N \to N} \forall x^{N} f (\overline{g} x) = 0) \end{matrix}) \end{matrix}) . \end{matrix}$ □
Proposition 3.8.
$IVT$ is normally reducible to ${WKL}^{c}$ in ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0}$ .
Proof.
By mimicking the proof of ${WKL}^{c} \to IVT$ in [1, Theorem 3] inside ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0}$ , we have that ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0}$ proves $\begin{matrix} \forall Φ^{N^{N} \to N^{N}}, ω^{N \to N} (\begin{matrix} \forall x^{N} U_{[0, 1]} (Φ, x, ω (x)) \land Φ (0) ⩽_{R} 0 ⩽_{R} Φ (1) \\ \to \exists f^{N \to N} (\begin{matrix} T (f, λ k^{N} .2) \land \forall x^{N} \exists u^{N} (| u | = x \land f (u) = 0) \land C (f) \land \\ \forall g^{N \to N} (\forall x^{N} f (\overline{g} x) = 0 \to \exists h^{N^{N}} (Φ (h) =_{R} 0 \land 0 ⩽_{R} h ⩽_{R} 1)) \end{matrix}) \end{matrix}) . \end{matrix}$ □
Remark 3.9.
Applying Theorem 2.10(6) to Propositions 3.7 (resp. Proposition 3.8), we have that ${WKL}_{2}$ (resp. $IVT$ ) is Kleene-primitive-recursive Weihrauch reducible to $IVT$ (resp. ${WKL}^{c}$ ) in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ (even in ${\hat{E - HA}}^{ω} ↾$ by the proof of Theorem 2.10(6)).
Remark 3.10.
In contrast to Propositions 3.7 and 3.8, the proof of $IVT \to {WKL}^{c}$ in [1, Theorem 3] does not show that ${WKL}^{c}$ is normally reducible to $IVT$ in ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0}$ . In the proof, for a given infinite convex tree f, $IVT$ is first used to construct an infinite convex subtree $f^{'}$ having at most 2 branches for each height, and then it is used again for taking an infinite path through $f^{'}$ . On the other hand, as mentioned in Remark 2.9, it follows from the proof that ${WKL}^{c}$ is normally reducible to $IVT$ in ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0} + IVT$ . Since $IVT$ is not provable even in $E - {HA}^{ω} + {AC}^{ω} + mr - {DNS}^{ω}$ (cf. [13, Section 5]), however, Theorem 2.10 is still not applicable.

4. A negative result

Our meta-theorem (Theorem 2.10) is applicable to normal existential sentences with ∃-free formulas in finite-type arithmetic. A natural question is whether one can extend the syntactical class of formulas to which our meta-theorem is applicable. In this section, using a discussion on the bounded König lemma in [15], we show that Theorem 2.10 does not hold for normal existential sentences with formulas not ∃-free but with low complexity.

Proposition 4.1.

Theorem 2.10 does not hold for the sentences of form $\begin{matrix} (8) & \forall f^{N \to N} (\exists x^{N} \forall y^{N} A_{qf} (f, x, y) \to \exists g^{N \to N} \forall z^{N} B_{qf} (f, g, z)) . \end{matrix}$

Proof.

Suppose that Theorem 2.10 holds for the sentences of the form (8) and consider the following principle: $\begin{matrix} B_{c} KL : \forall f^{N \to N}, c^{N} (T (f, λ k^{N} . c) \land \forall x^{N} \exists u^{N} (| u | = x \land f (u) = 0) \to \exists g^{N \to N} \forall x^{N} f (\overline{g} x) = 0) . \end{matrix}$ Note that $B_{c} KL$ is a generalized principle of $WKL$ but an instance of $BKL$ already discussed in Section 3.2. Then it follows from Proposition 3.2 (and Remark 2.7) that $B_{c} KL$ is Kleene-primitive-recursive Weihrauch reducible to $WKL$ in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ . Applying Theorem 2.10 to this fact, we have that ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0} + Σ_{1}^{0} - {DNS}^{0}$ proves $\begin{matrix} (9) & \forall f^{N \to N}, c^{N} (\begin{matrix} T (f, λ k^{N} . c) \land \forall x^{N} \exists u^{N} (| u | = x \land f (u) = 0) \\ \to \exists f^{' N \to N} (\begin{matrix} T (f^{'}, λ k^{N} .2) \land \forall x^{N} \exists u^{N} (| u | = x \land f^{'} (u) = 0) \land \\ \forall g^{' N \to N} (\forall x^{N} f^{'} (\overline{g^{'}} x) = 0 \to \exists g^{N \to N} \forall x^{N} f (\overline{g} x) = 0) \end{matrix}) \end{matrix}) . \end{matrix}$ Since (9) is intuitionistically equivalent to $\begin{matrix} \forall f^{N \to N} (\begin{matrix} \exists c^{N} T (f, λ k^{N} . c) \land \forall x^{N} \exists u^{N} (| u | = x \land f (u) = 0) \\ \to \exists f^{' N \to N} (\begin{matrix} T (f^{'}, λ k^{N} .2) \land \forall x^{N} \exists u^{N} (| u | = x \land f^{'} (u) = 0) \land \\ \forall g^{' N \to N} (\forall x^{N} f^{'} (\overline{g^{'}} x) = 0 \to \exists g^{N \to N} \forall x^{N} f (\overline{g} x) = 0) \end{matrix}) \end{matrix}), \end{matrix}$ we have that $\begin{matrix} B_{c}^{'} KL : \forall f^{N \to N} (\exists c^{N} T (f, λ k^{N} . c) \land \forall x^{N} \exists u^{N} (| u | = x \land f (u) = 0) \to \exists g^{N \to N} \forall x^{N} f (\overline{g} x) = 0) \end{matrix}$ is normally reducible to $WKL$ in ${\hat{E - HA}}^{ω} ↾ + QF - {AC}^{0, 0} + Σ_{1}^{0} - {DNS}^{0}$ . Since $B_{c}^{'} KL$ and $WKL$ are (equivalent to some) sentences of the form (8), by our assumption, $B_{c}^{'} KL$ is Kleene-primitive-recursive Weihrauch reducible to $WKL$ in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ . Let s and t be the witnessing terms.

We shall reason informally in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ and show that the sequential version $Seq (WKL)$ of $WKL$ implies the sequential version $Seq (B_{c}^{'} KL)$ of $B_{c}^{'} KL$ using the closed terms s and t in $T_{0}$ (see [15] for the precise definition of the sequential versions). Fix an infinite sequence ${⟨ f_{n} ⟩}_{n \in N}$ of constant bounded trees (in the sense of $B_{c}^{'} KL$ ). Since $s f_{n}$ is an infinite binary tree for all n, by $Seq (WKL)$ , there exists an infinite sequence ${⟨ g_{n}^{'} ⟩}_{n \in N}$ such that $g_{n}^{'}$ is an infinite path through $s f_{n}$ for all n. Define an infinite sequence ${⟨ g_{n} ⟩}_{n \in N}$ as $g_{n} = t f_{n} g_{n}^{'}$ . Then, since s and t are witnessing terms of that $B_{c}^{'} KL$ is Kleene-primitive-recursive Weihrauch reducible to $WKL$ in ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ , we have that $g_{n}$ is an infinite path through $f_{n}$ for all n. Thus ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ proves $Seq (WKL) \to Seq (B_{c}^{'} KL)$ .

Since ${\hat{E - PA}}^{ω} ↾ + QF - {AC}^{0, 0}$ is a conservative extension of ${RCA}_{0}$ (see [21, Proposition 3.1]) and $Seq (WKL)$ and $Seq (B_{c}^{'} KL)$ are equivalent over ${RCA}_{0}$ to $WKL$ and $ACA$ respectively (see [18, Lemma 5] and [15, Proposition 4(2)] respectively), we have that ${WKL}_{0}$ ( $= {RCA}_{0} + WKL$ ) proves $ACA$ , which is a contradiction (see [24]). □

Footnotes

Acknowledgements

Part of this work was carried out while the author had visited the Zukunftskolleg of the University of Konstanz for half a year from May 2019. The author thanks the institute for their hospitality. The author also thanks the anonymous referees for their helpful comments on the earlier version of this paper. This work is supported by JSPS KAKENHI Grant Numbers JP16H07289 and JP18K13450.

References

Berger,

Ishihara,

Kihara and

Nemoto, The binary expansion and the intermediate value theorem in constructive reverse mathematics, Arch. Math. Logic 58(1–2) (2019), 203–217. doi:10.1007/s00153-018-0627-2.

Bishop, Foundations of Constructive Analysis, McGraw-Hill Book Co., New York–Toronto, Ont.–London, 1967.

Brattka and

Gherardi, Weihrauch degrees, omniscience principles and weak computability, J. Symbolic Logic 76(1) (2011), 143–176. doi:10.2178/jsl/1294170993.

Brattka and

Gherardi, Effective choice and boundedness principles in computable analysis, Bull. Symbolic Logic 17(1) (2011), 73–117. doi:10.2178/bsl/1294186663.

Brattka,

Gherardi and

Pauly, Weihrauch complexity in computable analysis, Preprint, https://arxiv.org/pdf/1707.03202.pdf.

F.G.

Dorais, Classical consequences of continuous choice principles from intuitionistic analysis, Notre Dame J. Form. Log. 55(1) (2014), 25–39. doi:10.1215/00294527-2377860.

F.G.

Dorais,

D.D.

Dzhafarov,

J.L.

Hirst,

J.R.

Mileti and

Shafer, On uniform relationships between combinatorial problems, Trans. Amer. Math. Soc. 368(2) (2016), 1321–1359. doi:10.1090/tran/6465.

F.G.

Dorais,

J.L.

Hirst and

Shafer, Reverse mathematics, trichotomy and dichotomy, J. Log. Anal. 4(13) (2012), 1–14.

D.D.

Dzhafarov, Strong reductions between combinatorial principles, J. Symb. Log. 81(4) (2016), 1405–1431. doi:10.1017/jsl.2016.1.

10.

Y.L.

Ershov,

S.S.

Goncharov,

Nerode,

J.B.

Remmel and

V.W.

Marek (eds), Handbook of Recursive Mathematics. Vol. 2. Recursive Algebra, Analysis and Combinatorics, Studies in Logic and the Foundations of Mathematics, Vol. 139, North-Holland, Amsterdam, 1998.

11.

Fujiwara, Intuitionistic provability versus uniform provability in RCA, in: Evolving Computability, Lecture Notes in Comput. Sci., Vol. 9136, Springer, Cham, 2015, pp. 186–195. doi:10.1007/978-3-319-20028-6_19.

12.

Fujiwara, Effective computability and constructive provability for existence sentences (abstract), Logic Colloquium 2016, The Bulletin of Symbolic Logic 23 (2017), 241–242.

13.

Fujiwara and

Kohlenbach, Classical provability of uniform versions and intuitionistic provability, Math. Log. Q. 61(3) (2015), 132–150. doi:10.1002/malq.201300056.

14.

Fujiwara and

Kohlenbach, Interrelation between weak fragments of double negation shift and related principles, J. Symb. Log. 83(3) (2018), 991–1012. doi:10.1017/jsl.2017.63.

15.

Fujiwara and

Yokoyama, A note on the sequential version of

Π_{2}^{1}

statements, in: The Nature of Computation, Lecture Notes in Comput. Sci., Vol. 7921, Springer, Heidelberg, 2013, pp. 171–180.

16.

J.L.

Hirst, Combinatorics in subsystems of second order arithmetic, Thesis (Ph.D.) – The Pennsylvania State University, ProQuest LLC, Ann Arbor, MI, 1987.

17.

J.L.

Hirst, Marriage theorems and reverse mathematics, in: Logic and Computation (Pittsburgh, PA, 1987), Contemp. Math., Vol. 106, Amer. Math. Soc., Providence, RI, 1990, pp. 181–196. doi:10.1090/conm/106/1057822.

18.

J.L.

Hirst, Representations of reals in reverse mathematics, Bull. Pol. Acad. Sci. Math. 55(4) (2007), 303–316. doi:10.4064/ba55-4-2.

19.

J.L.

Hirst and

Mummert, Reverse mathematics and uniformity in proofs without excluded middle, Notre Dame J. Form. Log. 52(2) (2011), 149–162. doi:10.1215/00294527-1306163.

20.

Ishihara, Constructive reverse mathematics: Compactness properties, in: From Sets and Types to Topology and Analysis, Oxford Logic Guides, Vol. 48, Oxford Univ. Press, Oxford, 2005, pp. 245–267. doi:10.1093/acprof:oso/9780198566519.003.0016.

21.

Kohlenbach, Higher order reverse mathematics, in: Reverse Mathematics 2001, Lecture Notes in Logic, Cambridge University Press, 2005, pp. 281–295.

22.

Kohlenbach, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, Springer-Verlag, Berlin, 2008.

23.

Kuyper, On Weihrauch reducibility and intuitionistic reverse mathematics, J. Symb. Log. 82(4) (2017), 1438–1458. doi:10.1017/jsl.2016.61.

24.

S.G.

Simpson, Subsystems of Second Order Arithmetic, 2nd edn, Perspectives in Logic, Cambridge University Press, Cambridge, 2009.

25.

A.S.

Troelstra (ed.), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, Vol. 344, Springer-Verlag, Berlin, New York, 1973.

26.

Weihrauch, Computable Analysis: An Introduction, Texts in Theoretical Computer Science. An EATCS Series, Springer-Verlag, Berlin, 2000.