Cousin’s lemma in second-order arithmetic

Abstract

Cousin’s lemma is a compactness principle that naturally arises when studying the gauge integral, a generalisation of the Lebesgue integral. We study the axiomatic strength of Cousin’s lemma for various classes of functions, using Friedman and Simpson’s reverse mathematics in second-order arithmetic. We prove that, over $\mathsf{RCA}_{0}$:

(i)

Cousin’s lemma for continuous functions is equivalent to $\mathsf{WKL}_{0}$;

(ii)

Cousin’s lemma for Baire class 1 functions is equivalent to $\mathsf{ACA}_{0}$;

(iii)

Cousin’s lemma for Baire class 2 functions, or for Borel functions, is equivalent to $\mathsf{ATR}_{0}$ (modulo some induction).

1. Introduction

For real-valued functions, the most general version of the fundamental theorem of calculus relies on a generalisation of both the Lebesgue and (improper) Riemann integrals, called, among other names, the Denjoy integral Den12Gor94. This integral can integrate all derivatives, which the Riemann and Lebesgue integrals fail to do Gor94.

Denjoy Den12 first defined this integral in 1912, and shortly after, Luzin Luz12 and Perron Per14 gave equivalent characterisations. However, all these definitions were complex and highly non-constructive, making Denjoy’s integral impractical for applications Gor97. In 1957, Kurzweil Kur57 discovered an equivalent, “elementary” definition, in the style of the Riemann integral. This re-formulation is widely known as the gauge integral, or Henstock–Kurzweil integral.

For bounded functions with compact support, the gauge integral coincides with the Lebesgue integral, and hence the gauge integral gives a Riemann-like definition of the Lebesgue integral for a wide class of functions. We also remark that the gauge integral is suitable for integrating classes of highly discontinuous functions, and can be viewed as a mathematically rigorous formalisation of Feynman’s path integral Mul87.

A gauge is simply a function $\delta \colon [0,1]\to \mathbb{R}^+$ from the unit interval to the positive real numbers. A $\delta$-fine partition is a finite tagged partition $0=x_0 \le \xi _0 \le x_1 \le \xi _1 \le \dots \le x_n =1$ for which $\delta (\xi _i)\ge x_{i+1}-x_i$. This generalises the mesh size of a partition: a partition has mesh size $\le \delta$ if it is $\delta$-fine for the constant map with value $\delta$. The gauge integral is defined exactly like the Riemann integral, except that it allows arbitrary gauges rather than only constant ones: the integral $\int _0^1f\,dx$ is $K$ if for every $\varepsilon >0$ there is a gauge $\delta$ such that for every $\delta$-fine partition, the associated Riemann sum is within $\varepsilon$ of $K$. So every Riemann integrable function is gauge integrable, by choosing constant gauges. But also the function $x^{-1/2}$ is gauge integrable on $[0,1]$, by taking, given $\varepsilon >0$, a gauge that approaches 0 sufficiently rapidly so that the contribution of a leftmost interval to a Riemann sum cannot be unbounded. Similarly, Dirichlet’s function (the indicator function of the rationals) is integrable by taking $\delta (q_n) = \varepsilon 2^{-n}$, where ${\left\langle {q_n}\right\rangle }$ lists the rationals in $[0,1]$.

The key fact that enables the theory of the gauge integral is Cousin’s lemma Cou95, which states that for any gauge $\delta$, a $\delta$-fine partition exists. Without Cousin’s lemma, Kurzweil’s definition of the gauge integral would be vacuously satisfied by all functions and all values, trivialising the notion.

The gauge integral and Cousin’s lemma have had metamathematical exploration before; notably in the setting of descriptive set theory by Dougherty and Kechris DK91, Becker Bec92, and Walsh Wal17, for example. Recently, it was also explored in higher-order reverse mathematics by Normann and Sanders NS19NS20. These studies found that the gauge integral requires powerful axioms to prove. For example, working in third-order arithmetic, Normann and Sanders showed that Cousin’s lemma and the existence of the gauge integral were each equivalent to full second-order arithmetic.

The point is that Cousin’s lemma is a statement about all functions from $[0,1]$ to $\mathbb{R}^+$; no definability assumptions are involved. It is thus a statement which is not expressible in second-order arithmetic, which only allows quantification over real numbers (but not sets of real numbers). Second-order arithmetic is the study of countable mathematics, including objects which can be coded by countable objects, for instance separable metric spaces, continuous functions, and Borel sets.

Reverse mathematics of second-order arithmetic, as developed by H. Friedman and S. Simpson, is the project of understanding the proof-theoretic strength of the theorems of mathematics in terms of comprehension and induction strength required to prove them. What axioms of mathematics are actually required to prove a particular statement? The aim is to find optimal proofs, ones which require the least “amount” of axioms; and then show that these proofs are indeed the best that can be found, by finding a “reversal”: a proof of the axioms used, starting with the investigated theorem.

The main insight of the project of reverse mathematics is that almost all theorems of mainstream mathematics are equivalent to one of five axiomatic systems, and that these systems are linearly ordered by logical implication; see, for example, Sim09. One advantage of working within second-order arithmetic is that the proof-theoretic strength is often aligned with complexity, as defined using the tools of computability theory. Very informally speaking, a theorem which asserts the existence of complicated objects requires strong axioms to prove, and vice versa. This connection between computability and proof theory has resulted in a rich body of research.

It is thus natural to investigate the strength of Cousin’s lemma within second-order arithmetic, but in order to do so, we must restrict ourselves to classes of countably-coded functions. In this paper we consider Borel functions, and sub-classes of these.

Below we will observe that Cousin’s lemma is a form of a compactness principle. We would thus naturally start by looking at the system $\mathsf{WKL}_{0}$ (weak König’s lemma), which informally is understood to be equivalent to the compactness of the unit interval. But more specifically, it is equivalent to countable compactness, for example, to the statement that any countable open cover of $[0,1]$ has a finite subcover Sim09, Thm.IV.1.2. For continuous functions, Cousin’s lemma should be equivalent to its version for constant functions. Despite the fact that this equivalence seems to use a form of compactness, namely that continuous functions on $[0,1]$ obtain a minimum, we are able to show:

•

Cousin’s lemma for continuous gauges is equivalent to $\mathsf{WKL}_{0}$.

However, once we go up the hierarchy of Borel functions (as measured say by the Baire class of a function), it turns out that this form of uncountable compactness is significantly stronger:

•

Cousin’s lemma for Baire class 1 gauges is equivalent to $\mathsf{ACA}_{0}$.

•

Cousin’s lemma for all Borel gauges is provable in $\mathsf{ATR}_{0}+\Delta ^1_2$-induction.

•

Cousin’s lemma for Baire class 2 gauges implies $\mathsf{ATR}_{0}$.

We leave open the question of whether the extra induction is required. For background on reverse mathematics, and the definitions of these three subsystems of second-order arithmetic, see Sim09.

2. Cousin’s lemma and compactness

Let $\delta \colon [0,1]\to \mathbb{R}^+$ be a gauge. We can view $\delta$ as assigning, to each $x\in [0,1]$, the open interval $(x-\delta (x), x+\delta (x))$. Cousin’s lemma is very close to saying that this open cover of the unit interval has a finite subcover. It will be easier to work with this simplified version, rather than with tagged partitions, partly because this notion can be extended to other compact metric spaces; we will be working with Cantor space as well as the unit interval.

The metamathematical twist is that for our reversals, we will be working over $\mathsf{RCA}_{0}$. Some of the gauges that we will work with may be definable in some models of $\mathsf{RCA}_{0}$, but not have values in these models. For example, we will work with Baire class 1 functions, coded in a model by a sequence of continuous functions, where the values of the functions are Cauchy sequences, which need not converge. Nonetheless, relations such as $f(x)> r$ will be still definable in the model, and this will be enough to formalise Cousin’s lemma.

In light of this, it is important to note that a $\delta$-fine tagged partition $0= x_0 \le \xi _0 \le x_1 \le \xi _1 \le \dots \le x_{n-1}\le \xi _{n-1}\le x_n = 1$, with $x_{i+1}-x_i \le \delta (\xi _i)$, gives us not only the finite set of points $\xi _i$ giving us a cover, say $[0,1]\subseteq \bigcup _i (\xi _i-2\delta (\xi _i), \xi _i + 2\delta (\xi _i))$, but also the distances $x_{i+1}-x_i$, bounded by $\delta (\xi _i)$; and while $\delta (\xi _i)$ may not be in the model, the value $x_{i+1}-x_i$ is. Thus we define:

Definition 2.1.

Let $X$ be a compact metric space, and let $\delta \colon X\to \mathbb{R}^+$ be a gauge on $X$. A $\delta$-fine cover of $X$ is a finite set $P\subseteq X$ and a function $p\mapsto r_p$ from $P$ to $\mathbb{R}^+$ satisfying:

(i)

$X = \bigcup _{p\in P} B(p,r_p)$; and

(ii)

For all $p\in P$, $r_p \le \delta (p)$.

Assuming that $\delta$ is a function coded in the model for which the relations $\delta (x)\in B$ (for an open or closed ball $B$) are defined, we have:

Lemma 2.2 ($\mathsf{RCA}_{0}$).

Let $\delta \colon [0,1]\to \mathbb{R}^+$ be a gauge.

(a)

If there is a $\delta$-fine tagged partition then there is a $2\delta$-fine cover.

(b)

If there is a $\delta$-fine cover then there is a $2\delta$-fine tagged partition.

Proof.

For (a), suppose that $0=x_0 \le \xi _0 \le x_1 \le \xi _1 \le x_2 \le \dots \le \xi _{n-1} \le x_n=1$ is a $\delta$-fine partition: for all $i<n$, $\delta (\xi _i)\ge x_{i+1}-x_i$. Let $P = \{\xi _i\,:\, i<n\}$, and for $i< n$ let $r_{\xi _i} = 2(x_{i+1}-x_i)$. Then for all $i<n$, $r_{\xi _i} \le 2\delta (\xi _i)$ and trivially $[x_i,x_{i+1}]\subset (\xi _i-r_{\xi _i}, \xi _i + r_{\xi _i})$, so $P, \bar{r}_p$ is a $2\delta$-fine cover.

For (b), suppose that $P = \left\{ p_0 < p_1 < \dots < p_{n-1} \right\}$ equipped with $i\mapsto r_{p_i}$ is a $\delta$-fine cover. For brevity, for $p\in P$ let $U(p) = (p-r_p, p+r_p)$. By applying a reverse greedy algorithm, we may assume that $P$ is minimal in that for no distinct $p,q$ in $P$ do we have $U(p)\subseteq U(q)$. This implies that for all $i<n-1$, $p_{i+1}-p_i < r_{p_i} + r_{p_{i+1}}$; otherwise, a point between $p_i$ and $p_{i+1}$ would not be covered by $U(p_i)$ or by $U(p_{i+1})$; if $x\in U(p_j)$ then either $U(p_i)\subseteq U(p_j)$ (if $j<i$) or $U(p_{i+1})\subseteq U(p_j)$ (if $j>i+1$). So we choose

$$\begin{equation*} x_{i+1}\in (p_i,p_{i+1}) \cap U(p_i) \cap U(p_{i+1}), \end{equation*}$$

as well as $x_0 = 0$ and $x_n=1$; then $x_0 \le p_0 \le x_1 \le p_1 \le \dots$ is a $2\delta$-fine partition, as $[x_i,x_{i+1}]\subseteq U(p_i)$.

■

In light of Theorem 2.2, we state:

Definition 2.3 (Cousin’s lemma).

Let $X$ be a compact metric space, and let $\mathcal{K}$ be a class of functions. Cousin’s lemma for $\mathcal{K}$ on $X$ states that every $\delta \colon X\to \mathbb{R}^+$ in $\mathcal{K}$ has a $\delta$-fine cover.

If not stated otherwise, we work with $X = [0,1]$. For many of our arguments, though, it will be more convenient to work in Cantor space, under the metric $d(x,y) = 2^{-n}$ for the largest $n$ satisfying $x\,\upharpoonright \,n = y\,\upharpoonright \,n$. We state one connection between Cousin’s lemma on Cantor space and on the unit interval informally. Once we work with particular classes of functions, we will see that the following argument, in each particular case, can be made to hold in $\mathsf{RCA}_{0}$.

Lemma 2.4.

For reasonable classes $\mathcal{K}$ of functions, Cousin’s lemma for $\mathcal{K}$ on Cantor space implies Cousin’s lemma for $\mathcal{K}$ on the unit interval.

Proof.

We use the standard map $\varphi \colon 2^\omega \to [0,1]$ defined by

$$\begin{equation*} \varphi (x) = \sum x(n)2^{-n-1}. \end{equation*}$$

Then $\varphi$ is continuous and for all $x,y\in 2^\omega$,

$$\begin{equation*} |\varphi (x)-\varphi (y)| \le d(x,y). \end{equation*}$$

Hence, given $\delta \colon [0,1]\to \mathbb{R}^+$ in $\mathcal{K}$, we let $\hat{\delta }= \varphi \circ \delta$, which is a gauge on Cantor space. Suppose that $(\hat{P},\bar{r}_p)$ is a $\hat{\delta }$-fine cover. Let $P = \big \{ \varphi (p) \,:\, p\in \hat{P} \big \}$, and let $r_{\varphi (p)} = r_p$; this is a $\delta$-fine cover.

■

3. The Borel case

The “classical” proof of Cousin’s lemma can be carried out in the system of $\mathsf{ATR}_{0}+\Delta ^1_2$-induction. Note that while we can formalise Borel codes and functions in $\mathsf{RCA}_{0}$, in the system $\mathsf{ATR}_{0}$ we can prove that for every Borel function $f$ and every $x$, there is a point $f(x)$ (this follows from Sim09, Lem.V.3.7).

We need the following:

Lemma 3.1 ($\mathsf{ATR}_{0}+\Sigma ^1_1$-induction).

If $T\subseteq 2^{<\omega }$ is an infinite $\Pi ^1_1$-definable tree, then $T$ has a path.

Proof.

Let

$$\begin{equation*} S = \left\{ \sigma \in T \,:\, (\exists ^\infty \tau \succeq \sigma )\,\,\tau \in T \right\}. \end{equation*}$$

Then $S$ is $\Pi ^1_1$ (this uses $\Sigma ^1_1$-choice, which is provable in $\mathsf{ATR}_{0}$; see Sim09, VIII.3.21). By assumption, the empty sequence is in $S$; and every $\sigma \in S$ has a child $\sigma \hat{\,\,} i$ in $S$. So we can apply $\Pi ^1_1$-dependent choice on numbers, which is provable in $\mathsf{ATR}_{0}+\Sigma ^1_1$-induction Sim09, VIII.4.10.

■

Proposition 3.2 ($\mathsf{ATR}_{0}+\Delta ^1_2$-induction).

Cousin’s lemma holds for all Borel functions.

Proof.

The proof of Theorem 2.4 holds in $\mathsf{RCA}_{0}$ for the class $\mathcal{K}$ of Borel functions. Hence, we work with Cantor space. Let $\delta \colon 2^\omega \to \mathbb{R}^+$ be a Borel function. Let

$$\begin{equation*} G = \left\{ \sigma \in 2^{<\omega } \,:\, (\exists x\in [\sigma ])\,\,\, [\sigma ]\subseteq B(x,\delta (x)) \right\}, \end{equation*}$$

where $[\sigma ] = \left\{ x\in 2^{\omega } \,:\, \sigma \prec x \right\}$ is the clopen set determined by $\sigma$. Note that $[\sigma ]\subseteq B(x,\delta (x))$ if and only if $\delta (x)> 2^{-|\sigma |+1}$, so this is a Borel condition. However, the quantification over all $x\in [\sigma ]$ means that $G$ is $\Sigma ^1_1$ (relative to a code for $\delta$).

Now let

$$\begin{equation*} T = \left\{ \sigma \in 2^{<\omega } \,:\, (\forall \tau \preceq \sigma )\,\,\tau \notin G \right\}. \end{equation*}$$

Then $T$ is a $\Pi ^1_1$ tree. We claim that it is finite. If not, then by Theorem 3.1, $T$ has a path $y$. Let $n$ be sufficiently large so that $2^{-n}< \delta (y)$; this contradicts $y\,\upharpoonright \,n\in T$.

So we know that there is some $n$ which bounds the length of all the strings in $T$. By $\Delta ^1_2$ induction, $T$ exists, as a finite set: by induction on the length-lexicographic order of strings of length $\le n$, we show that for all $\tau \in 2^{\le n}$, $T\cap \{\sigma \,:\, \sigma \text{ precedes }\tau \}$ is a finite set in the model. The formula over which we induct is of the form $(\exists m\le 2^n)(\Pi ^1_1\,\,\,\&\,\,\, \Sigma ^1_1)$, so $\Delta ^1_2$-induction certainly suffices.

It follows that the set of leaves of $T$ exists (again as a finite set). By taking all immediate extensions of the leaves of $T$, we obtain a finite antichain $R\subseteq G$ of strings with $2^\omega = [R]^\preceq = \bigcup \left\{ [\sigma ] \,:\, \sigma \in R \right\}$.

Finally, there is a sequence ${\left\langle {x_{\sigma }\,:\, \sigma \in R}\right\rangle }$ witnessing that each $\sigma \in R$ is in $G$, i.e., $x_\sigma \in [\sigma ]$ and $[\sigma ]\subseteq B(x,\delta (x))$. This follows from $\Sigma ^1_1$-choice (or by $\Sigma ^1_1$-induction, as $R$ is finite). Letting $P = \left\{ x_\sigma \,:\, \sigma \in R \right\}$ and $r_{x_\sigma } = \delta (x_\sigma )$ gives a $\delta$-fine cover.

■

4. The continuous case

In this section we show that over the base system $\mathsf{RCA}_{0}$ of recursive comprehension, Cousin’s lemma for continuous functions is equivalent to weak König’s lemma $\mathsf{WKL}_{0}$. If $\delta$ is continuous then for all $x$, $\delta (x)$ exists, and so for a $\delta$-fine cover $(P,\bar{r}_p)$, we can always choose $r_p = \delta (p)$.

In one direction, the argument is quick.

Proposition 4.1 ($\mathsf{WKL}_{0}$).

Cousin’s lemma holds for continuous functions.

Proof.

Let $\delta \colon [0,1]\to \mathbb{R}^+$ be continuous. Weak König’s lemma implies that $\delta$ obtains a minimum $r$ Sim09, Th.IV.2.2, which must be positive. A partition of $[0,1]$ into intervals of length $2^{-n} < r$, and choosing any points as tags, gives a $\delta$-fine partition.

■

Note that the argument works for Cantor space as well.

In the other direction, we could argue directly by coding a $\Pi ^0_1$ class by an effectively closed subset of $[0,1]$; but the argument is combinatorially simpler by passing via the Heine-Borel theorem.

Theorem 4.2 ($\mathsf{RCA}_{0}$).

Cousin’s lemma for continuous functions implies $\mathsf{WKL}_{0}$.

Proof.

$\mathsf{WKL}_{0}$ is equivalent to the Heine-Borel theorem, which states the countable compactness of the unit interval: if ${\left\langle {U_n}\right\rangle }_{n\in \mathbb{N}}$ is a sequence of open intervals and $[0,1]\subseteq \bigcup _n U_n$, then there is finite subcover: there is some $N\in \mathbb{N}$ such that $[0,1]\subseteq \bigcup _{n<N} U_n$ (see Sim09, Lem IV.1.1).

Let ${\left\langle {U_n}\right\rangle }$ be such an open cover of $[0,1]$.

For $n\in \mathbb{N}$, let $d_n(x) = d(x,U_n^\complement )$ be the distance from a point $x$ to the complement of $U_n$. A code for $d_n$ as a continuous function can be obtained uniformly from the (end-points of) the interval $U_n$. Let

$$\begin{equation*} \delta (x) = \tfrac{1}{4}\sum _{n\in \mathbb{N}} 2^{-n}d_n(x). \end{equation*}$$

Then $\delta$ is a continuous function on $[0,1]$ (a code can be obtained effectively from the codes for the $d_n$’s). Since ${\left\langle {U_n}\right\rangle }$ covers the unit interval, for all $x$ there is some $n$ such that $d_n(x)>0$, so $\delta$ is positive on $[0,1]$.

We claim: for all $p\in [0,1]$ and $k\in \mathbb{N}$,

(*)

if $\delta (p)>2^{-k}$ then $(p-\delta (p),p+\delta (p))\subseteq \bigcup _{n\le k} U_n$.

Suppose not: then for all $n\le k$, $d_n(p)< \delta (p)$. As a result,

$$\begin{equation*} \delta (p) < \tfrac{1}{4} \sum _{n\le k}2^{-n}\delta (p) + \tfrac{1}{4}\sum _{n>k}2^{-n}d_n(p) \le \tfrac{1}{2} \delta (p) + \tfrac{1}{4} 2^{-k} < \delta (p), \end{equation*}$$

which is impossible; of course we use $d_n(p)\le 1$ for all $p$.

Now let $P\subset [0,1]$ be a $\delta$-fine cover (as mentioned we can choose $r_p = \delta (p)$). For each $p\in P$ find some $k$ with $\delta (p) > 2^{-k}$; by $\Sigma ^0_1$ bounding (see for example the proof of Sim09, Lem.IX.1.8), there is some $k$ such that for all $p\in P$, $\delta (p)> 2^{-k}$. Hence ${\left\langle {U_n}\right\rangle }_{n\le k}$ covers $[0,1]$, as required.

■

Remark 4.3.

The proof above may obscure the main intuition behind it. Consider a model in which $\mathsf{WKL}_{0}$ fails, witnessed by a “cover” ${\left\langle {U_n}\right\rangle }$ which is not really a cover: outside the model, there are points not covered by any $U_n$, but there are none such inside it. Let $C = [0,1]\setminus \bigcup _n U_n$. This is an effectively closed set (relative to an oracle in the model), and the rough idea is to let $\delta (x) = d(x,C)$. Then no $x\in C$ can be covered by a $\delta$-fine partition. The fact that for any finite $P$, $[0,1]$ is not covered by $\bigcup _{p\in P}(p-\delta (p),p+\delta (p))$ reflects down to the original model. The function $\delta$ is not really a gauge, but the model doesn’t see this, as it thinks that $C$ is empty.

The only difficulty is that $x\mapsto d(x,C)$, while continuous, is not computable relative to an oracle in the model; it is only lower semi-computable. In other words, the model does not contain a code for this function. The definition of $\delta$ in the proof above gives a continuous lower bound to $d(x,C)$ with a code in the model.

5. Baire class 1

A function is Baire class 1 if it is the pointwise limit of continuous functions. The Baire classes were introduced by Baire in his PhD thesis Bai99, as a natural generalisation of the continuous functions. One motivation for Baire functions is that many functions arising in analysis are not continuous, such as step functions Hea93, Walsh functions Wal23, or Dirichlet’s function Dir29. However, all such “natural” functions generally have low Baire class; for example, the derivative of any differentiable function is Baire class 1, as are functions arising from Fourier series KL90.

The Baire classes have previously been studied with respect to computability KT14PDD17. In particular, Kuyper and Terwijn showed that a real number $x$ is 1-generic if and only if every effective Baire 1 function is continuous at $x$ KT14. Indeed, the Turing jump function is in some sense a universal Baire class 1 function on Baire space.

In second-order arithmetic, we can formalise this notion as follows:

Definition 5.1.

A code for a Baire class 1 function is a sequence ${\left\langle {f_n}\right\rangle }$ of (codes of) continuous functions such that for all $x$, ${\left\langle {f_n(x)}\right\rangle }$ is a Cauchy sequence.

Note that we do not require the limit of this Cauchy sequence to exist; this would follow from arithmetic comprehension, but the definition still makes sense in $\mathsf{RCA}_{0}$. If ${\left\langle {f_n}\right\rangle }$ is a code in the model for a Baire class 1 function $f$, the relation “$f(x)\in B$” for an open or closed ball $B$ is definable, even if $f(x)$ is not an object in the model; for example, we say that $f(x)\in B(y,r)$ if for some $s<r$, for all but finitely many $n$, $f_n(x)\in B(y,s)$. Thus, it is meaningful to say that ${\left\langle {f_n}\right\rangle }$ is a code for a gauge.

In this section we show that Cousin’s lemma for Baire class 1 functions is equivalent to $\mathsf{ACA}_{0}$. We start with:

Lemma 5.2 ($\mathsf{RCA}_{0}$).

If $f\colon X\to Y$ is Baire class 1, then for open sets $U\subseteq Y$, $f^{-1}[U]$ is $F_\sigma$, uniformly.

Proof.

What this means: if $f = {\left\langle {f_n}\right\rangle }$ is a code for a Baire class 1 function, and ${\left\langle {U_n}\right\rangle }$ is a sequence of (codes of) open subsets of $Y$, then there is a sequence ${\left\langle {F_n}\right\rangle }$ of (codes of) $F_\sigma$ subsets of $X$ with

$$\begin{equation*} F_n = \left\{ x\in X \,:\, f(x)\in U_n \right\}, \end{equation*}$$

where again $f(x)\in U_n$ is a definable relation on $x$ and $n$.

The lemma is well-known. The $f$-preimage of a closed ball by a continuous function is closed, and an open ball is the union of closed balls. Hence

$$\begin{equation*} f(x)\in B(y,r) \,\,\Leftrightarrow \,\, (\exists s<r)(\exists n)(\forall m\ge n) \, d(f_n(x),q) \le s. \end{equation*}$$■

Remark 5.3.

In fact, classically, a function is Baire class 1 if and only if the pull back of open sets is $F_\sigma$. The other direction requires a little bit of work; it is like Shoenfield’s limit lemma, but for arbitrary spaces requires some topological considerations.

In second-order arithmetic, to make sense of the other direction, we would need to define codes for functions which pull back open sets to $F_\sigma$ sets, similar to how continuous functions are coded by collection of pairs indicating that the pull back of an open set contains some open set. For such a code, we can computably construct a Baire class 1 code for the function, but the argument seems to require $\Sigma ^0_2$ induction.

However, even stating the consistency of such a “Borel class 2” code seems complicated, as the containment relation between $F_\sigma$ sets is $\Pi ^1_1$ complete.

Proposition 5.4 ($\mathsf{ACA}_{0}$).

Cousin’s lemma holds for Baire class 1 gauges.

Proof.

The argument of Theorem 2.4 holds for Baire class 1 functions, and so it suffices to work in Cantor space. Let $\delta \colon 2^\omega \to \mathbb{R}^+$ be a Baire class 1 gauge. By $\mathsf{ACA}_{0}$, for all $x$, $\delta (x)$ exists.

Now the main two points are:

(i)

In $\mathsf{ACA}_{0}$, we can tell which $F_\sigma$ subsets of $2^\omega$ are empty;

(ii)

In $\mathsf{ACA}_{0}$, given a sequence ${\left\langle {H_n}\right\rangle }$ of non-empty $F_\sigma$ subsets of $2^\omega$, there is a choice sequence ${\left\langle {x_n}\right\rangle }$ so that $x_n\in H_n$ for all $n$.

The point is that whether a tree has a path is an arithmetic question, and so whether the union of a countable sequence of closed subsets of Cantor space is empty or not is also arithmetic. For (ii), using $\mathsf{ACA}_{0}$ we can obtain a sequence ${\left\langle {S_n}\right\rangle }$ of binary trees, each of which has a path, such that $[S_n]\subseteq H_n$ (where $[S_n]$ is the set of paths of $S_n$), and then apply $\mathsf{WKL}_{0}$ (or in $\mathsf{ACA}_{0}$, just take the leftmost path of each $S_n$).

We can therefore repeat the proof of Theorem 3.2. Let $\delta$ be a Baire class 1 gauge on Cantor space. We define the set $G$ and the tree $T$ in exactly the same way; $G$ and $T$ exist since they are arithmetically definable: $\delta (x) < 2^{-|\sigma |+1}$ is $\Sigma ^0_2$ by Theorem 5.2. The same argument shows that $T$ cannot have a path, and so by $\mathsf{WKL}_{0}$, $T$ is finite. As above, from $T$ we obtain a finite subset $R$ of $G$ which covers all of Cantor space. By (ii), we can find a sequence ${\left\langle {x_\sigma \,:\,\sigma \in R}\right\rangle }$ as required.

■

In the other direction:

Theorem 5.5 ($\mathsf{RCA}_{0}$).

Cousin’s lemma for Baire class 1 functions implies $\mathsf{ACA}_{0}$.

The idea of the proof is as follows. Suppose we have a Cauchy sequence ${\left\langle {z_n}\right\rangle }$ with no limit. The sequence of functions $x \mapsto {\left\lvert x-z_n \right\rvert }$ determines a Baire class 1 function $\delta$, which is a gauge since ${\left\langle {z_n}\right\rangle }$ has no limit. But there cannot be any $\delta$-fine partition, since no such partition $P$ can cover the gap where $\lim z_n$ should be. Here are the details.

Proof of Theorem 5.5.

If $\mathsf{ACA}_{0}$ fails then there is an increasing Cauchy sequence ${\left\langle {z_n}\right\rangle }_{n \in \mathbb{N}}$ of real numbers in the unit interval that has no limit Sim09, Thm.III.2.2. For each $n \in \mathbb{N}$, define

$$\begin{equation*} \delta _n(x) = {\left\lvert x-z_n \right\rvert }. \end{equation*}$$

This is a sequence of continuous functions. This sequence is pointwise Cauchy: for all $x$, $n$ and $m$,

$$\begin{equation*} {\left\lvert \delta _m(x) - \delta _n(x) \right\rvert }\ = \ \big |{\left\lvert x-z_m \right\rvert } - {\left\lvert x-z_n \right\rvert } \big | \ \leq \ {\left\lvert z_n - z_m \right\rvert }; \end{equation*}$$

so we use the fact that ${\left\langle {z_n}\right\rangle }$ is Cauchy. Note that in the “real world”, ${\left\langle {\delta _n}\right\rangle }$ converges uniformly to the continuous function $x\mapsto |x-z^*|$ where $z^* = \lim _n z_n$, but since $z^*$ does not exist in the model, this function does not have a code in the model. However in $\mathsf{RCA}_{0}$ we have just shown that ${\left\langle {\delta _n}\right\rangle }$ is a code for a Baire class 1 function, which we call $\delta$.

We claim that $\delta$ is a gauge. For all $x\in [0,1]$, since $x\ne \lim _n z_n$, and since ${\left\langle {z_n}\right\rangle }$ is Cauchy, there is some $\varepsilon >0$ such that for all but finitely many $n$, $|x-z_n|\ge \varepsilon$. Then $\delta (x) \ge \varepsilon$.

Now by Theorem 2.2 and Cousin’s lemma applied to the gauge $\tfrac{1}{2}\delta$, there is a $\delta$-fine tagged partition $0=x_0 \le \xi _0 \le x_1 \le \xi _1 \le x_2 \le \dots \le \xi _{n-1} \le x_n = 1$; recall that this means that $x_{i+1}-x_i \le \delta (x_i)$ for all $i<n$.

We derive a contradiction. By $\Sigma ^0_1$-induction, there is a least $i$ such that for all $n$, $z_n \le x_{i+1}$. Since ${\left\langle {z_n}\right\rangle }$ is increasing, for all but finitely many $n$, $z_n\in [x_{i},x_{i+1}]$. Since none of $x_{i}$, $\xi _{i}$ or $x_{i+1}$ are the limit of ${\left\langle {z_n}\right\rangle }$, there is some $\varepsilon >0$ such that one of the following happens:

•

for all but finitely many $n$, $z_n \in [x_{i}+\varepsilon ,\xi _{i}-\varepsilon ]$; or

•

for all but finitely many $n$, $z_n \in [\xi _{i}+\varepsilon ,x_{i+1}-\varepsilon ]$.

Without loss of generality, assume the former. Then for all but finitely many $n$,

$$\begin{equation*} \delta _n(\xi _{i}) = \xi _i - z_n \le (\xi _i -x_i)-\varepsilon \le (x_{i+1}-x_{i})-\varepsilon , \end{equation*}$$

whence $\delta (\xi _{i})< x_{i+1}-x_{i}$, contradicting our assumption. The argument in the other case is the same.

■

6. Higher Baire classes

Baire class 1 functions aren’t closed under taking pointwise limits. Indeed, by iterating the operation of taking pointwise limits, we obtain a transfinite hierarchy of functions, which exhausts all Borel functions.

In second-order arithmetic, recall that in $\mathsf{RCA}_{0}$, for a Baire class 1 function $f$, the relation $f(x)\in B$ for open or closed balls $B$ is definable even if $f(x)$ does not exist. We can therefore iterate. By (external) induction on standard $n$ we define:

Definition 6.1.

For each $n\ge 1$, a code for a Baire class $(n+1)$ function $f$ is a sequence ${\left\langle {f_n}\right\rangle }$ of codes for Baire class $n$ functions such that for all $x$, ${\left\langle {f_n(x)}\right\rangle }$ is Cauchy, in the sense that for all $\varepsilon >0$ there is an open ball $B$ of radius $<\varepsilon$ such that for all but finitely many $n$, $f_n(x)\in B$.

If ${\left\langle {f_n}\right\rangle }$ is such a code, then for any open ball $B = B(y,r)$, we say that $f(x)\in B$ if for some $s<r$, for all but finitely many $n$, $f_n(x)\in B(y,s)$.

Of course by taking constant sequences, we see that every Baire class $n$ function is also Baire class $n+1$, so the classes are increasing.

$\mathsf{ACA}_{0}$ implies, for each $n$, that if $f$ is Baire class $n$ then $f(x)$ exists for all $x$. Similarly to Theorem 5.2, the inverse images of open sets by Baire class $n$ functions are $\Sigma ^0_{1+n}$. We can further extend the definition to Baire class $\alpha$ functions for ordinals $\alpha$; a code in this case is an $\alpha$-ranked well-founded tree, where each non-leaf has full splitting, the leaves are labeled by continuous functions, and each non-leaf node represents the pointwise limit of the functions represented by its children. The relation $f(x)\in U$ is then defined by transfinite recursion on the rank of a node, and so it makes most sense to use $\mathsf{ATR}_{0}$ as a base system for this kind of development; we do not pursue it here. We remark that $\mathsf{ATR}_{0}$ implies that every Borel function is Baire class $\alpha$ for some $\alpha$.⁠¹

¹

This follows from the fact that every well-founded tree is ranked; see Hir00.

✖

Now the proof of Theorem 5.4 cannot be replicated for Baire class $n$ functions for any for $n>1$. While $\mathsf{ACA}_{0}$ suffices to determine if a given $\Sigma ^0_2$ subset of Cantor space is empty or not, it is $\Pi ^1_1$-complete to determine whether a given $\Pi ^0_2$ set is empty.⁠² And indeed we show that Cousin’s lemma for Baire class 2 functions is much stronger than $\mathsf{ACA}_{0}$: it implies $\mathsf{ATR}_{0}$.

²

Every $\Sigma ^1_1$ set is the projection of a $\Pi ^0_2$ set in Cantor space (see for example Sac90, Thm.I.1.5), and the question of whether a $\Sigma ^1_1$ set is empty or not is equivalent to a question about well-foundedness of a tree, which is $\Pi ^1_1$-complete.

✖

It would again be more convenient to work in Cantor space, and so we need a converse of Theorem 2.4.

Lemma 6.2 ($\mathsf{RCA}_{0}$).

Cousin’s lemma for Baire class 2 functions on the unit interval implies Cousin’s lemma for Baire class 2 functions on Cantor space.

Of course there is nothing special for the case $n=2$, the lemma holds for all Baire classes.

Proof.

We use the standard embedding of Cantor space into the unit interval: for $x\in 2^\omega$ let

$$\begin{equation*} \psi (x) = \sum _n 2x(n)3^{-n-1}, \end{equation*}$$

and let $C = \psi [2^\omega ]$ be the ternary Cantor set. We use the following facts: $\psi$ is continuous; the function $z\mapsto d(z,C)$ is computable on $[0,1]$; and: for $x,y\in 2^\omega$, if $d(x,y)= 2^{-n}$ then $|\psi (x)-\psi (y)| \ge 3^{-n}$, i.e.,

$$\begin{equation*} |\psi (x)-\psi (y)| \ge 3^{\log _2 d(x,y)} \end{equation*}$$

for all $x,y\in 2^\omega$.

Let $\delta$ be a Baire class 2 gauge on Cantor space. Define $\hat{\delta }\colon [0,1]\to \mathbb{R}$ by letting, for $z\in [0,1]$,

$$\begin{equation*} \hat{\delta }(z) = \begin{cases} 3^{\log _2 \psi ^{-1}(z)}, & \text{if $z\in C$; and} \\ d(x,C), & \text{otherwise.} \end{cases} \end{equation*}$$

Then $\hat{\delta }$ is positive on $[0,1]$, and it is Baire class 2; we use the fact that $1_C$ (the characteristic function of $C$) is Baire class 1, indeed with a very nice, uniformly computable approximation ${\left\langle {g_n}\right\rangle }$ of piecewise linear functions with $g_n(z)=1$ for all $n$ when $z\in C$, and $g_n(z)=0$ for all but finitely many $n$ when $z\notin C$.

Suppose that $(P,\bar{r}_p)$ is a $\hat{\delta }$-fine cover. Define $Q = \left\{ x\in 2^\omega \,:\, \psi (x)\in P \right\}$ and for $x\in Q$ let $s_x = 2^{\log _3 r_{\psi (x)}}$. Then $(Q,\bar{s}_x)$ is a $\delta$-fine cover. The main point is that $z\in C$ cannot be covered by any $p\in P\setminus Q$, as for such $p$ we have $\delta (p) = d(p,C) \le |p-z|$.

■

Before we give the reversal, we motivate our technique by showing something weaker: that $\mathsf{ACA}_{0}$ does not imply Cousin’s lemma for Baire class 2 functions. We will show that every $\omega$-model of $\mathsf{RCA}_{0}+$Cousin’s lemma for Baire class 2 functions must contain $0^{(\omega )}$ (in fact $0^{(\alpha )}$ for any computable ordinal $\alpha$), in particular Cousin’s lemma for Baire class 2 functions fails in the model consisting of the arithmetic sets.

We review some definitions. The Turing jump $x'$ of $x\in 2^\omega$ is the complete $\Sigma ^0_1(x)$ set, identified with an element of $2^\omega$. As mentioned above, the function $x\mapsto x'$ is Baire class 1, but more importantly, its graph (the relation $y = x'$) is $\Pi ^0_2$. We will use the following well-known fact, which is provable in $\mathsf{ACA}_{0}$:

Lemma 6.3 ($\mathsf{ACA}_{0}$).

Let $f\colon 2^\omega \to \mathbb{N}$ be a function. The following are equivalent:

(1)

$f$ is $\Delta ^0_3$-definable;

(2)

There is a computable function $\varphi \colon 2^\omega \to \mathbb{N}$ such that for all $x$, $f(x) = \varphi (x'')$;

(3)

$f$ is effective Baire class 2.

Proof.

This is a double application of Shoenfield’s limit lemma and Post’s hierarchy theorem: a function $f\colon \mathbb{N}\to \mathbb{N}$ is $\Delta ^0_3$-definable if and only if it is $\emptyset ''$-computable if and only if $f = \lim _s\lim _t g(-,s,t)$ for some computable $g\colon \mathbb{N}^3\to \mathbb{N}$ (see for example Soa87, Lem.III.3.3;Thm.IV.2.2). The lemma now follows from a uniform relativisation to oracles $x\in 2^\omega$.

■

As a result we get:

Lemma 6.4 ($\mathsf{RCA}_{0}$).

Suppose that $f\colon 2^\omega \to \mathbb{N}$ is $\Delta ^0_3$. Suppose that Cousin’s lemma for Baire class 2 functions holds. Then there is a finite $P\subset 2^\omega$ such that

$$\begin{equation*} 2^\omega = \bigcup _{p\in P} [p\,\upharpoonright \,f(p)]. \end{equation*}$$

Proof.

Define $\delta (x) = 2^{-f(x)}$. Then $\delta$ is $\Delta ^0_3$. By Theorem 6.3 (note that we already know that Cousin’s lemma for Baire class 2 functions implies $\mathsf{ACA}_{0}$), $\delta$ is a Baire class 2 gauge. A $\delta$-fine cover $P\subset 2^\omega$ is as required.

■

Recall the definition of a transfinite iteration of the Turing jump. Suppose that $\alpha$ is a linear ordering of a subset of $\mathbb{N}$, which will usually be well-founded. An iteration of the Turing jump along $\alpha$ is a set $H\subseteq \alpha \times \mathbb{N}$ satisfying, for all $\beta <\alpha$,

$$\begin{equation*} H^{[\beta ]} = \left(H^{[<\beta ]} \right)', \end{equation*}$$

where $H^{[\beta ]} = \left\{ k \,:\, (\beta ,k)\in H \right\}$ and $H^{[<\beta ]} = \left\{ (\gamma ,k)\in H \,:\, \gamma <\beta \right\}$. Again note that we view the domain of $\alpha$ as a subset of $\mathbb{N}$, so both $H^{[\beta ]}$ and $H^{[<\beta ]}$ are identified with elements of Cantor space, and so taking the Turing jump makes sense.

If $\alpha$ is indeed an ordinal (is well-founded), then $\mathsf{ACA}_{0}$ implies there is at most one iteration of the Turing jump along $\alpha$, and if $H$ is such, we write $H = 0^{(\alpha )}$. When this is relativised to an oracle $x$, we write $H = x^{(\alpha )}$. The relation “$H$ is an iteration of the Turing jump along $\alpha$” is $\Pi ^0_2$. $\mathsf{ATR}_{0}$ is equivalent to the statement that for all ordinals $\alpha$ and all $x$, $x^{(\alpha )}$ exists Sim09, Thm.VIII.3.15.

Now let $\mathcal{M}$ be an $\omega$-model of $\mathsf{ACA}_{0}$, let $\alpha$ be a computable ordinal, and suppose that $0^{(\omega )}\notin \mathcal{M}$; we show that Cousin’s lemma for Baire class 2 functions fails in $\mathcal{M}$. Let $X\in 2^\omega$. If $X\ne 0^{(\omega )}$, there is some $n<\omega$ such that

$$\begin{equation*} X^{[n]} \ne \big (X^{[<n]}\big )'; \end{equation*}$$

let $n(X)$ be the least such $n$. The function $X\mapsto n(X)$ (as well as its domain) is $\Delta ^0_3$. Further, for such $X$, we let $k(X)$ be the least $k$ such that

$$\begin{equation*} X^{[n(X)]}(k) \ne \big (X^{[<n(X)]}\big )'(k); \end{equation*}$$

the function $X\mapsto k(X)$ is $\Delta ^0_3$ as well. By their definition, for all $X\ne 0^{(\omega )}$,

$$\begin{equation*} X(n(X),k(X))\ne 0^{(\omega )}(n(X),k(X)), \end{equation*}$$

as $X^{[<n(X)]} = (0^{(\omega )})^{[<n(X)]}$. Hence, we let $f(X) = {\left\langle {n(X),k(X)}\right\rangle }+1$; for all $X\ne 0^{(\omega )}$,

$$\begin{equation*} 0^{(\omega )} \notin [X\,\upharpoonright \,f(X)]. \end{equation*}$$

Since $0^{(\omega )}\notin \mathcal{M}$, $f$ is total on $2^\omega \cap \mathcal{M}$, and since $\mathcal{M}$ is an $\omega$-model, the same $\Delta ^0_3$ definition holds in $\mathcal{M}$, so $\mathcal{M}$ believes that $f$ is a Baire class 2 gauge on Cantor space. Let $P\subset 2^\omega \cap \mathcal{M}$ be finite. Since $0^{(\omega )}\notin P$, we have

$$\begin{equation*} 0^{(\omega )} \notin \bigcup _{X\in P} [X\,\upharpoonright \,f(X)], \end{equation*}$$

and so

$$\begin{equation*} 2^\omega \ne \bigcup _{X\in P} [X\,\upharpoonright \,f(X)]. \end{equation*}$$

But since $P$ is finite, the latter fact is absolute for $\mathcal{M}$ (the set $\bigcup _{X\in P} [X\,\upharpoonright \,f(X)]$ is a clopen set and so its complement is a non-empty clopen set; $\mathcal{M}$ contains an element of any non-empty clopen set). Hence Theorem 6.4 fails in $\mathcal{M}$.

Exactly the same argument shows that for any computable ordinal $\alpha$, $0^{(\alpha )}$ is an element of every $\omega$-model of Cousin’s lemma for Baire class 2 functions. The more general argument below builds on this technique. In the meantime, we note that this argument gives a purely computability-theoretic result:

Theorem 6.5.

For every computable ordinal $\alpha$, there is an effective Baire class 2 gauge $\delta$ such that every $\delta$-fine partition must contain $0^{(\alpha )}$.

Proof.

Extend the function $f$ above to a function on all of $2^\omega$ by defining $f(0^{(\alpha )})=0$, and transform to a gauge as in the proof of Theorem 6.4. This is still a $\Delta ^0_3$-definable function since the relation $X = 0^{(\alpha )}$ is $\Delta ^0_3$ (indeed it is $\Pi ^0_2$).

■

Theorem 6.6 ($\mathsf{RCA}_{0}$).

Cousin’s lemma for Baire class 2 functions implies $\mathsf{ATR}_{0}$.

Proof.

By Theorem 5.5, we may work in $\mathsf{ACA}_{0}$.

Let $\alpha$ be an ordinal and let $x\in 2^\omega$; and suppose that $x^{(\alpha )}$ does not exist, i.e., there is no iteration of the Turing jump (relativised to $x$) along $\alpha$. For simplicity of notation, suppose $x = 0$.

Let

$$\begin{equation*} \mathcal{I} = \left\{ \beta <\alpha \,:\, 0^{(\beta )}\,\text{exists} \right\}. \end{equation*}$$

The set $\mathcal{I}$ does not exist (as a set in the model), but is definable. Again note that since $\mathsf{ACA}_{0}$ holds, for all $\beta \in \mathcal{I}$ there is exactly one iteration of the Turing jump along $\beta$, which is the set we call $0^{(\beta )}$. We observe that $\mathcal{I}$ cannot have a greatest element; if $0^{\beta }$ exists then by $\mathsf{ACA}_{0}$, so does $0^{(\beta +1)}$.

For any $X\in 2^\omega$, since $X$ is not an iteration of the Turing jump along $\alpha$, by arithmetic comprehension, there is a least $\beta <\alpha$ such that $X^{[\beta ]}\ne (X^{[<\beta ]})'$; call this $\beta (X)$. Then $X^{[<\beta (X)]} = 0^{(\beta (X))}$, so $\beta (X)\in \mathcal{I}$. Similar to the argument above, we also let $k(X)$ be the least $k$ such that

$$\begin{equation*} X^{[\beta (X)]}(k) \ne \big (X^{[<\beta (X)]}\big )'(k). \end{equation*}$$

From $k(X)$ and $\beta (X)$ we can compute some $f(X)\in \mathbb{N}$ such that for all $\gamma > \beta (X)$ in $\mathcal{I}$,

$$\begin{equation*} 0^{(\gamma )} \notin [X\,\upharpoonright \,f(X)]. \end{equation*}$$

Let $P\subset 2^\omega$ be finite. Then

$$\begin{equation*} \beta ^* = \max \{ \beta (X)\,:\, X\in P\} \end{equation*}$$

is an element of $\mathcal{I}$. Since $\mathcal{I}$ does not have a last element, take any $\gamma >\beta ^*$ in $\mathcal{I}$; then

$$\begin{equation*} 0^{(\gamma )} \notin \bigcup _{X\in P} [X\,\upharpoonright \,f(P)]. \end{equation*}$$

Therefore, Theorem 6.4 fails, and so Cousin’s lemma for Baire class 2 functions does not hold.

■