Separation and $\mathsf{ACA}_0$

Theorem 5.1   The following statements are pairwise equivalent over $\mathsf{RCA}_0$.

1.

$\mathsf{ACA}_0$.

2.

SEP3, the third separation theorem.

3.

Let A and B be disjoint, bounded, separably closed, convex sets in R². Assume also that A is compact. Then A and B can be separated. 

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

Trivially SEP3 implies statement 5.1.3.

It remains to prove that statement 5.1.3 implies $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$. Reasoning in $\mathsf{RCA}_0$, assume that $\mathsf{ACA}_0$ fails. Then there exists a bounded increasing sequence of rational numbers a_n, $n\in{\mathbf{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]\times\{0\}$, and let B be the separably closed convex hull of the points (a_n,1/n), $n\ge1$. Note that A and B are bounded, separably closed, convex sets in R². 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\ge1$. Thus B is the separable closure of S.

We claim: for all $n\ge1$ there exists $\varepsilon_n>0$ such that for all $(x,y)\in S$, if x<a_n then $y>\varepsilon_n$. To see this, note that

$$(x,y)\,\,\,=\,\,\,\sum_{i=1}^k\, q_i\left(a_{n_i},\frac1{n_i}\right)$$

where $\sum_{i=0}^k q_i=1$, q_i>0, $q_i\in{\mathbf{Q}}$. Thus $x=\sum_{i=0}^k q_i a_{n_i}$. Putting $r=\sum\{q_i\mid n_i\le n\}$ we have

$$a_n\,\,>\,\,\,x\,\,\,\ge\,\,\,ra_1+(1-r)a_{n+1}\,\,,$$

hence

$$r\,\,\,>\,\,\,\frac{a_{n+1}-a_n}{a_{n+1}-a_1}\,\,\,>\,\,\,0\,\,.$$

Furthermore

$$y\,\,\,=\,\,\,\sum_{i=0}^k\,q_i\,\frac1{n_i}\,\,\,\ge\,\,\, r\cdot\frac1n\,\,.$$

Therefore we put

$$\varepsilon_n\,\,\,=\,\,\,\frac{a_{n+1}-a_n}{a_{n+1}-a_1}\cdot\frac1n$$

and our claim is proved.

Now if $(x,0)\in A\cap B$, we clearly have x<a_n for some n. Since S is dense in B, let $(x',y')\in S$ be such that

$$\vert x-x'\vert\,,\,\vert y'\vert\,\,<\,\,\min(a_{n+1}-a_n,\varepsilon_{n+1})\,\,.$$

Then x'<a_n+1 and $y'<\varepsilon_{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 $\mathsf{ACA}_0$ is equivalent over $\mathsf{RCA}_0$ to the following even weaker-sounding statement: if A and B are disjoint, bounded, separably closed, convex sets in R², and if A is compact, then there exists an open set U such that $A\subseteq U$ and $U\cap B=\emptyset$.

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 (non-geometrical) 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 $\mathsf{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 $\mathsf{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.