Introduction

Let A and B be convex sets in a Banach space X. We say that Aand B are separated if there is a bounded linear functional $F:X\to{\mathbf{R}}$ and a real number $\alpha$ such that $F(x)<\alpha$ for all $x\in A$, and $F(x)\ge\alpha$ for all $x\in B$. We say that A and B are strictly separated if in addition $F(x)>\alpha$ for all $x\in 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 $\mathsf{ACA}_0$, $\mathsf{RCA}_0$, and above all $\mathsf{WKL}_0$. $\mathsf{ACA}_0$ is the system with arithmetical comprehension and arithmetical induction; it is conservative over first-order Peano arithmetic. $\mathsf{RCA}_0$ is the much weaker system with only $\Delta^0_1$ comprehension and $\Sigma^0_1$induction; it may be viewed as a formalized version of recursive mathematics. $\mathsf{WKL}_0$ consists of $\mathsf{RCA}_0$ plus an additional set existence axiom known as Weak König's Lemma. $\mathsf{WKL}_0$ and $\mathsf{RCA}_0$ are conservative over arithmetic with $\Sigma^0_1$ induction [9,18,20], hence much weaker than $\mathsf{ACA}_0$ in terms of proof-theoretic strength. Moreover, $\mathsf{WKL}_0$ and $\mathsf{RCA}_0$ are conservative over primitive recursive arithmetic for $\Pi^0_2$sentences [7,18,20]. The foundational significance of this result is that any mathematical theorem provable in $\mathsf{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 $\mathsf{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 $\mathsf{WKL}_0$ with respect to Hilbert's program of finitistic reductionism [19].

As a byproduct of our work on separation theorems in $\mathsf{WKL}_0$, we present new proofs of the closely related Hahn-Banach and extended Hahn-Banach theorems in $\mathsf{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 $\mathsf{WKL}_0$ over $\mathsf{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 $\mathsf{ACA}_0$ over $\mathsf{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 os/Ryll-Nardzewski [13]) but is apparently not widely known. We thank Ward Henson for bringing [13] to our attention.