Choice principles characterizing the difference between König’s lemma and weak König’s lemma in constructive reverse mathematics

Abstract

In the context of constructive reverse mathematics, we characterize the difference between König’s lemma and weak König’s lemma by a particular fragment of the countable choice principle. Specifically, we show that König’s lemma can be decomposed into weak König’s lemma and the choice principle over a weak intuitionistic two-sorted arithmetic.

Keywords

Constructive reverse mathematics König’s lemma weak König’s lemma uniqueness hypotheses choice principles

1. Introduction

This paper contributes to the program of constructive reverse mathematics, whose purpose is to classify various theorems by logical principles, function existence axioms and their combinations from the constructive standpoint (cf. [6]). In this paper, along the line of [4], we deal with so-called König’s lemma, which states that every infinite finitely-branching tree has a path. This fundamental lemma in graph theory plays an important role in classical reverse mathematics [10]. In that context, König’s lemma $KL$ is equivalent to the arithmetical comprehension axiom $ACA$ over a weak theory $R C A_{0}$ based on classical logic. On the other hand, weak König’s lemma $WKL$ , which is $KL$ restricted to ${0, 1}$ -trees, is strictly weaker than $ACA$ but still has many equivalent mathematical theorems over $R C A_{0}$ .

On the contrary, $WKL$ implies $KL$ constructively in the presence of the countable choice principle, which is accepted in Bishop’s constructive mathematics. Then it is desirable to reveal what kind of restriction of the countable choice principle characterizes the difference between $WKL$ and $KL$ . Motivated from this question, in [4], the first author introduced a variant ${BT}_{fb}$ of the countable choice principle in terms of some notions on trees, and showed that $KL$ is equivalent to $WKL$ plus ${BT}_{fb}$ over the intuitionistic counterpart $E L_{0}$ of $R C A_{0}$ augmented with $Σ_{2}^{0} - IND$ (the induction scheme for predicates of the form $\exists x^{N} \forall y^{N} A_{qf}$ where $A_{qf}$ is quantifier-free). The result is interesting but still not satisfactory from two perspectives. First, the principle ${BT}_{fb}$ is defined in terms of some notions on trees. For the purpose of the classification of mathematical theorems, decomposition into logical and choice principles in a preferably general form is desirable. Then it is expected to characterize ${BT}_{fb}$ by some fragment of the countable choice principle without using any notions on trees. Second, the base theory for the equivalence established in [4] contains $Σ_{2}^{0} - IND$ . Because of that, while the base theory is based on intuitionistic logic, it is proof theoretically stronger than $R C A_{0}$ in classical reverse mathematics. Then it is expected to elaborate the equivalence over merely $E L_{0}$ , which is employed as a base theory in some development of constructive reverse mathematics (cf. [2]).

In this paper, we completely solve the above mentioned issues on the characterization of the difference between $WKL$ and $KL$ . We introduce a fragment $QF - {MC}^{0, 0}$ of the countable choice principle without using any notions on trees (as well as some auxiliary principles), and show that it is equivalent to ${BT}_{fb}$ over $E L_{0}$ (see Theorem 3.1). Furthermore, we show that $KL$ is equivalent to $WKL$ plus $QF - {MC}^{0, 0}$ over $E L_{0}$ (see Theorem 4.3).

2. Preparation

The system $E L_{0}$ is a subsystem of intuitionistic analysis $E L$ [11, Section 1.9.10], which has two-sorted variables (one is for natural numbers and another is for functions over natural numbers) in its language. Note that the subscript 0 of $E L_{0}$ denotes the restriction of the induction scheme. See [8, Chapter 24, Sections 4 and 5] (where $E L$ and $E L_{0}$ in this paper are presented as $E L$ and $E L_{0}$ in the bold Roman font, and $E L$ and $E L_{0}$ in the sans-serif font denote other systems) or [3, Section 2.2.1] for the description of $E L_{0}$ . Recall that $E L_{0}$ contains number-number choice scheme for quantifier-free predicates

\begin{aligned} QF - {AC}^{0, 0} : \forall x^{N} \exists y^{N} A_{qf} (x, y) \to \exists f^{N \to N} \forall x^{N} A_{qf} (x, f (x)) \end{aligned}

and induction scheme for quantifier-free predicates

\begin{aligned} QF - IND : A_{qf} (0) \land \forall x^{N} (A_{qf} (x) \to A_{qf} (x + 1)) \to \forall x^{N} A_{qf} (x) \end{aligned}

where

A_{qf}

is quantifier-free. In fact,

E L_{0}

proves

Σ_{1}^{0} - IND

which is the induction scheme restricted to

Σ_{1}^{0}

predicates

\exists y^{N} A_{qf} (x, y)

(cf. [2, Proposition 1]), and

E L_{0}

augmented with the law-of-excluded-middle

LEM

is interpretable in the most popular base theory

R C A_{0}

of classical reverse mathematics and vice versa (cf. [8, Propositions 24.31 and 24.58]). Formally,

E L_{0}

does not contain bounded number-quantifiers

\forall x < t

and

\exists x < t

in the language. However, we shall use this kind of abbreviations to improve readability. Formulae that contain no quantifiers other than bounded number-quantifiers are called bounded formulae. Note that for each bounded formula, there is an equivalent quantifier-free formula over

E L_{0}

. We indicate the types of variables by their superscripts (

N

N^{N}

) but often suppress them when they are clear from the context. In particular, the letters x, y, z, i, j, k, m, n range over objects of type

N

(a type for natural numbers), the letters f, g, h, p, q range over objects of type

N^{N}

, which is also denoted by

N \to N

(a type for functions from natural numbers to natural numbers). We use the notation

A_{qf}

for quantifier-free predicates. Throughout the paper, we assume a fixed bijective coding of finite sequences of objects of type

N

defined by a bijective pairing function (see e.g. [11, Section 1.3.9]) and basic functions with respect to (coded) finite sequences in

E L_{0}

. In particular, we assume that our coding of finite sequences satisfies the following (provably in

E L_{0}

\begin{aligned} \forall u, v \in N^{*} (| u | = | v | \land \forall i < | u | (u_{i} ⩽ v_{i}) \to u ⩽ v), \end{aligned}

(1)

where we use the notations mentioned below.

Throughout the paper, we use the following notations with respect to finite sequences (as in [4]) with suppressing the tedious coding for improving readability. The letters u, v range over the set $N^{*}$ of (the codes of) finite sequences of objects of type $N$ . Under the fixed coding, inside $E L_{0}$ , we identify a finite sequence of objects of type $N$ with an object of type $N$ , and identify a subset of $N^{*}$ with the characteristic function of the corresponding codes. The length of a finite sequence u is denoted by $| u |$ , and if $i < | u |$ , then $u_{i}$ denotes the i-th entry of u. The concatenation of finite sequences u and v is denoted by $u * v$ . For f of type $N \to N$ , $\bar{f} n$ denotes the initial segment of f of length n, especially, $\bar{f} 0 = ⟨ ⟩$ . If u is a finite sequence, then $\bar{u} i$ denotes the initial segment of u of length i for $i ⩽ | u |$ .

We recall the following notions on trees over $N$ : $T \subseteq N^{*}$ is a tree if $\forall u, v \in N^{*} (u * v \in T \to u \in T)$ . A tree T is infinite if $\forall x^{N} \exists u \in N^{*} (| u | = x \land u \in T)$ . A tree T is finitely-branching if $\forall u \in T \exists k^{N} \forall x^{N} (u * ⟨ x ⟩ \in T \to x ⩽ k)$ . A tree T is height-wise bounded if $\forall i^{N} \exists k^{N} \forall u \in T (i < | u | \to u_{i} ⩽ k)$ . A height-wise bounding function of a tree T is a function $h^{N \to N}$ such that $\forall u \in T \forall j < | u | (u_{j} ⩽ h (j))$ . A binary tree is a tree having the constant-1 function $λ x .1$ as its height-wise bounding function. A path through a tree T is a function $p^{N \to N}$ such that $\forall i (\bar{p} i \in T)$ . A tree T does not have two paths if

\begin{aligned} \forall p^{N \to N}, q^{N \to N} (\exists n (p (n) \neq q (n)) \to \exists n (\bar{p} n \notin T) \lor \exists n (\bar{q} n \notin T)) . \end{aligned}

(2)

A tree T has at most one path if

\begin{aligned} \forall p^{N \to N}, q^{N \to N} (\forall n (\bar{p} n \in T) \land \forall n (\bar{q} n \in T) \to \forall n (p (n) = q (n))) . \end{aligned}

(3)

Uniqueness conditions (2) and (3) for binary trees were first studied in [1,9] and [7] respectively, and they have been generalized for any finitely-branching trees recently in [4]. Of course, conditions (2) and (3) are equivalent over classical logic. In contrast, over intuitionistic logic, condition (2) implies condition (3), but not vice versa. See [4, Section 4.2.1] for more information about conditions (2) and (3).

König’s lemma $KL$ states that for any infinite finitely-branching tree T, there exists a path through T. Weak König’s lemma $WKL$ states that for any infinite binary tree T, there exists a path through T. In this paper, we consider trees which are given by their characteristic functions. Then our trees are decidable. Thus $KL$ is formalized in terms of $E L_{0}$ as follows (where we still use the above-mentioned notations with respect to finite sequences and the informal description of the inequalities for readability):

\begin{aligned} \forall f^{N^{N}} (\begin{matrix} \forall u^{N} (f (u) = 0 \to \exists k^{N} \forall x^{N} (f (u * ⟨ x ⟩) = 0 \to x ⩽ k)) \\ \land \forall u^{N}, v^{N} (f (u * v) = 0 \to f (u) = 0) \\ \land \forall i^{N} \exists u^{N} (| u | = i \land f (u) = 0) \\ \to \exists p^{N^{N}} \forall n^{N} f (\bar{p} n) = 0 \end{matrix}) . \end{aligned}

(4)

Here

f (u) = 0

means

u \in T

since a tree T is now encoded by its characteristic function f. Then

WKL

is formalized in

E L_{0}

as (4) where the first hypothesis is replaced by

\begin{aligned} \forall u^{N} (f (u) = 0 \to \forall j < | u | (u_{j} ⩽ 1)) . \end{aligned}

In addition, $KL!$ (resp. $WKL!$ ) states that for any infinite finitely-branching (resp. binary) tree T which does not have two paths, there exists a path through T. Analogously, $KL!!$ (resp. $WKL!!$ ) states that for any infinite finitely-branching (resp. binary) tree T which has at most one path, there exists a path through T. Finally, ${BT}_{fb}$ (resp. ${BT}_{hb}$ ) states that for any infinite finitely-branching (resp. height-wise bounded) tree T, there exists a height-wise bounding function of T. It is remarkable that a principle $T_{fb \to hb}$ , which states that every infinite finitely-branching tree is height-wise bounded, is equivalent to $Σ_{2}^{0} - IND$ over $R C A_{0}$ (see [4, Theorem 4.33]).

3. Choice principles equivalent to

{BT}_{fb}

We consider a particular form of the choice principle from numbers to numbers:

\begin{aligned} \forall x^{N} \exists y^{N} A (x, y) \to \exists f^{N^{N}} \forall x^{N} A (x, f (x)), \end{aligned}

where

A (x, y)

is of the form

\begin{aligned} A_{qf} (x, y) \land \forall z^{N} (A_{qf} (x, z) \to z ⩽ y) \end{aligned}

(5)

with quantifier-free predicate

A_{qf} (x, y)

. Thus this choice principle states that if, for all

x^{N}

, there exists maximum

y^{N}

such that

A_{qf} (x, y)

holds, then there exists function

f^{N^{N}}

which attains the maximum y for an arbitrarily given x. Then we write this choice principle

QF - {MC}^{0, 0}

(which is named by the initial letters of “quantifier-free maximal choice”). Thus

QF - {MC}^{0, 0}

denotes the following:

\begin{aligned} \forall x^{N} \exists y^{N} (A_{qf} (x, y) \land \forall z^{N} (A_{qf} (x, z) \to z ⩽ y)) \to \exists f^{N^{N}} \forall x^{N} (A_{qf} (x, f (x)) \land \forall z^{N} (A_{qf} (x, z) \to z ⩽ f (x))) . \end{aligned}

Since (5) is intuitionistically equivalent to

\begin{aligned} \forall z^{N} (A_{qf} (x, y) \land (A_{qf} (x, z) \to z ⩽ y)), \end{aligned}

one can think of

QF - {MC}^{0, 0}

as a particular instance of

Π_{1}^{0} - {AC}^{0, 0}

(which is known to be equivalent to

ACA

over

R C A_{0}

under a suitable interpretation). Since such the maximum y is unique, moreover, one can even think of

QF - {MC}^{0, 0}

as a particular instance of

Π_{1}^{0} - {AC}^{0, 0}

! (

Π_{1}^{0} - {AC}^{0, 0}

with a uniqueness hypothesis) in [4, Section 4.2.2]. In [4, Lemma 4.15], the first author had already shown that

E L_{0} + Σ_{2}^{0} - IND + Π_{1}^{0} - {AC}^{0, 0}!

proves

{BT}_{fb}

. In the following, we show that the weakening

QF - {MC}^{0, 0}

Π_{1}^{0} - {AC}^{0, 0}!

is in fact equivalent to

{BT}_{fb}

over

E L_{0}

. For this purpose, we introduce a dependent variant of

QF - {MC}^{0, 0}

\begin{aligned} QF - {DMC}^{0, 0} : \begin{aligned} \forall u^{N} \exists y^{N} (A_{qf} (u, y) \land \forall z^{N} (A_{qf} (u, z) \to z ⩽ y)) \\ \to \exists f^{N^{N}} \forall x^{N} (A_{qf} (\bar{f} x, f (x)) \land \forall z^{N} (A_{qf} (\bar{f} x, z) \to z ⩽ f (x))) \end{aligned} \end{aligned}

and also a quantifier-free bounding choice principle

\begin{aligned} QF - {BC}^{0, 0} : \forall x^{N} \exists y^{N} \forall z^{N} (A_{qf} (x, z) \to z ⩽ y) \to \exists f^{N^{N}} \forall x^{N} \forall z^{N} (A_{qf} (x, z) \to z ⩽ f (x)) . \end{aligned}

For readability, we present our proofs in an informal (or semi-formal) manner. One can transcribe the formal proofs in terms of $E L_{0}$ from our informal presentations in a straightforward way. Theorem 3.1.

The following are pairwise equivalent over $E L_{0}$ :

${BT}_{fb}$ ;

${BT}_{hb}$ ;

$QF - {DMC}^{0, 0}$ ;

$QF - {MC}^{0, 0}$ ;

$QF - {BC}^{0, 0}$ .

Proof.

$(1 \to 2)$ is trivial since a height-wise bounded tree is finitely-branching.

$(1 \to 3)$ : Assume

\begin{aligned} \forall u \exists y (A_{qf} (u, y) \land \forall z (A_{qf} (u, z) \to z ⩽ y)) . \end{aligned}

Define

T \subseteq N^{*}

u \in T

if and only if

\begin{aligned} \forall i < | u | A_{qf} (\bar{u} i, u_{i}) . \end{aligned}

By our assumption, we have that T is a finitely branching tree. In addition, by

Σ_{1}^{0} - IND

, one can show that, for each

x^{N}

, there exists

u \in T

such that

| u | = x

, namely, T is infinite. Therefore, by

{BT}_{fb}

, there exists a height-wise bounding function

h^{N^{N}}

of this tree T. By recursion with using h, take a function

f^{N^{N}}

such that

\begin{aligned} f (x) = max {y | y ⩽ h (x) \land \bar{f} x * ⟨ y ⟩ \in T} . \end{aligned}

(6)

QF - IND

, we have that f is a path through T, and hence,

\forall x A_{qf} (\bar{f} x, f (x))

. In the following, we show

\forall x, z (A_{qf} (\bar{f} x, z) \to z ⩽ f (x))

. Fix

x^{N}

and

z^{N}

such that

A_{qf} (\bar{f} x, z)

. Since

\bar{f} x \in T

, we have

\bar{f} x * ⟨ z ⟩ \in T

. Since h is a height-wise bounding function of T, we have

z ⩽ h (x)

. Then

z ⩽ f (x)

follows from (6).

$(3 \to 4)$ : Assume

\begin{aligned} \forall x \exists y (A_{qf} (x, y) \land \forall z (A_{qf} (x, z) \to z ⩽ y)) . \end{aligned}

Put

A_{qf}^{^{'}} (u, y) :\equiv A_{qf} (| u |, y)

. Then, by

QF - {DMC}^{0, 0}

, there exists

f^{N^{N}}

such that

\begin{aligned} \forall x (A_{qf}^{^{'}} (\bar{f} x, f (x)) \land \forall z (A_{qf}^{^{'}} (\bar{f} x, z) \to z ⩽ f (x))), \end{aligned}

which is equivalent to

\begin{aligned} \forall x (A_{qf} (x, f (x)) \land \forall z (A_{qf} (x, z) \to z ⩽ f (x))) . \end{aligned}

$(2 \to 4)$ : Assume

\begin{aligned} \forall x \exists y (A_{qf} (x, y) \land \forall z (A_{qf} (x, z) \to z ⩽ y)) . \end{aligned}

(7)

Define

T \subseteq N^{*}

u \in T

if and only if

\begin{aligned} \forall i < | u | A_{qf} (i, u_{i}) . \end{aligned}

Then T is trivially a tree. By

QF - {AC}^{0, 0}

, there exists

g^{N^{N}}

such that

\forall x A_{qf} (x, g (x))

. Then we have

\forall x (\bar{g} x \in T)

. Thus T is infinite. Next, we claim that T is height-wise bounded. Fix

i^{N}

. By our assumption (7), there exists

y^{N}

such that

\forall z (A_{qf} (i, z) \to z ⩽ y)

. Fix

u \in T

such that

i < | u |

. By the definition of T, we have

A_{qf} (i, u_{i})

, and hence,

u_{i} ⩽ y

. Thus T is height-wise bounded. Therefore, by

{BT}_{hb}

, there exists a height-wise bounding function

h^{N^{N}}

of this tree T. Then, by (1), we have

\begin{aligned} \forall u \in T (u ⩽ \bar{h} | u |), \end{aligned}

where

u ⩽ \bar{h} | u |

is an order relation as codes. By (7), we have

\begin{aligned} \forall x \exists j (A_{qf} (x, j) \land \forall j^{'} ⩽ h (x) (A_{qf} (x, j^{'}) \to j^{'} ⩽ j)) . \end{aligned}

(8)

By using

QF - {AC}^{0, 0}

, we have a function

f^{N^{N}}

which attains a witness j for each x in (8). Fix

x^{N}

. Then we have

A_{qf} (x, f (x))

. In addition, for all

z^{N}

such that

A_{qf} (x, z)

, since

\bar{g} x * ⟨ z ⟩ \in T

, we have

z ⩽ f (x)

. Thus we have shown

\forall x (A_{qf} (x, f (x)) \land \forall z (A_{qf} (x, z) \to z ⩽ f (x)))

$(4 \to 5)$ : Assume

\begin{aligned} \forall x \exists y \forall z (A_{qf} (x, z) \to z ⩽ y) . \end{aligned}

Put

\begin{aligned} B_{qf} (x, y) :\equiv y = 0 \lor A_{qf} (x, y - 1) . \end{aligned}

Fix

x^{N}

. By our assumption, there exists

y^{N}

such that

\forall z (A_{qf} (x, z) \to z ⩽ y)

. Now

E L_{0}

proves

\forall z ⩽ y \neg A_{qf} (x, z)

\exists z ⩽ y A_{qf} (x, z)

. In the former case, put

y^{'}

as 0. In the latter case, put

y^{'}

max {z ⩽ y | A_{qf} (x, z)} + 1

. Then it is straightforward to see that

B_{qf} (x, y^{'})

and

\forall z (B_{qf} (x, z) \to z ⩽ y^{'})

hold (note that we have

\forall z \neg A_{qf} (x, z)

in the former case). By

QF - {MC}^{0, 0}

, there exists

f^{N^{N}}

such that

\begin{aligned} \forall x (B_{qf} (x, f (x)) \land \forall z (B_{qf} (x, z) \to z ⩽ f (x))) . \end{aligned}

Then

E L_{0}

proves that for all

x^{N}

and

z^{N}

A_{qf} (x, z)

implies

B_{qf} (x, z + 1)

, which implies

z + 1 ⩽ f (x)

, and hence,

z ⩽ f (x)

$(5 \to 1)$ : Let T be (the characteristic function of) an infinite finitely-branching tree. Put

\begin{aligned} A_{qf} (x, z) :\equiv x * ⟨ z ⟩ \in T, \end{aligned}

which is quantifier-free. In the following, we claim

\begin{aligned} \forall x \exists y \forall z (A_{qf} (x, z) \to z ⩽ y) . \end{aligned}

(9)

Fix

x^{N}

. If

x^{N}

is a code of a branch in T, since the tree T is finitely-branching, there exists

y^{N}

such that

\forall z (A_{qf} (x, z) \to z ⩽ y)

. Otherwise, arbitrary

y^{N}

plays the role since for any z,

x * ⟨ z ⟩

is not a code of a branch in T. Thus we have shown (9).

Applying $QF - {BC}^{0, 0}$ , we have $f^{N^{N}}$ such that

\begin{aligned} \forall x \forall z (A_{qf} (x, z) \to z ⩽ f (x)) . \end{aligned}

By recursion with using f, take

h^{N^{N}}

such that

\begin{aligned} h (j) = max {f (u) | | u | = j \land u ⩽ \bar{h} j \land u \in T} . \end{aligned}

(10)

In the following, we claim

\begin{aligned} \forall u \in T \forall j < | u | \forall i ⩽ j (u_{i} ⩽ h (i))) . \end{aligned}

(11)

Fix

u \in T

and

j < | u |

. We show

\forall i ⩽ j (u_{i} ⩽ h (i))

by course-of-values induction on i, which is available by

QF - IND

. The base case is trivial. For the induction step, assume

i + 1 ⩽ j

and

\forall i^{'} ⩽ i (u_{i^{'}} ⩽ h (i^{'}))

. Since

\bar{u} (i + 1) * u_{i + 1} \in T

, we have

A_{qf} (\bar{u} (i + 1), u_{i + 1})

, and hence,

u_{i + 1} ⩽ f (\bar{u} (i + 1))

. By the induction hypothesis and (1), we have

\bar{u} (i + 1) ⩽ \bar{h} (i + 1)

, and hence,

f (\bar{u} (i + 1)) ⩽ h (i + 1)

by (10). Therefore

u_{i + 1} ⩽ h (i + 1)

. Thus we have established our claim (11), which implies that h is a height-wise bounding function of T.

Remark 3.1.

The equivalence of ${BT}_{fb}$ and ${BT}_{hb}$ in Theorem 3.1 reveals that $T_{fb \to hb}$ is redundant in [4, Lemma 4.13(1)].

4. Decomposition results over

{EL}_{0}

In [4, Theorem 4.24], the first author showed that $KL!$ is equivalent to $WKL! + {BT}_{fb}$ over $E L_{0} + Σ_{2}^{0} - IND$ . On the other hand, it was open whether $Σ_{2}^{0} - IND$ can be omitted from the base theory. In this section, we give an affirmative answer to this question by applying the choice principle equivalent to ${BT}_{fb}$ in Section 3.

Lemma 4.1.

$E L_{0} + KL! ⊢ QF - {DMC}^{0, 0}$ .

Proof.

Assume

\begin{aligned} \forall u \exists y (A_{qf} (u, y) \land \forall z (A_{qf} (u, z) \to z ⩽ y)) . \end{aligned}

(12)

Define

T \subseteq N^{*}

u \in T

if and only if

\begin{aligned} \forall i < | u | (A_{qf} (\bar{u} i, u_{i}) \land \forall z < | u | (A_{qf} (\bar{u} i, z) \to z ⩽ u_{i})) . \end{aligned}

Then T is a tree obviously. In addition, for each fixed

u \in T

, there exists y such that

\begin{aligned} A_{qf} (u, y) \land \forall z (A_{qf} (u, z) \to z ⩽ y) \end{aligned}

by our assumption. Then, for any z such that

u * ⟨ z ⟩ \in T

, we have

A_{qf} (u, z)

and thus

z ⩽ y

. Thus T is finitely-branching.

Next, we show that T is infinite. Fix $x > 0$ . It is straightforward to show that, for all $j ⩽ x$ , there exists $u \in N^{*}$ such that $| u | = j$ and

\begin{aligned} \forall i < j (A_{qf} (\bar{u} i, u_{i}) \land \forall z < x (A_{qf} (\bar{u} i, z) \to z ⩽ u_{i})) \end{aligned}

(13)

by induction on

j ⩽ x

, which is available by

Σ_{1}^{0} - IND

since (13) is equivalent to some quantifier-free formula in

E L_{0}

. Note that the induction step is verified by our assumption (12). Then it follows that there exists

u \in T

such that

| u | = x

Finally, we show that T does not have two paths. Let $p^{N^{N}}$ , $q^{N^{N}}$ satisfy $p (m) \neq q (m)$ for some $m^{N}$ . Taking the least such m in $E L_{0}$ , we have

\begin{aligned} \bar{p} m = \bar{q} m . \end{aligned}

(14)

Without loss of generality, we may assume

q (m) > p (m)

. Now

\bar{q} (m + 1) \notin T

\bar{q} (m + 1) \in T

. In the former case, we are done. Suppose

\bar{q} (m + 1) \in T

. Then we have

\begin{aligned} A_{qf} (\bar{q} m, q (m)) . \end{aligned}

(15)

Put

k := m + q (m) + 1

. Suppose also

\bar{p} k \in T

. Then

\begin{aligned} A_{qf} (\bar{p} m, p (m)) \land \forall z < m + q (m) + 1 (A_{qf} (\bar{p} m, z) \to z ⩽ p (m)) . \end{aligned}

By (15) and (14), we have

q (m) ⩽ p (m)

, which is a contradiction. Thus we have shown

\bar{p} k \notin T

Therefore, by $KL!$ , there exists $p^{N^{N}}$ such that $\forall n^{N} (\bar{p} n \in T)$ , namely,

\begin{aligned} \forall n \forall i < n (A_{qf} (\bar{p} i, p (i)) \land \forall z < n (A_{qf} (\bar{p} i, z) \to z ⩽ p (i))) . \end{aligned}

Fix

x^{N}

and

z^{N}

. Since

\bar{p} (x + z + 1) \in T

, we have

A_{qf} (\bar{p} x, p (x))

and

A_{qf} (\bar{p} x, z) \to z ⩽ p (x)

. Thus we have shown

\begin{aligned} \forall x (A_{qf} (\bar{p} x, p (x)) \land \forall z (A_{qf} (\bar{p} x, z) \to z ⩽ p (x))) . \end{aligned}

For the decompositions of $KL!$ , $KL!!$ and $KL$ over $E L_{0}$ , we use so-called bounded König’s lemma $BKL$ , which states that for any infinite tree T which has a height-wise bounding function, there exists a path through T. The unique variants $BKL!$ and $BKL!!$ are defined as for $KL!$ and $KL!!$ (see [4, Section 4.2.1] for more information on $BKL!$ and $BKL!!$ ).

Theorem 4.1.

The following are pairwise equivalent over $E L_{0}$ :

$KL!$ ;

$WKL! + {BT}_{fb}$ ;

$WKL! + QF - {MC}^{0, 0}$ .

Proof.

Since $WKL!$ implies $BKL!$ (cf. [5, Corollary 1]) and $BKL! + {BT}_{fb}$ implies $KL!$ over $E L_{0}$ , our theorem follows from Lemma 4.1 and Theorem 3.1 immediately.

Theorem 4.2.

The following are pairwise equivalent over $E L_{0}$ :

$KL!!$ ;

$WKL!! + {BT}_{fb}$ ;

$WKL!! + QF - {MC}^{0, 0}$ .

Proof.

Since $KL!!$ implies $KL!$ , $WKL!!$ implies $BKL!!$ (cf. [4, Lemma 4.26]) and $BKL!! + {BT}_{fb}$ implies $KL!!$ over $E L_{0}$ , our theorem follows again from Lemma 4.1 and Theorem 3.1.

Theorem 4.3.

The following are pairwise equivalent over $E L_{0}$ :

$KL$ ;

$WKL + {BT}_{fb}$ ;

$WKL + QF - {MC}^{0, 0}$ .

Proof.

Since $KL$ implies $KL!$ , $WKL$ implies $BKL$ (cf. [4, Proposition 4.7]) and $BKL + {BT}_{fb}$ implies $KL$ over $E L_{0}$ , our theorem follows again from Lemma 4.1 and Theorem 3.1.

Footnotes

Acknowledgements

The authors thank the anonymous referees for their helpful comments on the earlier version of this paper. The first author was supported by JSPS KAKENHI Grant Numbers JP19J01239, JP20K14354 and JP23K03205, the second author by JP18K03392, and both authors by JP21KK0045.

References

Berger

Ishihara

, Brouwer’s fan theorem and unique existence in constructive analysis, Mathematical Logic Quarterly 51(4) (2005), 360–364. doi:10.1002/malq.200410038.

Berger

Ishihara

Kihara

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.

Fujiwara

, Intuitionistic and uniform provability in reverse mathematics, PhD thesis, Tohoku University, 2015.

Fujiwara

, König’s lemma, weak König’s lemma, and the decidable fan theorem, Mathematical Logic Quarterly 67(2) (2021), 241–257. doi:10.1002/malq.202000020.

Fujiwara

, An extension of the equivalence between Brouwer’s fan theorem and weak König’s lemma with a uniqueness hypothesis, in: Revolutions and Revelations in Computability, Berger

Franklin

J.N.Y.

Manea

Pauly

, eds, Springer International Publishing, Cham, 2022, pp. 115–124. doi:10.1007/978-3-031-08740-0_10.

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.

Moschovakis

J.R.

, Another unique weak König’s lemma, in: Logic, Construction, Computation, Ontos Mathematical Logic, Berger

Diener

Schuster

Seisenberger

, eds, De Gruyter, Berlin, Boston, 2012, pp. 343–352. doi:10.1515/9783110324921.343.

Nemoto

, Systems for constructive reverse mathematics, in: Handbook of Constructive Mathematics, Encyclopedia of Mathematics and Its Applications, Bridges

Ishihara

Rathjen

Schwichtenberg

, eds, Cambridge University Press, 2023, pp. 661–699. doi:10.1017/9781009039888.025.

Schwichtenberg

, A direct proof of the equivalence between Brouwer’s fan theorem and König’s lemma with a uniqueness hypothesis, Journal of Universal Computer Science 11(12) (2005), 2086–2095. doi:10.3217/jucs-011-12-2086.

10.

Simpson

S.G.

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

11.

Troelstra

A.S.

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