Big in Reverse Mathematics: measure and category

TL;DR

This paper explores the logical strength of measure and category theorems in higher-order Reverse Mathematics, revealing many are outside the standard classification and analyzing conditions that restore their provability.

Contribution

It identifies numerous theorems related to measure and category that lie outside the Big Five of Reverse Mathematics and examines conditions that make them provable within the standard framework.

Findings

Many measure and category theorems are outside the Big Five classification.

Restrictions like Baire 1 and quasi-continuity make these theorems provable in the Big Five.

Proofs of equivalences for measure and category theorems are surprisingly similar.

Abstract

The smooth development of large parts of mathematics hinges on the idea that some sets are `small' or `negligible' and can therefore be ignored for a given purpose. The perhaps most famous smallness notion, namely `measure zero', originated with Lebesgue, while a second smallness notion, namely `meagre' or `first category', originated with Baire around the same time. The associated Baire category theorem is a central result governing the properties of meagre (and related) sets, while the same holds for Tao's pigeonhole principle for measure spaes and measure zero sets. In this paper, we study these theorems in Kohlenbach's higher-order Reverse Mathematics, identifying a considerable number of equivalent theorems. The latter involve most basic properties of semi-continuous and pointwise discontinuous functions, Blumberg's theorem, Riemann integration, and Volterra's early work circa 1881. All the aforementioned theorems fall (far) outside of the Big Five of Reverse Mathematics, and we investigate natural restrictions like Baire 1 and quasi-continuity that make these theorems provable again in the Big Five (or similar). Finally, despite the fundamental differences between measure and category, the proofs of our equivalences turn out to be similar.

Equations

$$\{x\in [0,1]:F\text{ is differentiable at x with derivative }f(x)\}$$

$$T(x):=\{\begin{array}{ll}0& \text{if }x\in \mathbb{R}\setminus \mathbb{Q}\\ \frac{1}{q}& \text{if x=qp and p,q are co-prime}\end{array}.$$

$$(\forall x\in D,\epsilon >0)(\exists \delta >0)\underline{(\forall y\in D)}(|x-y|<\delta \to |f(x)-f(y)|<\epsilon )),$$

$$(\exists\varphi^{2}\leq_{2}1)(\forall f^{1})\big{[}(\exists n^{0})(f(n)=0)\leftrightarrow\varphi(f)=0\big{]}.$$

$$\displaystyle(\exists\mu^{2})(\forall f^{1})\big{[}(\exists n)(f(n)=0)\rightarrow[f(\mu(f))=0$$

$$\displaystyle\wedge[(\forall n)(f(n)\neq 0)\rightarrow\mu(f)=0]\big{]}.$$

$$(\exists\SS^{2}\leq_{2}1)(\forall f^{1})\big{[}(\exists g^{1})(\forall n^{0})(f(\overline{g}n)=0)\leftrightarrow\SS(f)=0\big{]}.$$

$$(\exists E^{3}\leq_{3}1)(\forall Y^{2})\big{[}(\exists f^{1})(Y(f)=0)\leftrightarrow E(Y)=0\big{]},$$

$$(\forall Y:[0,1]\to \mathbb{N})(\exists x,y\in [0,1])(x{\ne }_{\mathbb{R}}y\wedge Y(x){=}_{\mathbb{N}}Y(y)),$$

$$(w(m)\in 2^{\mathbb{N}}\wedge Y(w(m),m)=0)\leftrightarrow (\exists f\in 2^{\mathbb{N}})(Y(f,m)=0).$$

$$(\forall x,y\in A)(Y(x){=}_{0}Y(y)\to x{=}_{\mathbb{R}}y).$$

$$f(x)={\lim }_{m_1\to \infty }{\lim }_{m_2\to \infty }\dots {\lim }_{m_n\to \infty }{f}_{m_1,\dots ,m_n}(x).$$

$$D_k:=\{x\in [0,1]:|f(x)-f(x+)|>\frac{1}{2^k}\vee |f(x)-f(x-)|>\frac{1}{2^k}\}.$$

$$f$$

$$D_k:=\{x\in [0,1]:{\text{osc}}_f(x)\ge \frac{1}{2^k}\}\text{ for all k∈N.}$$

$$h(x):=\{\begin{array}{ll}0& x\notin {\cup }_{m\in \mathbb{N}}{X}_m\\ \frac{1}{2^{n+1}}& x\in X_n\text{ and n is the least such number}\end{array}.$$

$$(\exists l\in \mathbb{N})(\forall N\in \mathbb{N})(\exists z\in B(x_0,\frac{1}{2^N}))(f(z)\ge f(x_0)+\frac{1}{2^l}).$$

$$(\exists l\in \mathbb{N})(\forall N\in \mathbb{N})\underline{(\exists r\in B(x,\frac{1}{2^N})\cap \mathbb{Q})}(f(r)\ge f(x_0)+\frac{1}{2^l}),$$

$$f(x)\le q\wedge (\forall N\in \mathbb{N})(\exists z\in B(x,\frac{1}{2^N}))(f(z)>q).$$

$$f(x)\le q\wedge (\forall N\in \mathbb{N})\underline{(\exists r\in B(x,\frac{1}{2^N})\cap \mathbb{Q})}(f(r)>q),$$

$$(\exists l\in \mathbb{N})(\forall k\in \mathbb{N})(\exists y\in B(x,\frac{1}{2^k})(f(y)\ge f(x)+\frac{1}{2^l}),$$

$$(\exists l\in \mathbb{N})(\forall k\in \mathbb{N})\underline{(\exists r\in B(x,\frac{1}{2^k})\cap \mathbb{Q})}(f(r)\ge f(x)+\frac{1}{2^l}),$$

$$(\forall k\in \mathbb{N})(\forall y\in B(x,\Psi (x,k)))(f(y)<f(x)+\frac{1}{2^k}).$$

$$f(x)>q\vee (\exists N\in \mathbb{N})(\forall r\in B(x,\frac{1}{2^N})\cap \mathbb{Q})(f(r)\le q).$$

$$f(x)>q\leftrightarrow (\exists N\in \mathbb{N})(q<{\inf }_{y\in B(x,\frac{1}{2^N})}f(y)),$$

$$C_n:=\{x\in [0,1]:(\forall m\in \mathbb{N})(|f_m(x)|\le n)\}.$$

$$(\exists N\in \mathbb{N})(\forall y\in B(x,\frac{1}{2^N}))(y\in D_{m,n}),$$

$$\hat{h}(x):=\{\begin{array}{ll}0& x\notin {\cup }_{n\in \mathbb{N}}{X}_n\\ n& x\in X_n\text{ and n∈N is the least such number}\end{array},$$

$$|e(y)-e(z)|\le |e(y)-e^y|+|e^y-e^z|+|e(z)-e^z|,$$

$$(\exists N\in \mathbb{N})(\forall q,r\in B(x,\frac{1}{2^N})\cap \mathbb{Q})(|f(q)-f(r)|\le \frac{1}{2^m}).$$

$$(\exists M\in \mathbb{N})(\forall w,z\in B(x,\frac{1}{2^M}))(|f(w)-f(z)|\le \frac{1}{2^m}),$$

Full text

1. Introduction

In nutshell, we study basic theorems concerning measure and category in Kohlenbach’s higher-order Reverse Mathematics (RM for short; see Section 1.3.1). We obtain numerous equivalences for the Baire category theorem and Tao’s pigeonhole principle for measure spaces, involving basic properties of semi-continuous, Riemann integrable, and pointwise discontinuous functions, where the first notion is fairly tame and the latter is wild, as discussed in Remark 2.20. An overview of our results is in Section 1.1 while preliminaries may be found in Section 1.3. We discuss Volterra’s early work from 1881 in Section 1.2, as it pertains to this paper.

1.1. Summary and background

We provide some background for and an overview of the results to be proved in Sections 2 and 3.

First of all, it is a commonplace that the smooth development of large parts of mathematics hinges on the idea that some sets are ‘small’ or ‘negligible’ and can therefore be ignored for a given purpose. While some calculus students may not (ever) realise it, even introductory calculus depends (perhaps indirectly) on a specific smallness notion, in light of the Vitali-Lebesgue theorem as follows.

Theorem 1.1** (Vitali-Lebesgue).**

A function on the unit interval is Riemann integrable if and only if it is continuous almost everywhere and bounded.

The associated smallness notion ‘measure zero’ originated with Lebesgue ([lebesborn]) and is perhaps the most famous111A less famous smallness notion is porosity (see [poro]), which we may study in a future paper. such notion. A second smallness notion, namely ‘meagre’ or ‘first category’, originated with Baire around the same time ([beren2]). Tao discusses the connection between these two notions in [taoeps]*§1.7. As pointed out by Smith in [snutg], the conflation of measure and category led to a number of incorrect results by Hankel ([hankelwoot]) and others regarding the Riemann integral. In this context, Smith introduced the famous Cantor set some years before Cantor did ([snutg]).

Secondly, the Baire category theorem is a central result governing the properties of meagre sets (see [taokejes]§3.2), while Tao’s pigeonhole principle for measure spaces plays the same role for measure zero sets ([taoeps]§1.7). We shall use the obvious abbreviations $\textup{{BCT}}_{[0,1]}$ and $\textup{{PHP}}_{[0,1]}$ in the below. By Theorems 2.2 and 3.6, the third-order principles $\textup{{BCT}}_{[0,1]}$ and $\textup{{PHP}}_{[0,1]}$ are hard to prove in terms of conventional222The system ${\textsf{{Z}}}_{2}^{\omega}$ from Section 1.3.2 is a conservative extension of ${\textsf{{Z}}}_{2}$ via third-order comprehension functionals $\SS_{k}^{2}$ that decide $\Pi_{k}^{1}$-formulas. By [dagsamVII]*Theorem 6.16 or [dagsamX]*Theorem 3.4, ${\textsf{{Z}}}_{2}^{\omega}+\textup{{QF-AC}}^{0,1}$ cannot prove $\textup{{BCT}}_{[0,1]}$; a similar result is proved in Theorem 2.2. comprehension. Similar hardness results (see [dagsamVII]) exist for Kleene’s computability theory based on S1-S9 ([longmann]); moreover, we have established a large number of (S1-S9) computationally equivalent principles for $\textup{{BCT}}_{[0,1]}$ in [samcsl23]. By contrast, $\textup{{BCT}}_{[0,1]}$ and $\textup{{PHP}}_{[0,1]}$ restricted to second-order codes for closed sets (see [simpson2]*II.5.6) are provable in relatively weak systems by [simpson2]*II.5.8 and Theorem 3.6.

Thirdly, in light of the above, the RM-study of $\textup{{BCT}}_{[0,1]}$ and $\textup{{PHP}}_{[0,1]}$ is an important and natural enterprise, and constitutes the topic of this paper. In particular, we show in Section 2 that $\textup{{BCT}}_{[0,1]}$ is equivalent to the well-known principles listed below, working in higher-order RM (see Section 1.3.1). The notion of semi-continuity goes back to Baire ([beren]) while the notion of pointwise discontinuity goes back to Hankel ([hankelwoot]) and is equivalent to cliquishness (see Section 1.3.3 for definitions).

1. (i)

For upper semi-continuous (usco for short) $f:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous (or: quasi-continuous, or: Darboux). 2. (ii)

For Baire $1^{*}$ $f:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous. 3. (iii)

For fragmented $f:[0,1]\rightarrow{\mathbb{R}}$, there is $x\in[0,1]$ where $f$ is continuous. 4. (iv)

For cliquish $f:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous. 5. (v)

(Volterra [volaarde2]) For cliquish $f,g:[0,1]\rightarrow{\mathbb{R}}$, there is $x\in[0,1]$ such that $f$ and $g$ are both continuous or both discontinuous at $x$. 6. (vi)

(Volterra [volaarde2]) For cliquish $f:[0,1]\rightarrow{\mathbb{R}}$, there is either $q\in{\mathbb{Q}}\cap[0,1]$ where $f$ is discontinuous, or $x\in[0,1]\setminus{\mathbb{Q}}$ where $f$ is continuous. 7. (vii)

The previous two items restricted to usco functions. 8. (viii)

Blumberg’s theorem ([bloemeken]) restricted to cliquish (or: usco) functions.

Some of the above theorems stem from Volterra’s early work (1881) in the spirit of -but predating- the Baire category theorem, as discussed in Section 1.2. The (necessity for the) absence of ‘Baire 1’ from the above items is explained at the end of this section. In Section 3, we obtain equivalences for $\textup{{PHP}}_{[0,1]}$, including the following well-known principles, like the aforementioned Vitali-Lebesgue theorem.

1. (ix)

(Vitali-Lebesgue) For Riemann integrable $f:[0,1]\rightarrow{\mathbb{R}}$, the set of continuity points $C_{f}$ has measure one. 2. (x)

For Riemann integrable $f:[0,1]\rightarrow[0,1]$ such that $\int_{0}^{1}f(x)dx=0$, the set $\{x\in[0,1]:f(x)=0\}$ has measure one. 3. (xi)

(FTC) For Riemann integrable $f:[0,1]\rightarrow{\mathbb{R}}$ with $F(x):=\lambda x.\int_{0}^{x}f(t)dt$, the following set exists and has measure one:

[TABLE] 4. (xii)

The previous item restricted to usco or cliquish functions.

We obtain similar equivalences for $\textup{{WBCT}}_{[0,1]}$, a ‘hybrid’ version of $\textup{{BCT}}_{[0,1]}$ and $\textup{{PHP}}_{[0,1]}$, with equivalences that are interesting in their own right. The relation between these and related principles may be found in Figure 1 in Section 4.1.

Fourth, the above items suggests that our results are robust as follows:

A system is robust if it is equivalent to small perturbations of itself. ([montahue]*p. 432; emphasis in original)

Most of our results shall be seen to exhibit a similar (or stronger) level of robustness. For instance, item (iv) above can be restricted to any Baire class $\alpha\geq 2$ and the equivalence still goes through. In this light, we feel that $\textup{{BCT}}_{[0,1]}$ and $\textup{{PHP}}_{[0,1]}$ deserve the moniker ‘big’ system in the way this notion is used in second-order RM, namely as boasting many equivalences from different fields of mathematics.

Fifth, items (i)-(xii) are hard to prove in terms of conventional comprehension, in the sense of Footnote 2. We shall identify natural extra conditions that render the above items provable in terms of arithmetical comprehension (or at least the Big Five), like quasi-continuity (resp. Baire 1) for item (iv) (resp. item (i)). As discussed in Remark 2.20, quasi-continuity and cliquishness are however closely related. Moreover, usco (and fragmented) functions are of course Baire 1, say over ZF; there is no contradiction here as e.g. the statement

a bounded usco function on the unit interval is Baire 1

already implies (stronger principles than) $\textup{{BCT}}_{[0,1]}$ by Corollary 2.8. This explains why the above items (i)-(xii) do not (and cannot) deal with Baire 1 or quasi-continuous functions: the latter conditions make the associated theorems provable in relatively weak systems, like arithmetical comprehension.

Finally, we discuss the bigger picture relating to $\textup{{PHP}}_{[0,1]}$ and $\textup{{BCT}}_{[0,1]}$ in Section 4. We argue that the RM of the uncountability of ${\mathbb{R}}$ is the product of taking the RM of $\textup{{PHP}}_{[0,1]}$ and the RM of $\textup{{BCT}}_{[0,1]}$ and pushing everything down from usco/cliquish functions to the level of regulated/bounded variation functions. This explains why the RM of $\textup{{PHP}}_{[0,1]}$ and the RM of $\textup{{BCT}}_{[0,1]}$ are similar, despite the fundamental differences between measure and category. We also explore the connections between our results and set theory (Section 4.2), and show (Section 4.3) that slight variations of Banach’s theorem, i.e. that the continuous nowhere differentiable are dense in $C([0,1])$, are hard to prove in the sense of Footnote 2.

1.2. Volterra’s early work and related results

We introduce Volterra’s early work from [volaarde2], called a historical gem in [dendunne], and related results.

First of all, the Riemann integral was groundbreaking for a number of reasons, including its ability to integrate functions with infinitely many points of discontinuity, as shown by Riemann himself ([riehabi]). A natural question is then ‘how discontinuous’ a Riemann integrable function can be. In this context, Thomae introduced the function $T:{\mathbb{R}}\rightarrow{\mathbb{R}}$ around 1875 in [thomeke]*p. 14, §20 as follows:

[TABLE]

Thomae’s function $T$ is integrable on any interval, but has a dense set of points of discontinuity, namely ${\mathbb{Q}}$, and a dense set of points of continuity, namely ${\mathbb{R}}\setminus{\mathbb{Q}}$.

The perceptive student, upon seeing Thomae’s function as in (T), will ask for a function continuous at each rational point and discontinuous at each irrational one. Such a function cannot exist, as is generally proved using the Baire category theorem. However, Volterra in [volaarde2] already established this negative result about twenty years before the publication of the Baire category theorem.

Secondly, as to the content of Volterra’s paper [volaarde2], we find the following theorem, where a function is pointwise discontinuous if it has a dense set of continuity points. On the real line, this is equivalent to being cliquish (see Section 1.3.3).

Theorem 1.2** (Volterra, 1881).**

There do not exist pointwise discontinuous functions defined on an interval for which the continuity points of one are the discontinuity points of the other, and vice versa.

Volterra then states two corollaries, of which the following is perhaps well-known in ‘popular mathematics’ and constitutes the aforementioned negative result.

Corollary 1.3** (Volterra, 1881).**

There is no ${\mathbb{R}}\rightarrow{\mathbb{R}}$ function that is continuous on ${\mathbb{Q}}$ and discontinuous on ${\mathbb{R}}\setminus{\mathbb{Q}}$.

We note that pointwise discontinuous functions were already studied by Dini before 1878, including an equivalent definition (see [dinipi]§63) that amounts to cliquishness (see Section 1.3.3) and the observation that Riemann integrable functions are pointwise discontinuous, following Hankel (see [dinipi]§188 and [hankelwoot]).

Thirdly, Volterra’s results from [volaarde2] are generalised in [volterraplus, gaud]. The following theorem is immediate from these generalisations.

Theorem 1.4**.**

For any countable dense set $D\subset[0,1]$ and $f:[0,1]\rightarrow{\mathbb{R}}$, either $f$ is discontinuous at some point in $D$ or continuous at some point in $[0,1]\setminus D$.

A related result is as follows, which we will study for e.g. cliquish functions.

Theorem 1.5** (Blumberg’s theorem, [bloemeken]).**

For any $f:{\mathbb{R}}\rightarrow{\mathbb{R}}$, there is a dense subset $D\subset{\mathbb{R}}$ such that the restriction of $f$ to $D$, usually denoted $f_{\upharpoonright D}$, is continuous.

To be absolutely clear, the conclusion of Blumberg’s theorem means that

[TABLE]

where the underlined quantifier marks the difference with ‘usual’ continuity.

Fourth, the Baire category theorem for the real line was first proved by Osgood ([fosgood]) and later by Baire ([beren2]) in a more general setting.

Theorem 1.6** (Baire category theorem).**

If $(O_{n})_{n\in{\mathbb{N}}}$ is a sequence of dense open sets of reals, then $\bigcap_{n\in{\mathbb{N}}}O_{n}$ is non-empty.

We have previously studied the above theorem restricted to the unit interval in [dagsamVII], but failed to obtain any equivalences. In Section 2, we obtain a number of equivalences for the Baire category theorem. To this end, we will need some preliminaries and definitions, as in Section 1.3.

Fifth, Baire has shown that separately continuous ${\mathbb{R}}^{2}\rightarrow{\mathbb{R}}$ are quasi-continuous in one variable (see Section 1.3.3 for the latter). Baire mentions in [beren2]*p. 95 that the latter notion (without naming it) was suggested to him by Volterra. The naming and independent study was done later by Kempisty in [kemphaan].

Finally, in light of our definition of open set in Definition 1.8, our study of the Baire category theorem (and the same for [dagsamVII]) is based on a most general definition of open set, i.e. no additional (computational) information is given. Besides the intrinsic interest of such an investigation, there is a deeper reason, as discussed in Remark 1.14, namely that open sets without any representation are readily encountered ‘in the wild’.

1.3. Preliminaries and definitions

We briefly introduce the program Reverse Mathematics in Section 1.3.1. We introduce some essential axioms (Section 1.3.2) and definitions (Section 1.3.3). Our RM-study shall make (sometimes essential) use of oscillation functions, a construct which goes back to Riemann and Hankel, as discussed in Section 1.3.4.

1.3.1. Reverse Mathematics

Reverse Mathematics (RM hereafter) is a program in the foundations of mathematics initiated around 1975 by Friedman ([fried, fried2]) and developed extensively by Simpson ([simpson2]). The aim of RM is to identify the minimal axioms needed to prove theorems of ordinary, i.e. non-set theoretical, mathematics.

We refer to [stillebron] for a basic introduction to RM and to [simpson2, simpson1, damurm] for an overview of RM. We expect basic familiarity with RM, in particular Kohlenbach’s higher-order RM ([kohlenbach2]) essential to this paper, including the base theory $\textup{{RCA}}_{0}^{\omega}$. An extensive introduction can be found in e.g. [dagsamIII, dagsamV, dagsamX] and elsewhere.

We have chosen to include a brief introduction as a technical appendix, namely Section A. All undefined notions may be found in the latter, while we do point out here that we shall sometimes use common notations from type theory. For instance, the natural numbers are type [math] objects, denoted $n^{0}$ or $n\in{\mathbb{N}}$. Similarly, elements of Baire space are type $1$ objects, denoted $f\in{\mathbb{N}}^{{\mathbb{N}}}$ or $f^{1}$. Mappings from Baire space ${\mathbb{N}}^{{\mathbb{N}}}$ to ${\mathbb{N}}$ are denoted $Y:{\mathbb{N}}^{{\mathbb{N}}}\rightarrow{\mathbb{N}}$ or $Y^{2}$.

1.3.2. Some comprehension functionals

In second-order RM, the logical hardness of a theorem is measured via what fragment of the comprehension axiom is needed for a proof. For this reason, we introduce some axioms and functionals related to higher-order comprehension in this section. We are mostly dealing with conventional comprehension here, i.e. only parameters over ${\mathbb{N}}$ and ${\mathbb{N}}^{{\mathbb{N}}}$ are allowed in formula classes like $\Pi_{k}^{1}$ and $\Sigma_{k}^{1}$.

First of all, the functional $\varphi$ in $(\exists^{2})$ is also Kleene’s quantifier $\exists^{2}$ and is clearly discontinuous at $f=11\dots$ in Cantor space:

[TABLE]

In fact, $(\exists^{2})$ is equivalent to the existence of $F:{\mathbb{R}}\rightarrow{\mathbb{R}}$ such that $F(x)=1$ if $x>_{{\mathbb{R}}}0$, and [math] otherwise (see [kohlenbach2]*Prop. 3.12). Related to $(\exists^{2})$, the functional $\mu^{2}$ in $(\mu^{2})$ is called Feferman’s $\mu$ (see [avi2]) and may be found -with the same symbol- in Hilbert-Bernays’ Grundlagen ([hillebilly2]*Supplement IV):

[TABLE]

We have $(\exists^{2})\leftrightarrow(\mu^{2})$ over $\textup{{RCA}}_{0}^{\omega}$ (see [kohlenbach2]*§3) and $\textup{{ACA}}_{0}^{\omega}\equiv\textup{{RCA}}_{0}^{\omega}+(\exists^{2})$ proves the same sentences as $\textup{{ACA}}_{0}$ by [hunterphd]*Theorem 2.5.

Secondly, the functional $\SS^{2}$ in $(\SS^{2})$ is called the Suslin functional ([kohlenbach2]):

[TABLE]

The system $\Pi_{1}^{1}\text{-{{CA}}}_{0}^{\omega}\equiv\textup{{RCA}}_{0}^{\omega}+(\SS^{2})$ proves the same $\Pi_{3}^{1}$-sentences as $\Pi_{1}^{1}\text{-{{CA}}}_{0}$ by [yamayamaharehare]*Theorem 2.2. By definition, the Suslin functional $\SS^{2}$ can decide whether a $\Sigma_{1}^{1}$-formula as in the left-hand side of $(\SS^{2})$ is true or false. We similarly define the functional $\SS_{k}^{2}$ which decides the truth or falsity of $\Sigma_{k}^{1}$-formulas from $\textsf{{L}}_{2}$; we also define the system $\Pi_{k}^{1}\text{-{{CA}}}_{0}^{\omega}$ as $\textup{{RCA}}_{0}^{\omega}+(\SS_{k}^{2})$, where $(\SS_{k}^{2})$ expresses that $\SS_{k}^{2}$ exists. We note that the operators $\nu_{n}$ from [boekskeopendoen]*p. 129 are essentially $\SS_{n}^{2}$ strengthened to return a witness (if existant) to the $\Sigma_{n}^{1}$-formula at hand.

Thirdly, full second-order arithmetic ${\textsf{{Z}}}_{2}$ is readily derived from $\cup_{k}\Pi_{k}^{1}\text{-{{CA}}}_{0}^{\omega}$, or from:

[TABLE]

and we therefore define ${\textsf{{Z}}}_{2}^{\Omega}\equiv\textup{{RCA}}_{0}^{\omega}+(\exists^{3})$ and ${\textsf{{Z}}}_{2}^{\omega}\equiv\cup_{k}\Pi_{k}^{1}\text{-{{CA}}}_{0}^{\omega}$, which are conservative over ${\textsf{{Z}}}_{2}$ by [hunterphd]Cor. 2.6. Despite this close connection, ${\textsf{{Z}}}_{2}^{\omega}$ and ${\textsf{{Z}}}_{2}^{\Omega}$ can behave quite differently, as discussed in e.g. [dagsamIII]§2.2. The functional from $(\exists^{3})$ is also called ‘$\exists^{3}$’, and we use the same convention for other functionals.

Finally, the following negative results were established in [dagsamX, dagsamXI] using the technique Gandy selection from Kleene computability theory.

Neither ${\textsf{{Z}}}_{2}^{\omega}+\textup{{QF-AC}}^{0,1}$ nor ${\textsf{{Z}}}_{2}^{\omega}+\textup{{IND}}_{0}$ can prove $\textup{{NIN}}_{[01]}$, while ${\textsf{{Z}}}_{2}^{\Omega}$ can.

Here, $\textup{{NIN}}_{[0,1]}$ states that there is no injection from $[0,1]$ to ${\mathbb{N}}$ as follows:

[TABLE]

and $\textup{{IND}}_{0}$ is the following fragment of the induction axiom.

Definition 1.7** ($\textup{{IND}}_{0}$).**

Let $Y^{2}$ satisfy $(\forall n\in{\mathbb{N}})(\exists\textup{ at most one }f\in 2^{{\mathbb{N}}})(Y(f,n)=0)$. For $k\in{\mathbb{N}}$, there is $w^{1^{*}}$ with $|w|=k$ such that for $m\leq k$, we have:

[TABLE]

A limited number of equivalences for $\textup{{IND}}_{0}$ (resp. $\textup{{NIN}}_{[0,1]}$) may be found in [dagsamX]*§3 (resp. [samcie22]). A large number of equivalences for a slight variation of $\textup{{NIN}}_{[0,1]}$ may be found in [samBIG], as also discussed in Section 4.

1.3.3. Some definitions

We introduce some definitions needed in the below, mostly stemming from mainstream mathematics. We assume the standard ‘epsilon-delta’ definitions of continuity and Riemann integrability to be known. We note that subsets of ${\mathbb{R}}$ are given by their characteristic functions as in Definition 1.8, well-known from measure and probability theory. We shall generally work over $\textup{{ACA}}_{0}^{\omega}$ as some definitions make little sense over $\textup{{RCA}}_{0}^{\omega}$.

First of all, we make use the usual definition of (open) set, where $B(x,r)$ is the open ball with radius $r>0$ centred at $x\in{\mathbb{R}}$. We note that our notion of ‘measure zero’ does not depend on (the existence of) the Lebesgue measure.

Definition 1.8** (Sets).**

• •

A subset $A\subset{\mathbb{R}}$ is given by its characteristic function $F_{A}:{\mathbb{R}}\rightarrow\{0,1\}$, i.e. we write $x\in A$ for $F_{A}(x)=1$, for any $x\in{\mathbb{R}}$.

• •

A subset $O\subset{\mathbb{R}}$ is open in case $x\in O$ implies that there is $k\in{\mathbb{N}}$ such that $B(x,\frac{1}{2^{k}})\subset O$.

• •

A subset $C\subset{\mathbb{R}}$ is closed if the complement ${\mathbb{R}}\setminus C$ is open.

• •

A set $A\subset{\mathbb{R}}$ is enumerable if there is a sequence of reals that includes all elements of $A$.

• •

A set $A\subset{\mathbb{R}}$ is countable if there is $Y:{\mathbb{R}}\rightarrow{\mathbb{N}}$ that is injective on $A$, i.e.

[TABLE]

• •

A set $A\subset{\mathbb{R}}$ is measure zero if for any $\varepsilon>0$ there is a sequence of open intervals $(I_{n})_{n\in{\mathbb{N}}}$ such that $\cup_{n\in{\mathbb{N}}}I_{n}$ covers $A$ and $\varepsilon>\sum_{n=0}^{\infty}|I_{n}|$.

As discussed in Remark 1.14, the study of regulated functions already gives rise to open sets that do not come with additional representation beyond Definition 1.8. We will often assume $(\exists^{2})$ from Section 1.3.2 to guarantee that basic objects like the unit interval are sets in the sense of Def. 1.8. An interesting constructive enrichment of open sets from [dagsamVII] is as follows.

Definition 1.9**.**

A set $O\subset{\mathbb{R}}$ is R2-open if there is $Y:{\mathbb{R}}\rightarrow{\mathbb{R}}$ such that $x\in O$ implies $Y(x)>0\wedge B(x,Y(x))\subset O$. A set $C$ is R2-closed if ${\mathbb{R}}\setminus C$ is R2-open.

The R2-representation is strictly weaker than the RM-representation, i.e. unions of basic open sets as in [simpson2]*II.5.6. Nonetheless, the Baire category theorem for R2-open sets is provable in $\textup{{ACA}}_{0}^{\omega}$ by [dagsamVII]*Theorem 7.10.

Secondly, we study the following weak continuity notions, many of which are well-known and hark back to the days of Baire, Darboux, Dini, Hankel, and Volterra ([beren, beren2, darb, volaarde2, hankelwoot, hankelijkheid, dinipi]). We use ‘sup’ and related operators in the same ‘virtual’ or ‘comparative’ way as in second-order RM (see e.g. [simpson2]*X.1). In this way, a formula of the form ‘$\sup A>a$’ makes sense as shorthand for a formula in the language of all finite types, even when $\sup A$ need not exist in $\textup{{RCA}}_{0}^{\omega}$. As in [basket, basket2], the definition of Baire $n$-function proceeds via (external) induction over standard $n$.

Definition 1.10**.**

For $f:[0,1]\rightarrow{\mathbb{R}}$, we have the following definitions:

• •

$f$* is upper semi-continuous at $x_{0}\in[0,1]$ if $f(x_{0})\geq_{{\mathbb{R}}}\lim\sup_{x\rightarrow x_{0}}f(x)$,*

• •

$f$* is lower semi-continuous at $x_{0}\in[0,1]$ if $f(x_{0})\leq_{{\mathbb{R}}}\lim\inf_{x\rightarrow x_{0}}f(x)$,*

• •

$f$* is regulated if for every $x_{0}$ in the domain, the ‘left’ and ‘right’ limit $f(x_{0}-)=\lim_{x\rightarrow x_{0}-}f(x)$ and $f(x_{0}+)=\lim_{x\rightarrow x_{0}+}f(x)$ exist.*

• •

$f$* is Baire 0 if it is a continuous function.*

• •

$f$* is Baire $n+1$ if it is the pointwise limit of a sequence of Baire $n$ functions. *

• •

$f$* is effectively Baire $n$ $(n\geq 2)$ if there is a sequence $(f_{m_{1},\dots,m_{n}})_{m_{1},\dots,m_{n}\in{\mathbb{N}}}$ of continuous functions such that for all $x\in[0,1]$, we have*

[TABLE]

• •

$f$* is Baire 1∗** if333The notion of Baire 1∗* goes back to [ellis] and equivalent definitions may be found in [kerkje]. In particular, Baire 1*∗* is equivalent to the Jayne-Rogers notion of piecewise continuity from [JR].* there is a sequence of closed sets $(C_{n})_{n\in{\mathbb{N}}}$ such $[0,1]=\cup_{n\in{\mathbb{N}}}C_{n}$ and $f_{\upharpoonright C_{m}}$ is continuous for all $m\in{\mathbb{N}}$.*

• •

$f$* is *countably continuous444The notion of countably discontinuity, under a different name, goes back to Lusin (see [novady]). if there is a sequence of sets $(E_{n})_{n\in{\mathbb{N}}}$ such $[0,1]=\cup_{n\in{\mathbb{N}}}E_{n}$ and $f_{\upharpoonright E_{m}}$ is continuous for all $m\in{\mathbb{N}}$.

• •

$f$* is quasi-continuous at $x_{0}\in[0,1]$ if for $\epsilon>0$ and any open neighbourhood $U$ of $x_{0}$, there is non-empty open ${G\subset U}$ with $(\forall x\in G)(|f(x_{0})-f(x)|<\varepsilon)$.*

• •

$f$* is cliquish at $x_{0}\in[0,1]$ if for $\epsilon>0$ and any open neighbourhood $U$ of $x_{0}$, there is a non-empty open ${G\subset U}$ with $(\forall x,y\in G)(|f(x)-f(y)|<\varepsilon)$.*

• •

$f$* is upper (resp. lower) quasi-continuous at $x_{0}\in[0,1]$ if for $\epsilon>0$ and any open neighbourhood $U$ of $x_{0}$, there is a non-empty open ${G\subset U}$ with $(\forall x\in G)(f(x)<f(x_{0})+\varepsilon)$ *(resp.  $(\forall x\in G)(f(x)>f(x_{0})-\varepsilon)$).

As to notations, a common abbreviation is ‘usco’ and ‘lsco’ for the first two items and ‘uqco’ (resp. lqco) for the final item. Moreover, if a function has a certain weak continuity property at all reals in $[0,1]$ (or its intended domain), we say that the function has that property. Regarding the notion of ‘effectively Baire $n$’ in Definition 1.10, the latter is used, using codes for continuous functions, in second-order RM (see [basket, basket2]). Baire himself notes in [beren2]*p. 69 that Baire 2 functions can be represented by effectively Baire 2 functions. By the results in [dagsamXIV], there is a significant difference between the these notions.

Thirdly, the following sets are often crucial in proofs relating to discontinuous functions, as can be observed in e.g. [voordedorst]*Thm. 0.36.

Definition 1.11**.**

The sets $C_{f}$ and $D_{f}$ (if they exist) respectively gather the points where $f:{\mathbb{R}}\rightarrow{\mathbb{R}}$ is continuous and discontinuous.

One problem with the sets $C_{f},D_{f}$ is that the definition of continuity involves quantifiers over ${\mathbb{R}}$. In general, deciding whether a given ${\mathbb{R}}\rightarrow{\mathbb{R}}$-function is continuous at a given real, is as hard as $\exists^{3}$ from Section 1.3.2. For these reasons, the sets $C_{f},D_{f}$ only exist in strong systems. A solution is discussed in Section 1.3.4.

Fourth, we introduce some notions most of which are found already in e.g. the work of Volterra, Smith, and Hankel ([hankelwoot, snutg, volaarde2]).

Definition 1.12**.**

• •

A set $A\subset{\mathbb{R}}$ is dense in $B\subset{\mathbb{R}}$ if for $k\in{\mathbb{N}},b\in B$, there is $a\in A$ with $|a-b|<\frac{1}{2^{k}}$.

• •

A function $f:{\mathbb{R}}\rightarrow{\mathbb{R}}$ is pointwise discontinuous if for any $x\in{\mathbb{R}},k\in{\mathbb{N}}$ there is $y\in B(x,\frac{1}{2^{k}})$ such that $f$ is continuous at $y$.

• •

A set $A\subset{\mathbb{R}}$ is nowhere dense in $B\subset{\mathbb{R}}$ if $A$ is not dense in any open sub-interval of $B$.

• •

A function $f:[0,1]\rightarrow{\mathbb{R}}$ is simply continuous (sico) if for any open $G\subset{\mathbb{R}}$, the set $f^{-1}(G)$ is the union of an open and a nowhere dense set.

Fifth, we also need the notion of ‘intermediate value property’, also called the ‘Darboux property’ in light of Darboux’s work in [darb].

Definition 1.13** (Darboux property).**

Let $f:[0,1]\rightarrow{\mathbb{R}}$ be given.

• •

*A real $y\in{\mathbb{R}}$ is a left (resp. right) cluster value of $f$ at $x\in[0,1]$ if there is $(x_{n})_{n\in{\mathbb{N}}}$ such that $y=\lim_{n\rightarrow\infty}f(x_{n})$ and $x=\lim_{n\rightarrow\infty}x_{n}$ and $(\forall n\in{\mathbb{N}})(x_{n}\leq x)$ *(resp. $(\forall n\in{\mathbb{N}})(x_{n}\geq x)$).

• •

*A point $x\in[0,1]$ is a Darboux point of $f:[0,1]\rightarrow{\mathbb{R}}$ if for any $\delta>0$ and any left (resp. right) cluster value $y$ of $f$ at $x$ and $z\in{\mathbb{R}}$ strictly between $y$ and $f(x)$, there is $w\in(x-\delta,x)$ *(resp. $w\in(x,x+\delta)$) such that $f(w)=y$.

By definition, a point of continuity is also a Darboux point, but not vice versa.

Finally, the following remark is meant to express that closed sets as in Definition 1.8, i.e. without any additional representation (say provable in ${\textsf{{Z}}}_{2}^{\omega}$), are readily found in the wild. This even holds for the ‘weak’ representation from Def. 1.9.

Remark 1.14**.**

First of all, fix a regulated function $f:[0,1]\rightarrow{\mathbb{R}}$ and consider the set $D_{k}$ as in (1.1), definable using $\exists^{2}$ and such that $D_{f}=\cup_{k\in{\mathbb{N}}}D_{k}$.

[TABLE]

This set is central to many proofs involving regulated functions (see e.g. [voordedorst]*Thm. 0.36). Now, that $D_{k}$ is finite follows by a standard555If $A_{n}$ were infinite, the Bolzano-Weierstrass theorem implies the existence of a limit point $y\in[0,1]$ for $A_{n}$. One readily shows that $f(y+)$ or $f(y-)$ does not exist, a contradiction as $f$ is assumed to be regulated. This argument is readily formalised in $\textup{{ACA}}_{0}^{\omega}+\textup{{QF-AC}}^{0,1}$. compactness argument. Hence, working in ${\textsf{{Z}}}_{2}^{\Omega}$ from Section 1.3.2, one readily proves the following:

there is a sequence $(C_{k})_{k\in{\mathbb{N}}}$ of RM-codes for the sequence of closed sets $(D_{k})_{k\in{\mathbb{N}}}$,

there is a sequence $(Y_{k})_{k\in{\mathbb{N}}}$ of R2-representations for the closed sets $(D_{k})_{k\in{\mathbb{N}}}$.

However, ${\textsf{{Z}}}_{2}^{\omega}$ cannot666The Baire category theorem for RM-open and R2-open sets is provable in $\textup{{ACA}}_{0}^{\omega}$ by [simpson2]*II.5.8 and [dagsamVII]*Theorem 7.10. Hence, in case $D_{k}$ as in (1.1) have RM-codes or R2-representations, the associated Baire category theorem implies that $D_{f}=\cup_{k\in{\mathbb{N}}}D_{k}$ is not $[0,1]$, i.e. $C_{f}$ is non-empty. By [samBIG]*Theorem 3.7, we obtain $\textup{{NIN}}_{[0,1]}$ which is not provable in ${\textsf{{Z}}}_{2}^{\omega}$ by [dagsamX]Theorem 3.1. prove either of the centred coding statements about (1.1). Since regulated functions are usco and cliquish (by definition, say in $\textup{{RCA}}_{0}^{\omega}$), this observation applies to the topic of this paper as well. We can obtain the same results for functions of bounded variation, following [samBIG]§3.4.

1.3.4. On oscillation functions

In this section, we introduce oscillation functions and establish some required properties. We have previously studied usco, Baire 1 and cliquish functions in Kleene’s computability theory using oscillation functions (see [samcsl23]). As will become clear, such functions are generally necessary for the RM-study in Section 2 and 3.

First of all, the study of regulated functions in [dagsamXI, dagsamXII, dagsamXIII] is really only possible thanks to the associated left- and right limits (see Definition 1.10) and the fact that the latter are computable in $\exists^{2}$. Indeed, for regulated $f:{\mathbb{R}}\rightarrow{\mathbb{R}}$, the formula

[TABLE]

involves quantifiers over ${\mathbb{R}}$ but is equivalent to the arithmetical formula $f(x+)=f(x)=f(x-)$. In this light, we can define the set $D_{f}$ of discontinuity points of $f$ -using only $\exists^{2}$- and proceed with the usual (textbook) proofs. An analogous approach, namely the study of usco, Baire 1, and cliquish functions in Kleene’s computability theory, was used in [samcsl23]. To this end, we used oscillation functions as in Definition 1.15. We note that Riemann and Hankel already considered the notion of oscillation in the context of Riemann integration ([hankelwoot, rieal]).

Definition 1.15** (Oscillation functions).**

For any $f:{\mathbb{R}}\rightarrow{\mathbb{R}}$, the associated oscillation functions are defined as follows: $\textup{{osc}}_{f}([a,b]):=\sup_{{x\in[a,b]}}f(x)-\inf_{{x\in[a,b]}}f(x)$ and $\textup{{osc}}_{f}(x):=\lim_{k\rightarrow\infty}\textup{{osc}}_{f}(B(x,\frac{1}{2^{k}})).$

We stress that $\textup{{osc}}_{f}:{\mathbb{R}}\rightarrow{\mathbb{R}}$ is only777To be absolutely clear, the notation ‘$\textup{{osc}}_{f}$’ and the appearance of $f$ therein in particular, is purely symbolic and lambda abstraction involving ‘$\lambda f$’ is expressly forbidden. a third-order function, as clearly indicated by its type. On a related technical note, while the suprema, infima, and limits in Definition 1.15 do not always exist in weak systems, formulas like $\textup{{osc}}_{f}(x)>y$ always make sense as shorthand for the standard definition of the suprema, infima, and limits involved; this ‘virtual’ or ‘comparative’ meaning is part and parcel of (second-order) RM in light of [simpson2]*X.1.

Now, our main interest in Definition 1.15 is that (C) is equivalent to the arithmetical formula $\textup{{osc}}_{f}(x)=0$, assuming the latter function is given. Hence, in the presence of $\textup{{osc}}_{f}:{\mathbb{R}}\rightarrow{\mathbb{R}}$ and $\exists^{2}$, we can define $D_{f}$ and proceed with the usual (textbook) proofs, which is the approach we took in [samcsl23]. Below, we also show that we can avoid the use of oscillation functions for usco functions.

Secondly, we sketch the connection between usco (or: cliquish) functions and the Baire category theorem, in both directions, to further motivate our use of oscillation functions. In one direction, fix a usco function $f:[0,1]\rightarrow{\mathbb{R}}$ and its oscillation function $\textup{{osc}}_{f}:{\mathbb{R}}\rightarrow{\mathbb{R}}$. A standard textbook technique is to decompose the set $D_{f}=\{x\in[0,1]:\textup{{osc}}_{f}(x)>0\}$ as the union of the closed sets

[TABLE]

The complement $O_{n}:=[0,1]\setminus D_{k}$ can be shown to be open and dense, as required for the antecedent of the Baire category theorem, i.e. $C_{f}$ is non-empty as a result. This connection also goes in the other direction as follows: fix a sequence of dense and open sets $(O_{n})_{n\in{\mathbb{N}}}$ in the unit interval, define $X_{n}:=[0,1]\setminus O_{n}$ and consider the following function $h:[0,1]\rightarrow{\mathbb{R}}$ defined using $\mu^{2}$:

[TABLE]

The function $h$ may be found in the literature ([myerson]*p. 238) and is usco by Theorem 1.18. Moreover, for $x\in C_{h}$ we also have $x\in\cap_{n\in{\mathbb{N}}}O_{n}$, as required for the consequent of the Baire category theorem. Thus, the Baire category theorem is intimately connected to continuity properties of usco functions (in both directions). One can similarly obtain the same connection for e.g. Baire $1^{*}$ and cliquish functions, assuming we have access to (1.2), which is why we assume $\textup{{osc}}_{f}:{\mathbb{R}}\rightarrow{\mathbb{R}}$ to be given in general.

Thirdly, much to our own surprise, the ‘counterexample’ function from (H) has nice properties that are provable in weak systems.

Theorem 1.16** ($\textup{{ACA}}_{0}^{\omega}$).**

Let $(X_{n})_{n\in{\mathbb{N}}}$ be an increasing sequence of closed nowhere dense sets. Then $h:[0,1]\rightarrow{\mathbb{R}}$ from (H) is its own oscillation function.

Proof.

Consider $h:[0,1]\rightarrow{\mathbb{R}}$ as in (H) where $(X_{n})_{n\in{\mathbb{N}}}$ is an increasing sequence of closed nowhere dense sets. We will show that $h(x)=\textup{{osc}}_{h}(x)$ for all $x\in[0,1]$, i.e. $h$ is its own oscillation function. To this end, we proceed by case distinction.

• •

In case $h(x_{0})=0$ for some $x_{0}\in[0,1]$, then $x_{0}\in\cap_{n\in{\mathbb{N}}}Y_{n}$ where $Y_{n}:=[0,1]\setminus X_{n}$ is open. Hence, for any $m\in{\mathbb{N}}$, there is $N\in{\mathbb{N}}$ such that $B(x_{0},\frac{1}{2^{N}})\subset Y_{m}$, as the latter is open. By the definition of $\textup{{osc}}_{h}$, we have $\textup{{osc}}_{h}(x_{0})<\frac{1}{2^{m}}$ for all $m\in{\mathbb{N}}$, i.e. $\textup{{osc}}_{h}(x_{0})=h(x_{0})=0$.

• •

In case $\textup{{osc}}_{h}(x_{0})=0$ for some $x_{0}\in[0,1]$, we must have $x_{0}\not\in\cup_{n\in{\mathbb{N}}}X_{n}$ and hence $h(x_{0})=0$ by definition. Indeed, if $x_{0}\in X_{n_{0}}$, then $\textup{{osc}}_{h}(x_{0})\geq\frac{1}{2^{n_{0}+1}}$ because $\inf_{x\in B(x_{0},\frac{1}{2^{k}})}h(x)=0$ due to $Y_{m}$ being dense in $[0,1]$ for any $m\in{\mathbb{N}}$, while of course $\sup_{x\in B(x_{0},\frac{1}{2^{k}})}h(x)\geq h(x_{0})\geq\frac{1}{2^{n_{0}+1}}$.

• •

In case $h(x_{0})=\frac{1}{2^{n_{0}+1}}$ for some $x_{0}\in[0,1]$, suppose $\textup{{osc}}_{h}(x_{0})\neq\frac{1}{2^{n_{0}+1}}$. Since by definition (and the previous item) $\textup{{osc}}_{h}(x_{0})\geq h(x_{0})=\frac{1}{2^{n_{0}+1}}$, we have $\textup{{osc}}_{h}(x_{0})>\frac{1}{2^{n_{0}+1}}$, implying $\textup{{osc}}_{h}(x_{0})\geq\frac{1}{2^{n_{0}}}$ and $n_{0}>0$. Now, if $x_{0}\in Y_{n_{0}-1}$, then $B(x_{0},\frac{1}{2^{N}})\subset Y_{n_{0}-1}$ for $N$ large enough, as $Y_{n_{0}-1}$ is open; by definition, the latter inclusion implies that $\textup{{osc}}_{h}(x_{0})\leq\frac{1}{2^{n_{0}}}$, a contradiction. However, $x_{0}\not\in Y_{n_{0}-1}$ also leads to a contradiction as then $h(x_{0})\geq\frac{1}{2^{n_{0}}}$. In conclusion, we have $h(x_{0})=\frac{1}{2^{n_{0}+1}}=\textup{{osc}}_{h}(x_{0})$.

• •

In case $\textup{{osc}}_{h}(x_{0})>0$ for some $x_{0}\in[0,1]$, suppose $h(x_{0})\neq\textup{{osc}}_{h}(x_{0})$. By definition (and the first item) we have $\textup{{osc}}_{h}(x_{0})\geq h(x_{0})>0$, implying $\textup{{osc}}_{h}(x_{0})>h(x_{0})=\frac{1}{2^{n_{0}+1}}$ for some $n_{0}\in{\mathbb{N}}$. In turn, we must have $\textup{{osc}}_{h}(x_{0})\geq\frac{1}{2^{n_{0}}}$ and $n_{0}>0$. Now, if $x_{0}\in Y_{n_{0}}$, then $B(x_{0},\frac{1}{2^{N}})\subset Y_{n_{0}}$ for $N$ large enough, as $Y_{n_{0}}$ is open; by definition, the latter inclusion implies that $\textup{{osc}}_{h}(x)\leq\frac{1}{2^{n_{0}+1}}$, a contradiction. However, $x_{0}\not\in Y_{n_{0}}$, also leads to a contradiction as then $h(x_{0})\geq\frac{1}{2^{n_{0}}}$. Since both cases lead to contradiction, we have $h(x_{0})=\textup{{osc}}_{h}(x_{0})$.

We thus have $h(x)=\textup{{osc}}_{h}(x)$ for all $x\in[0,1]$, as required. ∎

As it happens, functions that are their own oscillation function have been studied in the mathematical literature (see e.g. [kosten]). The previous theorem is surprising: computing the oscillation function of arbitrary functions is as hard as $\exists^{3}$.

Fourth, we establish the well-known fact that oscillation functions are usco.

Theorem 1.17** ($\textup{{ACA}}_{0}^{\omega}$).**

For any $f:{\mathbb{R}}\rightarrow{\mathbb{R}}$ such that the oscillation function $\textup{{osc}}_{f}:{\mathbb{R}}\rightarrow{\mathbb{R}}$ exists, the latter is usco.

Proof.

Fix $x_{0}\in{\mathbb{R}}$ and consider $y\in{\mathbb{R}}$ such that $y>\textup{{osc}}_{f}(x_{0})$. Say $y>\textup{{osc}}_{f}(x_{0})+\varepsilon$ for $\varepsilon>0$ and let $n_{0}$ be such that for all $n\geq n_{0}$, we have $|\textup{{osc}}_{f}(B(x_{0},\frac{1}{2^{n}}))-\textup{{osc}}_{f}(x_{0})|<\varepsilon/2$. Now pick $z\in{\mathbb{R}}$ and $m_{0}\in{\mathbb{N}}$ such that $B(z,\frac{1}{2^{m_{0}}})\subset B(x_{0},\frac{1}{2^{n_{0}}})$. By definition, we have $\textup{{osc}}_{f}([a,b])\leq\textup{{osc}}_{f}([c,d])$ in case $[a,b]\subseteq[c,d]$. Hence, we have $\textup{{osc}}_{f}(z)\leq\textup{{osc}}_{f}(B(z,\frac{1}{2^{m_{0}}}))\leq\textup{{osc}}_{f}(B(x_{0},\frac{1}{2^{n_{0}}}))\leq\textup{{osc}}_{f}(x_{0})+\varepsilon/2<y$, i.e. $f$ is usco at $x_{0}$ and we are done. ∎

Fifth, we provide a direct proof of some properties of equation (H).

Theorem 1.18** ($\textup{{ACA}}_{0}^{\omega}$).**

Let $(X_{n})_{n\in{\mathbb{N}}}$ be an increasing sequence of closed sets. The function $h:[0,1]\rightarrow{\mathbb{R}}$ from (H) is usco and cliquish.

Proof.

First of all, fix $x_{0}\in[0,1]$ and note that if $h(x_{0})=0$, we have $x_{0}\in Y_{n}:=[0,1]\setminus X_{n}$ for all $n\in{\mathbb{N}}$. These sets are open, i.e. for each $n\in{\mathbb{N}}$ there is $N\in{\mathbb{N}}$ with $B(x_{0},\frac{1}{2^{N}})\subset Y_{n}$. Then $h(x)<\frac{1}{2^{n+1}}$ in the latter ball, i.e. the definition of usco is satisfied. The definition of usco is trivially satisfied if $h(x)=\frac{1}{2}$ as the latter is the supremum of $h$ on $[0,1]$. In case $h(x_{0})=\frac{1}{2^{n_{0}+1}}$ for $n_{0}>0$, then we have $(\exists N\in{\mathbb{N}})(\forall y\in B(x_{0},\frac{1}{2^{N}})(y\not\in X_{n_{0}-1})$. Indeed, if $(\forall N\in{\mathbb{N}})(\exists y\in B(x_{0},\frac{1}{2^{N}})(y\in X_{n_{0}-1})$, then $y\in X_{n_{0}-1}$ as the latter set is closed, contradicting the leastness of $n_{0}$. For $N_{0}\in{\mathbb{N}}$ such that $(\forall y\in B(x_{0},\frac{1}{2^{N_{0}}})(y\not\in X_{n_{0}-1})$, we have $h(y)\leq\frac{1}{2^{n_{0}+1}}$ in this ball.

Secondly, $h$ from (H) is also cliquish. To see this, fix $\varepsilon>0$ and $x_{0}\in[0,1]$ and take large enough $n_{0}\in{\mathbb{N}}$ such that $\frac{1}{2^{n_{0}}}<\varepsilon$. Since $Y_{n_{0}}$ is dense, we can find $x_{1}\in Y_{n_{0}}$ arbitrarily close to $x_{0}$. However, since $Y_{n_{0}}$ is open, we have $B(x_{1},\frac{1}{2^{N_{1}}})\subset Y_{n_{0}}$ for some $N_{1}\in{\mathbb{N}}$. Since $h$ is at most $\frac{1}{2^{n_{0}+1}}$ on this ball, we observe that the definition of cliquish function is satisfied. ∎

The previous theorem is illustrative as follows: in case each $X_{n}$ is a ‘fat’ Cantor set of measure at least $1-\frac{1}{2^{n}}$, then $h$ from (H) is a usco function that is continuous on a measure zero set, namely the complement of $\cup_{n\in{\mathbb{N}}}X_{n}$. These facts can be established in $\textup{{ACA}}_{0}^{\omega}$ in light of [simpson2]*p. 129.

Finally, the computational equivalences in [samcsl23] deal with usco, Baire 1, and cliquish functions, while the RM-equivalences in this paper are only about usco and cliquish functions. The deeper reason for the absence of ‘Baire 1’ in our equivalences is unveiled by Theorems 2.7, 2.10, and 3.7: even for the smaller class of usco functions, the extra assumption that the latter are also Baire 1, makes e.g. the semi-continuity lemma provable in much weaker systems.

2. The Baire category theorem

In this section, we obtain the equivalences sketched in Section 1.1 involving the Baire category theorem and theorems about semi-continuous and cliquish functions (see Section 1.3.3 for the latter notions). We recall that the Baire category theorem has been studied in second-order RM (see e.g. [trevor, mietje]); the use of codes for open sets means the theorem is provable in the base theory $\textup{{RCA}}_{0}$ or similarly weak system. To avoid issues of the representation of real numbers and sets thereof, we will always assume $\mu^{2}$ or $\exists^{2}$ from Section 1.3.2. We shall often make use of the preliminary results from Section 1.3.4.

2.1. Introduction

In this section, we introduce the Baire category theorem and describe the results to be obtained in the below sections.

First of all, we shall study the Baire category theorem formulated as follows.

Principle 2.1** ($\textup{{BCT}}_{[0,1]}$).**

If $(O_{n})_{n\in{\mathbb{N}}}$ is a decreasing sequence of dense open sets of reals in $[0,1]$, then $\bigcap_{n\in{\mathbb{N}}}O_{n}$ is non-empty.

We assume that $O_{n+1}\subseteq O_{n}$ for all $n\in{\mathbb{N}}$ to avoid the use of induction to prove that a finite intersection of open and dense sets is again open and dense.

Secondly, $\textup{{BCT}}_{[0,1]}$ is hard to prove in terms of (conventional) comprehension by [dagsamVII]*Theorem 6.16, while the following theorem provides a slick proof of this fact.

Theorem 2.2**.**

The system ${\textsf{{Z}}}_{2}^{\omega}+\textup{{IND}}_{0}$ cannot prove $\textup{{BCT}}_{[0,1]}$.

Proof.

Let $Y:[0,1]\rightarrow{\mathbb{N}}$ be an injection and define $C_{n}:=\{x\in[0,1]:Y(x)\leq n\}$. Use $\textup{{IND}}_{0}$ to prove that this set is closed and nowhere dense for each $n\in{\mathbb{N}}$. By assumption, $[0,1]=\cup_{n\in{\mathbb{N}}}C_{n}$, i.e. we have established $\textup{{BCT}}_{[0,1]}\rightarrow\textup{{NIN}}_{[0,1]}$ via contraposition; the latter is not provable in ${\textsf{{Z}}}_{2}^{\omega}+\textup{{IND}}_{0}$ by [dagsamXI]*Theorem 2.16. ∎

By contrast, the restriction of $\textup{{BCT}}_{[0,1]}$ to R2-open sets from Section 1.3.3 can be proved in $\textup{{ACA}}_{0}^{\omega}$ by [dagsamVII]*Thm 7.10. Basically, one follows the constructive proof (see e.g. [bish1]) while avoiding the Axiom of (countable) Choice thanks to the R2-representation. This begs the question which other constructive enrichments make $\textup{{BCT}}_{[0,1]}$ (and equivalent theorems) provable in weak(er) systems.

We explore this ‘constructivisation’ theme in Theorems 2.3, 2.7, and 2.19 as follows: the latter theorems show that replacing ‘cliquish’ by the closely related notion ‘quasi-continuous’ (see Remark 2.20) results in theorems provable in $\textup{{ACA}}_{0}^{\omega}$. The same holds for the addition of ‘Baire 1’ to theorems about usco functions; there is no contradiction here as the (classically true) statement

a bounded usco function on the unit interval is Baire 1

already implies (stronger principles than) $\textup{{BCT}}_{[0,1]}$ by Corollary 2.8. Nonetheless, cliquishness and quasi-continuity (and the same for Baire 1 and usco) are closely related notions (see again Remark 2.20), yet there is a great divide -or abyss- between their continuity properties.

Thirdly, we shall obtain the following RM-results in the below sections.

• •

We connect $\textup{{BCT}}_{[0,1]}$ to the semi-continuity lemma in Section 2.2.

• •

We generalise the results in Section 2.2 to Baire $1^{*}$ in Section 2.3.

• •

We connect $\textup{{BCT}}_{[0,1]}$ to the uniform boundedness principle in Section 2.4.

• •

We connect $\textup{{BCT}}_{[0,1]}$ to properties of cliquish functions in Section 2.5.

• •

We connect $\textup{{BCT}}_{[0,1]}$ to properties of fragmented functions in Section 2.6.

• •

We connect $\textup{{BCT}}_{[0,1]}$ to Volterra’s early work (Section 1.2) in Section 2.7.

As discussed in Remark 2.20, the class of cliquish functions is quite large/wild and is identical to the class of pointwise discontinuous function, i.e. we study Volterra’s theorem in full generality. We note that ‘Baire 1’ and ‘fragmented’ are equivalent on ${\mathbb{R}}$ in strong enough systems (see Section 2.6), but not in ${\textsf{{Z}}}_{2}^{\omega}$ by Corollary 2.24.

Finally, we have studied the RM of the gauge integral in [dagsamIII, dagsamVI]. This integral generalises the Lebesgue integral but remains conceptually close to the Riemann integral by -intuitively speaking- replacing the real ‘$\delta>0$’ by a gauge function ‘$\delta:{\mathbb{R}}\rightarrow{\mathbb{R}}^{+}$’ in the usual epsilon-delta definition ([bartle]). This gauge function can be taken to be usco ([gepeperd]) in very general cases, i.e. the RM of usco functions in this paper may well shed new light on the RM of the gauge integral.

2.2. The semi-continuity lemma

We establish the equivalence between $\textup{{BCT}}_{[0,1]}$ and the semi-continuity lemma; the latter expresses that the continuity points of a semi-continuous functions are dense, and is therefore not provable in ${\textsf{{Z}}}_{2}^{\omega}$. We also identify (slight) variations that are provable in weaker systems like $\textup{{ACA}}_{0}^{\omega}$.

First of all, we have the following theorem pertaining to usco functions; note that all items are immediately generalised from ‘one point of continuity’ to ‘a dense set of points of continuity’. Regarding item (e) and (f), there are semi-continuous functions that are not countably continuous ([novady]) or not bounded888Define $f:{\mathbb{R}}\rightarrow{\mathbb{R}}$ as: $f(x)=\frac{-1}{x}$ if $x>0$ and $f(x)=1$ if $x\leq 0$, which is usco but not bounded below. By [dagsamXIV]*Theorem 2.9, usco functions are bounded above in $\textup{{RCA}}_{0}^{\omega}+\textup{{QF-AC}}^{0,1}+\textup{{WKL}}$. below.

Theorem 2.3** ($\textup{{ACA}}_{0}^{\omega}$).**

The following are equivalent.

1. (a)

The Baire category theorem as in $\textup{{BCT}}_{[0,1]}$. 2. (b)

For usco $f:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous. 3. (c)

For usco $f:[0,1]\rightarrow{\mathbb{R}}$ which has an oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous. 4. (d)

For usco $f:[0,1]\rightarrow{\mathbb{R}}$ which is its own oscillation function, there is a point $x\in[0,1]$ where $f$ is continuous. 5. (e)

For usco and countably continuous $f:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous. 6. (f)

Any usco $f:[0,1]\rightarrow{\mathbb{R}}$ is bounded below on some interval, i.e. there exist $q\in{\mathbb{Q}}$ and $c,d\in[0,1]$ such that $(\forall y\in(c,d))(f(y)\geq q)$. 7. (g)

For usco $f:[0,1]\rightarrow{\mathbb{R}}^{+}$, there are $c,d\in[0,1]$ with $0<\inf_{x\in[c,d]}f(x)$.

Proof.

First of all, assume item (d) and fix a decreasing sequence of dense open sets $(O_{n})_{n\in{\mathbb{N}}}$. Define the nowhere dense closed set $X_{n}:=[0,1]\setminus O_{n}$ and consider $h:[0,1]\rightarrow{\mathbb{R}}$ as in (H). Following Theorems 1.16 and 1.18, item (d) yields a point of continuity $y\in[0,1]$ of $h$. If $\frac{1}{2^{m_{0}+1}}=h(y)>0$, then by definition $y\in X_{m_{0}}$ where $m_{0}\in{\mathbb{N}}$ is the least such number. Since $h$ is continuous at $y$, there is $N\in{\mathbb{N}}$ such that $z\in B(y,\frac{1}{2^{N}})$ implies $|h(z)-h(y)|<\frac{1}{2^{m_{0}+2}}$. However, $O_{m_{0}+2}$ is dense in $[0,1]$, implying there is $z_{0}\in B(y,\frac{1}{2^{N}})\cap O_{m_{0}+2}$. Since $h(z_{0})\leq\frac{1}{2^{m_{0}+3}}$ by definition, we obtain a contradiction. Hence, we must have $h(y)=0$ and the latter implies $y\in\cap_{n\in{\mathbb{N}}}O_{n}$ by definition, as required for $\textup{{BCT}}_{[0,1]}$.

Secondly, for item (b), we first formulate a proof (say in ${\textsf{{Z}}}_{2}^{\Omega}$) and then show how this proof goes through in $\textup{{ACA}}_{0}^{\omega}+\textup{{BCT}}_{[0,1]}$. Thus, fix lsco $f:[0,1]\rightarrow{\mathbb{R}}$ and define $C_{q}:=\{x\in[0,1]:f(x)\leq q\}$, which is closed by definition. Define $F_{q}$ as $C_{q}\setminus\textsf{int}(C_{q})$, where the open set $\textsf{int}(X)$ is the interior of $X$, i.e. those $x\in X$ such that there is $N\in{\mathbb{N}}$ with $B(x,\frac{1}{2^{N}})\subset X$. By definition, $F_{q}$ is closed and is nowhere dense, i.e. the Baire category theorem shows that there is y\in\big{(}[0,1]\setminus\cup_{q\in{\mathbb{Q}}}F_{q}\big{)}. The Baire category theorem is provable in ${\textsf{{Z}}}_{2}^{\Omega}$ by [dagsamVII]*§6.

We now show that for each $x\in[0,1]$ where $f$ is discontinuous, there is $q\in{\mathbb{Q}}$ such that $x\in F_{q}$, establishing that $f$ is continuous at the aforementioned point $y$, as required. Thus, let $f$ be discontinuous at $x_{0}\in[0,1]$ and note that $f$ cannot be usco at $x_{0}\in[0,1]$, i.e. we have

[TABLE]

Let $l_{0}$ be as in (2.1) and consider $q_{0}\in{\mathbb{Q}}$ such that $f(x_{0})<q_{0}<f(x_{0})+\frac{1}{2^{l_{0}}}$. By definition, $x_{0}\in F_{q_{0}}$, as required.

We now show how the above proof goes through in $\textup{{ACA}}_{0}^{\omega}+\textup{{BCT}}_{[0,1]}$. The (only) two obstacles are as follows:

• •

the definition of $\textsf{int}(X)$ involves quantification over ${\mathbb{R}}$, i.e. the former set cannot be defined in $\textup{{ACA}}_{0}^{\omega}$.

• •

the formula (2.1) involves quantification over ${\mathbb{R}}$, i.e. the numbers $l_{0}$ and $q_{0}$ cannot be defined in terms of $x_{0}$.

Both problems have (about) the same solution, as follows. For the second item, since $f$ is lsco, (2.1) is equivalent to

[TABLE]

where the underlined quantifier is crucial. Since (2.2) is decidable using $\exists^{2}$, the functional $\mu^{2}$ computes $l_{1}\in{\mathbb{N}}$, the least $l\in{\mathbb{N}}$ satisfying (2.2); clearly, $l=l_{1}+1$ then witnesses (2.1). Hence, $q_{0}$ from the previous paragraph is definable in terms of $x_{0}$ (and $f$ and $\mu^{2}$).

For the first item, i.e. relating to the interior of sets, the following formula expresses that $x\in F_{q}=(C_{q}\setminus\textsf{int}(C_{q})$, by definition:

[TABLE]

Similar to the second item and (2.1), since $f$ is lsco, (2.3) is equivalent to

[TABLE]

where again the underlined quantifier is crucial. Hence, we can define $F_{q}$ using $\exists^{2}$ and (2.4). Using an enumeration of ${\mathbb{Q}}$, one readily obtains an increasing sequence of closed nowhere dense sets. The rest of the proof now goes through. Since for lsco $f:[0,1]\rightarrow{\mathbb{R}}$, the function $-f$ is usco, this item is finished.

For item (e), it is clear that $h$ from (H) is countably continuous as it is constant on each $X_{n}$ and the complement of $\cup_{n\in{\mathbb{N}}}X_{n}$.

To prove item (f) from $\textup{{BCT}}_{[0,1]}$, fix usco $f:[0,1]\rightarrow{\mathbb{R}}$ and note that $C_{n}:=\{x\in[0,1]:f(x)\geq-n\}$ is closed and satisfies $[0,1]=\cup_{n\in{\mathbb{N}}}C_{n}$. By $\textup{{BCT}}_{[0,1]}$, at least one $C_{n}$ is not nowhere dense, as required for item (f). Now assume the latter and let $(X_{n})_{n\in{\mathbb{N}}}$ be an increasing sequence of closed sets such that $[0,1]=\cup_{n\in{\mathbb{N}}}X_{n}$. Define $\tilde{h}:[0,1]\rightarrow{\mathbb{R}}$ as follows: $\tilde{h}(x)=-n$ in case $x\in X_{n}$ and $n\in{\mathbb{N}}$ is the least such number. Similar to $h:[0,1]\rightarrow{\mathbb{R}}$ from (H), the function $\tilde{h}$ is usco. Item (f) provides $N\in{\mathbb{N}}$ and $c,d\in[0,1]$ such that $\tilde{h}(y)\geq-N$ for $y\in(c,d)$. By definition, we have $(c,d)\subset X_{N}$, i.e. the latter is not nowhere dense. Item (g) follows in the same way using $h$ from (H) and $C_{n}:=\{x\in[0,1]:f(x)\geq\frac{1}{2^{n}}\}$. ∎

Secondly, proofs in real analysis often use $C_{f}$ and $D_{f}$, the set of continuity and discontinuity points, as their starting points. The definition of continuity involves a quantifier over ${\mathbb{R}}$, i.e. these sets cannot be defined in general in e.g. ${\textsf{{Z}}}_{2}^{\omega}$. In light of the proof of Theorem 2.3, we can define these sets for usco functions as follows.

Theorem 2.4** ($\textup{{ACA}}_{0}^{\omega}$).**

For usco $f:[0,1]\rightarrow{\mathbb{R}}$, the sets $C_{f}$ and $D_{f}$ exist.

Proof.

First of all, it is a matter of definitions to show the equivalence between:

• •

$g:{\mathbb{R}}\rightarrow{\mathbb{R}}$ is continuous at $x\in{\mathbb{R}}$,

• •

$g:{\mathbb{R}}\rightarrow{\mathbb{R}}$ is usco and lsco at $x\in{\mathbb{R}}$.

Secondly, for lsco $f:[0,1]\rightarrow{\mathbb{R}}$, ‘$f$ is discontinuous at $x\in[0,1]$’ is equivalent to

[TABLE]

which expresses that $f$ is not usco at $x\in[0,1]$. Now, (2.5) is equivalent to

[TABLE]

where in particular the underlined quantifier in (2.6) has rational range due to $f$ being lsco. Since (2.6) is arithmetical, $\exists^{2}$ allows us to define $D_{f}$, and hence $C_{f}$. ∎

An important observation is that Theorem 2.4 only states that the set $C_{f}$ exists but does not claim it to be non-empty. The latter claim can only999In fact, it is consistent with ${\textsf{{Z}}}_{2}^{\omega}+\textup{{QF-AC}}^{0,1}$ that there are bounded usco functions on the unit interval that are everywhere discontinuous (see [dagsamXIV]*§3). be made in $\textup{{ACA}}_{0}^{\omega}$ if we have additional information about the function $f$, e.g. as in Theorem 2.7.

Thirdly, Theorem 2.3 has a number of fairly easy generalisations. There is also degree of robustness: we may similarly replace ‘measure zero’ by ‘measure at most $a\in(0,1)$’.

Theorem 2.5**.**

Theorem 2.3 still goes through with the following restrictions.

• •

Replace ‘continuous’ in the consequent of items (b)-(d) by:

regulated, (lower) quasi-continuituous, cadlag, Darboux, or lsco.

• •

Restrict ‘usco’ to ‘usco and such that $C_{f}$ has measure zero’.

• •

Restrict $\textup{{BCT}}_{[0,1]}$ to open sets such that $\cap_{n\in{\mathbb{N}}}O_{n}$ has measure zero.

Proof.

For the first item, we only need to derive $\textup{{BCT}}_{[0,1]}$ from items items (b)-(d) in the theorem with ‘continuity’ weakened to the notions from the corollary. This is a straightforward verification and we only establish the corollary for the weakest notion, namely lower quasi-continuity. Thus, assume item (b) with ‘lqco’ in the consequent and consider the real $y\in[0,1]$ as in the first paragraph of the proof of the theorem. If $\frac{1}{2^{m_{0}+1}}=h(y)>0$, then by definition $y\in X_{m_{0}}$ where $m_{0}\in{\mathbb{N}}$ is the least such number. Since $h$ is lqso at $y$, we have that for $\varepsilon=\frac{1}{2^{m_{0}+2}}$ and any $N\in{\mathbb{N}}$, there is $(a,b)\subset B(y,\frac{1}{2^{N}})$ such that $z\in(a,b)$ implies $h(z)>h(y)-\frac{1}{2^{m_{0}+2}}=\frac{1}{2^{m_{0}+2}}$. However, $O_{m_{0}+4}$ is dense in $[0,1]$, implying there is $z_{0}\in(a,b)\cap O_{m_{0}+4}$. Since $h(z_{0})\leq\frac{1}{2^{m_{0}+5}}$, we obtain a contradiction. Hence, we must have $h(y)=0$ and the latter implies $y\in\cap_{n\in{\mathbb{N}}}O_{n}$ by definition, as required for $\textup{{BCT}}_{[0,1]}$.

For the second item, consider the first paragraph of the proof of Theorem 2.3. Assuming $[0,1]=\cup_{n\in{\mathbb{N}}}X_{n}$, the usco function $h$ from (H) is such that $C_{f}=\emptyset$, i.e. definitely measure zero. Now proceed with the original proof and derive a contradiction. Thus, we may restrict the items (b)-(d) from Theorem 2.3 to usco $f$ such that $C_{f}$ has measure zero.

For the third item, the Cantor set can be defined in $\textup{{RCA}}_{0}$ (see [simpson2]*p. 129), and similar for ‘fat’ Cantor sets, i.e. closed nowhere dense sub-sets of $[0,1]$ that can have measure $1-\varepsilon$ for any $\varepsilon>0$. Thus, let $(C_{n})_{n\in{\mathbb{N}}}$ be a sequence of fat Cantor sets in $[0,1]$ such that $C_{n}$ has measure at least $1-\frac{1}{2^{n}}$ for all $n\in{\mathbb{N}}$. Now let $(O_{n})_{n\in{\mathbb{N}}}$ be any sequence of dense open sets in $[0,1]$ and note that $O_{n}\cap V_{n}$ is also open and dense, where $V_{n}=:[0,1]\setminus C_{n}$. Since $\cap_{n\in{\mathbb{N}}}V_{n}$ has measure zero, the third item in the theorem applies to $(O_{n}\cap V_{n})_{n\in{\mathbb{N}}}$, i.e. there is y\in\cap_{n\in{\mathbb{N}}}\big{(}O_{n}\cap V_{n}\big{)}\subset\cap_{n\in{\mathbb{N}}}O_{n}, as required for $\textup{{BCT}}_{[0,1]}$. ∎

Ironically, the third item of Theorem 2.5 suggests that the essence of $\textup{{BCT}}_{[0,1]}$, a fundamental statement about category, in fact involves measure theory.

Fourth, by Theorem 2.3, the constructive enrichment provided by oscillation functions does not change the strength of the semi-continuity lemma. Let us consider another constructive enrichment: a modulus for usco $f:[0,1]\rightarrow{\mathbb{R}}$ is any function $\Psi:[0,1]\rightarrow{\mathbb{R}}^{+}$ such that we have:

[TABLE]

Given a modulus, the semi-continuity lemma is provable in a weaker system.

Theorem 2.6** ($\textup{{ACA}}_{0}^{\omega}$).**

Let $f:[0,1]\rightarrow{\mathbb{R}}$ be usco with a modulus. Then $C_{f}\neq\emptyset$.

Proof.

By definition, for usco $f:[0,1]\rightarrow{\mathbb{R}}$, the set $\{x\in[0,1]:f(x)\geq a\}$ is closed for any $a\in{\mathbb{R}}$. Let $O_{a}$ be the complement of the previous set. When given a modulus $\Psi$, one readily defines $Y:[0,1]\rightarrow{\mathbb{R}}$ such that $B(y,Y(y))\subset O_{a}$ in case $y\in O_{a}$. Hence, $O_{a}$ is R2-open and the Baire category theorem for such sets is provable in $\textup{{ACA}}_{0}^{\omega}$ by [dagsamVII]*Theorem 7.10. One can now repeat the (modified) proof of item (b) in Theorem 2.3 in $\textup{{ACA}}_{0}^{\omega}$, noting that $\textsf{int}(C_{q})$ has an R2-open representation in light of the equivalence between (2.5) and (2.6). ∎

Fifth, comparing Theorems 2.3 and 2.6, the constructive enrichment provided by oscillation functions does not change the strength of the semi-continuity lemma, while a modulus for usco does make a significant difference. We now show that the constructive enrichment provided by the usual definition of ‘Baire 1’ is significant.

Theorem 2.7** ($\textup{{ACA}}_{0}^{\omega}$).**

Let $f:[0,1]\rightarrow{\mathbb{R}}$ be usco and let $(f_{n})_{n\in{\mathbb{N}}}$ be a sequence of continuous functions that converges pointwise to $f$ on $[0,1]$. Then $C_{f}\neq\emptyset$.

Proof.

We use the proof of (a) $\rightarrow$ (b) from Theorem 2.3. In this proof, one defines a sequence of closed and nowhere dense sets $(F_{q})_{q\in{\mathbb{Q}}}$ such that the union contains $D_{f}$ for lsco $f:[0,1]\rightarrow{\mathbb{R}}$. Applying $\textup{{BCT}}_{[0,1]}$, the set $C_{f}$ is observed to be non-empty. We show that the extra information provided by the Baire 1 representation of $f$ allows us to define an R2-representation for $F_{q}$. Instead of $\textup{{BCT}}_{[0,1]}$, we can then apply the Baire category theorem for R2-representations, which is provable in $\textup{{ACA}}_{0}^{\omega}$ by [dagsamVII]*Theorem 7.10. In particular, we note that by (the proof of) [dagsamXIV]*Theorem 2.9, there is $\Phi:({\mathbb{R}}\times{\mathbb{N}})\rightarrow{\mathbb{R}}$ such that $\Phi(x,N)$ equals $\inf_{y\in B(x,\frac{1}{2^{N}})}f(y)$ for Baire 1 $f$.

Let $f:[0,1]\rightarrow{\mathbb{R}}$ be lsco and let $(f_{n})_{n\in{\mathbb{N}}}$ be a sequence of continuous functions with pointwise limit $f$ on the unit interval. Recall the set $F_{q}\subset[0,1]$ defined as those $x\in[0,1]$ satisfying (2.4), where the latter is equivalent to (2.3). Define $O_{q}:=[0,1]\setminus F_{q}$ and note that ‘$x\in O_{q}$’ is exactly

[TABLE]

In case $x\in O_{q}$ satisfies the second disjunct in (2.7), we use $\mu^{2}$ to find the least $N\in{\mathbb{N}}$ such that \big{(}B(x,\frac{1}{2^{N}})\cap{\mathbb{Q}}\big{)}\subset O_{q}. Now, since $f$ is lsco, the latter implies $B(x,\frac{1}{2^{N}})\subset O_{q}$, as required for a R2-representation. In case $x\in O_{q}$ satisfies the first disjunct in (2.7), observe that

[TABLE]

as $f$ is lsco. Since the infimum in the right-hand side of (2.8) is given by a function $\Phi:({\mathbb{R}}\times{\mathbb{N}})\rightarrow{\mathbb{R}}$, we may use $\mu^{2}$ to find the least $N_{0}\in{\mathbb{N}}$ such that $q<\inf_{y\in B(x,\frac{1}{2^{N_{0}}})}f(y)$. By the definition of $O_{q}$, we have $B(x,\frac{1}{2^{N_{0}}})\subset O_{q}$, as required for a R2-representation. Hence, we have obtained a R2-representation of $O_{q}$ based on the case distinction (decidable by $\exists^{2}$) provided by (2.7). ∎

Next, it is well-known that usco functions are Baire 1, but this fact is not provable in ${\textsf{{Z}}}_{2}^{\omega}$ by Corollary 2.8. In particular, the previous proof does not go through for usco functions (without a Baire 1 representation) as by [dagsamXIV]*Theorem 2.32, the supremum principle for usco functions implies $\textup{{NIN}}_{[0,1]}$.

Corollary 2.8** ($\textup{{ACA}}_{0}^{\omega}$).**

The statement

any usco function $f:[0,1]\rightarrow{\mathbb{R}}$ is Baire 1**

both implies $\textup{{BCT}}_{[0,1]}$ and the principle

open:* open sets in the unit interval have RM-codes.*

Proof.

The first part is immediate from Theorem 2.3 and the theorem. For the second part, a set $C\subset[0,1]$ is closed if and only if $\mathbb{1}_{C}$ is usco. Now, in case $x\in O:=[0,1]\setminus C$, we have $(\exists N\in{\mathbb{N}})(0=\sup_{y\in B(x,\frac{1}{2^{N}})}\mathbb{1}_{C}(y))$. As noted in the proof of the theorem, the latter supremum is not just notation but given by a functional in case the function is also Baire 1. Hence, we can use $\mu^{2}$ to define $Y:{\mathbb{R}}\rightarrow{\mathbb{N}}$ such that $B(x,\frac{1}{2^{Y(x)}})\subset O$ in case $x\in O$. As $\mu^{2}$ returns the least witness, $\cup_{q\in O\cap{\mathbb{Q}}}B(q,\frac{1}{2^{Y(q)+1}})$ is an RM-code for $O$, and we are done. ∎

The principle open in Corollary 2.8 is ‘explosive’ in that $\Pi_{1}^{1}\text{-{{CA}}}_{0}^{\omega}+\textup{{open}}$ proves $\Pi_{2}^{1}\text{-{{CA}}}_{0}$ (see [dagsamXI]), while $\Pi_{1}^{1}\text{-{{CA}}}_{0}^{\omega}$ is $\Pi_{3}^{1}$-conservative over $\Pi_{1}^{1}\text{-{{CA}}}_{0}$ (see [yamayamaharehare]). As an exercise, the first centred principle of Corollary 2.8 is similarly explosive when restricted to usco functions that are continuous almost everywhere. We also have the following stronger result in a stronger system.

Corollary 2.9** ($\textup{{ACA}}_{0}^{\omega}+\Pi_{1}^{1}\text{-{{CA}}}_{0}$).**

Let $f:[0,1]\rightarrow[0,1]$ be usco and effectively Baire $n$ for $n\geq 2$. Then $C_{f}\neq\emptyset$.

Proof.

The supremum principle for bounded effectively Baire $n$ ($n\geq 2$) functions is provable in $\textup{{ACA}}_{0}^{\omega}+\Pi_{1}^{1}\text{-{{CA}}}_{0}$ by [dagsamXIV]*Theorem 2.22. ∎

Finally, we show that e.g. items (a) and (f) of Theorem 2.3 have a proof in $\textup{{ACA}}_{0}^{\omega}$ for Baire 1 functions.

Theorem 2.10** ($\textup{{ACA}}_{0}^{\omega}$).**

Let $f:[0,1]\rightarrow{\mathbb{R}}$ be Baire 1.

• •

There exists $x\in[0,1]$ such that $f$ is continuous at $x$.

• •

There exist $N\in{\mathbb{N}}$ and $c,d\in[0,1]$ such that $(\forall y\in(c,d))(|f(y)|\leq N+1)$.

• •

The oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$ exists.

Proof.

Let $(f_{n})_{n\in{\mathbb{N}}}$ be a sequence of continuous functions with pointwise limit $f$. By [dagsamXIV]*Cor. 2.5, there is an associated sequence of RM-codes $(\Phi_{n})_{n\in{\mathbb{N}}}$. For the second item, define the closed set $C_{n}$ as follows:

[TABLE]

Thanks to the RM-codes $\Phi_{n}$ for $f_{n}$, the formula $(\forall m\in{\mathbb{N}})(f_{m}(x)\leq n)$ is (second-order) $\Pi_{1}^{0}$. Hence, the sets $C_{n}$ have corresponding RM-codes by [simpson2]*II.5.7. Since $[0,1]=\cup_{n\in{\mathbb{N}}}C_{n}$, the Baire category theorem for RM-codes of open sets (provable in $\textup{{RCA}}_{0}^{\omega}$ by [simpson2]*II.5.8), yields that at least one $C_{n}$ is not nowhere dense.

For the first item, define $D_{m,n}:=\{x\in[0,1]:(\forall k\geq m)(|f_{k}(x)-f_{m}(x)|\leq\frac{1}{2^{n}})$. As in the previous paragraph, each $D_{m,n}$ is RM-closed. To define the interior of the latter sets, put $x\in\textsf{int}(D_{m,n})$ if and only if $(\exists N\in{\mathbb{N}})(\forall r\in B(x,\frac{1}{2^{N}})\cap{\mathbb{Q}})(r\in D_{m,n})$. Due to the continuity of the $f_{n}$, $x\in\textsf{int}(D_{m,n})$ is equivalent to

[TABLE]

i.e. the ‘real’ definition of the interior of $D_{m,n}$ As in the proof of Theorem 2.3, define $F_{m,n}:=D_{m,n}\setminus\textsf{int}(D_{m,n})$, which is RM-closed and nowhere dense, and note that each point where $f$ is discontinuous, is included in $\cup_{m,n\in{\mathbb{N}}}F_{m,n}$. The Baire category theorem for RM-codes (provable in $\textup{{RCA}}_{0}$ by [simpson2]*II.5.7) finishes the proof.

Finally, for the third item. as noted in the proof of Theorem 2.7, we have access to the supremum operator for Baire 1 functions following [dagsamXIV]*Theorem 2.9. Hence, one readily defines the oscillation function using $\exists^{2}$. ∎

In conclusion, we have established some equivalences involving $\textup{{BCT}}_{[0,1]}$ and the semi-continuity lemma. We have also shown that the latter become much easier to prove when assuming e.g. a Baire 1 representation or a modulus of usco.

2.3. Continuity properties of Baire one star functions

We generalise the equivalences from the previous section. In particular, we show that Theorem 2.3 goes through if we replace ‘usco’ by ‘bounded Baire $1^{*}$’.

First of all, we have the following theorem establishing a decomposition theorem for Baire $1^{*}$ functions.

Theorem 2.11** ($\textup{{ACA}}_{0}^{\omega}$).**

For bounded Baire $1^{*}$ $f:[0,1]\rightarrow{\mathbb{R}}$, there exists usco $g_{0}:[0,1]\rightarrow{\mathbb{R}}$ and lsco $g_{1}:[0,1]\rightarrow{\mathbb{R}}$ such that $f=g_{0}+g_{1}$ on $[0,1]$.

Proof.

The proof of [mentoch]*Lemma 5 goes through with no modification since we assume an upper and lower bound for $f$. ∎

We study bounded Baire $1^{*}$ functions as otherwise the proof of Theorem 2.11 would need NCC and MCC from [dagsamIX], which are rather non-trivial fragments of the Axioms of Choice (though provable in ${\textsf{{Z}}}_{2}^{\Omega}$).

Secondly, the previous decomposition theorem gives rise to the following equivalences, where we only treat some basic cases compared to Theorem 2.3.

Theorem 2.12** ($\textup{{ACA}}_{0}^{\omega}$).**

The following are equivalent.

1. (a)

The Baire category theorem as in $\textup{{BCT}}_{[0,1]}$. 2. (b)

For Baire $1^{*}$ $f:[0,1]\rightarrow[0,1]$, there is $x\in[0,1]$ where $f$ is continuous. 3. (c)

*For Baire $1^{*}$ $f:[0,1]\rightarrow[0,1]$ which has an oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous. *

Proof.

Assume $\textup{{BCT}}_{[0,1]}$ and note that Theorem 2.3 implies that for usco $g_{0}$ and lsco $g_{1}$, the sets $C_{g_{0}}$ and $C_{g_{1}}$ are dense, and hence the intersection is non-empty. Theorem 2.11 now implies items (b)-(c).

Now assume item (c) and suppose $(X_{n})_{n\in{\mathbb{N}}}$ is an increasing sequence of nowhere dense sets such that $[0,1]=\cup_{n\in{\mathbb{N}}}X_{n}$. Now consider $h:[0,1]\rightarrow{\mathbb{R}}$ from (H), which is Baire $1^{*}$ as $f_{\upharpoonright X_{n}}$ is continuous for any $n\in{\mathbb{N}}$. Item (c) provides a point of continuity, which yields $x\not\in\cup_{n\in{\mathbb{N}}}X_{n}$ as in the proof of Theorem 2.3, as required. ∎

By contrast, we have the following theorem.

Theorem 2.13** ($\textup{{ACA}}_{0}^{\omega}$).**

For $f:[0,1]\rightarrow[0,1]$ in Baire $1^{*}$ and Baire 1, $C_{f}\neq\emptyset$.

Proof.

The decomposition $f=g_{0}+g_{1}$ from Theorem 2.11 is provided by the proof of [mentoch]*Lemma 5. By the latter, a Baire 1 representation of $f$ also provides a Baire 1 representation of $g_{0}$ and $g_{1}$. Now apply Theorem 2.7 to conclude that $C_{g_{0}}$ and $C_{g_{1}}$ are non-empty (and dense). Then $C_{g_{0}}\cap C_{g_{1}}\neq\emptyset$, and we are done. ∎

Finally, we mention a class between the continuous and the Baire $1^{*}$ functions, namely the Baire 1*∗∗* functions introduced in [pawla]. Trivially, Baire $1^{**}$ functions have a point of continuity, i.e. we cannot obtain equivalences as in Theorem 2.12.

2.4. The uniform boundedness principle

In this section, we connect the Baire category theorem and the uniform boundedness principle from [bro].

First of all, the uniform boundedness principle can be obtained by applying the Baire category theorem to the pointwise boundedness (see Def. 2.14) condition in the former, as done in the second-order proof ([simpson2]*II.10.8). One readily observes that this application of the Baire category theorem does not require continuity, but in fact immedately generalises to lsco functions, as has been established in e.g. [bro, kozy, nguyen1]. Moreover, by [bro]*Theorem 1, one can characterise meagreness in terms of the uniform bounded principle for lsco functions. In this light, the RM-study of the uniform boundedness principle for lsco functions from [bro] is only natural.

Secondly, we need the following definitions to formulate Theorem 2.15.

Definition 2.14**.**

A sequence of functions $(f_{n})_{n\in{\mathbb{N}}}$ is

• •

(pointwise) bounded* on $X$ if $(\forall x\in X)(\exists N\in{\mathbb{N}})(\forall n\in{\mathbb{N}})(f_{n}(x)\leq N)$,*

• •

uniformly bounded* on $X$ if $(\exists M\in{\mathbb{N}})(\forall x\in X,m\in{\mathbb{N}})(f_{m}(x)\leq M)$.*

Theorem 2.15** ($\textup{{ACA}}_{0}^{\omega}$).**

The following are equivalent.

1. (a)

The Baire category theorem as in $\textup{{BCT}}_{[0,1]}$. 2. (b)

(Uniform boundedness principle [bro])* A sequence of lsco functions that is pointwise bounded on $[0,1]$, is uniformly bounded on some $(c,d)\subset[0,1]$.*

Proof.

Assume $\textup{{BCT}}_{[0,1]}$ and let $(f_{n})_{n\in{\mathbb{N}}}$ be a sequence of lsco functions that is pointwise bounded on $[0,1]$. By definition, the set $E_{n,N}:=\{x\in[0,1]:f_{n}(x)\leq N\}$ is closed, and so is $F_{N}:=\cap_{n\in{\mathbb{N}}}E_{n,N}$. By pointwise boundedness, we have $[0,1]=\cup_{N\in{\mathbb{N}}}F_{N}$ and $\textup{{BCT}}_{[0,1]}$ implies there is $N_{0}\in{\mathbb{N}}$ such that $(c,d)\subset F_{N_{0}}$ for some $c,d\in[0,1]$. This interval is as required for uniform boundedness in item (b).

For the reversal, assume item (b) and define $\hat{h}:[0,1]\rightarrow{\mathbb{R}}$ as follows:

[TABLE]

where $(X_{n})_{n\in{\mathbb{N}}}$ is an increasing sequence of closed sets such that $[0,1]=\cup_{n\in{\mathbb{N}}}X_{n}$. Now define $\hat{h}_{n}:[0,1]\rightarrow{\mathbb{R}}$ as follows: $\hat{h}_{n}(x):=\hat{h}(x)$ in case $\hat{h}(x)<n$, and $\hat{h}_{n}(x):=n$ otherwise. One readily verifies that the functions $\hat{h},\hat{h}_{n}$ are lsco using the definition. Now, $(\hat{h}_{n})_{n\in{\mathbb{N}}}$ is pointwise bounded on $[0,1]$, as $(\forall x\in X)(\forall n\in{\mathbb{N}})(\hat{h}_{n}(x)\leq\hat{h}(x))$ by definition. Apply item (b) to find $(c,d)\subset[0,1]$ where $(\hat{h}_{n})_{n\in{\mathbb{N}}}$ is uniformly bounded, i.e. $(\exists M\in{\mathbb{N}})(\forall m\in{\mathbb{N}},x\in(c,d))(\hat{h}_{m}(x)\leq M)$. Taking $m=M+1$, we note that $(c,d)\subset X_{M}$, as required for $\textup{{BCT}}_{[0,1]}$. ∎

Next, basic properties of metric spaces imply NIN in light of [dagsamX]*§3.2.3. These results are based on the observation that an injection from $[0,1]\rightarrow{\mathbb{N}}$ gives rise to a ‘strange’ metric on $[0,1]$. We have not been able to obtain similarly ‘strange’ norms on basic vector spaces. Without such a norm, it seems we cannot obtain an equivalence between $\textup{{BCT}}_{[0,1]}$ and associated theorems about Banach spaces.

Finally, the following theorem is often proved using the Baire category theorem:

for continuous $f:[0,+\infty)\rightarrow{\mathbb{R}}$ such that $\lim_{n\rightarrow\infty}f(nx)=0$ for all $x\in[0,+\infty)$, we have $\lim_{x\rightarrow+\infty}f(x)=0$.

Like the uniform boundedness principle, the centred statement generalises to lsco functions, which is an interesting exercise for the reader.

2.5. Continuity properties of cliquish functions

We establish equivalences between $\textup{{BCT}}_{[0,1]}$ and basic theorems about cliquish and simply continuous functions (Theorems 2.16 and 2.18), which makes these basic theorems unprovable in ${\textsf{{Z}}}_{2}^{\omega}$. By contrast, the associated theorems for quasi-continuous functions are provable in $\textup{{ACA}}_{0}^{\omega}$ (Theorem 2.19). We discuss the intimate connection between cliquishness, simple continuity, and quasi-continuity in Remark 2.20.

First of all, we have the following results involving continuity where we note that item (e) deals with any function that is totally discontinuous. We also note that item (b) expresses the non-trivial part of the equivalence between ‘cliquish’ and ‘pointwise discontinuous’ on the reals, which was already observed by Dini ([dinipi]*§63) and is discussed in detail in Remark 2.20.

Theorem 2.16** ($\textup{{ACA}}_{0}^{\omega}$).**

The following are equivalent.

1. (a)

The Baire category theorem as in $\textup{{BCT}}_{[0,1]}$. 2. (b)

For cliquish $f:[0,1]\rightarrow{\mathbb{R}}$ which has an oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous. 3. (c)

For cliquish $f:[0,1]\rightarrow{\mathbb{R}}$ which has an oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is lqco. 4. (d)

For cliquish and uqco $f:[0,1]\rightarrow{\mathbb{R}}$ which has an oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous. 5. (e)

For totally discontinuous $f:[0,1]\rightarrow{\mathbb{R}}$ with oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, there is $N\in{\mathbb{N}}$ and $c,d\in[0,1]$ with $\textup{{osc}}_{f}(x)\geq\frac{1}{2^{N}}$ for $x\in(c,d)$.

Proof.

First of all, assume item (b) and fix a decreasing sequence of dense open sets $(O_{n})_{n\in{\mathbb{N}}}$. Define the nowhere dense closed set $X_{n}:=[0,1]\setminus O_{n}$ and consider $h:[0,1]\rightarrow{\mathbb{R}}$ as in (H). Following Theorem 1.18, item (b) yields a point of continuity $y\in[0,1]$ of $h$. If $\frac{1}{2^{m_{0}+1}}=h(y)>0$, then by definition $y\in X_{m_{0}}$ where $m_{0}\in{\mathbb{N}}$ is the least such number. Since $h$ is continuous at $y$, there is $N\in{\mathbb{N}}$ such that $z\in B(y,\frac{1}{2^{N}})$ implies $|h(z)-h(y)|<\frac{1}{2^{m_{0}+2}}$. However, $O_{m_{0}+4}$ is dense in $[0,1]$, implying there is $z_{0}\in B(y,\frac{1}{2^{N}})\cap O_{m_{0}+3}$. Since $h(z_{0})\leq\frac{1}{2^{m_{0}+5}}$, we obtain a contradiction. Hence, we must have $h(y)=0$ and the latter implies $y\in\cap_{n\in{\mathbb{N}}}O_{n}$ by definition, as required for $\textup{{BCT}}_{[0,1]}$. As $h$ from (H) is usco by Theorem 1.18, item (d) also applies. For item (c), one uses the proof of Theorem 2.5.

Secondly, assume $\textup{{BCT}}_{[0,1]}$ and define $D_{m}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{m}}\}$, which is closed by definition (or by Theorem 1.17). Suppose $D_{f}=\cup_{n\in{\mathbb{N}}}D_{n}$ equals $[0,1]$. By $\textup{{BCT}}_{[0,1]}$, there is $n_{0}\in{\mathbb{N}}$ such that $D_{n_{0}}$ is not nowhere dense, i.e. there is $[a,b]\subset D_{n_{0}}$. Now fix $x_{0}\in[0,1]$, $\varepsilon_{0}:=\frac{1}{2^{n_{0}+1}}$, and $N_{0}\in{\mathbb{N}}$ such that $B(x_{0},\frac{1}{2^{N_{0}}})\subset(a,b)$. Since $f$ is cliquish, there is an interval $(c,d)\subset B(x_{0},\frac{1}{2^{N_{0}}})$ such that for all $z,w\in(c,d)$, we have $|f(z)-f(w)|<\varepsilon_{0}$. The latter implies that $\textup{{osc}}_{f}(z)\leq\varepsilon_{0}$ for $z\in(c,d)$, which however contradicts the fact that $z\in(c,d)\subset D_{n_{0}}$. Hence, $D_{f}$ does not equal $[0,1]$, as required for item (b).

Fourth, item (d) follows since $h$ from (H) is usco by Theorem 1.18.

Fifth, let $f:[0,1]\rightarrow{\mathbb{R}}$ be as in item (e) and define the closed set $D_{k}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{k}}\}$. By assumption, $[0,1]=\cup_{k\in{\mathbb{N}}}D_{k}$ and $\textup{{BCT}}_{[0,1]}$ implies there is $k_{0}\in{\mathbb{N}}$ and $(c,d)\subset[0,1]$ such that $(c,d)\subset D_{k_{0}}$, as required. For the reversal, assume item (e) and let $f:[0,1]\rightarrow{\mathbb{R}}$ be cliquish with oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$. In case $C_{f}\neq\emptyset$, we are done in light of item (b). In case $C_{f}=\emptyset$, $f$ is totally discontinuous and we can apply item (e). Let $N_{0}\in{\mathbb{N}}$ and $c,d\in[0,1]$ be such that $\textup{{osc}}_{f}(x)\geq\frac{1}{2^{N_{0}}}$ for $x\in(c,d)$. Now fix $\varepsilon_{0}>0$ and $x_{0}\in(c,d)$ such that $\varepsilon_{0}<\frac{1}{2^{N_{0}}}$ and $B(x_{0},\varepsilon_{0})\subset(c,d)$; as $f$ is cliquish, there is an interval $(a,b)\subset B(x_{0},\varepsilon_{0})$ such that for all $x,y\in(a,b)$, we have $|f(x)-f(y)|<\varepsilon_{0}$. However, this implies that $\textup{{osc}}_{f}(z)\leq\frac{1}{2^{N_{0}}}$ for $z\in(a,b)$, contradicting $\textup{{osc}}_{f}(z)>\frac{1}{2^{N_{0}}}$ by $z\in(a,b)\subset(c,d)$. ∎

Secondly, the next theorem is motivated by the supremum principle for cliquish functions; this principle implies $\textup{{NIN}}_{[0,1]}$ by [dagsamXIV]*Theorem 2.32 and states the existence of $F:{\mathbb{Q}}^{2}\rightarrow{\mathbb{R}}$ such that $F(p,q)=\sup_{x\in[p,q]}f(x)$ for $p,q\in[0,1]\cap{\mathbb{Q}}$. Perhaps surprisingly, the above equivalences for $\textup{{BCT}}_{[0,1}$ still go through if we restrict to cliquish functions that have a supremum functional.

Theorem 2.17** ($\textup{{ACA}}_{0}^{\omega}+\textup{{QF-AC}}^{0,1}$).**

The following are equivalent.

1. (a)

The Baire category theorem as in $\textup{{BCT}}_{[0,1]}$. 2. (b)

For cliquish $f:[0,1]\rightarrow{\mathbb{R}}$ with a supremum functional and oscillation functional, there is $x\in[0,1]$ where $f$ is continuous.

Proof.

The first item implies the second item by Theorem 2.16. Now assume the second item and let $(X_{n})_{n\in{\mathbb{N}}}$ be an increasing sequence of closed nowhere dense sets such that $[0,1]=\cup_{n\in{\mathbb{N}}}X_{n}$. Define $Z(x)$ as the least $n\in{\mathbb{N}}$ such that $x\in X_{n}$ and $e(x):=\sum_{n=0}^{Z(x)+1}\frac{x^{n}}{n!}$, implying $e(x)<e^{x}$ for $x\in[0,1]$ and $\sup_{x\in[p,q]}e(x)=e^{q}$ by definiton. To show that $\lambda x.e(x)$ is cliquish, fix $x_{0}\in[0,1]$ and consider

[TABLE]

to which the usual ‘epsilon over three’ trick applies as follows: the middle term can be made arbitrarily small thanks to the uniform continuity of $\lambda x.e^{x}$ on $[0,1]$. The other two terms can be made arbitrarily small by picking large enough $k\in{\mathbb{N}}$ and picking $x_{1}\in O_{k}:=[0,1]\setminus X_{k}$ close enough to $x_{0}$ (using the density of the sets $O_{n}$). Indeed, $B(x_{1},\frac{1}{2^{N_{0}}})\subset O_{k}$ for some $N_{0}\in{\mathbb{N}}$, implying that $Y(w)\geq k$ for $w$ in the former ball, i.e. $e(w)$ approaches $e^{w}$ as $k$ grows. Since $\lambda x.e(x)$ is totally discontinuous, item (b) yields a contradiction. Hence, there must be $y\not\in\cup_{n\in{\mathbb{N}}}X_{n}$ as required for $\textup{{BCT}}_{[0,1]}$, and we are done. ∎

Thirdly, as discussed in Remark 2.20, the sico functions yields a class between the quasi-continuous and cliquish ones. As it happens, we can restrict to sico functions in Theorem 2.16 if we deal with sequentially101010A function $f:[0,1]\rightarrow{\mathbb{R}}$ is sequentially sico if for any sequence of open sets $(G_{n})_{n\in{\mathbb{N}}}$, there are sequences $(O_{n})_{n\in{\mathbb{N}}}$ and $(N_{n})_{n\in{\mathbb{N}}}$ of open and nowhere dense sets with $f^{-1}(G_{n})=O_{n}\cup{N_{n}}$. The proof that sico functions are cliquish (see [nieuwbronna2]*Theorem 2.1 and 2.2) goes through without extra induction or fragments of the Axiom of Choice if we assume sequentially sico functions. sico functions. This restriction is interesting as e.g. Thomae’s function from (T) is cliquish but not sico.

Theorem 2.18** ($\textup{{ACA}}_{0}^{\omega}+\textup{{QF-AC}}^{0,1}$).**

The following are equivalent.

1. (a)

The Baire category theorem as in $\textup{{BCT}}_{[0,1]}$. 2. (b)

For sequentially sico $f:[0,1]\rightarrow{\mathbb{R}}$, there is $x\in[0,1]$ where $f$ is continuous.

Proof.

First of all, sico functions are cliquish (say in ZFC) while the proof of [nieuwbronna2]*Theorem 2.1 immediately establishes that sequentially sico functions are cliquish, working over $\textup{{ACA}}_{0}^{\omega}+\textup{{BCT}}_{[0,1]}$. Hence, item (b) immediately follows from $\textup{{BCT}}_{[0,1]}$ via Theorem 2.16.

Secondly, let $(X_{n})_{n\in{\mathbb{N}}}$ be an increasing sequence of closed and nowhere dense sets such that $[0,1]=\cup_{n\in{\mathbb{N}}}X_{n}$ and consider $h:[0,1]\rightarrow{\mathbb{R}}$ as in (H). Fix $G\subset{\mathbb{R}}$ and consider the following two cases which show that $h$ is (sequentially) sico.

• •

In case $(\forall n\in{\mathbb{N}})(\exists m>n)(\frac{1}{2^{m+1}}\in G)$, we have $h^{-1}(G)=\cup_{n\in{\mathbb{N}}}X_{n}=[0,1]$.

• •

In case $n_{0}\in{\mathbb{N}}$ is the least $n$ with $(\forall m>n)(\frac{1}{2^{m+1}}\not\in G)$, then $h^{-1}(G)=X_{n_{0}}$.

Note that $\mu^{2}$ can find the number $n_{0}$ from the second item and decide which case holds, i.e. $h$ is also sequentially sico. Following Theorem 1.16, item (b) now provides a point of continuity for $h$, and $\textup{{BCT}}_{[0,1]}$ readily follows. ∎

Folllowing [nieuwbronna2]*§3, it seems that Theorem 2.18 can be generalised to pseudo-continuity, a notion equivalent to cliquishness where the inverse image of open sets is the union of an open and a meagre set.

Fourth, while quasi-continuous functions can be quite ‘wild’ in light of Remark 2.20, their basic properties are readily obtained in relatively weak systems by Theorem 2.19. Comparing to Theorem 2.16, the latter result is all the more surprising since ‘cliquish’ is quite close to ‘quasi-continuous’, the former essentially being the closure of the latter under sums, as also discussed in Remark 2.20.

Theorem 2.19** ($\textup{{ACA}}_{0}^{\omega}$).**

For quasi-continuous $f:[0,1]\rightarrow{\mathbb{R}}$, we have the following:

• •

the set $C_{f}$ exists and is dense,

• •

there is a sequence $(D_{n})_{n\in{\mathbb{N}}}$ of R2-closed nowhere dense sets with $D_{f}=\cup_{n\in{\mathbb{N}}}D_{n}$,

• •

the oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$ exists.

Proof.

Fix quasi-continuous $f:[0,1]\rightarrow{\mathbb{R}}$ and use $\exists^{2}$ to define $x\in O_{m}$ in case

[TABLE]

By quasi-continuity, the formula (2.10) is equivalent to

[TABLE]

which immediately implies that $O_{m}$ is open. Apply $\mu^{2}$ to (2.10) to obtain an R2-representation of $O_{m}$. Now define $D_{m}:=[0,1]\setminus O_{m}$ and note that $D_{f}:=\cup_{m\in{\mathbb{N}}}D_{m}$ contains all points where $f$ is discontinuous (essentially by definition). By [dagsamVII]*Theorem 7.10, $\textup{{ACA}}_{0}^{\omega}$ proves $\textup{{BCT}}_{[0,1]}$ for R2-open sets, i.e. the first and second item now follow. Finally, by [dagsamXIV]*Theorem 2.9, the supremum and infimum of $f$ exist (uniformly on any interval) given $\exists^{2}$. Hence, the oscillation function as in the third item is readily defined, where we note that $D_{m}$ is by definition $\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{m}}\}$, i.e. the usual definition. ∎

Finally, we discuss general properties of quasi-continuous and cliquish functions.

Remark 2.20**.**

First of all, the class of cliquish functions on ${\mathbb{R}}$ has nice technical and conceptual properties, as witnessed by the following list.

• •

The class of cliquish functions is exactly the class of sums of quasi-continuous functions ([bors, quasibor2, malin]). In particular, cliquish functions are closed under sums while quasi-continuous ones are not.

• •

The pointwise limit (if it exists) of quasi-continuous functions, is always cliquish ([holausco]*Cor. 2.5.2).

• •

Similar to Baire 1 functions, cliquish functions are exactly the limits of lqco and uqco sequences (see [ewert2]).

• •

The set $C_{f}$ is dense in ${\mathbb{R}}$ if and only if $f:{\mathbb{R}}\rightarrow{\mathbb{R}}$ is cliquish ([bors, dobo, dinipi]), i.e. the cliquish functions are exactly the pointwise discontinuous ones. The forward implication is trivial, while the other one is not by Theorem 2.16.

• •

The simply continuous functions on ${\mathbb{R}}$ yield a class intermediate between the quasi-continuous and cliquish ones (see [bors]).

Secondly, quasi-continuous functions can be quite ‘wild’: if $\mathfrak{c}$ is the cardinality of ${\mathbb{R}}$, there are $2^{\mathfrak{c}}$ non-measurable quasi-continuous $[0,1]\rightarrow{\mathbb{R}}$-functions and $2^{\mathfrak{c}}$ measurable non-Borel quasi-continuous $[0,1]\rightarrow[0,1]$-functions (see [holaseg]). Also, the class of quasi-continuous functions is closed under taking transfinite limits ([nieuwebronna]).

2.6. Continuity properties of Baire one functions

We establish equivalences between $\textup{{BCT}}_{[0,1]}$ and basic theorems about Baire 1 functions (Theorem 2.23), which makes the latter unprovable in ${\textsf{{Z}}}_{2}^{\omega}$. By Theorem 2.7, basic theorems about Baire 1 functions are provable in weak systems, explaining why we need equivalent definitions of Baire 1 as in Definition 2.21.

First of all, there are a surprisingly large number of rather diverse equivalent definitions of ‘Baire 1’ on the reals ([leebaire, beren, koumer]), including the following ones by [koumer]Theorem 2.3 and [kura]§34, VII.

Definition 2.21**.**

For a function $f:[0,1]\rightarrow{\mathbb{R}}$, we say that

• •

$f$* is fragmented if for any $\varepsilon>0$ and closed $C\subset[0,1]$, there is non-empty relatively111111For $A\subseteq B\subset{\mathbb{R}}$, we say that $A$ is relatively open (in $B$) if for any $a\in A$, there is $N\in{\mathbb{N}}$ such that $B(x,\frac{1}{2^{N}})\cap B\subset A$. Note that $B$ is always relatively open in itself. open $O\subset C$ such that $\textup{{diam}}(f(O))<\varepsilon$,*

• •

$f$* is $B$-measurable of class 1 if for every open $Y\subset{\mathbb{R}}$, the set $f^{-1}(Y)$ is ${\bf F}_{\sigma}$, i.e. a union over ${\mathbb{N}}$ of closed sets.*

The diameter of a set $X$ of reals is defined as usual, namely $\textup{{diam}}(X):=\sup_{x,y\in X}|x-y|$, where the latter supremum need not exist for Definition 2.21.

Secondly, fragments of the induction axiom are sometimes used in an essential way in second-order RM (see e.g. [neeman]). An important role of induction is to provide ‘finite comprehension’ (see [simpson2]*X.4.4). We shall need the following fragment of finite comprehension for Theorem 2.23 and in Section 3.

Principle 2.22** ($\textup{{IND}}_{{\mathbb{R}}}$).**

For $F:({\mathbb{R}}\times{\mathbb{N}})\rightarrow{\mathbb{N}},k\in{\mathbb{N}}$, there is $X\subset{\mathbb{N}}$ such that

[TABLE]

Thirdly, we have the following results for Baire 1 functions as in Def. 2.21.

Theorem 2.23** ($\textup{{ACA}}_{0}^{\omega}+\textup{{IND}}_{{\mathbb{R}}}$).**

The following are equivalent.

1. (a)

The Baire category theorem as in $\textup{{BCT}}_{[0,1]}$. 2. (b)

For fragmented $f:[0,1]\rightarrow{\mathbb{R}}$ which has an oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous. 3. (c)

For $B$-measurable of class 1 and cliquish $f:[0,1]\rightarrow{\mathbb{R}}$ which has an oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, there is $x\in[0,1]$ where $f$ is continuous.

Proof.

First of all, we show that fragmented functions are cliquish (in $\textup{{ACA}}_{0}^{\omega}$); Theorem 2.16 then establishes the implication from $\textup{{BCT}}_{[0,1]}$ to item (b). Let $f:[0,1]\rightarrow{\mathbb{R}}$ be fragmented and fix $\varepsilon>0$, $N\in{\mathbb{N}}$, and $x\in[0,1]$. For closed $C:=[x_{0}-\frac{1}{2^{N_{0}}},x_{0}+\frac{1}{2^{N_{0}}}]$, there is a relatively open $O\subset C$ with $\textup{{diam}}(f(O))<\varepsilon$. Since $C$ is a closed interval, the relative openness of $O$ implies that there are $a,b\in{\mathbb{R}}$ with $(a,b)\subset O$. Since $\textup{{diam}}(f(O))<\varepsilon$, we have $|f(x)-f(y)|<\varepsilon$ for $x,y\in(a,b)\subset B(x,\frac{1}{2^{N_{0}}})$, i.e. $f$ is cliquish.

Secondly, we show that item (b) implies $\textup{{BCT}}_{[0,1]}$. To this end, let $(X_{n})_{n\in{\mathbb{N}}}$ be an increasing sequence of closed nowhere dense sets in $[0,1]$ such that $[0,1]=\cup_{n\in{\mathbb{N}}}X_{n}$. We now show that $h:[0,1]\rightarrow{\mathbb{R}}$ from (H) is fragmented. Fix $\varepsilon>0$ and closed $C\subset[0,1]$ and consider the following case distinction.

• •

In case $C\subset X_{0}$, put $O:=C$ and note that $O$ is relatively open (in $C$). Moreover, $f(x)=\frac{1}{2}$ for $x\in O\subset X_{0}$, i.e. Definition 2.21 is trivially satisfied.

• •

In case $C\subset\cup_{k\leq k_{0}}X_{k}$ for (minimal) $k_{0}>0$, put $O:=C\cap O_{k_{0}-1}$ where $O_{k}:=[0,1]\setminus X_{k}$. Since $O_{k_{0}-1}$ is open, $O$ is relatively open (in $C$). Similar to the previous item, $f(x)=\frac{1}{2^{k_{0}}}$ for $x\in O$, i.e. Definition 2.21 is again trivially satisfied.

• •

For the remaining case, since $C\cap X_{k}\neq\emptyset$ for any $k\in{\mathbb{N}}$, choose $k_{0}\in{\mathbb{N}}\setminus\{0\}$ with $\frac{1}{2^{k_{0}}}<\varepsilon$ and define $O:=C\cap O_{k_{0}-1}$. Similar to the previous item, $O_{k_{0}-1}$ is open and $O$ is relatively open (in $C$). By assumption, $f(x)<\frac{1}{2^{k_{0}}}$ for $x\in O\subset[0,1]\setminus X_{k_{0}}$. Hence, $\textup{{diam}}(f(O))\leq\frac{1}{2^{k_{0}}}<\varepsilon$, as required.

Hence $h$ from (H) is fragmented while the second item seems to need $\textup{{IND}}_{{\mathbb{R}}}$ to guarantee that $k_{0}$ is minimal. We also obtain an oscillation function by Theorem 1.16, i.e. we may apply item (b) to show that $h$ is continuous at some $x_{0}\in[0,1]$. As in the proof of Theorem 2.16, we obtain $\textup{{BCT}}_{[0,1]}$, and we are done.

Thirdly, item (c) implies $\textup{{BCT}}_{[0,1]}$ as follows: let $(X_{n})_{n\in{\mathbb{N}}}$ be an increasing sequence of closed nowhere dense sets in $[0,1]$ such that $[0,1]=\cup_{n\in{\mathbb{N}}}X_{n}$. Now consider $h$ from (H) and note that for any $G\subset{\mathbb{R}}$, $h^{-1}(G)$ is the union of all $X_{n}$ such that $\frac{1}{2^{n+1}}\in G$, i.e. ${\bf F}_{\sigma}$ by definition. Together with Theorem 1.18, we observe that item (c) applies to $h$; as in the proof of Theorem 2.16, we obtain $\textup{{BCT}}_{[0,1]}$. The other direction is immediate by Theorem 2.16. ∎

Corollary 2.24** ($\textup{{ACA}}_{0}^{\omega}$).**

The following statement

any fragmented function $f:[0,1]\rightarrow{\mathbb{R}}$ is Baire 1**

implies $\textup{{BCT}}_{[0,1]}$ and the statement open from Corollary 2.8.

Proof.

The first part is immediate from Theorem 2.10 and the theorem. For the second part, one readily shows that for closed $C\subset[0,1]$, the function $\mathbb{1}_{C}$ is fragmented. As in the proof of Corollary 2.8, one obtains an RM-code for $C$. ∎

Finally, we have not been able to obtain similar results for other equivalent definitions of Baire 1 functions on the reals.

2.7. On Volterra’s early work

In this section, we connect the Baire category theorem and Volterra’s early work as sketched in Section 1.2, including a version of Blumberg’s theorem. As a result, Volterra’s theorem and corollary cannot be proved in ${\textsf{{Z}}}_{2}^{\omega}$ while the restrictions to quasi-continuous functions are provable in $\textup{{ACA}}_{0}^{\omega}$ by Theorem 2.26.

First of all, we have the following theorem, where we recall that ‘cliquish’ and ‘pointwise discontinuous’ are equivalent on the reals (see Remark 2.20). However, in light of Theorem 2.16, this equivalence cannot be proved in ${\textsf{{Z}}}_{2}^{\omega}$.

As in the previous sections, we observe a certain robustness for our results: we could replace ‘usco’ by any notion between the latter and cliquishness.

Theorem 2.25** ($\textup{{ACA}}_{0}^{\omega}$).**

The following are equivalent.

1. (a)

The Baire category theorem $\textup{{BCT}}_{[0,1]}$. 2. (b)

Volterra’s theorem*: there do not exist two pointwise discontinuous $f,g:[0,1]\rightarrow{\mathbb{R}}$ with associated oscillation functions for which the continuity points of one are the discontinuity points of the other, and vice versa.* 3. (c)

Volterra’s theorem* for ‘pointwise discontinuous’ replaced by ‘cliquish’.* 4. (d)

Volterra’s theorem* for ‘pointwise discontinuous’ replaced by ‘usco’.* 5. (e)

Volterra’s corollary*: there is no function with an oscillation function that is continuous on ${\mathbb{Q}}\cap[0,1]$ and discontinuous on $[0,1]\setminus{\mathbb{Q}}$.* 6. (f)

Volterra’s corollary* restricted to usco functions.* 7. (g)

*Generalised Volterra’s corollary *(*Theorem 1.4) for usco functions and enumerable $D$ *(or: countable $D$, or: strongly countable $D$). 8. (h)

Blumberg’s theorem ([bloemeken])* restricted to usco (or cliquish with an oscillation function) functions on $[0,1]$.*

The equivalences remain correct if we replace ‘usco’ by ‘Baire $1^{*}$’.

Proof.

First of all, to prove item (d) using $\textup{{BCT}}_{[0,1]}$, suppose $f,g:[0,1]\rightarrow{\mathbb{R}}$ are usco and such that $C_{f}=D_{g}$ and $C_{g}=D_{f}$, noting that these sets exist by Theorem 2.4. Now consider the (closed and nowhere dense) sets $F_{q}$ from the proof of Theorem 2.3 and let $H_{q}$ be the associated (closed and nowhere dense) sets for $g$. Since $D_{f}\subset\cup_{q\in{\mathbb{Q}}}F_{q}$ and $D_{g}\subset\cup_{q\in{\mathbb{Q}}}H_{q}$, we have $[0,1]=C_{f}\cup D_{f}=D_{g}\cup D_{f}=\cup_{q\in{\mathbb{Q}}}(F_{q}\cup H_{q})$, which contradicts $\textup{{BCT}}_{[0,1]}$.

A similar proof goes through for item (c), namely by defining $D_{k}^{f}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{k}}\}$ and noting that $[0,1]=\cup_{n\in{\mathbb{N}}}(D_{n}^{f}\cup D_{n}^{g})$ where the latter sets are nowhere dense as in the proof of Theorem 2.16. Items (e) and (f) follow from items (c) and (d) as Thomae’s function from (T) is continuous on the irrationals and discontinuous on ${\mathbb{Q}}$; this function is also usco and cliquish. By definition, pointwise discontinuous functions are cliquish, i.e. item (b) also follows.

Secondly, we now derive $\textup{{BCT}}_{[0,1]}$ from Volterra’s corollary as in item (e) or (f). To this end, let $(X_{n})_{n\in{\mathbb{N}}}$ be a sequence of closed nowhere dense sets such that $[0,1]\setminus{\mathbb{Q}}=\cup_{n\in{\mathbb{N}}}X_{n}$. Now consider $h:[0,1]\rightarrow{\mathbb{R}}$ as in (H), which is as required for item (e) or (f) by Theorems 1.16 and 1.18. By Theorem 1.16, $h$ is also continuous at any $q\in{\mathbb{Q}}\cap[0,1]$ (since $h(q)=\textup{{osc}}_{h}(q)=0$) and discontinuous at any $y\in[0,1]\setminus{\mathbb{Q}}$ (since $h(y)=\textup{{osc}}_{h}(y)>0$). This contradicts Volterra’s corollary (for usco or cliquish functions), and $\textup{{BCT}}_{[0,1]}$ follows. The same argument works for item (b) using Thomae’s function and $h:[0,1]\rightarrow{\mathbb{R}}$ as the latter is pointwise discontinuous, namely continuous at every rational, by assumption.

Thirdly, we only need to show that $\textup{{BCT}}_{[0,1]}$ implies item (g), as ${\mathbb{Q}}$ is enumerable and dense. To this end, proceed as in the previous paragraph, replacing ${\mathbb{Q}}$ by a countable dense set $D\subset[0,1]$ wherever relevant. Note in particular that $D=\cup_{n\in{\mathbb{N}}}\{x\in D:Y(x)=n\}$ suffices to replace an enumeration of ${\mathbb{Q}}$ if $Y:[0,1]\rightarrow{\mathbb{N}}$ is injective on $D$.

Fourth, $\textup{{BCT}}_{[0,1]}$ implies items (h) by Theorem 2.3 since $D=C_{f}$ is as required. To prove (h)$\rightarrow\textup{{BCT}}_{[0,1]}$, let $(X_{n})_{n\in{\mathbb{N}}}$ be a sequence of closed and nowhere dense sets in $[0,1]$ and consider $h:[0,1]\rightarrow{\mathbb{R}}$ from (H), which is usco and cliquish by Theorem 1.18. Let $D$ be the dense set provided by item (h) and consider $y\in D$. In case $h(y)\neq 0$, say $h(y)\geq\frac{1}{2^{k_{0}}}$, note that $O_{k_{0}}\cap D$ is dense in $[0,1]$. Hence, for any $N\in{\mathbb{N}}$ there is $z\in B(x,\frac{1}{2^{N}})\cap D$ with $h(z)\leq\frac{1}{2^{k_{0}+1}}$, i.e. $h_{\upharpoonright D}$ is not continuous (on $D$). This contradiction implies that $h(y)=0$, meaning $y\in[0,1]\setminus\cup_{n\in{\mathbb{N}}}X_{n}$, i.e. $\textup{{BCT}}_{[0,1]}$ follows. The final sentence is immediate in light of Theorem 2.11. ∎

We could use the notion height countable (see [dagsamX]) for item (g) of Theorem 2.25, but then we need (at least) extra induction to accommodate finite sets.

Next, we show that Volterra’s theorems from [volaarde2] and related results are readily proved if we restrict to quasi-continuous functions.

Theorem 2.26** ($\textup{{ACA}}_{0}^{\omega}$).**

1. (a)

Volterra’s theorem*: there do not exist two quasi-continuous functions defined on the unit interval for which the continuity points of one are the discontinuity points of the other, and vice versa.* 2. (b)

Volterra’s corollary*: there is no quasi-continuous function that is continuous on ${\mathbb{Q}}\cap[0,1]$ and discontinuous on $[0,1]\setminus{\mathbb{Q}}$.* 3. (c)

*Generalised Volterra’s corollary *(*Theorem 1.4) for quasi-continuous functions and enumerable $D$ *(or: countable $D$, or: strongly countable $D$). 4. (d)

Blumberg’s theorem ([bloemeken])* restricted to quasi-continuous functions on $[0,1]$.*

Proof.

For item (a), for quasi-continuous $f,g:[0,1]\rightarrow{\mathbb{R}}$, the sets $D_{f}$ and $D_{g}$ exist and be can be expressed as unions $\cup_{n\in{\mathbb{N}}}D_{n}^{f}$ and $\cup_{m\in{\mathbb{N}}}D_{m}^{g}$ of R2-closed nowhere dense sets by Theorem 2.19. Hence, in case $C_{f}=D_{g}$ and $C_{g}=D_{f}$, we have $[0,1]=C_{f}\cup D_{f}=D_{g}\cup D_{f}=\bigcup_{n,m\in{\mathbb{N}}}D_{n}^{f}\cup D_{m}^{g}$. However, the Baire category theorem for R2-closed sets is provable in $\textup{{ACA}}_{0}^{\omega}$ ([dagsamVII]*Theorem 7.10), a contradiction. The other items are proved in the same way. ∎

In conclusion, we have established equivalences involving $\textup{{BCT}}_{[0,1]}$ and Volterra’s early work (and related results), rendering the latter unprovable in ${\textsf{{Z}}}_{2}^{\omega}$. The latter deal with pointwise discontinuous function, which are exactly the cliquish ones by Remark 2.20. Also by the latter, cliquish functions are closely related to quasi-continuous functions, but Volterra’s results for quasi-continuous functions are readily proved in $\textup{{ACA}}_{0}^{\omega}$ by Theorem 2.26. In contrast to the close relation between cliquishness and quasi-continuity, there is a great divide, some might say ‘abyss’, between $\textup{{ACA}}_{0}^{\omega}$ and ${\textsf{{Z}}}_{2}^{\omega}$. We have no explanation for this phenomenon at the moment and welcome any suggestions.

3. Tao’s pigeonhole principle for measure spaces

3.1. Introduction

In this section, we establish the equivalences sketched in Section 1.1 for $\textup{{PHP}}_{[0,1]}$, i.e. Tao’s pigeonhole principle for measure spaces from [taoeps]. We also study $\textup{{WBCT}}_{[0,1]}$, a ‘hybrid’ principle between $\textup{{PHP}}_{0,1}$ and $\textup{{BCT}}_{[0,1]}$ which is interesting in its own right, also from a historical point of view.

First of all, it is trivial that ‘measure zero’ implies ‘nowhere dense’. Replacing the latter by the former in $\textup{{BCT}}_{[0,1]}$, we obtain the weaker $\textup{{WBCT}}_{[0,1]}$ (see Principle 3.2 in Section 3.2) and the equivalences from the previous section then go through mutatis mutandis. Nonetheless, this weakening is more than spielerei as $\textup{{WBCT}}_{[0,1]}$ is connected to Hankel’s 1870 work on Riemann integration ([hankelwoot]). In a nutshell, Hankel formulates necessary and sufficient conditions for the Riemann integral akin to the Vitali-Lebesgue theorem from Section 1.1. While Hankel’s theorem is correct, the proof is not: he incorrectly tries to reverse the implication that a Riemann integrable function is pointwise discontinuous, leading to Smith’s counterexample based on Cantor sets ([snutg]) and Ascoli’s proof of Hankel’s theorem ([ascoli1]). Equivalences involving $\textup{{WBCT}}_{[0,1]}$ and Hankel’s results for usco and cliquish functions are studied in Section 3.2, including the fundamental theorem of calculus.

Secondly, $\textup{{WBCT}}_{[0,1]}$ only replaces ‘nowhere dense’ by ‘measure zero’ in the antecedent; Tao’s pigeonhole principle for measure spaces from [taoeps] ensues if we perform this replacement in the consequent as well. In Section 3.3, we study the RM of the latter principle, called $\textup{{PHP}}_{[0,1]}$, obtaining an equivalence to the Vitali-Lebesgue theorem (including restrictions to usco and cliquish functions). As will become clear, the RM of $\textup{{PHP}}_{[0,1]}$ is rather similar to the RM of $\textup{{WBCT}}_{[0,1]}$, which is in turn similar to the RM of $\textup{{BCT}}_{[0,1]}$, despite the fundamental differences between measure and category. Finally, the restrictions of the aforementioned theorems to quasi-continuous or Baire 1 functions, are provable in $\textup{{ACA}}_{0}^{\omega}$ by Theorem 3.7. Recall that quasi-continuity is very close to cliquishness by Remark 2.20.

3.2. Measure-theoretic Baire category theorem

We introduce a ‘measure-theoretic’ version of the Baire category theorem and obtain some equivalences to well-known theorems, including (variations of) the fundamental theorem of calculus and the Vitali-Lebesgue theorem from Section 1.1.

First of all, one part of the Vitali-Lebesgue theorem is readily proved.

Theorem 3.1** ($\textup{{ACA}}_{0}^{\omega}+\textup{{QF-AC}}^{0,1}$).**

A Riemann integrable $f:[0,1]\rightarrow{\mathbb{R}}$ is bounded.

Proof.

Suppose $f:[0,1]\rightarrow{\mathbb{R}}$ is Riemann integrable and unbounded, i.e. $(\forall n\in{\mathbb{N}})(\exists x\in[0,1])(|f(x)|>n)$. Apply $\textup{{QF-AC}}^{0,1}$ to obtain a sequence $(x_{n})_{n\in{\mathbb{N}}}$ with $|f(x_{n})|>n$ for $n\in{\mathbb{N}}$. By sequential compactness (see [simpson2]*III.2.2), there is a convergent sub-sequence $(y_{n})_{n\in{\mathbb{N}}}$, say with limit $y\in[0,1]$. In particular, $f(y_{n})$ is arbitrarily large as $y_{n}$ approaches $y$. Thus, for any Riemann sum $\sum_{i=0}^{k}f(t_{i})(x_{i+1}-x_{i})$, consider the point $t_{j}$ such that $y\in[x_{j},x_{j+1}]$ and the latter contains infinitely many elements of the sequence $(y_{n})_{n\in{\mathbb{N}}}$. Changing this $t_{j}$ to $y_{m}$ for large enough $m\in{\mathbb{N}}$, the Riemann sum can be arbitrarily large, a contradiction. ∎

Similarly, $\textup{{ACA}}_{0}^{\omega}+\textup{{QF-AC}}^{0,1}$ establishes that a continuous almost everywhere bounded function, is Riemann integrable on the unit interval; the proof of [brownrie]Lemma is readily formalised, as it is based (only) on Riemann sums, i.e. avoiding the Darboux integral and Lebesgue measure. Alternative proofs surely exist in the modern literature, noting that [brownrie] is almost 100 years old. As an aside, the Darboux integral is not directly available as the supremum principle for Riemann integrable functions is hard121212As observed below Corollary 2.8, the principle open in the latter is ‘explosive’ in that $\Pi_{1}^{1}\text{-{{CA}}}_{0}^{\omega}+\textup{{open}}$ proves $\Pi_{2}^{1}\text{-{{CA}}}_{0}$ ([dagsamXI]), while $\Pi_{1}^{1}\text{-{{CA}}}_{0}^{\omega}$ is $\Pi_{3}^{1}$-conservative over $\Pi_{1}^{1}\text{-{{CA}}}_{0}$ ([yamayamaharehare]). The supremum principle for Riemann integrable functions (even with a modulus) behaves the same. to prove by the results in [dagsamXIV]§2.8.

Secondly, let $\textup{{WBCT}}_{[0,1]}$ be the restriction of $\textup{{BCT}}_{[0,1]}$ to measure one sets.

Principle 3.2** ($\textup{{WBCT}}_{[0,1]}$).**

If $(O_{n})_{n\in{\mathbb{N}}}$ is a decreasing sequence of measure one open sets of reals in $[0,1]$, then $\bigcap_{n\in{\mathbb{N}}}O_{n}$ is non-empty.

Recall that, like in second-order RM, statements like ‘$E\subset[0,1]$ has measure [math]’ can be made without introducing the Lebesgue measure (see Definition 1.8). The RM of $\textup{{WBCT}}_{[0,1]}$ seems to require the principle $\textup{{IND}}_{{\mathbb{R}}}$ introduced in Section 2.6.

Thirdly, we have the following theorem where we note that Hankel studies Riemann integration using oscillation functions in [hankelwoot]. We also invite the reader to compare item (d) to the main topic of [hahakaka], which we discuss further in Section 4.2.

Theorem 3.3** ($\textup{{ACA}}_{0}^{\omega}+\textup{{IND}}_{{\mathbb{R}}}+\textup{{QF-AC}}^{0,1}$).**

The following are equivalent.

1. (a)

The weak Baire category theorem $\textup{{WBCT}}_{[0,1]}$. 2. (b)

(Hankel [hankelwoot] & Dini [dinipi]§188*)* For Riemann integrable $f:[0,1]\rightarrow{\mathbb{R}}$ with an oscillation function, the set $C_{f}\neq\emptyset$ (or: is dense).* 3. (c)

For Riemann integrable usco $f:[0,1]\rightarrow{\mathbb{R}}$, the set $C_{f}\neq\emptyset$ (or: is dense). 4. (d)

*For Riemann integrable $f:[0,1]\rightarrow{\mathbb{R}}$ with an oscillation function and $\int_{0}^{1}f(x)dx=0$, there is $x\in[0,1]$ with $f(x)=0$. (Bourbaki, **[boereng]**p. 61). 5. (e)

*For Riemann integrable usco $f:[0,1]\rightarrow[0,1]$ with $\int_{0}^{1}f(x)dx=0$, there is $x\in[0,1]$ with $f(x)=0$. (Bourbaki, **[boereng]**p. 61). 6. (f)

(FTC)* For Riemann integrable $f:[0,1]\rightarrow{\mathbb{R}}$ with an oscillation function and $F(x):=\lambda x.\int_{0}^{x}f(t)dt$, there is $x_{0}\in(0,1)$ where $F(x)$ is differentiable with derivative $f(x_{0})$.* 7. (g)

(FTC)* For Riemann integrable usco $f:[0,1]\rightarrow{\mathbb{R}}$ with $F(x):=\lambda x.\int_{0}^{x}f(t)dt$, there is $x_{0}\in(0,1)$ where $F(x)$ is differentiable with derivative $f(x_{0})$.* 8. (h)

For Riemann integrable usco $f:[0,1]\rightarrow{\mathbb{R}}^{+}$, there are $a,b\in[0,1]$ with $0<\inf_{x\in[a,b]}f(x)$. 9. (i)

For Riemann integrable $f:[0,1]\rightarrow{\mathbb{R}}^{+}$ with an oscillation function, there are $a,b\in[0,1]$ with $0<\inf_{x\in[a,b]}f(x)$. 10. (j)

For totally discontinuous $f:[0,1]\rightarrow{\mathbb{R}}$ with oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, there is $N\in{\mathbb{N}}$ and $E\subset[0,1]$ of positive measure with $\textup{{osc}}_{f}(x)\geq\frac{1}{2^{N}}$ for $x\in E$. 11. (k)

Volterra’s theorem*: there do not exist two Riemann integrable $f,g:[0,1]\rightarrow{\mathbb{R}}$ with associated oscillation functions for which the continuity points of one are the discontinuity points of the other, and vice versa.* 12. (l)

Volterra’s corollary*: there is no Riemann integrable function with an oscillation function that is continuous on ${\mathbb{Q}}\cap[0,1]$ and discontinuous on $[0,1]\setminus{\mathbb{Q}}$.*

We can replace ‘usco’ by ‘cliquish with an oscillation function’ in the above. We can restrict to pointwise discontinuous functions in items (k)-(l).

Proof.

First of all, assume $\textup{{WBCT}}_{[0,1]}$ and let $f:[0,1]\rightarrow{\mathbb{R}}$ be Riemann integrable with oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$. Suppose $[0,1]=D_{f}=\cup_{k\in{\mathbb{N}}}D_{k}$ where $D_{k}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{k}}\}$, which is closed since any oscillation function is usco by Theorem 1.17. By $\textup{{WBCT}}_{[0,1]}$, there is $k_{0}\in{\mathbb{N}}$ such that $D_{k_{0}}$ does not have measure zero. Let $\varepsilon_{0}>0$ be such that the measure of $D_{k_{0}}$ is at least $\varepsilon_{0}$ and let $\delta_{0}>0$ be as provided by the definition of Riemann integrability for $\varepsilon=\varepsilon_{0}\frac{1}{2^{k_{0}+1}}$. For any partition $P$ with mesh below $\delta_{0}$ given by $0=x_{0},t_{0},x_{1},t_{1},x_{1},\dots,x_{k-1},t_{k},x_{k}=1$, we define two partitions $P^{\prime},P^{\prime\prime}$ as follows: in case $D_{k_{0}}\cap[x_{i},x_{i+1}]=\emptyset$, do nothing; otherwise, change $t_{i}$ from $P$ to some $t_{i}^{\prime}$ for $P^{\prime}$ and $t_{i}^{\prime\prime}$ for $P^{\prime\prime}$ such that $|f(t_{i}^{\prime})-f(t_{i}^{\prime\prime})|>\frac{1}{2^{k_{0}+1}}$. The latter reals exist by the assumption $D_{k_{0}}\cap[x_{i},x_{i+1}]\neq\emptyset$. One readily shows that $|S(f,P^{\prime})-S(f,P^{\prime\prime})|>\varepsilon_{0}\frac{1}{2^{k_{0}+1}}$, i.e. a contradiction, and item (b) follows. Note that the finite manipulation of $P$ can be done using $\textup{{IND}}_{{\mathbb{R}}}$. Item (l) follows in the same way by assuming $[0,1]\setminus{\mathbb{Q}}=D_{f}$; the proof then proceeds in the same way by noting $[0,1]=\cup_{k\in{\mathbb{N}}}E_{k}$ where $E_{k}:=D_{k}\cup\{q_{k}\}$ is closed and where $(q_{n})_{n\in\in{\mathbb{N}}}$ is an enumeration of the rationals in $[0,1]$. Noting that Thomae’s function from (T) is Riemann integrable, item (k) also follows.

Secondly, assume item (b) and let $(O_{n})_{n\in{\mathbb{N}}}$ be a sequence as in $\textup{{WBCT}}_{[0,1]}$. Define $X_{n}:=[0,1]\setminus O_{n}$ and consider $h:[0,1]\rightarrow{\mathbb{R}}$ from (H), which we show to be Riemann integrable with zero integral. To this end, fix $\varepsilon>0$ and let $n_{0}\in{\mathbb{N}}$ be such that $\frac{1}{2^{n_{0}+1}}<\varepsilon$. Since $X_{n_{0}}$ has measure zero, we can find a sequence $(I_{n})_{n\in{\mathbb{N}}}$ of intervals that covers $X_{n_{0}}$ and has total length at most $\frac{1}{2^{n_{0}+2}}$. By [dagsamVII]*Theorem 3.3, the closed set $X_{n_{0}}$ is also covered by $\cup_{n\leq k_{0}}I_{n}$ for some $k_{0}\in{\mathbb{N}}$. Now let $P$ be any partition with mesh at most $\frac{1}{2^{n_{0}+2}}$. To show that $\varepsilon>S(f,P)=\sum_{i=0}^{|P|}h(t_{i})(x_{i+1}-x_{i})$, we split the intervals $[x_{i},x_{i+1}]$ into sub-intervals $[x_{i+1},a_{0}],[a_{0},a_{1}],\dots,[a_{m},a_{m+1}],[a_{m+1},x_{i}]$, where the $a_{i}$ are end-points of the $I_{n}$ in $[x_{i+1}-x_{i}]$ for some $n\leq k_{0}$. Now split $S(f,p)$ into two sums, one over the intervals not in $\cup_{n\leq k_{0}}I_{n}$, and one with the rest. By our assumptions, each separate sum is at most $\frac{1}{2^{n_{0}+2}}$ as required. Now apply item (b) for $h$ (see Theorem 1.16 for $\textup{{osc}}_{h}:[0,1]\rightarrow{\mathbb{R}}$) and note that $y\in C_{h}$ implies $h(y)=\textup{{osc}}_{h}(y)=0$, i.e. $y\in\cap_{n\in{\mathbb{N}}}O_{n}$, as required for $\textup{{WBCT}}_{[0,1]}$. Similarly, item (l) implies $\textup{{WBCT}}_{[0,1]}$ by considering (H) where $(X_{n})_{n\in{\mathbb{N}}}$ is a sequence of closed sets with $[0,1]\setminus{\mathbb{Q}}=\cup_{n\in{\mathbb{N}}}X_{n}$. Moreover, item (k) implies item (l) in light of Thomae’s function from (T),

Thirdly, for item (c), the absence of an oscillation function complicates matters (slightly). We modify $F_{q}$ defined as in (2.3) as follows: let $`x\in E_{q,l}$’ in case

[TABLE]

As in the proof of Theorem 2.3, $E_{q,l}$ is closed and $D_{f}\subseteq\cup_{l\in{\mathbb{N}},q\in{\mathbb{Q}}}E_{q,l}$. Now suppose $C_{f}=\emptyset$, i.e. $\cup_{l\in{\mathbb{N}},q\in{\mathbb{Q}}}E_{q,l}=[0,1]$. By $\textup{{WBCT}}_{[0,1]}$, there is $l_{0}\in{\mathbb{N}}$, $q_{0}\in{\mathbb{Q}}$ such that $E_{q_{0},l_{0}}$ has non-zero measure. As in the first paragraph of the proof, $f$ is not Riemann integrable, and item (c) follows. The latter implies $\textup{{WBCT}}_{[0,1]}$ in the same way as in the previous paragraph, noting that $h$ from (H) is usco by Theorem 1.18.

Fourth, for items (d) and (e), the latter follow from items (b) and items (c) by noting that $x\in C_{f}$ and $\int_{0}^{1}f(x)dx=0$ implies $f(x)=0$. For the reversals, use $h:[0,1]\rightarrow{\mathbb{R}}$ from (H), which has Riemann integral equal to zero by the second paragraph of this proof.

Fifth, for items (f) and (g), the latter are equivalent to items (d) and (e) in the same way. In particular, the function $h:[0,1]\rightarrow{\mathbb{R}}$ from (H) has a primitive, namely the constant zero function. Moreover, the usual epsilon-delta proof establishes that $F(x):=\int_{0}^{x}f(t)dt$ is continuous and that $F^{\prime}(y)=f(y)$ if $f$ is continuous at $y$.

Sixth, item (h) immediately follows from item (b) by taking a small enough ball around a point of continuity. Similarly, item (h) implies item (e) by noting that $\int_{a}^{b}f(x)dx\leq\int_{c}^{d}f(x)dx$ in case $f$ is non-negative and $[a,b]\subset[c,d]$. Item (i) is treated in the same way. The final sentence follows by Theorem 1.18.

Seventh, let $f:[0,1]\rightarrow{\mathbb{R}}$ be as in item (j) and define the closed set $D_{k}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{k}}\}$. By assumption, $[0,1]=\cup_{k\in{\mathbb{N}}}D_{k}$ and $\textup{{WBCT}}_{[0,1]}$ implies there is $k_{0}\in{\mathbb{N}}$ and $E\subset[0,1]$ of positive measure such that $E\subset D_{k_{0}}$, as required. For the reversal, assume item (j) and let $f:[0,1]\rightarrow{\mathbb{R}}$ be Riemann integrable and with oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$. In case $C_{f}\neq\emptyset$, we are done in light of item (c). In case $C_{f}=\emptyset$, $f$ is totally discontinuous and we can apply item (j). Let $N_{0}\in{\mathbb{N}}$ and $E\subset[0,1]$ of positive measure be such that $\textup{{osc}}_{f}(x)\geq\frac{1}{2^{N_{0}}}$ for $x\in E$. As in the first paragraph of this proof, $f$ is not Riemann integrable, a contradiction. For the penultimate sentence, it suffices to observe that $h$ from (H) is cliquish and has an oscillation function by Theorems 1.16 and 1.18. The final sentence follows by observing that the functions used in the above proof of the implications $\eqref{topanga4}\rightarrow\eqref{topanga3}\rightarrow\textup{{WBCT}}_{[0,1]}$ are pointwise discontinuous. ∎

In the previous theorem, we can replace the use of $\textup{{QF-AC}}^{0,1}$ (not provable in ZF) by NCC (provable in ${\textsf{{Z}}}_{2}^{\Omega}$) from [dagsamIX]. It seems we can (also) avoid the use of $\textup{{QF-AC}}^{0,1}$ if we require the sets to have Jordan measure zero. We do not know if we can weaken the induction axiom in Theorem 3.3. We do have the following corollary, which is of separate interest.

Corollary 3.4** ($\textup{{ACA}}_{0}^{\omega}$).**

For Riemann integrable $f:[0,1]\rightarrow{\mathbb{R}}$ with oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, $D_{k}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{k}}\}$ has measure zero.

Proof.

The first paragraph of the proof of the theorem contains the required proof by contradiction, starting with ‘Let $\varepsilon_{0}>0$ be such that…’. ∎

Corollary 3.4 identifies the ‘missing link’ to the Vitali-Lebesgue theorem: each $D_{k}$ has measure zero and since $D_{f}=\cup_{k\in{\mathbb{N}}}D_{k}$, we only need Tao’s pigeonhole principle for measure spaces to conclude that $D_{f}$ has measure zero.

Finally, with the gift of hindsight, one can show that the following strengthening of $\textup{{WBCT}}_{[0,1]}$ is equivalent to $\textup{{BCT}}_{[0,1]}$ again.

For a sequence $(C_{n})_{n\in{\mathbb{N}}}$ of closed sets with $[0,1]=\cup_{n\in{\mathbb{N}}}C_{n}$, there is $m\in{\mathbb{N}}$ such that $C_{m}$ has non-zero measure and $[0,1]$ cannot be covered by finite copies of $C_{m}$.

We could also obtain an equivalence between $\textup{{WBCT}}_{[0,1]}$ and a version of the uniform boundedness principle from Theorem 2.15. Moreover, $\textup{{WBCT}}_{[0,1]}$ implies the following interesting statement, which follows from e.g. [bage]*Theorem,

for a closed set $E\subset{\mathbb{R}}$ of measure zero, there is $x\in{\mathbb{R}}$ such that $x+E\subset{\mathbb{R}}\setminus{\mathbb{Q}}$,

and we expect a reversal to be possible.

3.3. The pigeonhole principle

We introduce Tao’s pigeonhole principle for measure spaces from [taoeps] and obtain equivalences involving the fundamental theorem of calculus and the Vitali-Lebesgue theorem. Hence, the latter theorems are not provable in ${\textsf{{Z}}}_{2}^{\omega}$ while the restrictions to Baire 1 and quasi-continuous functions and RM-closed sets are provable in $\textup{{ACA}}_{0}^{\omega}$ by Theorems 3.6 and 3.7.

First of all, we shall study the pigeonhole principle for closed sets as in $\textup{{PHP}}_{[0,1]}$ below. We recall that like in second-order RM, statements of the form ‘$E\subset[0,1]$ has measure [math]’ can be made without introducing the Lebesgue measure.

Principle 3.5** ($\textup{{PHP}}_{[0,1]}$).**

If $(X_{n})_{n\in{\mathbb{N}}}$ is an increasing sequence of measure zero closed sets of reals in $[0,1]$, then $\bigcup_{n\in{\mathbb{N}}}X_{n}$ is measure zero.

By the the main result of [trohim], not all nowhere dense measure zero sets are the countable union of measure zero closed sets, i.e. $\textup{{PHP}}_{[0,1]}$ does not generate ‘all’ measure zero sets. With some effort, one can derive $\textup{{PHP}}_{[0,1]}$ restricted to R2-closed sets from Cousin’s lemma as studied in [dagsamIII].

Secondly, we establish that while $\textup{{PHP}}_{[0,1]}$ is hard to prove in terms of conventional comprehension, the former principle can be proved without the Axiom of Choice, i.e. in a fragment of ZF. Thus, the properties of $\textup{{PHP}}_{[0,1]}$ are not due to the latter implying (a fragment of) the Axiom of Choice. By contrast, $\textup{{PHP}}_{[0,1]}$ restricted to RM-codes is provable in a relatively weak system.

Theorem 3.6**.**

• •

The ${\textsf{{Z}}}_{2}^{\omega}+\textup{{QF-AC}}^{0,1}$ does not prove $\textup{{PHP}}_{[0,1]}$.

• •

The system ${\textsf{{Z}}}_{2}^{\Omega}$ proves $\textup{{PHP}}_{[0,1]}$.

• •

The system $\textup{{ACA}}_{0}^{\omega}$ proves $\textup{{PHP}}_{[0,1]}$ restricted to RM-codes for closed sets.

Proof.

For the first item, we have $\textup{{PHP}}_{[0,1]}\rightarrow\textup{{NIN}}_{[0,1]}$ as for any injection $Y:[0,1]\rightarrow{\mathbb{N}}$, the set $E_{n}:=\{x\in[0,1]:Y(x)=n\}$ has measure zero but the union does not. By [dagsamXI]*Theorem 3.1, the system ${\textsf{{Z}}}_{2}^{\omega}+\textup{{QF-AC}}^{0,1}$ cannot prove $\textup{{NIN}}_{[0,1]}$.

For the second item, the following formula expresses that $(X_{n})_{n\in{\mathbb{N}}}$ is a sequence of closed measure zero sets.

[TABLE]

where each $I_{n}$ is an open interval with rational end-points. By [dagsamIX]*Theorems 3.1 and 3.5, ${\textsf{{Z}}}_{2}^{\Omega}$ proves that countable coverings of closed sets have finite sub-coverings. Applying this covering result to (3.1), we obtain the following formula

[TABLE]

where the formula in square brackets is decidable using $\exists^{3}$. Now apply $\textup{{QF-AC}}^{0,0}$, provable in ZF and included in $\textup{{RCA}}_{0}^{\omega}$, to obtain the conclusion of $\textup{{PHP}}_{[0,1]}$.

For the third item, consider (3.1) and assume $(X_{n})_{n\in{\mathbb{N}}}$ is given as a sequence $(C_{n})_{n\in{\mathbb{N}}}$ of RM-closed sets. By [brownphd]*Lemma 3.13, a countable covering of an RM-closed set has a finite sub-covering assuming $\textup{{WKL}}_{0}$, i.e. we obtain

[TABLE]

In case the formula in square brackets is decidable (using $\exists^{2}$), we can apply $\textup{{QF-AC}}^{0,0}$ and obtain the required interval covering of $\cup_{n\in{\mathbb{N}}}C_{n}$.

To show that $C_{n}\subset\cup_{1\leq i\leq k}(q_{2i-1},q_{2i})$ is decidable using $\exists^{2}$, note that this formula is equivalent to ‘$(\forall x\in[0,1])(x\in O_{n,k})$’, where the RM-open set $O_{n,k}\subset[0,1]$ is the union of the RM-open sets $[0,1]\setminus C_{n}$ and $\cup_{1\leq i\leq k}(q_{2i-1},q_{2i})$. By [simpson2]*II.7.1, there is a (code for a) continuous function $f_{n,k}$ such that $x\in O_{n,k}\leftrightarrow f_{n,k}(x)>0$ for all $n,k\in{\mathbb{N}}$ and $x\in[0,1]$. By [dagsamXIV]*Theorem 2.2, codes for continuous functions on ${\mathbb{R}}$ yield third-order functions on ${\mathbb{R}}$, even in $\textup{{RCA}}_{0}^{\omega}$. Using $\exists^{2}$, we may compute the infimum of $f_{n,k}$ on $[0,1]$ by [kohlenbach2]*Prop. 3.14. The following equivalence now holds for all $n,k\in{\mathbb{N}}$:

[TABLE]

as continuous functions attain their infimum on the unit interval given $\textup{{WKL}}_{0}$ by [simpson2]*IV.2.3. The right-hand side of (3.2) is decidable given $\exists^{2}$. ∎

In light of the previous proof, $\textup{{PHP}}_{[0,1]}$ follows from the principle MCC from [dagsamIX]. Moreover, the third item in Theorem 3.6 goes through for ‘$\textup{{ACA}}_{0}^{\omega}$’ replaced by ‘$\textup{{RCA}}_{0}^{\omega}+\textup{{WKL}}$’, using [kohlenbach2]*Prop. 3.15 to obtain (3.2) without recourse to $(\exists^{2})$.

Thirdly, the following theorem should be contrasted with Theorem 3.8, keeping in mind the close connection between quasi-continuity and cliquishness (see Remark 2.20); the set $C_{f}$ exists by Theorems 2.10 and 2.19.

Theorem 3.7** ($\textup{{ACA}}_{0}^{\omega}$).**

• •

For Riemann integrable quasi-contiuous $f:[0,1]\rightarrow{\mathbb{R}}$, $C_{f}$ has measure one.

• •

For Riemann integrable Baire 1 $f:[0,1]\rightarrow{\mathbb{R}}$, the set $C_{f}$ has measure one.

Proof.

For the first item, let $f:[0,1]\rightarrow{\mathbb{R}}$ be quasi-continuous. Our starting point is the proof of Theorem 2.19, in particular the set $O_{m}$ defined as the collection of all $x\in[0,1]$ such that (2.10). By the definition of quasi-continuity, (2.10) and (2.11) are equivalent, and this remains true if $N=M$. Using $\mu^{2}$, let $Y_{m}(x)$ be the least $N\in{\mathbb{N}}$ as in (2.10), if such exists, and zero otherwise. Hence, we $x\in O_{m}\leftrightarrow x\in\cup_{q\in{\mathbb{Q}}\cap O_{m}}B(q,\frac{1}{2^{Y_{m}(q)}})$, for any $x\in[0,1]$. In this way, we have obtained an RM-code for the sequence $(O_{m})_{m\in{\mathbb{N}}}$. Recall that $D_{f}=\cup_{m\in{\mathbb{N}}}D_{m}$ where $D_{m}:=[0,1]\setminus O_{m}$ and $D_{m}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{m}}\}$ If $f:[0,1]\rightarrow{\mathbb{R}}$ is also Riemann integrable then Corollary 3.4 guarantees that the set $D_{k}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{k}}\}$ has measure zero. Now apply Theorem 3.6 to conclude that $D_{f}$ has measure zero.

For the second item, let $f:[0,1]\rightarrow{\mathbb{R}}$ be the pointwise limit of the sequence of continuous functions $(f_{n})_{n\in{\mathbb{N}}}$. Now consider the sets $F_{m,n}$ from the proof of Theorem 2.10. One readily proves that $\cup_{m\in{\mathbb{N}}}F_{m,n}\subset D_{n}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{n}}\}$. The latter is measure zero by Corollary 3.4, in case $f$ is also Riemann integrable. By the proof of Theorem 2.10, $F_{n,m}$ is represented by RM-codes, i.e. we may apply the third item of Theorem 3.6 to conclude that $\cup_{n,m\in{\mathbb{N}}}F_{m,n}$ has measure zero. Since $D_{f}$ is a subset of the latter union, we are done. ∎

Fourth, we have the following theorem where we note that the sets $C_{f}$ and $D_{f}$ exists by Theorem 2.4 in e.g. item (c) of Theorem 3.8. The last sentence of the theorem should be contrasted with Corollary 3.7, recalling Remark 2.20. We recall the induction fragment $\textup{{IND}}_{{\mathbb{R}}}$ introduced in Section 2.6.

Theorem 3.8** ($\textup{{ACA}}_{0}^{\omega}+\textup{{IND}}_{{\mathbb{R}}}+\textup{{QF-AC}}^{0,1}$).**

The following are equivalent.

1. (a)

The pigeonhole principle for measure spaces as in $\textup{{PHP}}_{[0,1]}$. 2. (b)

(Vitali-Lebesgue)* For Riemann integrable $f:[0,1]\rightarrow{\mathbb{R}}$ with an oscillation function, the set $D_{f}$ has measure [math].* 3. (c)

For Riemann integrable usco $f:[0,1]\rightarrow{\mathbb{R}}$, the set $D_{f}$ has measure [math]. 4. (d)

*For Riemann integrable $f:[0,1]\rightarrow[0,1]$ with an oscillation function and $\int_{0}^{1}f(x)dx=0$, the set $\{x\in[0,1]:f(x)=0\}$ has measure one. * 5. (e)

For Riemann integrable usco $f:[0,1]\rightarrow[0,1]$ with $\int_{0}^{1}f(x)dx=0$, the set $\{x\in[0,1]:f(x)=0\}$ has measure one. 6. (f)

(FTC)* For Riemann integrable $f:[0,1]\rightarrow{\mathbb{R}}$ with an oscillation function and $F(x):=\lambda x.\int_{0}^{x}f(t)dt$, the following set exists:*

[TABLE]

and has measure one. 7. (g)

(FTC)* The previous item for usco functions.* 8. (h)

For $f:[0,1]\rightarrow{\mathbb{R}}$ not continuous almost everywhere with oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$, there is $N\in{\mathbb{N}}$ and $E\subset[0,1]$ of positive measure such that $\textup{{osc}}_{f}(x)\geq\frac{1}{2^{N}}$ for $x\in E$.

We can replace ‘usco’ by ‘cliquish with an oscillation function’ in the above.

Proof.

First of all, most items follows as in the proof of Theorem 3.3. For instance, assume $\textup{{PHP}}_{[0,1]}$ and suppose for $f:[0,1]\rightarrow{\mathbb{R}}$ as in item (b) of the theorem, $D_{f}$ has positive measure. Then some $D_{k}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{k}}\}$ has positive measure by $\textup{{PHP}}_{[0,1]}$. Now proceed as in the first paragraph of the proof of Theorem 3.3 to derive a contradiction.

In turn, item (b) of the theorem implies $\textup{{PHP}}_{[0,1]}$ by fixing a sequence $(X_{n})_{n\in{\mathbb{N}}}$ of closed sets and considering the second paragraph of the proof of Theorem 3.3; the only modification is that $C_{h}$ has measure one, which implies that $\cup_{n\in{\mathbb{N}}}X_{n}$ has measure zero (instead of just being a strict subset), and $\textup{{PHP}}_{[0,1]}$ follows as required for the equivalence between the first two items. The equivalences for items (c)-(e) are proved in the same way.

For items (3.3) and (g), the usual epsilon-delta proof establishes that $F(x):=\int_{0}^{x}f(t)dt$ is continuous and that $F^{\prime}(y)=f(y)$ if and only if $f$ is continuous at $y$. Hence, the set $C_{f}$ is exactly the set in (3.3).

Finally, let $f:[0,1]\rightarrow{\mathbb{R}}$ be as in item (h) and define the closed set $D_{k}:=\{x\in[0,1]:\textup{{osc}}_{f}(x)\geq\frac{1}{2^{k}}\}$. By assumption, $D_{f}=\cup_{k\in{\mathbb{N}}}D_{k}$ has positive measure and $\textup{{PHP}}_{[0,1]}$ implies there is $k_{0}\in{\mathbb{N}}$ such that $D_{k_{0}}$ has positive measure, as required. For the reversal, assume item (h) and let $f:[0,1]\rightarrow{\mathbb{R}}$ be Riemann integrable oscillation function $\textup{{osc}}_{f}:[0,1]\rightarrow{\mathbb{R}}$. In case $C_{f}$ has measure one, we are done in light of item (b). In case $C_{f}$ does not have measure one, $f$ is not continuous almost everywhere and we can apply item (h). Let $N_{0}\in{\mathbb{N}}$ and $E\subset[0,1]$ of positive measure be such that $\textup{{osc}}_{f}(x)\geq\frac{1}{2^{N_{0}}}$ for $x\in E$. As in the first paragraph of this proof, $f$ is not Riemann integrable, a contradiction, and we are done. ∎

We note that $\textup{{PHP}}_{[0,1]}$ does not (seem to) provide a proof of the fact that sequences of measure zero sets have RM-codes. Similar to the third item of Theorem 2.5, we could study $\textup{{PHP}}_{[0,1]}$ restricted to sequences $(X_{n})_{n\in{\mathbb{N}}}$ such that $[0,1]\setminus\cup_{n\in{\mathbb{N}}}X_{n}$ is dense. By Theorem 3.3, this study would however require either $\textup{{WBCT}}_{[0,1]}$ or the restriction to Riemann integrable functions with dense $C_{f}$. This suggests an asymmetry between measure and category from the RM-point of view.

Thus, we have established equivalences involving $\textup{{PHP}}_{[0,1]}$ and the Vitali-Lebesgue theorem, rendering the latter unprovable in ${\textsf{{Z}}}_{2}^{\omega}$. The same holds for the restrictions to usco or cliquish functions while the restrictions to quasi-continuous functions are provable in $\textup{{ACA}}_{0}^{\omega}$. In contrast to the close relation between cliquishness and quasi-continuity, there is a great divide, some might say ‘abyss’, between $\textup{{ACA}}_{0}^{\omega}$ and ${\textsf{{Z}}}_{2}^{\omega}$. We have no explanation for this phenomenon at the moment.

Finally, the following theorem can be proved using the Baire category theorem.

For any continuous $f:[0,1]\rightarrow{\mathbb{R}}$, define $f_{0}=f$ and $f_{k+1}(x):=\int_{0}^{x}f_{k}(t)dt$. In case $(\forall x\in[0,1])(\exists k\in{\mathbb{N}})(f_{k}(x)=0)$, then $f$ is identically zero.

Replacing ‘continuous $f:[0,1]\rightarrow{\mathbb{R}}$’ by ‘Riemann integrable $f:[0,1]\rightarrow[0,1]$’ and ‘identically’ by ‘almost everywhere’, the resulting theorem is equivalent to $\textup{{PHP}}_{[0,1]}$. We conjecture there to be many more similar variations.

4. A Bigger Picture

In this section, we discuss the bigger picture associated with our above results.

• •

In Section 4.1, we discuss the intimate connection between our above results and the RM of the uncountability of ${\mathbb{R}}$ ([samBIG]).

• •

In Section 4.2, we exhibit parallels between some of our results and well-known properties of the Axiom of Choice in set theory.

• •

In Section 4.3, we discuss Banach’s theorem from [kanach] as follows:

the continuous nowhere differentiable functions are dense in $C([0,1])$.

We show that slight variations of Banach’s result are not provable in ${\textsf{{Z}}}_{2}^{\omega}$.

Regarding the final item, we shall study the notion of generalised absolute continuity, which is intermediate between the continuous and absolutely continuous functions. We refer to e.g. [bartle, gordonkordon, saks] for details but do mention that generalised absolute continuity is intimately connected to integration theory and the (most general version of) the fundamental theorem of calculus.

Finally, the reader should recall Remark 1.14 before reading Section 4.3. In the former remark, it is shown that closed sets as in Definition 1.8, i.e. without any additional representation, are readily found in basic analysis, like the study of regulated or bounded variation functions. The above study of usco functions provides similar, but less basic, examples. The results in Section 4.3 are the most basic in nature, as they pertain to continuous functions. The implications for coding in second-order RM are clearly significant.

4.1. Reflections on and of Reverse Mathematics

We discuss Figure 1 below which summarises how the above principles are related; we also discuss how our results are intimately connected to the RM of the uncountability of ${\mathbb{R}}$ from [samBIG].

First of all, we note that the statement a countable set is meagre has a trivial proof in $\textup{{RCA}}_{0}^{\omega}$, i.e. there is some non-trivial asymmetry between measure and category in Figure 1. Furthermore, we conjecture that $\textup{{BCT}}_{[0,1]}$ does not imply $\textup{{PHP}}_{[0,1]}$, say over ${\textsf{{Z}}}_{2}^{\omega}+\textup{{QF-AC}}^{0,1}$, and vice versa.

Secondly, we have developed the RM of the uncountability of ${\mathbb{R}}$ in [samBIG]. The following where shown to be equivalent over $\textup{{ACA}}_{0}^{\omega}+\textup{{QF-AC}}^{0,1}+\textup{{FIN}}$, where the axiom FIN allows one to neatly handle finite sets of reals.

1. (a)

The principle $\textup{{NIN}}_{\textup{{alt}}}$: for a sequence of finite sets $(X_{n})_{n\in{\mathbb{N}}}$ in $[0,1]$, there is $x\in[0,1]\setminus\cup_{n\in{\mathbb{N}}}X_{n}$. 2. (b)

For regulated $f:[0,1]\rightarrow{\mathbb{R}}$, there is a point $x\in[0,1]$ where $f$ is continuous (or quasi-continuous, or lower semi-continuous, or Darboux). 3. (c)

For regulated $f:[0,1]\rightarrow[0,1]$ with Riemann integral $\int_{0}^{1}f(x)dx=0$, there is $x\in[0,1]$ with $f(x)=0$ (Bourbaki, [boereng]*p. 61, Cor. 1). 4. (d)

(Volterra [volaarde2]) For regulated $f,g:[0,1]\rightarrow{\mathbb{R}}$, there is $x\in[0,1]$ such that $f$ and $g$ are both continuous or both discontinuous at $x$. 5. (e)

(Volterra [volaarde2]) For regulated $f:[0,1]\rightarrow{\mathbb{R}}$, there is either $q\in{\mathbb{Q}}\cap[0,1]$ where $f$ is discontinuous, or $x\in[0,1]\setminus{\mathbb{Q}}$ where $f$ is continuous. 6. (f)

(FTC) For regulated $f:[0,1]\rightarrow{\mathbb{R}}$, there is $y\in(0,1)$ where $F(x):=\lambda x.\int_{0}^{x}f(t)dt$ is differentiable with derivative equal to $f(y)$. 7. (g)

Blumberg’s theorem ([bloemeken]) restricted to regulated functions.

Clearly item (f) involves the fundamental theorem of calculus while item (d) involves Volterra’s early work, all restricted to regulated functions. We have obtained similar results for functions of bounded variation. In this paper, we have shown that item (f) for usco functions is equivalent to $\textup{{BCT}}_{[0,1]}$ (Theorem 2.25) while item (d) for usco functions is equivalent to $\textup{{PHP}}_{[0,1]}$ (Theorem 3.8). We have obtained similar results for cliquish functions (that come with an oscillation function).

In light of the above, we can say that the RM of the uncountability of ${\mathbb{R}}$ is the product of taking the RM of $\textup{{PHP}}_{[0,1]}$ and the RM of $\textup{{BCT}}_{[0,1]}$ and pushing everything down from usco/cliquish functions to the level of regulated/bounded variation functions. This observation provides a partial explanation why the RM of $\textup{{PHP}}_{[0,1]}$ and the RM of $\textup{{BCT}}_{[0,1]}$ can proceed along the same lines despite the apparent differences between measure and category.

Thirdly, with the gift on hindsight, we could obtain equivalences between the following principles, say working over the aforementioned system $\textup{{ACA}}_{0}^{\omega}+\textup{{QF-AC}}^{0,1}+\textup{{FIN}}$ from [samBIG]. The first item expresses that countable sets have measure zero, as can be found in Figure 1 on the right-hand side.

• •

For a sequence of finite sets $(X_{n})_{n\in{\mathbb{N}}}$ in $[0,1]$, $\cup_{n\in{\mathbb{N}}}X_{n}$ has measure zero.

• •

For regulated $f:[0,1]\rightarrow{\mathbb{R}}$, the set $C_{f}$ has measure one.

• •

The previous item for ‘continuity’ replaced by quasi-continuity or usco.

• •

For regulated $f:[0,1]\rightarrow[0,1]$ with Riemann integral $\int_{0}^{1}f(x)dx=0$, the set $\{x\in[0,1]:f(x)=0\}$ has measure one.

• •

A set $A\subset{\mathbb{R}}$ without limit points has measure zero.

• •

…

Similar equivalences are possible for functions of bounded variation, like in [samBIG]*§3.4, and the many intermediate classes of ‘generalised’ bounded variation (see [voordedorst]). A real challenge would be to study Carleson’s theorem in this context ([carleson1]).

Finally, the above analogy is not absolute: while symmetrically continuous functions feature in the RM of the uncountability of ${\mathbb{R}}$ (see [samBIG]*Theorem 3.9), we have not been able to obtain similar results for $\textup{{BCT}}_{[0,1]}$, $\textup{{PHP}}_{[0,1]}$, or $\textup{{WBCT}}_{[0,1]}$.

4.2. Reflections on and of set theory

We discuss the relationship between our results and set theory; the reader disinterested in foundational musings will skip this section. In a nutshell, we will show evidence for a parallel between our results and some central results in set theory, like the mercurial nature of the cardinality of the real numbers, disasters in the absence of the Axiom of Choice (AC for short), and the essential role of AC in measure and integration theory.

First of all, following the famous work of Gödel ([goeset]) and Cohen ([cohen1, cohen2]), the Continuum Hypothesis cannot be proved or disproved in ZFC, i.e. Zermelo-Fraenkel set theory with AC, the usual foundations of mathematics. Thus, the exact cardinality of ${\mathbb{R}}$ cannot be established in ZFC. A parallel observation in higher-order RM is that ${\textsf{{Z}}}_{2}^{\omega}$ cannot prove that there is no injection from ${\mathbb{R}}$ to ${\mathbb{N}}$ (see [dagsamX] for details). In a nutshell, the cardinality of ${\mathbb{R}}$ has a particularly mercurial nature, in both set theory and higher-order arithmetic.

Secondly, many standard results in mainstream mathematics are not provable in ZF, i.e. ZFC with AC removed, as explored in great detail [heerlijkheid]. The absence of AC is even said to lead to disasters in topology and analysis (see [kermend]). A parallel phenomenon was observed in [dagsamVII, dagsamV], namely that certain rather basic equivalences go through over $\textup{{RCA}}_{0}^{\omega}+\textup{{QF-AC}}^{0,1}$, but not over ${\textsf{{Z}}}_{2}^{\omega}$.

Examples include the equivalence between compactness results and local-global principles, which are intimately related according to Tao ([taokejes]). In this light, it is fair to say that disasters happen in both set theory and higher-order arithmetic in the absence of AC. It should be noted that $\textup{{QF-AC}}^{0,1}$ (not provable in ZF) can be replaced by NCC from [dagsamIX] (provable in ${\textsf{{Z}}}_{2}^{\Omega}$) in the aforementioned.

Thirdly, we discuss the essential role of AC in measure and integration theory, which leads to rather concrete parallel observations in higher-order arithmetic. Indeed, the full pigeonhole principle for measure spaces is not provable in ZF, which immediately follows from e.g. [heerlijkheid]*Diagram 3.4. A parallel phenomenon in higher-order arithmetic is that even the restriction to closed sets, namely $\textup{{PHP}}_{[0,1]}$ cannot be proved in ${\textsf{{Z}}}_{2}^{\omega}+\textup{{QF-AC}}^{0,1}$ by Theorem 3.6 (but ${\textsf{{Z}}}_{2}^{\Omega}$ suffices).

Moreover, a more ‘down to earth’ observation is obtained by comparing the topic of [hahakaka] and item (d) in Theorem 3.3. Regarding [hahakaka], the authors show that AC is needed to justify our intuition of the Lebesgue integral as the area under the graph of a function. Theorem 3.3 establishes the parallel observation that the same justification for the Riemann integral cannot be proved in ${\textsf{{Z}}}_{2}^{\omega}+\textup{{QF-AC}}^{0,1}$ (but ${\textsf{{Z}}}_{2}^{\Omega}$ suffices as usual).

4.3. On the scope of coding

In the above, we have obtained equivalences for the Baire category theorem as in $\textup{{BCT}}_{[0,1]}$, which is not provable in ${\textsf{{Z}}}_{2}^{\omega}$ by Theorem 2.2. By contrast, the restrictions of $\textup{{BCT}}_{[0,1]}$ to RM-codes and R2-representations are provable in $\textup{{ACA}}_{0}^{\omega}$, following [simpson2]*II.5.8 and [dagsamVII]*Theorem 7.10. A natural question is whether the latter ‘coded’ versions suffice for the study of $C([0,1])$, the space of continuous functions. In this section, we discuss this question and provide a counterexample based on generalised absolute continuity as in Definition 4.1.

First of all, Banach ([kanach]) already showed that ‘most’ continuous functions on the unit interval are nowhere differentiable, in the sense that such functions are dense in $C([0,1])$. Nemoto ([nemoto1]*Theorem 5.4) provides a proof of this fact in constructive mathematics, with the same coding for $C([0,1])$ and for open sets as in second-order RM ([simpson2]*II.5.6 and IV.2.13). In particular, the proof makes use of the second-order Baire category theorem ([simpson2]II.5.8 and [nemoto1]§3) and goes through (up to insignificant technical details) in $\textup{{RCA}}_{0}$ with intuitionistic logic, following the results in [nemoto2]. By [dagsamXIV]*Cor. 2.5, continuous functions on the unit interval have RM-codes, i.e. Banach’s aforementioned theorem about $C([0,1])$ without codes can be proved using the Baire category theorem for RM-codes, working in $\textup{{RCA}}_{0}^{\omega}+\textup{{WKL}}$.

Secondly, we now show that slight variations of the aforementioned theorem by Banach cannot be proved in ${\textsf{{Z}}}_{2}^{\omega}$. To this end, we introduce some sub-classes of $C([0,1])$ in Definition 4.1 that are connected to integration theory. In particular, $f:[0,1]\rightarrow{\mathbb{R}}$ is gauge (or: Perron, or: Denjoy) integrable if and only if there is $F\in\textup{{ACG}}^{*}$ such that $F^{\prime}=f$ almost everywhere. Details may be found in [bartle, gordonkordon, saks].

Definition 4.1** (Generalised absolute continuity).**

Fix $f:[0,1]\rightarrow{\mathbb{R}}$ and $X\subset[0,1]$.

• •

We say that $f\in\textup{{AC}}(X)$ if for all $\varepsilon>0$, there is $\delta>0$ such that for any finite collection of pairwise disjoint $(a_{0},b_{0}),(a_{1},b_{1}),\dots,(a_{k},b_{k})$ with endpoints in $X$ we have $\sum_{i\leq k}|a_{i}-b_{i}|<\delta\rightarrow\sum_{i\leq k}|f(a_{i})-f(b_{i})|<\varepsilon$.

• •

We say that $f\in\textup{{AC}}^{*}(X)$ if it satisfies the previous item with ‘$|f(a_{i})-f(b_{i})|$’ replaced by ‘$\textup{{osc}}_{f}([a_{i},b_{i}])$’ in the conclusion.

• •

We say that $f\in\textup{{ACG}}$ in case it is continuous on $[0,1]$ and there is a sequence of closed sets $(C_{n})_{n\in{\mathbb{N}}}$ such that $f_{\upharpoonright C_{n}}$ is $\textup{{AC}}(C_{n})$ for each $n\in{\mathbb{N}}$.

• •

We say that $f\in\textup{{ACG}}^{*}$ for the previous item with ‘AC’ replaced by ‘$\textup{{AC}}^{*}$’.

Lee establishes the equivalence of various definitions of $\textup{{ACG}}^{*}$ in [ACG]. The previous definition from [ACG] is the most basic one, in our opinion. By Remark 1.14, closed sets as in Definition 1.8, i.e. without any representation, already pop up ‘in the wild’ in the study of regulated and bounded variation functions. In this light, we should not assume closed sets to have extra constructive data, like RM-codes or R2-representations.

Thirdly, we have the following theorem where we note that ACG and $\textup{{ACG}}^{*}$ functions are not nowhere differentiable ([ACG]*Theorem 4 and [gordonkordon]*p. 235). In other words, the complements of ACG and $\textup{{ACG}}^{*}$ are larger than the class of nowhere differential functions from Banach’s aforementioned theorem.

Theorem 4.2**.**

The following cannot be proved in ${\textsf{{Z}}}_{2}^{\omega}+\textup{{IND}}_{0}$.

• •

Any function in ACG is differentiable at some point of the unit interval.

• •

Any function in $\textup{{ACG}}^{*}$ is differentiable at some point of the unit interval.

• •

The complement of ACG is dense in $C([0,1])$.

• •

The complement of $\textup{{ACG}}^{*}$ is dense in $C([0,1])$.

Proof.

First of all, a continuous and nowhere differentiable function is readily defined in $\textup{{RCA}}_{0}$ following the results in [nemoto1]. One could also use the well-known definition of Weierstrass’ function and establish its properties directly using [simpson2]*II.6.5.

Secondly, we recall that $\textup{{NIN}}_{[0,1]}$ is not provable in ${\textsf{{Z}}}_{2}^{\omega}+\textup{{IND}}_{0}$ by [dagsamXI]*Theorem 2.16. To establish the theorem, we show that all items imply $\textup{{NIN}}_{[0,1]}$ over $\textup{{ACA}}_{0}^{\omega}+\textup{{IND}}_{0}$. To this end, let $Y:[0,1]\rightarrow{\mathbb{N}}$ be an injection, fix continuous $f:[0,1]\rightarrow{\mathbb{R}}$, and define $C_{n}:=\{x\in[0,1]:Y(x)\leq n\}$. Using $\textup{{IND}}_{0}$, one proves that each $C_{n}$ is closed (because finite), and $[0,1]=\cup_{n\in{\mathbb{N}}}C_{n}$ by assumption. By definition, $f_{\upharpoonright C_{n}}$ is in $\textup{{AC}}(C_{n})$ and $\textup{{AC}}^{*}(C_{n})$, again using $\textup{{IND}}_{0}$, for $n\in{\mathbb{N}}$. Hence, we have shown that $C([0,1])$ equals ACG and $\textup{{ACG}}^{*}$, which yields a contradiction with the first two items, as Weierstrass’ function is nowhere differentiable. The last two items similarly yield a contradiction, and we are done. ∎

We note that the notion of generalised bounded variation ([gordonkordon]) can be treated in the same way as in the previous theorem. Similarly, one can treat Gordon’s classes ACGs and $\textup{{ACG}}_{\delta}$ from [gordon1, gordonkordon].

Acknowledgement 4.3**.**

We thank Anil Nerode for his valuable advice, especially the suggestion of studying nsc for the Riemann integral, and discussions related to Baire classes. We thank Dave R. Renfro for his efforts in providing a most encyclopedic summary of analysis, to be found online. Our research was supported by the Deutsche Forschungsgemeinschaft via the DFG grant SA3418/1-1 and the Klaus Tschira Boost Fund via the grant Projekt KT43. We express our gratitude towards the aforementioned institutions.

Appendix A Technical Appendix: introducing Reverse Mathematics

We discuss Reverse Mathematics (Section A.1) and introduce -in full detail- Kohlenbach’s base theory of higher-order Reverse Mathematics (Section A.2). Some common notations may be found in Section A.3.

A.1. Introduction

Reverse Mathematics (RM for short) is a program in the foundations of mathematics initiated around 1975 by Friedman ([fried, fried2]) and developed extensively by Simpson ([simpson2]). The aim of RM is to identify the minimal axioms needed to prove theorems of ordinary, i.e. non-set theoretical, mathematics.

We refer to [stillebron] for a basic introduction to RM and to [simpson2, simpson1, damurm] for an overview of RM. We expect basic familiarity with RM, but do sketch some aspects of Kohlenbach’s higher-order RM ([kohlenbach2]) essential to this paper, including the base theory $\textup{{RCA}}_{0}^{\omega}$ (Definition A.1).

First of all, in contrast to ‘classical’ RM based on second-order arithmetic ${\textsf{{Z}}}_{2}$, higher-order RM uses a subset of $\textsf{{L}}_{\omega}$, the richer language of higher-order arithmetic. Indeed, while the former is restricted to natural numbers and sets of natural numbers, higher-order arithmetic can accommodate sets of sets of natural numbers, sets of sets of sets of natural numbers, et cetera. To formalise this idea, we introduce the collection of all finite types $\mathbf{T}$, defined by the two clauses:

(i) $0\in\mathbf{T}$ and (ii) If $\sigma,\tau\in\mathbf{T}$ then $(\sigma\rightarrow\tau)\in\mathbf{T}$,

where [math] is the type of natural numbers, and $\sigma\rightarrow\tau$ is the type of mappings from objects of type $\sigma$ to objects of type $\tau$. In this way, $1\equiv 0\rightarrow 0$ is the type of functions from numbers to numbers, and $n+1\equiv n\rightarrow 0$. Viewing sets as given by characteristic functions, we note that ${\textsf{{Z}}}_{2}$ only includes objects of type [math] and $1$.

Secondly, the language $\textsf{{L}}_{\omega}$ includes variables $x^{\rho},y^{\rho},z^{\rho},\dots$ of any finite type $\rho\in\mathbf{T}$. Types may be omitted when they can be inferred from context. The constants of $\textsf{{L}}_{\omega}$ include the type [math] objects $0,1$ and $<_{0},+_{0},\times_{0},=_{0}$ which are intended to have their usual meaning as operations on ${\mathbb{N}}$. Equality at higher types is defined in terms of ‘$=_{0}$’ as follows: for any objects $x^{\tau},y^{\tau}$, we have

[TABLE]

if the type $\tau$ is composed as $\tau\equiv(\tau_{1}\rightarrow\dots\rightarrow\tau_{k}\rightarrow 0)$. Furthermore, $\textsf{{L}}_{\omega}$ also includes the recursor constant $\mathbf{R}_{\sigma}$ for any $\sigma\in\mathbf{T}$, which allows for iteration on type $\sigma$-objects via generalisations of the defining axiom in item (c) of Definition A.1. Formulas and terms are defined as usual. One obtains the sub-language $\textsf{{L}}_{n+2}$ by restricting the above type formation rule to produce only type $n+1$ objects (and related types of similar complexity).

A.2. The base theory of higher-order Reverse Mathematics

We introduce Kohlenbach’s base theory $\textup{{RCA}}_{0}^{\omega}$, first introduced in [kohlenbach2]*§2.

Definition A.1**.**

The base theory $\textup{{RCA}}_{0}^{\omega}$ consists of the following axioms.

1. (a)

Basic axioms expressing that $0,1,<_{0},+_{0},\times_{0}$ form an ordered semi-ring with equality $=_{0}$. 2. (b)

Basic axioms defining the well-known $\Pi$ and $\Sigma$ combinators (aka $K$ and $S$ in **[avi2]), which allow for the definition of $\lambda$-abstraction. 3. (c)

The defining axiom of the recursor constant $\mathbf{R}_{0}$: for $m^{0}$ and $f^{1}$:

[TABLE] 4. (d)

The axiom of extensionality: for all $\rho,\tau\in\mathbf{T}$, we have:

[TABLE] 5. (e)

The induction axiom for quantifier-free formulas of $\textsf{{L}}_{\omega}$. 6. (f)

$\textup{{QF-AC}}^{1,0}$: the quantifier-free Axiom of Choice as in Definition A.2.

Note that variables (of any finite type) are allowed in quantifier-free formulas of the language $\textsf{{L}}_{\omega}$: only quantifiers are banned. Gödel called the functionals obtained from $\mathbf{R}_{\rho}$ for all $\rho\in\mathbf{T}$ the primitive recursive functionals of finite type. Their theory is axiomatised by Gödel’s system $T$, studied in detail in [avi2]*Section 2.2.

Definition A.2**.**

The axiom QF-AC consists of the following for all $\sigma,\tau\in\textbf{T}$:

[TABLE]

for any quantifier-free formula $A$ in the language of $\textsf{{L}}_{\omega}$.

As discussed in [kohlenbach2]*§2, $\textup{{RCA}}_{0}^{\omega}$ and $\textup{{RCA}}_{0}$ prove the same sentences ‘up to language’ as the latter is set-based and the former function-based. This conservation results is obtained via the so-called ECF-interpretation, which we now discuss.

Remark A.3** (The ECF-interpretation).**

The (rather) technical definition of ECF may be found in [troelstra1]p. 138, §2.6. Intuitively, the ECF-interpretation $[A]_{\textup{{ECF}}}$ of a formula $A\in\textsf{{L}}_{\omega}$ is just $A$ with all variables of type two and higher replaced by type one variables ranging over so-called ‘associates’ or ‘RM-codes’ (see [kohlenbach4]§4); the latter are (countable) representations of continuous functionals. The ECF-interpretation connects $\textup{{RCA}}_{0}^{\omega}$ and $\textup{{RCA}}_{0}$ (see [kohlenbach2]*Prop. 3.1) in that if $\textup{{RCA}}_{0}^{\omega}$ proves $A$, then $\textup{{RCA}}_{0}$ proves $[A]_{\textup{{ECF}}}$, again ‘up to language’, as $\textup{{RCA}}_{0}$ is formulated using sets, and $[A]_{\textup{{ECF}}}$ is formulated using types, i.e. using type zero and one objects.

In light of the widespread use of codes in RM and the common practise of identifying codes with the objects being coded, it is no exaggeration to refer to ECF as the canonical embedding of higher-order into second-order arithmetic.

A.3. Notations and the like

We introduce the usual notations for common mathematical notions, like real numbers, as also introduced in [kohlenbach2].

Definition A.4** (Real numbers and related notions in $\textup{{RCA}}_{0}^{\omega}$).**

1. (a)

Natural numbers correspond to type zero objects, and we use ‘$n^{0}$’ and ‘$n\in{\mathbb{N}}$’ interchangeably. Rational numbers are defined as signed quotients of natural numbers, and ‘$q\in{\mathbb{Q}}$’ and ‘$<_{{\mathbb{Q}}}$’ have their usual meaning. 2. (b)

Real numbers are coded by fast-converging Cauchy sequences $q_{(\cdot)}:{\mathbb{N}}\rightarrow{\mathbb{Q}}$, i.e.  such that $(\forall n^{0},i^{0})(|q_{n}-q_{n+i}|<_{{\mathbb{Q}}}\frac{1}{2^{n}})$. We use Kohlenbach’s ‘hat function’ from [kohlenbach2]*p. 289 to guarantee that every $q^{1}$ defines a real number. 3. (c)

We write ‘$x\in{\mathbb{R}}$’ to express that $x^{1}:=(q^{1}_{(\cdot)})$ represents a real as in the previous item and write $[x](k):=q_{k}$ for the $k$-th approximation of $x$. 4. (d)

Two reals $x,y$ represented by $q_{(\cdot)}$ and $r_{(\cdot)}$ are equal, denoted $x=_{{\mathbb{R}}}y$, if $(\forall n^{0})(|q_{n}-r_{n}|\leq{2^{-n+1}})$. Inequality ‘$<_{{\mathbb{R}}}$’ is defined similarly. We sometimes omit the subscript ‘${\mathbb{R}}$’ if it is clear from context. 5. (e)

Functions $F:{\mathbb{R}}\rightarrow{\mathbb{R}}$ are represented by $\Phi^{1\rightarrow 1}$ mapping equal reals to equal reals, i.e. extensionality as in $(\forall x,y\in{\mathbb{R}})(x=_{{\mathbb{R}}}y\rightarrow\Phi(x)=_{{\mathbb{R}}}\Phi(y))$. 6. (f)

The relation ‘$x\leq_{\tau}y$’ is defined as in (A.1) but with ‘$\leq_{0}$’ instead of ‘$=_{0}$’. Binary sequences are denoted ‘$f^{1},g^{1}\leq_{1}1$’, but also ‘$f,g\in C$’ or ‘$f,g\in 2^{{\mathbb{N}}}$’. Elements of Baire space are given by $f^{1},g^{1}$, but also denoted ‘$f,g\in{\mathbb{N}}^{{\mathbb{N}}}$’. 7. (g)

For a binary sequence $f^{1}$, the associated real in $[0,1]$ is $\mathbb{r}(f):=\sum_{n=0}^{\infty}\frac{f(n)}{2^{n+1}}$. 8. (h)

Sets of type $\rho$ objects $X^{\rho\rightarrow 0},Y^{\rho\rightarrow 0},\dots$ are given by their characteristic functions $F^{\rho\rightarrow 0}_{X}\leq_{\rho\rightarrow 0}1$, i.e. we write ‘$x\in X$’ for $F_{X}(x)=_{0}1$.

For completeness, we list the following notational convention for finite sequences.

Notation A.5** (Finite sequences).**

The type for ‘finite sequences of objects of type $\rho$’ is denoted $\rho^{*}$, which we shall only use for $\rho=0,1$. Since the usual coding of pairs of numbers goes through in $\textup{{RCA}}_{0}^{\omega}$, we shall not always distinguish between [math] and $0^{*}$. Similarly, we assume a fixed coding for finite sequences of type $1$ and shall make use of the type ‘$1^{*}$’. In general, we do not always distinguish between ‘$s^{\rho}$’ and ‘$\langle s^{\rho}\rangle$’, where the former is ‘the object $s$ of type $\rho$’, and the latter is ‘the sequence of type $\rho^{*}$ with only element $s^{\rho}$’. The empty sequence for the type $\rho^{*}$ is denoted by ‘$\langle\rangle_{\rho}$’, usually with the typing omitted.

Furthermore, we denote by ‘$|s|=n$’ the length of the finite sequence $s^{\rho^{*}}=\langle s_{0}^{\rho},s_{1}^{\rho},\dots,s_{n-1}^{\rho}\rangle$, where $|\langle\rangle|=0$, i.e. the empty sequence has length zero. For sequences $s^{\rho^{*}},t^{\rho^{*}}$, we denote by ‘$s*t$’ the concatenation of $s$ and $t$, i.e. $(s*t)(i)=s(i)$ for $i<|s|$ and $(s*t)(j)=t(|s|-j)$ for $|s|\leq j<|s|+|t|$. For a sequence $s^{\rho^{*}}$, we define $\overline{s}N:=\langle s(0),s(1),\dots,s(N-1)\rangle$ for $N^{0}<|s|$. For a sequence $\alpha^{0\rightarrow\rho}$, we also write $\overline{\alpha}N=\langle\alpha(0),\alpha(1),\dots,\alpha(N-1)\rangle$ for any $N^{0}$. By way of shorthand, $(\forall q^{\rho}\in Q^{\rho^{*}})A(q)$ abbreviates $(\forall i^{0}<|Q|)A(Q(i))$, which is (equivalent to) quantifier-free if $A$ is.