On the computational properties of the Baire category theorem

Abstract

Computability theory is a discipline in the intersection of computer science and mathematical logic where the fundamental question is:

Given two mathematical objects X and Y, does X compute Y in principle?

In case $X$ and $Y$ are real numbers, Turing’s famous ‘machine’ model provides the standard interpretation of ‘computation’ for this question. To formalise computation involving (total) abstract objects, Kleene introduced his S1–S9 computation schemes. In turn, Dag Normann and the author have introduced a version of the lambda calculus involving fixed point operators that exactly captures S1–S9 and accommodates partial objects. In this paper, we use this new model to develop the computability theory of various well-known theorems due to Baire and Volterra and related results; these theorems only require basic mathematical notions such as continuity, open sets, and density. We show that these theorems due to Baire and Volterra are computationally equivalent from the point of view of our new model, sometimes working in rather tame fragments of Gödel’s $T$ .

Keywords

higher-order computability theory Kleene S1–S9 Baire category theorem Baire 1 functions

1. Introduction

1.1. Motivation and overview

Computability theory is a discipline in the intersection of theoretical computer science and mathematical logic where the fundamental question is as follows:

Given two mathematical objects X and Y, does X compute Y in principle?

In case $X$ and $Y$ are real numbers, Turing’s [1] famous ‘machine’ model is the standard approach to this question, that is, ‘computation’ is interpreted in the sense of Turing machines. To formalise computation involving (total) abstract objects, such as functions on the real numbers or well-orderings of the reals, Kleene [2] introduced his S1–S9 computation schemes. We assume basic familiarity with the latter as in Longley and Normann [3], while an introductory sketch may be found in Section 1.3.1.

In turn, Dag Normann and the author [4] have recently introduced a version of the lambda calculus involving fixed point operators that exactly captures S1–S9 and accommodates partial objects. In this paper, we use this new model to develop the computability theory of various theorems due to Baire and Volterra and related results. We show that these theorems are computationally equivalent from the point of view of our new model, as laid down by Definition 1.1. We stress that these theorems due to Baire and Volterra only require basic mathematical notions, such as continuity, open sets, and density. All non-basic definitions and some background may be found in Sections 1.2 and 1.3.

In more detail, consider the following three theorems proposed by Baire [5] and Volterra [6] from the 19th century. The notion of Baire 1 function is also by Baire [5] and means that the function is the limit of a sequence of continuous functions.

(Baire category theorem) Let $(O_{n})_{n \in N}$ be a sequence of dense and open sets of reals. Then the intersection $\cap_{n \in N} O_{n}$ is non-empty (and dense).

(Volterra) There is no function that is continuous on the rationals and discontinuous on the irrationals.

(Baire) For $f : [0, 1] \to R$ in Baire 1, the set of continuity points is non-empty (and dense).

The first item is well-studied in other computational approaches to mathematics such as computable analysis [7,8] or constructive mathematics Bishop [9, p.84] and Nemoto [10]). The second item is a mainstay of popular mathematics [11,12], and usually proved via the first item [13]. More detailed background may be found in Section 1.2.

The above theorems yield the following natural computational operations. A functional operating item (a) is called a Baire realiser [14].

(a)
On input a sequence of dense and open sets of reals $(O_{n})_{n \in N}$ , output a real $x \in \cap_{n \in N} O_{n}$ .
(b)
On input a Baire 1 function from reals to reals, output a rational where it is discontinuous, or an irrational where it is continuous.
(c)
On input a Baire 1 function from reals to reals, output a point of continuity.
We show in Section 2 that the operations in items (a)–(c), as well as a number of related ones, are computationally equivalent as defined in Definition 1.1. We emphasise that each of the items (a)–(c) should be viewed as a specification for a class of (possibly partial) functionals that produce certain outputs given certain inputs. The computational equivalence between two specifications $(A)$ and $(B)$ is defined as follows, where ${e} (\vec{α})$ is the Kleene algorithm with index $e$ and inputs $\vec{α}$ .
Definition 1.1 Computational equivalence

Let $(A)$ and $(B)$ be specifications for classes of functionals. We say that $(A)$ and $(B)$ are computationally equivalent if there are algorithms with index $e, d \in N$ such that:

for any functional $Γ$ satisfying (A), the functional ${e} (Γ)$ satisfies (B),

for any functional $Λ$ satisfying (B), the functional ${d} (Λ)$ satisfies (A).

Computational equivalence relative to $κ$ is the above allowing

{e} (Γ, κ)

and

{d} (Λ, κ)

In most cases below, we can replace Kleene’s S1–S9 or our model from Normann and Sanders [4] by rather tame fragments of Gödel’s $T$ and Feferman’s $μ^{2}$ from Section 1.3.2. We note that our specifications are generally restricted to functionals that map $R \to R$ functions to $R \to R$ functions, or constructs of similar rank limitations.

Finally, to study continuous functions in computability theory (or constructive mathematics), such functions are usually given together with a modulus of continuity, that is, a constructive enrichment providing computational information about continuity (Intuitively speaking, a modulus of continuity is a functional that witnesses the usual ‘epsilon-delta’ definition of continuity. In this way, a modulus of continuity essentially outputs a suitable ‘delta’ on input any $ε > 0$ and $x$ in the domain, as in the usual epsilon-delta definition.) As discussed in detail in Section 2.1, our study of Baire 1 functions in computability theory also makes use of some kind of constructive enrichment, namely that Baire 1 functions are given together with their oscillation function (see Definition 2.1), a construct going back to [15,16].

1.2. Volterra’s early work and related results

We introduce Volterra’s [6] early work as it pertains to this paper. We let $R$ be the set of real numbers while $Q$ is the set of rational numbers.

First of all, Riemann’s [17] integral was groundbreaking in its day for a number of reasons, including its ability to integrate functions with infinitely many points of discontinuity. A natural question is then ‘how discontinuous’ a Riemann integrable function can be. In this context, Thomae [18, p.14, Section 20] introduced the following function $T : R \to R$ around 1875:

T (x) := {\begin{cases} 0 & if x \in R ∖ Q, \\ \frac{1}{q} & if x = \frac{p}{q} and p, q are co-prime . \end{cases}

($\textsf{T}$)

Thomae’s function

T

is Riemann integrable on

[0, 1]

, but has a dense set of points of discontinuity, namely

Q

, and a dense set of points of continuity, namely

R ∖ Q

The perceptive student, upon seeing Thomae’s function as in (), 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 [6] already established this negative result about 20 years before the publication of the Baire category theorem, using a rather elementary argument.

Secondly, as to the content of Volterra’s [6], we find the following theorem on the first page, where a function is pointwise discontinuous if it has a dense set of continuity points.

Theorem 1.2 Volterra [6]

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 [6]

There is no $R \to R$ function that is continuous on $Q$ and discontinuous on $R ∖ Q$ .

Thirdly, we shall study Volterra’s theorem and corollary restricted to Baire 1 functions (see Section 1.3.3). The latter types of functions are automatically ‘pointwise discontinuous’ in the sense of Volterra.

Fourth, Volterra’s [6] results are generalised in Silva and Wu [19] and Gauld [20]. The following theorem is immediate from these generalisations.

Theorem 1.4
For any countable dense set $D \subset [0, 1]$ and $f : [0, 1] \to R$ , either $f$ is discontinuous at some point in $D$ or continuous at some point in $R ∖ D$ .

Perhaps surprisingly, this generalisation is computationally equivalent to the original (both restricted to Baire 1 functions).

Fifth, the Baire category theorem for the real line was first proved by Osgood [21] and later by Baire [5] in a more general setting.
Theorem 1.5 Baire category theorem

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

Based on this theorem, Dag Normann and the author [14] have introduced the following.

Definition 1.6
A Baire realiser $ξ : (N \to (R \to N)) \to R$ is a functional such that if $(O_{n})_{n \in N}$ is a sequence of dense open sets of reals, $ξ (λ n . O_{n}) \in \cap_{n \in N} O_{n}$ .

We shall obtain a number of computational equivalences (Definition 1.1) for Baire realisers in Section 2. To this end, we will need some preliminaries and definitions, as in Section 1.3.

Finally, in light of our definition of open set in Definition 1.8, our study of the Baire category theorem (and the same in Normann and Sanders [14]) is based on a most general definition of open set, that is, no additional (computational) information is given. Besides the intrinsic interest of such an investigation, there is a deeper reason, as discussed in Section 3.1. In a nutshell, in the study of Baire 1 functions, one readily encounters open sets ‘in the wild’ that do not come with any additional (computational) information. In fact, finding such additional (computational) information turns out to be at least as hard as finding a Baire realiser.
1.3. Preliminaries and definitions

We briefly introduce Kleene’s higher-order computability theory in Section 1.3.1. We introduce some essential axioms (Section 1.3.2) and definitions (Section 1.3.3). A full introduction may be found in, for example, Section 2 in Normann and Sanders [22] or Longley and Normann [3]. Since Kleene’s computability theory borrows heavily from type theory, we shall often use common notations from the latter; for instance, the natural numbers are type $0$ objects, denoted $n^{0}$ or $n \in N$ . Similarly, elements of Baire space are type 1 objects, denoted $f \in N^{N}$ or $f^{1}$ . Mappings from Baire space $N^{N}$ to $N$ are denoted $Y : N^{N} \to N$ or $Y^{2}$ . An overview of this kind of notation is in Appendix A and the general literature (see, in particular, Longley and Normann [3]).

1.3.1. Kleene’s computability theory

Our main results are in computability theory and we make our notion of ‘computability’ precise as follows:

(I)
We adopt $ZFC$ , that is, Zermelo–Fraenkel set theory with the axiom of choice, as the official metatheory for all results, unless explicitly stated otherwise.
(II)
We adopt Kleene’s notion of higher-order computation as given by his nine clauses S1–S9 (see Chapter 5 in Longley and Normann [3] or Kleene [2]) as our official notion of ‘computable’ involving total objects.
We mention that S1–S8 are rather basic and merely introduce a kind of higher-order primitive recursion with higher-order parameters. The real power comes from S9, which essentially hard codes the recursion theorem for S1–S9 computability in an ad hoc way. By contrast, the recursion theorem for Turing machines is derived from first principles in Soare [23].

On a historical note, it is part of the folklore of computability theory that many have tried (and failed) to formulate models of computation for objects of all finite types and in which one derives the recursion theorem in a natural way. For this reason, Kleene ultimately introduced S1–S9, which were initially criticised for their aforementioned ad hoc nature, but eventually received general acceptance.

Now, Dag Normann and the author [4] have introduced a new computational model based on the lambda calculus with the following properties:
S1–S8 are included while the ‘ad hoc’ scheme S9 is replaced by more natural (least) fixed point operators,

the new model exactly captures S1–S9 computability for total objects,

the new model accommodates ‘computing with partial objects’,

the new model is more modular than S1–S9 in that sub-models are readily obtained by leaving out certain fixed point operators.
We refer to Longley and Normann [3] and Normann and Sanders [4] for a thorough overview of higher-order computability theory. We do mention the distinction between ‘normal’ and ‘non-normal’ functionals based on the following definition from Section 5.4 of Longley and Normann [3] . We only make use of $\exists^{n}$ for $n = 2, 3$ , as defined in Section 1.3.2.
Definition 1.7
For $n \geq 2$ , a functional of type $n$ is called normal if it computes Kleene’s $\exists^{n}$ following S1–S9, and non-normal otherwise.

It is a historical fact that higher-order computability theory, based on Kleene’s S1–S9 schemes, has focused primarily on the world of normal functionals; this opinion can be found in Section 5.4 of Longley and Normann [3]. Nonetheless, we have previously studied the computational properties of new non-normal functionals, namely those that compute the objects claimed to exist by:
covering theorems proposed by Heine-Borel, Vitali, and Lindelöf [24–26],

the Baire category theorem [14],

local–global principles such as Pincherle’s theorem [27],

weak fragments of the axiom of (countable) choice [28],

the uncountability of $R$ and the Bolzano–Weierstrass theorem for countable sets in Cantor space [22,29],

the Jordan decomposition theorem and related results [4,30].
In this paper, we greatly extend the study of the Baire category theorem mentioned in the second item; the operations sketched in Section 1.1 are all non-normal, in that they do not compute Kleene’s $\exists^{2}$ from Section 1.3.2.

Finally, we have obtained many computational equivalences in Normann and Sanders [4] and Sanders [31], mostly related to the Jordan decomposition theorem and the uncountability of $R$ . With considerable effort, we even obtained terms of Gödel’s $T$ witnessing (some of) these equivalences (see, e.g. Theorem 4.14 of Normann and Sanders [4]). Many of the below equivalences go through in tame fragments Gödel’s $T$ extended with Feferman’s $μ^{2}$ from Section 1.3.2.
1.3.2. Some comprehension functionals

In Turing-style computability theory, computational hardness is measured in terms of where the oracle set fits in the well-known comprehension hierarchy. 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, that is, only parameters over $N$ and $N^{N}$ are allowed in formula classes such as $Π_{k}^{1}$ and $Σ_{k}^{1}$ .

First of all, the functional $φ^{2}$ , also called Kleene’s quantifier $\exists^{2}$ , as it is clearly discontinuous at $f = 11 \dots$ ; in fact, $\exists^{2}$ is (computationally) equivalent to the existence of $F : R \to R$ such that $F (x) = 1$ if $x >_{R} 0$ , and $0$ otherwise via Grilliot’s trick (see Section 3 of Kohlenbach [32]).

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

($\exists^{2}$)

Related to (), the functional

μ^{2}

in () is called Feferman’s $μ$ [33].

\begin{aligned} (\exists μ^{2}) (\forall f^{1}) ([(\exists n) (f (n) = 0) \end{aligned}

($\mu^{2}$)

\begin{aligned} \to [f (μ (f)) = 0 \land (\forall i < μ (f)) (f (i) \neq 0)] \land [(\forall n) (f (n) \neq 0) \to μ (f) = 0]) . \end{aligned}

We have ()

\leftrightarrow

() over Kohlenbach’s base theory [32], while

\exists^{2}

and

μ^{2}

are also computationally equivalent. In Supplement IV of Hilbert and Bernays [34] , the authors formalise considerable swaths of mathematics using only

μ^{2}

Secondly, the functional $S^{2}$ in () is called the Suslin functional (Kohlenbach [32]).

(\exists S^{2} \leq_{2} 1) (\forall f^{1}) [(\exists g^{1}) (\forall n^{0}) (f (\bar{g} n) = 0) \leftrightarrow S (f) = 0] .

(S²)

By definition, the Suslin functional

S^{2}

can decide whether a

Σ_{1}^{1}

formula as in the left-hand side of () is true or false. We similarly define the functional

S_{k}^{2}

, which decides the truth or falsity of

Σ_{k}^{1}

formulas. We note that the Feferman–Sieg operators

ν_{n}

from Buchholz et al. [35, p.29] are essentially

S_{n}^{2}

strengthened to return a witness (if existant) to the

Σ_{n}^{1}

formula at hand.

Thirdly, the functional $E^{3}$ clearly computes $\exists^{2}$ and $S_{k}^{2}$ for any $k \in N$ :

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

($\exists^{3}$)

The functional from () is also called Kleene’s quantifier $\exists^{3}$ , and we use the same – by now obvious – convention for other functionals. In Supplement IV of Hilbert and Bernays [34], a functional

ν^{3}

is introduced, and the latter is essentially

\exists^{3}

which also provides a witness like

ν_{k}

does.

In conclusion, the operations sketched in Section 1.1 are computable in $\exists^{3}$ but not in any $S_{k}^{2}$ , is established in Section 6 of Normann and Sanders [14]. Many non-normal functionals exhibit the same ‘computational hardness’ and we merely view this as support for the development of a separate scale for classifying non-normal functionals.

1.3.3. Some definitions

We introduce some definitions needed, mostly stemming from mainstream mathematics. We note that subsets of $R$ are given by their characteristic functions (Definition 1.8), where the latter is common in measure and probability theory. In this paper, ‘continuity’ refers to the usual ‘epsilon-delta’ definition, well-known from the literature.

Zeroth of all, we make use of the usual definition of a (open) set, where $B (x, r)$ is the open ball with radius $r > 0$ centred at $x \in R$ .

Definition 1.8 Set

Subsets $A \subset R$ are given by its characteristic function $F_{A} : R \to {0, 1}$ , that is, we write $x \in A$ for $F_{A} (x) = 1$ for all $x \in R$ .

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

A subset $C \subset R$ is closed if the complement $R ∖ C$ is open.

The reader will find more motivation for our definition of open set in Section 3.1.

First of all, we study the following continuity notions, in part by Baire [5].

Definition 1.9 Weak continuity

For $f : [0, 1] \to R$ , we have the following:

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

$f$ is lower semi-continuous at $x_{0} \in [0, 1]$ if $f (x_{0}) \leq_{R} lim inf_{x \to 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 \to x_{0} -} f (x)$ and $f (x_{0} +) = lim_{x \to x_{0} +} f (x)$ exist.

In case the weak continuity notion is satisfied at each point of the domain, the associated function satisfies the italicised notion.

Secondly, Baire [5] introduces the hierarchy of Baire classes. We shall only need the first Baire class, defined as follows.

Definition 1.10 (Baire 1 function)

A function $f : R \to R$ is Baire 1 if there exists a sequence $(f_{n})_{n \in N}$ of continuous $R \to R$ functions such that $f (x) = lim_{n \to \infty} f_{n} (x)$ for all $x \in R$ . We use $B_{1}$ to denote the class of Baire 1 functions.

Thirdly, the following sets are often crucial in proofs relating to discontinuous functions, as can be observed in, for example, Theorem 0.36 in Appell et al. [36]

Definition 1.11
The sets $C_{f}$ and $D_{f}$ , respectively, gather the points where $f : R \to R$ is continuous and discontinuous.

One problem with the sets $C_{f}, D_{f}$ is that the definition of continuity involves quantifiers over $R$ . In general, deciding whether a given $R \to 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}$ do exist, but are not available as inputs for algorithms in general. A solution is discussed in Section 2.1.

Fourth, we introduce two notions to be found already in, for example, the work of Volterra [6], Smith [37], and Hankel [15] .
Definition 1.12

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

A function $f : R \to R$ is pointwise discontinuous in case $C_{f}$ is dense in $R$ .

A set $A \subset R$ is nowhere dense (in $R$ ) if $A$ is not dense in any open interval.

Fifth, we need the ‘intermediate value property’, also called ‘Darboux property’.
Definition 1.13 (Darboux property)

Let $f : [0, 1] \to R$ be given.

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

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

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

2. Baire category theorem and computational equivalences

In this section, we obtain the computational equivalences sketched in Section 1.1 involving the Baire category theorem and basic properties of Baire 1 and pointwise discontinuous functions (see Section 1.3.3 for the latter). We will always assume $μ^{2}$ or $\exists^{2}$ from Section 1.3.2, as motivated in Remark 2.7.

2.1. Preliminaries

As discussed in Section 1.1, we shall study Baire 1 functions that are given together with their oscillation function (see Definition 2.1 for the latter). We briefly discuss and motivate this construct in this section.

First of all, the study of regulated functions in Normann and Sanders [4,29,30] is really only possible thanks to the associated left and right limits (see Definition 1.9) and the fact that the latter are computable in $\exists^{2}$ . Indeed, for regulated $f : R \to R$ , the formula

f is continuous at a given real x \in R

(\textsf{C})

involves quantifiers over

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. Now, we would like to use an analogous approach for the study of pointwise discontinuous or Baire 1 functions. To this end, we consider the oscillation function defined as follows.

Definition 2.1 (Oscillation function)

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

Riemann [16] and Hankel [15] already considered the notion of oscillation in the context of Riemann integration. Our main interest in Definition 2.1 is that () is now equivalent to the arithmetical formula ${osc}_{f} (x) = 0$ . Hence, in the presence of ${osc}_{f}$ , we can again define $D_{f}$ – using nothing more than $\exists^{2}$ – and proceed with the usual (textbook) proofs. In the below, we will (only) study Baire 1 and pointwise discontinuous functions $f : [0, 1] \to R$ that are given together with the associated oscillation function ${osc}_{f} : [0, 1] \to R$ . We stress that such ‘constructive enrichment’ is common in computability theory and constructive mathematics.

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

D_{k} := {x \in [0, 1] : {osc}_{f} (x) \geq \frac{1}{2^{k}}} for all k \in N .

(2.1)

The complement

O_{n} := [0, 1] ∖ D_{k}

can be shown to be open and dense, as required for the antecedent of the Baire category theorem. This connection also goes in the other direction as follows: fix a sequence of dense and open sets

(O_{n})_{n \in N}

in the unit interval, define

X_{n} := [0, 1] ∖ O_{n}

and consider the following function

h : [0, 1] \to R

h (x) := {\begin{cases} 0 & x \notin \cup_{m \in N} X_{m}, \\ \frac{1}{2^{n + 1}} & x \in X_{n} and n is the least such number . \end{cases}

(\textsf{\textrm{H}})

The function

h

may be found in the literature and is Baire 1 Myerson [38, p.238]. In conclusion, the Baire category theorem seems intimately connected to Baire 1 functions (in both directions), assuming we have access to (2.1), which is why we assume the oscillation

{osc}_{f}

to be given.

Thirdly, we list basic facts about Baire 1 and pointwise discontinuous functions.

Theorem 2.2

Upper semi-continuous functions are Baire 1; the latter are pointwise discontinuous.

Any $f : [0, 1] \to R$ is upper semi-continuous iff for any $a \in R$ , $f^{- 1} ([a, + \infty))$ is closed.

For any $R \to R$ -function, the set $D_{f}$ is $F_{σ}$ , that is, the union over $N$ of closed sets.

For a sequence of closed $(X_{n})_{n \in N}$ , the function $h$ in () is Baire 1.

Characteristic functions of subsets of the Cantor set (and variations) are pointwise discontinuous, but need not be Borel or Riemann integrable.

The class of bounded Baire 1 functions $B_{1}$ is the union of all ‘small’ Baire 1 classes $B_{1}^{ξ}$ for $ξ < ω_{1}$ (see Kechris and Louveau [39] for the definition of the latter).

Proof.

Proofs may be found in, for example, Section 7 of Oxtoby [40, pp 31–33], Baire [5], Myerson [38], and Kechris and Louveau [39].

We will tacitly use Theorem 2.2. We will need one additional property of $h : [0, 1] \to R$ as in (), which we could not find in the literature.

Theorem 2.3

Let $(X_{n})_{n \in N}$ be a sequence of closed and nowhere dense sets and let $h : [0, 1] \to R$ be as in (). Then ${osc}_{h} : [0, 1] \to R$ is computable in $\exists^{2}$ .

Proof.

Consider $h : [0, 1] \to R$ as in the theorem. We will show that $h$ equals ${osc}_{h}$ everywhere on $[0, 1]$ , that is, $h$ is its own oscillation function. To this end, we proceed by the following case distinction.

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

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

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

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

In conclusion, we have

h (x) = {osc}_{h} (x)

for all

x \in [0, 1]

, as required.

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

2.2. Main results

In this section, we establish the computational equivalences sketched in Section 1.1. The function $h$ from () plays a central role.

In particular, we have the following theorem where we note that Volterra’s [6] original results (see Section 1.2) are formulated for pointwise discontinuous functions. Regarding Definition 1.1, we sometimes abuse notation by identifying a specification and the class of functionals satisfying this specification.

Theorem 2.4
Assuming $\exists^{2}$ , the following are computationally equivalent. (a)
(Class of Baire realisers: Definition 1.6) On input a sequence $(O_{n})_{n \in N}$ of dense and open subsets of $[0, 1]$ , outputs $x \in \cap_{n \in N} O_{n}$ .
(b)
On input $f : [0, 1] \to R$ in $B_{1}$ and its oscillation ${osc}_{f} : [0, 1] \to R$ , output $y \in [0, 1]$ where $f$ is continuous (or lower semi-continuous, or Darboux).
(c)
(Volterra) On input $f : [0, 1] \to R$ in $B_{1}$ and its oscillation ${osc}_{f} : [0, 1] \to R$ , output either $q \in Q \cap [0, 1]$ where $f$ is discontinuous, or $x \in [0, 1] ∖ Q$ where $f$ is continuous.
(d)
(Volterra) On input $f, g : [0, 1] \to R$ in $B_{1}$ and their oscillation functions ${osc}_{f}, {osc}_{g} : [0, 1] \to R$ , output a real $x \in [0, 1]$ such that $f$ and $g$ are both continuous or both discontinuous at $x$ .
(e)
(Baire, [5, p.66]) On input a sequence $(f_{n})_{n \in N}$ in $B_{1}$ and oscillation functions $({osc}_{f_{n}})_{n \in N}$ , output $x \in [0, 1]$ such that all $f_{n}$ are continuous at $x$ .
(f)
On input $f : [0, 1] \to R$ in $B_{1}$ and its oscillation function ${osc}_{f}$ , output $a, b \in [0, 1]$ such that ${x \in [0, 1] : f (a) \leq f (x) \leq f (b)}$ is infinite.
(g)
The previous items with ‘Baire 1’ generalised to ‘pointwise discontinuous’.
(h)
The previous items with ‘Baire 1’ restricted to ‘upper semi-continuous’.
(i)
The previous items with ‘Baire 1’ restricted to ‘small Baire class $B_{1}^{ξ}$ ’ for any countable ordinal $1 \leq ξ < ω_{1}$ .

Proof.
First of all, many results will be proved using $h : [0, 1] \to R$ as in (). By Theorem 2.3, the associated oscillation function ${osc}_{h} : [0, 1] \to R$ is available.

For the implication (a) $\to$ (b), let $f : [0, 1] \to R$ be Baire 1 and let ${osc}_{f} : [0, 1] \to R$ be its oscillation. The following set, readily defined using $\exists^{2}$ , is closed and nowhere dense, as can be found in, for example, Section 7 in Oxtoby [40, p.31]:
$D_{k} := {x \in [0, 1] : {osc}_{f} (x) \geq \frac{1}{2^{k}}},$
(2.2)
The union $D_{f} = \cup_{k \in N} D_{k}$ collects all points where $f$ is discontinuous. Hence, $O_{k} := [0, 1] ∖ D_{k}$ is open and dense for all $k \in N$ , while $y \in \cap_{k \in N} O_{k}$ implies ${osc}_{f} (y) = 0$ , that is, $y$ is a point of continuity of $f$ by definition (of the oscillation function). Hence, we have established that a Baire realiser computes some $x \in C_{f}$ for a Baire 1 function $f$ and its oscillation function, that is, item (b) follows. The generalisation involving pointwise discontinuous functions (item (g)) is now immediate, as the very same proof goes through.

For the implication (b) $\to$ (a), let $(O_{n})_{n \in N}$ be a sequence of open and dense sets. Then $(X_{n})_{n \in N}$ for $X_{n} := [0, 1] ∖ O_{n}$ is a sequence of closed and nowhere dense sets. Now consider the function $h : [0, 1] \to R$ from (), which is Baire 1 as noted above.

Item (b) yields $y \in [0, 1]$ where $h$ is continuous and we must have $y \in \cap_{n \in N} O_{n}$ . Indeed, in case $y \in X_{m_{0}}$ , there is $N \in N$ such that $h (z) > 1 / 2^{m_{0} + 1}$ for $z \in B (y, 1 / 2^{N})$ , by the continuity of $h$ at $y$ . However, since $O := \cap_{n \leq m_{0} + 2} O_{n}$ is dense in $[0, 1]$ , there is some $z_{0} \in B (y, 1 / 2^{N}) \cap O$ , which yields $h (z_{0}) \leq 1 / 2^{m_{0} + 2}$ by the definition of $h$ , a contradiction. Hence, we have $y \in \cap_{n \in N} O_{n}$ as required by the specification of Baire realisers as in item (a). The same argument works for lower semi-continuity and the (local) Darboux property.

For the implication (b) $\to$ (c), let $f$ and ${osc}_{f}$ be as in the latter item. Note that $μ^{2}$ can find $q \in Q \cap [0, 1]$ such that ${osc}_{f} (q) >_{R} 0$ , if such exists. If there is no such rational, the functional from item (b) must output an irrational $y \in [0, 1]$ such that $f$ is continuous at $y$ . Hence, item (c) follows while the generalisation involving pointwise discontinuous functions (item (g)) is again immediate.

For the implication (c) $\to$ (b), let $f$ and ${osc}_{f}$ be as in the latter item. Note that $μ^{2}$ can find $q \in Q \cap [0, 1]$ such that ${osc}_{f} (q) =_{R} 0$ , if such exists; such rational is a point of continuity of $f$ , which is required for item (b). If there is no such rational, the functional from item (c) must output an irrational $y \in [0, 1]$ such that $f$ is continuous at $y$ . Hence, item (b) follows from item (c) while the generalisation involving pointwise discontinuous functions (item (g)) is again immediate.

Next, assume item (d) and recall Thomae’s function $T$ as in (), which is regulated and hence Baire 1; the oscillation function is ${osc}_{T}$ readily defined using $\exists^{2}$ . Since $T$ is continuous on $R ∖ Q$ , item (d) yields item (c). To obtain item (d) from a Baire realiser, let $f, g : [0, 1]$ be Baire 1 with oscillation functions ${osc}_{f}$ and ${osc}_{g}$ . Consider the set $D_{k}$ as in (2.2) and let $E_{k}$ be the same set for $g$ , that is, defined as:
$E_{k} := {x \in [0, 1] : {osc}_{g} (x) \geq \frac{1}{2^{k}}} .$
(2.3)
Then $O_{n} := [0, 1] ∖ (D_{n} \cup E_{n})$ is open and dense as in the previous paragraphs. Now use a Baire realiser to obtain $y \in \cap_{n \in N} O_{n}$ . By definition, $f$ and $g$ are continuous at $y$ , that is, item (b) follows. The generalisation for pointwise discontinuous functions (item (g)) is immediate.

For item (e), consider the following (nowhere dense and closed as for (2.2)) set:
$D_{k, n} := {x \in [0, 1] : {osc}_{f_{n}} (x) \geq \frac{1}{2^{k}}} for k, n \in N,$
(2.4)
where each $f_{n} : [0, 1] \to R$ is Baire 1 with oscillation ${osc}_{f_{n}} : [0, 1] \to R$ . Since each $f_{n}$ is continuous outside of $D_{f_{n}} := \cup_{k \in N} D_{k, n}$ , any $y \notin \cup_{k, n \in N} D_{k, n}$ is such that each $f_{n}$ is continuous at $y$ . Hence, item (e) follows from item (a).

For item (f), consider $h$ as in () and note that if $h (a) > 0$ , then ${x \in [0, 1] : h (a) \leq h (x) \leq h (b)}$ is finite. Hence, item (f) must provide $a \in [0, 1]$ such that $h (a) = 0$ , which by definition satisfies $a \notin \cup_{n \in N} X_{n}$ , that is, item (a) follows.

Finally, regarding item (h), the function $h : [0, 1] \to R$ from () is in fact upper semi-continuous, assuming $(X_{n})_{n \in N}$ is a sequence of closed and nowhere dense sets. One can show this directly using the definition of semi-continuity, or observe that $h^{- 1} ([a, + \infty))$ is either $\emptyset$ , $[0, 1]$ , or a finite union of $X_{i}$ , all of which are closed. Regarding item (i), the class $B_{1}^{ξ}$ includes the (upper and lower) semi-continuous functions if $ξ \geq 1$ (see Section 2 in Kechris and Louveau [39]). Hence, the equivalences for the restrictions of item (b) as in items (h) or (i) have been established; the very same argument applies to the other items, that is, items (h) and (i) are finished.

The reader easily verifies that most equivalences in Theorem 2.4 go through for S1–S9 replaced by a small fragment of Gödel’s $T$ .

Next, we isolate the following result as we need to point out the meaning of ‘countable set’ as an input of a functional. As in Normann and Sanders [4,30] and Sanders [31], we assume that a countable set $D \subset R$ is given together with $Y : [0, 1] \to N$ which is injective on $D$ and that these two objects $D$ and $Y$ are an input for the functional at hand, for example, as in item (k) from Corollary 2.5.
Corollary 2.5
Given $\exists^{2}$ , the following operation $(k)$
on input a countable dense $D \subset [0, 1]$ , a function $f : [0, 1] \to R$ in Baire 1, and its oscillation ${osc}_{f}$ , outputs either $d \in D$ such that $f$ is discontinuous at $d$ , or $x \notin D$ such that $f$ is continuous at $x$ ,
is computationally equivalent to the class of Baire realisers. The equivalence remains correct if we require a bijection from $D$ to $N$ (instead of an injection).
Proof.
For item (k), the latter clearly implies item (c) for $D = Q$ , even if we require a bijection from $D$ to $N$ . To establish item (k) assuming item (a), let $D \subset [0, 1]$ and $Y : [0, 1] \to N$ be such that the former is dense and the latter is injective on the former. Now fix $f : [0, 1] \to R$ in Baire 1 and ${osc}_{f}$ . Define $E_{k} := D_{k} \cup {x \in D : Y (x) \leq k}$ where the former is as in (2.2) and the latter is finite. Hence, $O_{n} := [0, 1] ∖ E_{n}$ is open and dense. Any Baire realiser therefore provides $y \in \cap_{n \in N} O_{n}$ , which is such that $f$ is continuous at $y \notin D$ , as required.

Note that item (k) in the corollary is based on the generalisation of Volterra’s theorem as in Theorem 1.4. We believe many similar results can be established, for example, by choosing different (but equivalent over strong systems) definitions of ‘countable set’, as discussed in Section 3.2.

We finish this section with some conceptual remarks, including potential generalisations of Theorem 2.4.
Remark 2.6 (Generalisations)

First of all, items (h) and (i) of Theorem 2.4 imply that certain ‘small’ sub-classes of $B_{1}$ already yield the required equivalences. One may wonder whether the same holds for the sub-classes $B_{1}^{*}$ and $B_{1}^{* *}$ of $B_{1}$ (see, e.g. Sworowski and Sieg [42] for the latter). As far as we can see, the function $h$ (and variations) from () does not belong to $B_{1}^{*}$ or $B_{1}^{* *}$ .

Secondly, pointwise discontinuous functions are exactly those for which $D_{f}$ is meagre [5,38,39,40], that is, the union of nowhere dense sets. Since the complement of closed and nowhere dense sets is open and dense, it seems we cannot generalise Theorem 2.4 beyond pointwise discontinuous functions (without extra effort).

Remark 2.7 (Kleene’s quantifier $\exists^{2}$ )

The computational equivalences in this section are established assuming Kleene’s $\exists^{2}$ . We discuss one important motivation and a possible alternative approach.

First of all, so-called Grilliot’s trick is a computability-theoretic device for computing $\exists^{2}$ from a discontinuous function on Baire space [43]. Hence, one could restrict the above operations to (certain) discontinuous inputs. The first step is then always obtaining $\exists^{2}$ via Grilliot’s trick. Moreover, for basic sets such as the unit interval to be given as characteristic functions, one simply needs $\exists^{2}$ , that is, the latter practically ‘falls out’ of our definitions. The curious reader then wonders if we can change the latter, which is the topic of the next paragraph.

Secondly, to avoid the use of $\exists^{2}$ in a more structural way, one could adopt the following ‘more constructive’ definition of set.

A subset $A \subset R$ is given by a representation function $F_{A} : R \to R$ , that is, we write $x \in A$ for $F_{A} (x) >_{R} 0$ for all $x \in R$ .

The coding of open sets via sequences of open balls amounts to taking

F_{A}

to be continuous (and with a continuous modulus or RM code) as per Section II.7.1 of Simpson [44]. In this way, the previous item extends the usual definition from, for example, Reverse Mathematics. The associated development is of course beyond the scope of the current paper, but we look forward to studying this construct.

3. Related results

We discuss some results related (directly or indirectly) to Baire realisers.

3.1. Baire 1 functions and open sets

In this section, we motivate the study of the definition of open set from Normann and Sanders [14] and Definition 1.8 in Section 1.3.3, which amounts to (R.1). In particular, Theorem 3.4 below expresses that the closed sets $D_{k}$ as in (2.2) are just closed sets without any additional information. Hence, the study of Baire 1 already boasts (general) open sets that only satisfy the (R.1) definition of open sets, that is, for which other representations (see (R.2)–(R.4)) are not computable, even assuming $S_{k}^{2}$ ; we conjecture that we can add non-trivial non-normal functionals.

First of all, the following representations of open sets were reported in Section 7 of Normann and Sanders [14].

Definition 3.1 (Representations of open sets)

(R.1)
The open set $O$ is represented by its characteristic function. We just have the extra information that $O$ is open (Definition 1.8).
(R.2)
The set $O$ is represented by a function $Y : [0, 1] \to [0, 1]$ such that (i)
we have $O = {x ∣ Y (x) >_{R} 0}$ ,
(ii)
if $Y (x) > 0$ , then $(x - Y (x), x + Y (x)) \cap [0, 1] \subseteq O$ .

(R.3)
The set $O$ is represented by the continuous function $Y$ where (i)
$Y (x)$ is the distance from $x$ to $[0, 1] ∖ O$ if the latter is non-empty,
(ii)
$Y$ is constant 1 if $O = [0, 1]$ .

(R.4)
The set $O$ is given as the union of a sequence of open rational intervals $(a_{i}, b_{i})$ , the sequence being a representation of $O$ .

We note that the (R.4) representation is used in frameworks based on second-order arithmetic (see, e.g. Section II.5.6 of Simpson [44]).

Secondly, assuming $\exists^{2}$ , it is clear that the information given by a representation increases when going down the list. As expected, (R.3) and (R.4) are ‘the same’ by the following theorem.
Theorem 3.2
The functional $\exists^{2}$ computes an (R.3) representation given an (R.4) representation, and vice versa.
Proof.
Immediate from Theorem 7.1 of Normann and Sanders [14].

The (R.2) and (R.3) representations are not computationally equivalent. Indeed, the functional $Δ^{3}$ from Section 7.1 of Normann and Sanders [14] converts open sets as in (R.2) to open sets as in (R.3). This functional is not computable in any $S_{k}^{2}$ and computes nothing new when combined with $\exists^{2}$ , as discussed in detail in Section 7 of Normann and Sanders [14].

Thirdly, we have the following main theorem, where $Ω_{fin}$ is studied in Normann and Sanders [4,29] and Sanders [31] based on the following definition.
Definition 3.3
A finiteness realiser $Ω_{fin}$ is defined when the input $X \subset R$ is finite and $Ω_{fin} (X)$ then outputs a finite sequence of reals that includes all elements of $X$ .

We note that $Ω_{fin}$ is explosive in that $Ω_{fin} + S_{1}^{2}$ computes $S_{2}^{2}$ [4,29] while many computational equivalences are established for the class of finiteness realisers in Normann and Sanders [4] , for example, involving the Jordan decomposition theorem.
Theorem 3.4
Together with $\exists^{2}$ , the following computes a Baire realiser (Definition 1.6):
A functional that on input $f : [0, 1] \to R$ in Baire 1, its oscillation function ${osc}_{f}$ , and $n \in N$ , outputs an (R.2) representation of $[0, 1] ∖ D_{n}$ as in (2.2).

Combining the centred operation with $Δ$ , which converts (R.2) representations into (R.3) ones, we can compute $Ω_{fin}$ .
Proof.
For the first part, the centred operation provides an (R.2) representation for the open and dense set $O_{n} := [0, 1] ∖ D_{n}$ . It is a straightforward verification that, given an (R.2) representation for a sequence of open and sense sets, the usual constructive proof of the Baire category theorem goes through (see Bishop [9, p.84] for the latter). A detailed proof, assuming $\exists^{2}$ , can be found in Theorem 7.10 of Normann and Sanders [14]. In other words, given an (R.2) representation for each $O_{n}$ , we can compute $y \in \cap_{n \in N} O_{n}$ assuming $\exists^{2}$ , and we are done.

For the second part, let $X \subset R$ be finite. Define $F_{X} : R \to R$ as $1$ in case $x \in X$ , and $0$ otherwise. Clearly, $F_{X}$ is Baire 1 and the function ${osc}_{F_{X}}$ is just $F_{X}$ itself. The centred operation from the theorem, together with $Δ$ and Theorem 3.2, provides an (R.4) representation of each $[0, 1] ∖ D_{n}$ . However, by Lemma 4.11 of Normann and Sanders [4], there is a functional $E$ , computable in $\exists^{2}$ , such that for any sequences $(a_{n})_{n \in N}$ , $(b_{n})_{n \in N}$ , if the closed set $C = [0, 1] ∖ \cup_{n \in N} (a_{n}, b_{n})$ is countable, then $E (λ n . (a_{n}, b_{n}))$ enumerates the points in $C$ . Hence, the functional $E$ can enumerate the finite set $D_{k}$ for any $k \in N$ , and therefore yields an enumeration of $X$ .

Note that for the second part, we could restrict the centred operation to some fixed $n \in N$ .
3.2. Functionals related to Baire realisers

We show that Baire realisers compute certain witnessing functionals for the uncountability of $R$ , called strong Cantor realisers, as studied in Sanders [31] and Normann and Sanders [4,30]. This is interesting as (we believe that) witnessing functionals for the Heine–Borel theorem (see Normann and Sanders [24,25]) cannot compute any strong Cantor realiser.

First of all, we introduce the following notion of a countable set, equivalent to the usual definition over strong enough logical systems.

Definition 3.5 (Height countable)

A set $A \subset R$ is height countable if there is a height $H : R \to N$ for $A$ , that is, for all $n \in N$ , $A_{n} := {x \in A : H (x) < n}$ is finite.

The notion of ‘height’ is mentioned in, for example, Moll [45], Vatssa [46], and Royden [47] in connection to countability. The following remark is crucial for the below.

Remark 3.6 (Inputs and heights)

A functional defined on height countable sets always takes two inputs: the set $A \subset R$ and the height $H : R \to N$ . We note that given a sequence of finite sets $(X_{n})_{n \in N}$ in $R$ , a height can be defined as $H (x) := (μ n) (x \in X_{n})$ using Feferman’s $μ^{2}$ . A set is therefore height countable iff it is the union over $N$ of finite sets.

The following witnessing functional for the uncountability of $R$ is from Sanders [31].

Definition 3.7 (Strong Cantor realiser)

A strong Cantor realiser is any functional that on input a height countable $A \subset [0, 1]$ , outputs $y \in [0, 1] ∖ A$ .

Following Remark 3.6, a strong Cantor realiser takes as input a countable set and its height as in Definition 3.5. Modulo $\exists^{2}$ , this amounts to an input consisting of a sequence $(X_{n})_{n \in N}$ of finite sets in $[0, 1]$ and an output $y \in [0, 1] ∖ \cup_{n \in N} X_{n}$ . It was shown in Sanders [31] that many operations on regulated functions are computationally equivalent to strong Cantor realisers, thereby justifying Definition 3.5. By contrast, we could not find comparable computational equivalences for ‘normal’ and ‘weak’ Cantor realisers (see Normann and Sanders [30] and Sanders [31]), which make use of the more standard definition of ‘countable set’ based on injections and bijections to $N$ .

Next, we have the following theorem connecting some of the aforementioned functionals, including $Ω_{fin}$ from Definition 3.3.

Theorem 3.8

Assuming $\exists^{2}$ , we have that

any Baire realiser computes a strong Cantor realiser,

the functional $Ω_{fin}$ computes a strong Cantor realiser.

Proof.

Fix a height countable set $A \subset [0, 1]$ and its height function $H : R \to N$ . By definition $A_{n} := {x \in [0, 1] : H (x) < n}$ is finite, hence $O_{n} := [0, 1] ∖ A_{n}$ is open and dense. A Baire realiser provides $y \in \cap_{n \in N} O_{n}$ , which immediately yields $y \notin A$ . Similarly, $Ω_{fin} (A_{n})$ yields an enumeration of $A_{n}$ and $μ^{2}$ readily yields a sequence $(a_{n})_{n \in N}$ containing all elements of $A$ . There are (efficient) algorithms (see Gray [48]) to find $y \in [0, 1]$ such that $y \neq a_{n}$ for all $n \in N$ , and we are done.

On a related note, the reader easily verifies that Corollary 2.5 goes through for ‘countable’ replaced by ‘height ountable’, keeping in mind Remark 3.6. We believe that many such variations are possible.

Finally, the study of the Baire category theorem in computability theory is closely related to its study in Kohlenbach’s higher-order Reverse Mathematics [32]. Before the completion of this paper, only very few results were known about the Baire category theorem in either discipline (see Normann and Sanders [14]). After the completion of this paper, the author undertook the study of the Baire category theorem in higher-order Reverse Mathematics [49,50], leading to numerous equivalences.

There is however a big difference between the Reverse Mathematics results and the results in this paper: most results about Baire 1 functions, such as the supremum principle, can be proved in Kohlenbach’s base theory ${RCA}_{0}^{ω}$ extended with the (second-order) Big Five [51]. By contrast, basic results about semi-continuous functions (including supremum principle or the fact that they are Baire 1) cannot be proved from the Big Five (and much stronger systems), as studied in detail in Sanders [49,50] and Normann and Sanders [51]. We stress that semi-continuous functions are of course Baire 1, but this basic fact is rather hard to prove.

Footnotes

Funding

The author disclosed receipt of the following financial support for the research, authorship, and/or publication of this article: Our research was supported by the Klaus Tschira Boost Fund via the grant Projekt KT43.

Declaration of conflicting interests

The author declared no potential conflicts of interest with respect to the research, authorship and/or publication of this article.

Appendix A. Some details of Kleene’s computability theory

Kleene’s computability theory borrows heavily from type theory and higher-order arithmetic. We briefly sketch some of the associated notions.

First of all, Kleene’s S1–S9 schemes define ‘ $Ψ$ is computable in terms of $Φ$ ’ for objects $Φ, Ψ$ of any finite type. Now, the collection of all finite types $T$ is defined by the following two clauses:

\begin{aligned} (i) 0 \in T and~(ii)~if σ, τ \in T then (σ \to τ) \in T, \end{aligned}

where

0

is the type of natural numbers and

σ \to τ

is the type of mappings from objects of type

σ

to objects of type

τ

. In this way,

1 \equiv 0 \to 0

is the type of function from numbers to numbers, and

n + 1 \equiv n \to 0

. We view sets

X

of type

σ

objects as given by characteristic functions

F_{X}^{σ \to 0}

Secondly, for variables $x^{ρ}, y^{ρ}, z^{ρ}, \dots$ of any finite type $ρ \in T$ , types may be omitted when they can be inferred from context. The constants include the type $0$ objects $0, 1$ and $<_{0}, +_{0}, \times_{0}, =_{0},$ which are intended to have their usual meaning as operations on $N$ . Equality at higher types is defined in terms of ‘ $=_{0}$ ’ as follows: for any objects $x^{τ}, y^{τ}$ , we have (A.1)

[x =_{τ} y] \equiv (\forall z_{1}^{τ_{1}} \dots z_{k}^{τ_{k}}) [x z_{1} \dots z_{k} =_{0} y z_{1} \dots z_{k}],

if the type

τ

is composed as

τ \equiv (τ_{1} \to \dots \to τ_{k} \to 0)

Thirdly, we introduce the usual notations for common mathematical notions, such as real numbers, as also can be found in Kohlenbach [32]. Definition 4.1 (Real numbers and related notions)

(a)

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

(b)

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

(c)

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

(d)

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

(e)

Functions $F : R \to R$ are represented by $Φ^{1 \to 1}$ mapping equal reals to equal reals, that is, extensionality as in $(\forall x, y \in R) (x =_{R} y \to Φ (x) =_{R} Φ (y))$ .

(f)

The relation ‘ $x \leq_{τ} 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^{N}$ ’. Elements of Baire space are given by $f^{1}, g^{1}$ , but also denoted ‘ $f, g \in N^{N}$ ’.

(g)

Sets of type $ρ$ objects $X^{ρ \to 0}, Y^{ρ \to 0}, \dots$ are given by their characteristic functions $F_{X}^{ρ \to 0} \leq_{ρ \to 0} 1$ , that is, we write ‘ $x \in X$ ’ for $F_{X} (x) =_{0} 1$ .

For completeness, we list the following notational convention for finite sequences. Notation 4.2 (Finite sequences)

The type for ‘finite sequences of objects of type $ρ$ ’ is denoted $ρ^{*}$ , which we shall only use for $ρ = 0, 1$ . We shall not always distinguish between $0$ 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^{ρ}$ ’ and ‘ $⟨ s^{ρ} ⟩$ ’, where the former is ‘the object $s$ of type $ρ$ ’, and the latter is ‘the sequence of type $ρ^{*}$ with only element $s^{ρ}$ ’. The empty sequence for the type $ρ^{*}$ is denoted by ‘ $⟨ ⟩_{ρ}$ ’, usually with the typing omitted.

Furthermore, we denote by ‘ $| s | = n$ ’ the length of the finite sequence $s^{ρ^{*}} = ⟨ s_{0}^{ρ}, s_{1}^{ρ}, \dots, s_{n - 1}^{ρ} ⟩$ , where $| ⟨ ⟩ | = 0$ , that is, the empty sequence has length zero. For sequences $s^{ρ^{*}}, t^{ρ^{*}}$ , we denote by ‘ $s * t$ ’ the concatenation of $s$ and $t$ , that is, $(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^{ρ^{*}}$ , we define $\bar{s} N := ⟨ s (0), s (1), \dots, s (N - 1) ⟩$ for $N^{0} < | s |$ . For a sequence $α^{0 \to ρ}$ , we also write $\bar{α} N = ⟨ α (0), α (1), \dots, α (N - 1) ⟩$ for any $N^{0}$ . By way of shorthand, $(\forall q^{ρ} \in Q^{ρ^{*}}) A (q)$ abbreviates $(\forall i^{0} < | Q |) A (Q (i))$ , which is (equivalent to) quantifier-free if $A$ is.

References

Turing

. On computable numbers, with an application to the Entscheidungs problem. Proc Lond Math Soc 1936; 42: 230–265.

Kleene

. Recursive functionals and quantifiers of finite types. I. Trans Am Math Soc 1959; 91: 1–52.

Longley

Normann

. Higher-order computability. In: Theory and applications of computability. Springer, 2015.

Normann

Sanders

. On the computational properties of basic mathematical notions. J Log Comput 2022; 44.

Baire

. Sur les fonctions de variables réelles. Ann Mat 1899; 3: 1–123.

Volterra

. Alcune osservasioni sulle funzioni punteggiate discontinue. G Mat XIX 1881; 76–86.

Brattka

Hendtlass

Kreuzer

. On the uniform computational content of the Baire category theorem. Notre Dame J Form Log 2018; 59: 605–636.

Brattka

. Computable versions of Baire’s category theorem. In: Mathematical foundations of computer science, 2001 (Mariánské Láznue). Lecture notes in computer science, vol. 2136. Berlin: Springer, 2001, pp.224–235.

Bishop

. Foundations of constructive analysis. McGraw-Hill, 1967.

10.

Nemoto

. A constructive proof of the dense existence of nowhere-differentiable functions in

C [0, 1]

. Computability 2020; 9: 315–326.

11.

Sholapurkar

. On a theorem of Vito Volterra. Resonance 2007; 12: 76–79.

12.

Kim

. A characterization of the set of points of continuity of a real function. Am Math Mon 1999; 106: 258–259.

13.

Dunham

. A historical gem from Vito Volterra. Math Mag 1990; 63: 234–237.

14.

Normann

Sanders

. Open sets in reverse mathematics and computability theory. J Log Comput 2020; 30: 40.

15.

Hankel

. Untersuchungen über die unendlich oft oscillirenden und unstetigen Functionen. Ludwig Friedrich Fues, Memoir presented at the University of Tübingen on 6 March 1870.

16.

Riemann

Baker

Christenson

Orde

(trans.). Bernhard Riemann: collected works. Kendrick Press, 2004.

17.

Riemann

. Ueber die Darstellbarkeit einer Function durch eine trigonometrische Reihe. In: Abhandlungen der Königlichen Gesellschaft der Wissenschaften zu Göttingen, vol. 13. Habilitation thesis defended in 1854, published in 1867, p.47.

18.

Thomae

CJT

. Einleitung in die Theorie der bestimmten Integrale. Halle a.S.: Louis Nebert, 1875.

19.

Silva

. No functions continuous only at points in a countable dense set. Preprint, 2018, arxiv: https://arxiv.org/abs/1809.06453v3.

20.

Gauld

. Did the Young Volterra know about Cantor? Math Mag 1993; 66: 246–247.

21.

Osgood

. Non-uniform convergence and the integration of series term by term. Am J Math 1897; 19: 155–190.

22.

Normann

Sanders

. On the uncountability of

R

. J Symb Log 2022; 87: 1474–1521 SEP.

23.

Soare

. Recursively enumerable sets and degrees. In: Perspectives in mathematical logic. Springer, 1987.

24.

Normann

Sanders

. Nonstandard analysis, computability theory, and their connections. J Symb Log 2019; 84: 1422–1465.

25.

Normann

Sanders

. The strength of compactness in computability theory and nonstandard analysis. Ann Pure Appl Log 2019; 170. Article 102710.

26.

Normann

Sanders

. Vitali’s covering theorem in computability theory and reverse mathematics. To appear in Ann Pure Appl Log 2025; 176: 103505.

27.

Normann

Sanders

. Pincherle’s theorem in reverse mathematics and computability theory. Ann Pure Appl Logic 2020; 171: Article 102788.

28.

Normann

Sanders

. The axiom of choice in computability theory and reverse mathematics. J Log Comput 2021; 31: 297–325.

29.

Normann

Sanders

. On robust theorems due to Bolzano, Jordan, Weierstrass, and Cantor in reverse mathematics. J Symb Log 2024; 89: 1077–1127 .

30.

Normann

Sanders

. Betwixt Turing and Kleene. In: LNCS 13137, proceedings of LFCS22, Deerfield Beach, FL, USA, 2022, p.18. Springer.

31.

Sanders

. On the computational properties of the uncountability of the reals. To appear in Lecture notes in computer science. Proceedings of WoLLIC22. vol. 13468. Springer, 2022, pp.362–377. https://arxiv.org/abs/2206.12721.

32.

Kohlenbach

. Higher order reverse mathematics. In: Simpson SG (ed.) Reverse mathematics 2001, Lecture Notes in Logic, vol. 21. A.K. Peters, 2005, pp.281–295.

33.

Avigad

Feferman

. Gödel’s functional “Dialectica” interpretation. In: Handbook of proof theory, studies in logic and the foundations of mathematics, vol. 137. 1998, pp.337–405.

34.

Hilbert

Bernays

. Grundlagen der Mathematik. II, Zweite Auflage. In: Die Grundlehren der mathematischen Wissenschaften. Band 50. Springer, 1970.

35.

Buchholz

Feferman

Pohlers

, et al. Iterated inductive definitions and subsystems of analysis. In: LNM 897. Springer, 1981.

36.

Appell

Banaś

Merentes

. Bounded variation and around. In: De Gruyter series in nonlinear analysis and applications, vol. 17. Berlin: De Gruyter, 2014.

37.

Smith

HJS

. On the integration of discontinuous functions. Proc Lond Math Soc 1874/75; 6: 140–153.

38.

Myerson

. First-class functions. Am Math Mon 1991; 98: 237–240.

39.

Kechris

Louveau

. A classification of Baire class

1

functions. Trans Am Math Soc 1990; 318: 209–236.

40.

Oxtoby

. Measure and category. A survey of the analogies between topological and measure spaces. In: Graduate texts in mathematics. 2nd ed., vol. 2. Springer, 1980.

41.

Kostyrko

. Some properties of oscillation. Math Slov 1980; 30: 157–162.

42.

Sworowski

Sieg

. Uniform limits of

B_{1}^{* *}

-functions. Topol Appl 2021; 292: Article No. 107630.

43.

Grilliot

. On effectively discontinuous type-

2

objects. J Symb Log 1971; 36: 245–248.

44.

Simpson

. Subsystems of second order arithmetic. In: Perspectives in logic, 2nd ed. CUP, 2009.

45.

Moll

. Numbers and functions. In: Student mathematical library, vol. 65. American Mathematical Society, 2012.

46.

Vatssa

. Discrete mathematics. 4th ed. New Age International, 1993.

47.

Royden

. Real analysis. In: Lecture notes in mathematics. Pearson Education, 1989.

48.

Gray

. Georg Cantor and transcendental numbers. Am Math Mon 1994; 101: 819–832.

49.

Sanders

. Big in reverse mathematics: measure and category. J Symb Log 2023; 1–46.

50.

Sanders

. Approximation theorems throughout reverse mathematics. To appear in J Symbol Log, 2023. https://arxiv.org/abs/2311.11036.

51.

Normann

Sanders

. The biggest five of reverse mathematics. To appear in J Math Log, 2023. https://arxiv.org/abs/2212.00489.

On the computational properties of the Baire category theorem

Abstract

Keywords

1. Introduction

1.1. Motivation and overview

1.2. Volterra’s early work and related results

Corollary 1.3 Volterra [6]

1.3.1. Kleene’s computability theory

Definition 1.8 Set

Definition 1.9 Weak continuity

Definition 1.10 (Baire 1 function)

2. Baire category theorem and computational equivalences

2.1. Preliminaries

Remark 2.7 (Kleene’s quantifier ∃ 2 )

3. Related results

3.1. Baire 1 functions and open sets

Definition 3.1 (Representations of open sets)

Definition 3.5 (Height countable)

Remark 3.6 (Inputs and heights)

Definition 3.7 (Strong Cantor realiser)

Footnotes

Funding

Declaration of conflicting interests

Appendix A. Some details of Kleene’s computability theory

References

Remark 2.7 (Kleene’s quantifier $\exists^{2}$ )