SEPARATION AND WEAK KÖNIG’S LEMMA

A. JAMES HUMPHREYS STEPHEN G. SIMPSON

Abstract. We continue the work of [14, 3, 1, 19, 16, 4, 12, 11, 20] investigating the strength of set existence axioms needed for separable Banach space theory. We show that the separation theorem for open convex sets is equivalent to WKL_{0} over RCA_{0}. We show that the separation theorem for separably closed convex sets is equivalent to ACA_{0} over RCA_{0}. Our strategy for proving these geometrical Hahn–Banach theorems is to reduce to the finite-dimen-sional case by means of a compactness argument.

1. Introduction

Let A and B be convex sets in a Banach space X. We say that A and B are separated if there is a bounded linear functional F : X → ℝ and a real number α such that F (x) < α for all x ∈ A, and F (x) ≥ α for all x ∈ B. We say that A and B are strictly separated if in addition F (x) > α for all x ∈ B.

There are several well-known theorems of Banach space theory to the effect that any two disjoint convex sets satisfying certain conditions can be separated or strictly separated. A good reference for such theorems is Conway [6]. The purpose of this paper is to consider the question of which set existence axioms are needed to prove such theorems. We study this question in the context of subsystems of second order arithmetic.

The subsystems of second order arithmetic that are relevant here are ACA_{0}, RCA_{0}, and above all WKL_{0}. ACA_{0} is the system with arithmetical comprehension and arithmetical induction; it is conservative over firstorder Peano arithmetic. RCA_{0} is the much weaker system with only Δ_{1}^{0} comprehension and Σ_{1}^{0} induction; it may be viewed as a formalized version of recursive mathematics. WKL_{0} consists of RCA_{0} plus an additional set existence axiom known as Weak König’s Lemma. WKL_{0} and

Date: September 2, 1997.

Simpson’s research was partially supported by NSF grant DMS-9303478.

Accepted October 10, 1997 for Journal of Symbolic Logic.

SEPARATION AND WEAK KÖNIG’S LEMMA 2

RCA_{0} are conservative over arithmetic with Σ_{1}^{0} induction [9, 18, 20], hence much weaker than ACA_{0} in terms of proof-theoretic strength. Moreover, WKL_{0} and RCA_{0} are conservative over primitive recursive arithmetic for Π_{2}^{0} sentences [7, 18, 20]. The foundational significance of this result is that any mathematical theorem provable in WKL_{0} is finitistically reducible [19].

The main new result of this paper is that the basic separation theorem for convex sets in separable Banach spaces is provable in WKL_{0}; see Theorem 3.1 below. It follows that the basic separation theorem is finitistically reducible. This provides further confirmation of the well-known significance of WKL_{0} with respect to Hilbert’s program of finitistic reductionism [19].

As a byproduct of our work on separation theorems in WKL_{0}, we present new proofs of the closely related Hahn–Banach and extended Hahn–Banach theorems in WKL_{0}; see Section 4 below. These new proofs are more transparent than the ones that have appeared previously [3, 16, 20, 12].

We also obtain reversals in the sense of Reverse Mathematics. We show that the basic separation theorem is logically equivalent to WKL_{0} over RCA_{0}; see Theorem 4.4 below. Thus Weak König’s Lemma is seen to be logically indispensable for the development of this portion of functional analysis. In addition, we show that another separation theorem requires stronger set existence axioms, in that it is equivalent to ACA_{0} over RCA_{0}; see Theorem 5.1 below.

One aspect of this paper may be of interest to readers who are familiar with Banach spaces but do not share our concern with foundational issues. Namely, we present a novel and elegant proof of the various separation and Hahn–Banach theorems. Our approach is to reduce to the finite-dimensional Euclidean case by means of a straightforward compactness argument. A similar proof strategy has been used previously (see Łoś/Ryll-Nardzewski [13]) but is apparently not widely known. We thank Ward Henson for bringing [13] to our attention.

2. Preliminaries

The prerequisite for a thorough understanding of this paper is familiarity with the basics of separable Banach space theory as developed in RCA_{0}. This material has been presented in several places: [3, §§2-5], [4, §1], [12, §4], [20, §II.10]. We briefly review some of the concepts that we shall need.

Within RCA_{0}, a (code for a) complete separable metric space X = Â is defined to be a countable set A ⊆ ℕ together with a function d : A×A → ℝ satisfying d(a, a) = 0, d(a, b) = d(b, a), and d(a, b)+d(b, c) ≥

SEPARATION AND WEAK KÖNIG’S LEMMA 3

d(a, c). A (code for a) point of X is defined to be a sequence x = ⟨a_{n}⟩_{n∈ℕ} of elements of A such that ∀m∀n(m < n → d(a_{m}, a_{n}) ≤ 1/2^{m}). We extend d from A to X in the obvious way. For x, y ∈ X we define x = y to mean that d(x, y) = 0.

Within RCA_{0}, (a code for) an open set in X is defined to be a sequence of ordered pairs U = ⟨(a_{m}, r_{m})⟩_{m∈ℕ} where a_{m} ∈ A and r_{m} ∈ ℚ, the rational numbers. We write x ∈ U to mean that d(a_{m}, x) < r_{m} for some m ∈ ℕ. A closed set C ⊆ X is defined to be the complement of an open set U, i.e., ∀x ∈ X(x ∈ C ↔ x ∉ U).

It will sometimes be necessary to consider a slightly different notion. A (code for a) separably closed set K = \overline{S} ⊆ X is defined to be a countable sequence of points S ⊆ X. We write x ∈ K to mean that for all ε > 0 there exists y ∈ S such that d(x, y) < ε. It is provable in ACA_{0} (but not in weaker systems) that for every separably closed set K there exists an equivalent closed set C, i.e., ∀x ∈ X(x ∈ C ↔ x ∈ K). For further details on separably closed sets, see [2, 3, 4].

Within RCA_{0}, a compact set K ⊆ X is defined to be a separably closed set such that there exists a sequence of finite sequences of points x_{ni} ∈ K, i ≤ k_{n}, n ∈ ℕ, such that for all n ∈ ℕ and all x ∈ K there exists i ≤ k_{n} with d(x, x_{ni}) < 1/2^{n}. The sequence of positive integers k_{n}, n ∈ ℕ, is also required to exist. It is provable in RCA_{0} that compact sets are closed and located [8]. It is provable in WKL_{0} that compact sets have the Heine–Borel covering property, i.e., any covering of K by a sequence of open sets has a finite subcovering.

Within RCA_{0}, a (code for a) separable Banach space X = Â is defined to be a countable pseudonormed vector space A over ℚ. With d(a, b) = ∥a − b∥, X is a complete separable metric space and has the usual structure of a Banach space over ℝ. A bounded linear functional F : X → ℝ may be defined as a continuous function which is linear. The equivalence of continuity and boundedness is provable in RCA_{0}. We write ∥F ∥ ≤ α to mean that |F (x)| ≤ α∥x∥ for all x ∈ X.

3. Separation in WKL_{0}

The purpose of this section is to prove the following theorem.

Theorem 3.1. The following is provable in WKL_{0}. Let X be a separable Banach space. Let A be an open convex set in X, and let B be a separably closed convex set in X. If A and B are disjoint, then A and B can be separated.

Remark 3.2. Theorem 3.1 verifies a conjecture that appeared in [11], page 61. A special case of this result had been conjectured earlier in [12], page 4246. Corollary 5.1.2 of [11] (see also Lemma 4.10 of [12]) is essentially our present Theorem 3.1 with WKL_{0} replaced by ACA_{0}.

Toward the proof of Theorem 3.1, we first prove a separation result for finite-dimensional Euclidean spaces.

Lemma 3.3. The following is provable in WKL_{0}. Let A and B be compact convex sets in ℝ^{n}. If A and B are disjoint, then A and B can be strictly separated.

Proof. For x, y ∈ ℝ^{n} we denote by x · y the dot product of x and y. The norm on ℝ^{n} is given by ∥x∥^{2} = x · x. We imitate the argument of Lemma 3.1 of [5].

Put C = B − A = {y − x | x ∈ A, y ∈ B}. Then C is a compact convex set in ℝ^{n}. Since A ∩ B = ∅, we have 0 ∉ C. The function z ↦ ∥z∥ is continuous on C, so it follows in WKL_{0} that there exists c ∈ C of minimum norm, i.e., 0 < ∥c∥ ≤ ∥z∥ for all z ∈ C.

We claim that ∥c∥^{2} ≤ c · z for all z ∈ C. Suppose not. Let z ∈ C be such that ∥c∥^{2} − c · z = ε > 0. Consider w = tz + (1 − t)c where 0 < t ≤ 1. Since C is convex, we have w ∈ C, hence 0 < ∥c∥ ≤ ∥w∥. Expansion of ∥w∥^{2} = w · w gives

∥w∥^{2} = ∥c∥^{2} + t^{2}(∥z∥^{2} − ∥c∥^{2}) − 2t(1 − t)ε

and from this it follows that t(∥z∥^{2} − ∥c∥^{2}) ≥ 2(1 − t)ε. Now set

t = \frac{ε}{∥z∥^{2} − ∥c∥^{2} + 2ε}

and note that 0 < t ≤ 1/2. With this t we have

t(∥z∥^{2} − ∥c∥^{2}) = ε − 2εt < 2ε − 2εt = 2(1 − t)ε ,

a contradiction. This proves our claim.

Define F : ℝ^{n} → ℝ by F (z) = c · z. Since c ∈ C = B − A, we may fix a ∈ A and b ∈ B such that c = b − a. Using our claim, it is easy to show that F (x) ≤ F (a) < F (b) ≤ F (y) for all x ∈ A and y ∈ B. Thus A and B are strictly separated.

In order to reduce Theorem 3.1 to the finite-dimensional Euclidean case, we need some technical lemmas.

Lemma 3.4. The following is provable in WKL_{0}. Let X and K be complete separable metric spaces. Assume that K is compact. If C ⊆ X × K is closed, then

{x ∈ X | (x, y) ∈ C for some y ∈ K}

is closed.

Proof. Reasoning in WKL_{0}, put V = (X × K) \ C and

U = {x ∈ X | (x, y) ∈ V for all y ∈ K} .

We shall prove that U is open.

Since V is open, there is a sequence of open balls B((a_{m}, b_{m}), r_{m}), (a_{m}, b_{m}) ∈ X × K, r_{m} ∈ ℚ, m ∈ ℕ, such that

V = ⋃_{m=0}^{∞} B((a_{m}, b_{m}), r_{m}) .

Since K is compact, there is a sequence of points y_{ni} ∈ K, i ≤ k_{n}, n ∈ ℕ, such that K = ⋃_{i≤k_{n}} B(y_{i,n}, 1/2^{n}) for each n.

We claim that

∃n ∀i ≤ k_{n} ∃m d((a_{m}, b_{m}), (x, y_{ni})) + 1/2^{n} < r_{m} (1)

is a necessary and sufficient condition for x ∈ U. Obviously (1) is sufficient since it implies {x}×K ⊆ ⋃_{i≤k_{n}} B((x, y_{ni}), 1/2^{n}) ⊆ V whence x ∈ U. For the necessity, let x ∈ U be given. Then {x} × K ⊆ ⋃_{m=0}^{∞} B((a_{m}, b_{m}), r_{m}). By Heine–Borel compactness of K in WKL_{0} it follows that {x} × K ⊆ ⋃_{m=0}^{k} B((a_{m}, b_{m}), q_{m}) for some k ∈ ℕ and finite sequence q_{m} ∈ ℚ, m ≤ k, q_{m} < r_{m}. Let n be such that 1/2^{n} < min_{m≤k}(r_{m} − q_{m}). Then for each i ≤ k_{n} there exists m ≤ k such that d((a_{m}, b_{m}), (x, y_{ni})) < q_{m}, hence d((a_{m}, b_{m}), (x, y_{ni})) + 1/2^{n} < r_{m}. This gives condition (1) and our claim is proved.

Since the condition (1) is Σ_{1}^{0}, it follows by Lemma II.5.7 of [20] that U ⊆ X is open. Therefore, the complementary set is closed. This proves our lemma.

Lemma 3.5. The following is provable in WKL_{0}. Let X be a separable Banach space. Fix n ≥ 1 and let Y = ⋃_{m=1}^{n} X^{m} be the space of all finite sequences of elements of X of length ≤ n. Then

{s ∈ Y | s is linearly independent}

is an open set in Y.

Proof. Consider the compact space K = ⋃_{m=1}^{n} K_{m} where

K_{m} = {⟨α_{1}, …, α_{m}⟩ | |α_{1}| + ⋯ + |α_{m}| = 1} .

Here the α_{i}’s are real numbers. Note that s = ⟨x_{1}, …, x_{m}⟩ ∈ Y is linearly dependent if and only if α_{1}x_{1} + ⋯ + α_{m}x_{m} = 0 for some ⟨α_{1}, …, α_{m}⟩ ∈ K. Hence by Lemma 3.4 the set of all such s is closed. It follows that the complementary set is open.

SEPARATION AND WEAK KÖNIG’S LEMMA 6

Lemma 3.6. The following is provable in WKL_{0}. Let K be a compact metric space, and let ⟨C_{j}⟩_{j∈ℕ} be a sequence of nonempty closed sets in K. Then there exists a sequence of points ⟨x_{j}⟩_{j∈ℕ} such that x_{j} ∈ C_{j} for all j.

Proof. Since K is compact, there is a sequence of points x_{ni} ∈ K, i ≤ k_{n}, n ∈ ℕ, such that K = ⋃_{i≤k_{n}} B(x_{in}, 1/2^{n}) for each n ∈ ℕ. Let S be the bounded tree consisting of all finite sequences σ ∈ ℕ^{<ℕ} such that σ(n) ≤ k_{n} for all n < the length of σ. Construct a sequence of trees T_{j} ⊆ S, j ∈ ℕ, such that for each j there is a one-to-one correspondence between infinite paths g in T_{j} and points x ∈ C_{j}, the correspondence being given by x = lim_{n} x_{ng(n)}. For details of the construction of the T_{j}’s, see Section IV.1 of [20].

Let (−, −) : ℕ × ℕ → ℕ be a primitive recursive pairing function which is onto and monotone in both arguments. Let T = ⨁_{j∈ℕ} T_{j} be the interleaved tree, defined by putting τ ∈ T if and only if τ_{j} ∈ T_{j} for all j, where τ_{j}(n) = τ((j, n)). Note that T is a bounded tree, the bounding function h : ℕ → ℕ being given by h((j, n)) = k_{n} + 1. In order to show that T is infinite, we prove that for all m there exists τ ∈ T of length m such that for all j and all n ≥ length of τ_{j}, τ_{j} has at least one extension of length n in T_{j}. This Π_{1}^{0} statement is easily proved by Π_{1}^{0} induction on m, using the fact that each of the T_{j}’s is infinite.

Since T is an infinite bounded tree, it follows by Bounded König’s Lemma in WKL_{0} (see Section IV.1 of [20]) that T has an infinite path, f. Then for each j we have an infinite path f_{j} in T_{j} given by f_{j}(n) = f((j, n)). Thus we obtain a sequence of points ⟨x_{j}⟩_{j∈ℕ} where x_{j} = lim_{n} x_{nf_{j}(n)} is a point of C_{j}.

Lemma 3.7. The following is provable in WKL_{0}. Let X be a separable Banach space, and let x_{1}, …, x_{n} be a finite set of elements of X. Then there is a closed subspace X′ = span(x_{1}, …, x_{n}) ⊆ X consisting of all linear combinations of x_{1}, …, x_{n}. Moreover, there exists a finite set

x_{i_{1}}, …, x_{i_{m}} , 1 ≤ i_{1} < ⋯ < i_{m} ≤ n ,

which is a basis of X′, i.e., each element of X′ is uniquely a linear combination of x_{i_{1}}, …, x_{i_{m}}.

Proof. We first prove that X′ has a basis. By lemma 3.5, the set of all linearly independent s ∈ ⋃_{m=0}^{n} X^{m} is open. By bounded Σ_{1}^{0} comprehension in WKL_{0}, it follows that

I = {I ⊆ {1, …, n} | {x_{i} | i ∈ I} is linearly independent}

SEPARATION AND WEAK KÖNIG’S LEMMA 7

is a finite set of subsets of {1, …, n}. Let M = {i_{1}, …, i_{m}} be a maximal element of I. Then clearly each of x_{1}, …, x_{n} is a linear combination of x_{i_{1}}, …, x_{i_{m}}. Moreover, we can apply Lemma 3.6 to obtain a double sequence of coefficients α_{ij}, i = 1, …, n, j = 0, 1, …, m, such that

|α_{i0}| + |α_{i1}| + ⋯ + |α_{im}| = 1

and

α_{i0}x_{i} + α_{i1}x_{i_{1}} + ⋯ + α_{im}x_{i_{m}} = 0

for each i = 1, …, n. Obviously α_{i0} ≠ 0 so we may put β_{ij} = −α_{ij}/α_{i0} to obtain

x_{i} = β_{i1}x_{i_{1}} + ⋯ + β_{im}x_{i_{m}}

for each i = 1, …, n. With this it is clear that every linear combination of x_{1}, …, x_{n} is uniquely a linear combination of x_{i_{1}}, …, x_{i_{m}}.

It remains to prove that X′ is a closed subspace of X. As a code for X′ we may use ℚ^{n} identifying ⟨q_{1}, …, q_{n}⟩ ∈ ℚ^{n} with q_{1}x_{1}+⋯+q_{n}x_{n} ∈ X. Thus X′ is a subspace of X. The fact that X′ is closed follows easily from Lemma 3.5.

We are now ready to prove Theorem 3.1.

Proof of Theorem 3.1. Reasoning within WKL_{0}, let X, A, B be as in the hypotheses of Theorem 3.1. We need to prove that A and B can be separated. Since A is open, we may safely assume that

{x ∈ X | ∥x∥ ≤ 1} ⊆ A .

With this assumption, reasoning in WKL_{0}, our goal will be to prove the existence of a bounded linear functional F : X → ℝ such that F (x) ≤ 1 for all x ∈ A, and F (x) ≥ 1 for all x ∈ B; these properties easily imply that F (x) < 1 for all x ∈ A. Observe also that any such F will necessarily have ∥F ∥ ≤ 1.

Since X is a separable Banach space, there exists a countable vector space D over the rational field ℚ such that D ⊆ X and D is dense in X. Since B is separably closed, there exists a countable sequence S ⊆ B such that S is dense in B. We may safely assume that S ⊆ D. With this assumption, consider the compact product space

K = ∏_{d∈D} [−∥d∥, ∥d∥] .

Note that any bounded linear functional F : X → ℝ with ∥F ∥ ≤ 1 may be identified with a point of K in an obvious way, namely F =

SEPARATION AND WEAK KÖNIG’S LEMMA 8

⟨F (d)⟩_{d∈D}. Thus our goal may be expressed as follows: to prove that there exists a point ⟨α_{d}⟩_{d∈D} ∈ K satisfying the conditions

1. α_{d} ≤ 1 for all d ∈ D ∩ A;

2. α_{d} ≥ 1 for all d ∈ S;

3. α_{d} = q_{1}α_{d_{1}} + q_{2}α_{d_{2}} for all d, d_{1}, d_{2} ∈ D and q_{1}, q_{2} ∈ ℚ such that

d = q_{1}d_{1} + q_{2}d_{2}. Let Φ be this countable set of Π_{1}^{0} conditions. By Heine–Borel compactness of K in WKL_{0}, it suffices to show that each finite subset of Φ is satisfied by some point of K.

Suppose we are given a finite set of conditions Φ′ ⊆ Φ. Let a_{1}, …, a_{m} be the elements of D∩A that are mentioned in Φ′. Let b_{1}, …, b_{n} be the elements of S that are mentioned in Φ′. Let d_{1}, …, d_{k} be the nonzero elements of D that are mentioned in Φ′. By Lemma 3.7, let X′ be the finite-dimensional subspace of X spanned by d_{1}, …, d_{k}. Let A′ be the convex hull of a_{1}, …, a_{m}, ±d_{1}/∥d_{1}∥, …, ±d_{k}/∥d_{k}∥. Let B′ be the convex hull of b_{1}, …, b_{n}. Note that A′ ⊆ A ∩ X′ and B′ ⊆ B ∩ X′; hence A′ ∩ B′ = ∅. Moreover A′ and B′ are compact. By Lemmas 3.7 and 3.3, there exists a bounded linear functional F′ : X′ → ℝ such that F′(x) ≤ 1 for all x ∈ A′, and F′(x) ≥ 1 for all x ∈ B′. In particular F′(±d_{i}/∥d_{i}∥) ≤ 1 for all i = 1, …, k; hence |F′(d_{i})| ≤ ∥d_{i}∥. Put α′_{d} = F′(d) for d = d_{1}, …, d_{k}, and α′_{d} = 0 for d ∈ D \ {d_{1}, …, d_{k}}. Then ⟨α′_{d}⟩_{d∈D} is a point of K which satisfies Φ′. This completes the proof.

Remark 3.8. Our proof of a separation theorem in WKL_{0} (Theorem 3.1) was accomplished by means of a reduction to the finite-dimensional Euclidean case using a compactness argument. This proof technique is not entirely new (see [13]) but does not seem to be widely known.

4. Reversal via Hahn–Banach

Let X be a separable Banach space. Consider the following statements:

SEP1: (First Separation) Let A be an open convex set in X, let B be a separably closed convex set in X, and assume A ∩ B = ∅. Then A and B can be separated.

SEP2: (Second Separation) Let A and B be open convex sets in X

such that A ∩ B = ∅. Then A and B can be strictly separated. SEP3: (Third Separation) Let A and B be separably closed, convex

sets in X such that A ∩ B = ∅. Assume also that A is compact. Then A and B can be strictly separated.

HB: (Hahn–Banach) Let S be a subspace of X, and let f : S → ℝ be a bounded linear functional with ∥f∥ ≤ α on S. Then there

SEPARATION AND WEAK KÖNIG’S LEMMA 9

exists a bounded linear functional F : X → ℝ such that F extends f and ∥F ∥ ≤ α on X.

EHB: (Extended Hahn–Banach) Let p : X → ℝ be a continuous sublinear functional. Let S be a subspace of X, and let f : S → ℝ be a bounded linear functional such that f(x) ≤ p(x) for all x ∈ S. Then there exists a bounded linear functional F : X → ℝ such that F extends f and F (x) ≤ p(x) for all x ∈ X.

It is known [3, 12] that EHB and HB are equivalent to WKL_{0} over RCA_{0}. We are now going to prove that SEP1 and SEP2 are also equivalent to WKL_{0} over RCA_{0}; see Theorem 4.4 below. In the next section we shall prove that SEP3 is equivalent to ACA_{0}, hence properly stronger than WKL_{0}, over RCA_{0}; see Theorem 5.1 below.

Lemma 4.1. It is provable in RCA_{0} that SEP1 implies SEP2.

Proof. Reasoning in RCA_{0}, assume SEP1 and let A and B be disjoint, open, convex sets. Let B′ be the separable closure of B. Clearly B′ is convex and A ∩ B′ = ∅. By SEP1, let F and α be such that F < α on A and F ≥ α on B′. It follows that F > α on B. Thus we have SEP2. This completes the proof.

Lemma 4.2. It is provable in RCA_{0} that SEP2 implies EHB.

Proof. Reasoning in RCA_{0}, assume SEP2 and let p, S, and f be as in the hypotheses of EHB. Let A be the convex hull of

{x ∈ S | f(x) < 1} ∪ {y ∈ X | p(y) < 1} ,

and let B be the convex hull of

{x ∈ S | f(x) > 1} ∪ {y ∈ X | −p(−y) > 1} .

Clearly A and B are open.

We claim that A and B are disjoint. If not, then for some 0 ≤ α ≤ 1, 0 ≤ β ≤ 1, x_{1} ∈ S, y_{1} ∈ X, x_{2} ∈ S, y_{2} ∈ X we have f(x_{1}) < 1, p(y_{1}) < 1, f(x_{2}) > 1, −p(−y_{2}) > 1, and

(1 − α)x_{1} + αy_{1} = (1 − β)x_{2} + βy_{2} .

Note that αy_{1} − βy_{2} ∈ S. Hence

f(αy_{1} − βy_{2}) ≤ p(αy_{1} − βy_{2})
≤ αp(y_{1}) + βp(−y_{2})
≤ α − β ,

yet on the other hand we have

f(αy_{1} − βy_{2}) = f((1 − β)x_{2} − (1 − α)x_{1})
= (1 − β)f(x_{2}) − (1 − α)f(x_{1})
≥ (1 − β) − (1 − α)
= α − β ,

hence f(αy_{1} −βy_{2}) = α−β. Since at least one of the above inequalities must be strict, we obtain a contradiction. This proves our claim.

By SEP2, there exists a bounded linear functional F : X → ℝ such that F (x) < 1 for all x ∈ A, and F (x) > 1 for all x ∈ B. Clearly F extends f. It remains to show that F (y) ≤ p(y) for all y ∈ X. Suppose not, say p(y) < F (y). If F (y) > 0, then for a suitably chosen r > 0 we have p(ry) < 1 < F (ry), a contradiction. If F (y) ≤ 0, then for a suitably chosen r > 0 we have p(ry) < −1 < F (ry). Putting z = −ry we get −p(−z) > 1 > F (z), again a contradiction. This completes the proof.

Lemma 4.3. It is provable in RCA_{0} that EHB implies HB.

Proof. HB is a special case of EHB with p(x) = α∥x∥.

Theorem 4.4. The following statements are pairwise equivalent over RCA_{0}.

1. SEP1, the first separation theorem.

2. SEP2, the second separation theorem.

3. EHB, the extended Hahn–Banach theorem.

4. HB, the Hahn–Banach theorem.

5. WKL_{0}.

Proof. Lemmas 4.1, 4.2, 4.3 give the implications SEP1 ⇒ SEP2 and SEP2 ⇒ EHB and EHB ⇒ HB. The equivalence HB ⇔ WKL_{0} is the main result of [3]; see also [14] and [16] and Chapter IV of [20]. Theorem 3.1 gives the implication WKL_{0} ⇒ SEP1. This completes the proof.

Corollary 4.5. The extended Hahn–Banach theorem, EHB, is provable in WKL_{0}.

Remark 4.6. Corollary 4.5 has been stated in the literature; see Theorem 4.9 of [12]. However, the proof given above is new. In addition, the proof given above contains full details, while the proof in [12] was presented in a very sketchy way.

Corollary 4.7. The Hahn–Banach theorem, HB, is provable in WKL_{0}.

SEPARATION AND WEAK KÖNIG’S LEMMA 11

Remark 4.8. Corollary 4.7 has been proved several times in the literature; see [3] and [16] and Chapter IV of [20]. The proof given here is new and, from some points of view, more perspicuous.

Remark 4.9. Hatzikiriakou [10] has shown that that an algebraic separation theorem for countable vector spaces over ℚ is equivalent to WKL_{0} over RCA_{0}. This result may be compared to our Theorem 4.4. We do not see any easy way of deducing our result from that of [10] or vice versa, but the comparison is interesting.

5. Separation and ACA_{0}

Theorem 5.1. The following statements are pairwise equivalent over RCA_{0}.

1. ACA_{0}.

2. SEP3, the third separation theorem.

3. Let A and B be disjoint, bounded, separably closed, convex sets in ℝ^{2}. Assume also that A is compact. Then A and B can be separated.

Proof. Reasoning in ACA_{0}, let A and B satisfy the hypotheses of SEP3. In ACA_{0}, separably closed implies closed (see [2]), so B is closed. Hence we can use Heine–Borel compactness of A to find δ > 0 such that ∥x − y∥ > δ for all x ∈ A and y ∈ B. Let B(0, δ/2) be the open ball of radius δ/2 centered at 0. Then A′ = A + B(0, δ/2) and B′ = B + B(0, δ/2) are disjoint open convex sets. By SEP2 we can strictly separate A′ and B′. This proves SEP3 in ACA_{0}.

Trivially SEP3 implies statement 5.1.3.

It remains to prove that statement 5.1.3 implies ACA_{0} over RCA_{0}. Reasoning in RCA_{0}, assume that ACA_{0} fails. Then there exists a bounded increasing sequence of rational numbers a_{n}, n ∈ ℕ, such that sup_{n} a_{n} does not exist. (See Chapter III of [20].) We may safely assume 0 < a_{n} < 1. Let A = [0, 1] × {0}, and let B be the separably closed convex hull of the points (a_{n}, 1/n), n ≥ 1. Note that A and B are bounded, separably closed, convex sets in ℝ^{2}. Moreover A is compact, and clearly A and B cannot be separated. Thus we have a counterexample to 5.1.3, once we show that A and B are disjoint.

To show that A and B are disjoint, let S be the countable set consisting of all rational convex combinations of points (a_{n}, 1/n), n ≥ 1. Thus B is the separable closure of S.

We claim: for all n ≥ 1 there exists ε_{n} > 0 such that for all (x, y) ∈ S, if x < a_{n} then y > ε_{n}. To see this, note that

(x, y) = ∑_{i=1}^{k} q_{i} (a_{n_{i}}, \frac{1}{n_{i}} )

where ∑_{i=0}^{k} q_{i} = 1, q_{i} > 0, q_{i} ∈ ℚ. Thus x = ∑_{i=0}^{k} q_{i}a_{n_{i}}. Putting r = ∑{q_{i} | n_{i} ≤ n} we have

a_{n} > x ≥ ra_{1} + (1 − r)a_{n+1} ,

hence

r > \frac{a_{n+1} − a_{n}}{a_{n+1} − a_{1}} > 0 .

Furthermore

y = ∑_{i=0}^{k} q_{i} \frac{1}{n_{i}} ≥ r · \frac{1}{n} .

Therefore we put

ε_{n} = \frac{a_{n+1} − a_{n}}{a_{n+1} − a_{1}} · \frac{1}{n}

and our claim is proved.

Now if (x, 0) ∈ A ∩ B, we clearly have x < a_{n} for some n. Since S is dense in B, let (x′, y′) ∈ S be such that

|x − x′| , |y′| < min(a_{n+1} − a_{n}, ε_{n+1}) .

Then x′ < a_{n+1} and y′ < ε_{n+1}, a contradiction. Thus A and B are disjoint. This completes the proof.

Remark 5.2. A modification of the above argument shows that ACA_{0} is equivalent over RCA_{0} to the following even weaker-sounding statement: if A and B are disjoint, bounded, separably closed, convex sets in ℝ^{2}, and if A is compact, then there exists an open set U such that A ⊆ U and U ∩ B = ∅.

Remark 5.3. In the functional analysis literature, separation results such as SEP1, SEP2, and SEP3 are sometimes referred to as “geometrical forms of the Hahn–Banach theorem.” It is therefore of interest to perform a detailed comparison of these separation results with the (nongeometrical) Hahn–Banach and extended Hahn–Banach theorems. Our results in this paper shed some light on the logical or foundational aspect of such a comparison. We note that, although SEP1 and SEP2 are logically equivalent to HB and EHB over RCA_{0} (Theorem 4.4), SEP3 is logically stronger (Theorem 5.1). Moreover, even though SEP2 and EHB turn out to be equivalent in this sense, we were unable to find a direct proof of this fact; the proof that we found is highly indirect, via WKL_{0}. Thus we conclude that, from our foundational standpoint, it is somewhat inaccurate to view the separation theorems as trivial variants of the Hahn–Banach or extended Hahn–Banach theorems.

References

1. Douglas K. Brown, Functional Analysis in Weak Subsystems of Second Order Arithmetic, Ph.D. thesis, The Pennsylvania State University, 1987, vii + 150 pages.

2. , Notions of closed subsets of a complete separable metric space in weak subsystems of second order arithmetic, [17], 1990, pp. 39–50.

3. Douglas K. Brown and Stephen G. Simpson, Which set existence axioms are needed to prove the separable Hahn-Banach theorem?, Annals of Pure and Applied Logic 31 (1986), 123–144.

4. , The Baire category theorem in weak subsystems of second order arithmetic, Journal of Symbolic Logic 58 (1993), 557–578.

5. Neil Cameron, Introduction to Linear and Convex Programming, Cambridge University Press, 1985, 149 pages.

6. John B. Conway, A Course in Functional Analysis, 2nd ed., Springer-Verlag, 1990, XVI + 399 pages.

7. Harvey Friedman, unpublished communication to Leo Harrington, 1977.

8. Mariagnese Giusto and Stephen G. Simpson, Located sets and reverse mathematics, Journal of Symbolic Logic (1999), 37 pages, accepted August 1998, to appear.

9. Leo Harrington, unpublished communication to Harvey Friedman, 1977.

10. Kostas Hatzikiriakou, WKL_{0} and Stone’s separation theorem for convex sets, Annals of Pure and Applied Logic 77 (1996), 245–249.

11. A. James Humphreys, On the Necessary Use of Strong Set Existence Axioms in Analysis and Functional Analysis, Ph.D. thesis, Pennsylvania State University, 1996, viii + 83 pages.

12. A. James Humphreys and Stephen G. Simpson, Separable Banach space theory needs strong set existence axioms, Transactions of the American Mathematical Society 348 (1996), 4231–4255.

13. J. Łoś and C. Ryll-Nardzewski, On the application of Tychonoff’s theorem in mathematical proofs, Fundamenta Mathematicae 38 (1951), 233–237.

14. George Metakides, Anil Nerode, and Richard A. Shore, On Bishop’s Hahn-Banach theorem, [15], 1985, pp. 85–91.

15. M. Rosenblatt (ed.), Errett Bishop, Reflections on Him and His Research, Contemporary Mathematics, American Mathematical Society, 1985, xvii + 91 pages.

16. Naoki Shioji and Kazuyuki Tanaka, Fixed point theory in weak second-order arithmetic, Annals of Pure and Applied Logic 47 (1990), 167–188.

17. W. Sieg (ed.), Logic and Computation, Contemporary Mathematics, American Mathematical Society, 1990, xiv + 297 pages.

18. Wilfried Sieg, Fragments of arithmetic, Annals of Pure and Applied Logic 28 (1985), 33–71.

19. Stephen G. Simpson, Partial realizations of Hilbert’s program, Journal of Symbolic Logic 53 (1988), 349–363.

20. , Subsystems of Second Order Arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, 1998, XIV + 445 pages.

  E-mail address: jimbo@math.psu.edu, simpson@math.psu.edu

The Pennsylvania State University