Nets and reverse mathematics

Abstract

Nets are generalisations of sequences involving possibly uncountable index sets; this notion was introduced about a century ago by Moore and Smith. They also established the generalisation to nets of various basic theorems of analysis due to Bolzano–Weierstrass, Dini, Arzelà, and others. More recently, nets are central to the development of domain theory, providing intuitive definitions of the associated Scott and Lawson topologies, among others. This paper deals with the Reverse Mathematics study of basic theorems about nets. We restrict ourselves to nets indexed by subsets of Baire space, and therefore third-order arithmetic, as such nets suffice to obtain our main results. Over Kohlenbach’s base theory of higher-order Reverse Mathematics, the Bolzano–Weierstrass theorem for nets implies the Heine–Borel theorem for uncountable covers. We establish similar results for other basic theorems about nets and even some equivalences, e.g. for Dini’s theorem for nets. Finally, we show that replacing nets by sequences is hard, but that replacing sequences by nets can obviate the need for the Axiom of Choice, a foundational concern in domain theory. In an appendix, we study the power of more general index sets, establishing that the ‘size’ of a net is directly proportional to the power of the associated convergence theorem.

Keywords

Reverse mathematics higher-order computability theory nets Moore–Smith sequences

1. Aim and motivation

1.1. Introduction

The move to more abstract mathematics can be quite concrete and specific: E. H. Moore presented a framework called General Analysis at the 1908 ICM in Rome [69] that was to be a ‘unifying abstract theory’ for various parts of analysis. For instance, Moore’s framework captures various limit notions in one abstract concept [70]. This theory also included a generalisation of the concept of sequence to possibly uncountable index sets, nowadays called nets or Moore–Smith sequences. These were first described in [71] and then formally introduced by Moore and Smith in [73]. They also established the generalisation to nets of various basic theorems due to Bolzano–Weierstrass, Dini, and Arzelà [73, §8–9]. More recently, nets are central to the development of domain theory (see [44,45,47]), including a definition of the Scott and Lawson topologies in terms of nets. Moreover, sequences cannot be used in this context, as expressed in a number of places:

Turning to foundations, we feel that the necessity to choose chains where directed subsets are naturally available (such as in function spaces) and thus to rely on the Axiom of Choice without need, is a serious stain on this approach. [1, §2.2.4].

[…] clinging to ascending sequences would produce a mathematical theory that becomes rather bizarre, whence our move to directed1

¹
Nets can have uncountable index sets, and the latter are called directed sets.

families. [47, p. 59]

Thus, nets enjoy a rich history, as well as a mainstream (and essential) status in mathematics and computer science. Motivated by the above, this paper deals with the study of nets in Reverse Mathematics (RM hereafter); the latter program is briefly introduced in Section 2. Since uncountable index sets are first-class citizens in the theory of nets, we work in Kohlenbach’s higher-order RM (see Section 2.1). The exact formalisation of nets in higher-order RM is detailed in Definition 2.4 and Section 2.3. In the main part of this paper, we restrict ourselves to nets indexed by subsets of Baire space, i.e. part of third-order arithmetic, as such nets are already general enough to obtain our main results. More motivation for the RM-study of nets is provided in Section 1.3, and we summarise our results in Section 1.2.

1.2. Summary of results

First of all, the Bolzano–Weierstrass theorem for nets implies both the sequential and uncountable open-cover compactness of $[0, 1]$ . The latter notion is captured by $HBU$ (see Section 2.2) and the minimal2

²
In classical RM, the sequential compactness of $[0, 1]$ is equivalent to ${ACA}_{0}$ by [98, III.2.2], while the (countable) open-cover compactness of the unit interval is equivalent to ${WKL}_{0}$ by [98, IV.1]. In higher-order RM, the open-cover compactness for uncountable covers of the unit interval, called $HBU$ , cannot be proved in $Π_{k}^{1} {- CA}_{0}^{ω} + {QF-AC}^{0, 1}$ by [81,84], while $Z_{2}^{Ω}$ suffices. These higher-order systems are conservative over their (obvious) second-order counterparts by Section 2.2.

comprehension axioms needed to prove the latter imply second-order arithmetic by [84, §3]. We establish this and similar results in Section 3.

In particular, we study the following theorems generalised to nets: the Bolzano–Weierstrass theorem (Section 3.1.1), the monotone convergence theorem (see Section 3.1.2), the so-called anti-Specker property (Section 3.1.3), Cauchy nets (Section 3.1.4), Dini’s theorem (Section 3.2.1), and Arzelà’s theorem (Section 3.2.2). In each case, we shall obtain $HBU$ , and sometimes an equivalence over a reasonable base theory. We also discuss unordered sums in Section 3.1.5 as the study of such sums by Moore in [70] was a step towards the Moore–Smith theory in [73].

Secondly, we study the role of the Axiom of Choice. In particular, we show that:

replacing nets by sequences requires the Axiom of (countable) Choice,

replacing sequences by nets can obviate the need for the latter axiom.

As to goal (i), the minimal comprehension axioms needed to prove basic results about nets are rather strong, i.e. these minimal axioms imply full second-order arithmetic. It may therefore seem desirable (and in line with the coding practice of classical/second-order RM) to replace the limit process involving nets by a ‘countable’ limit process involving sequences, i.e. if a net converges to some limit, then there should be a sequence in the net that also converges to the same limit. This ‘sub-sequence property’ was studied by Bourbaki [20] and we show in Section 4.2 that a highly elementary instance implies the Lindelöf lemma for

R

, which is at least3

Note that $LIN + WKL$ implies $HBU$ by [98, IV.1], and there are versions of $LIN$ that imply fragments of the Axiom of (countable) Choice (see [81, §5]), in contrast to $HBU$ .

as hard to prove as

HBU

. An even weaker instance is shown to be equivalent to a fragment of the Axiom of (countable) Choice, not provable in

ZF

Secondly, as to goal (ii), we establish in Section 4.3 the local equivalence between ‘epsilon-delta’ continuity and the notion of continuity provided by nets without using the Axiom of Choice; the latter axiom is essential for the equivalence involving sequential continuity. We prove a similar result for closed4

⁴

As discussed in Section 4.4, ‘(sequentially) closed’ sets are represented by $R \to R$ -functions.

and sequentially closed sets in Section 4.4. In other words, while basic properties of nets are hard to prove, nets can also obviate the need for the Axiom of Choice, a foundationally important observation, as discussed in Section 4.1. Finally, we stress that the definition of closed sets in [45] and the definition of continuity in [45,47] are given in terms of nets, i.e. nets are central to domain theory and are used to define basic notions. It should be noted that the notion of Scott continuity (also defined via nets) is more central than the aforementioned continuity notions in domain theory.

Thirdly, as noted above, the main part of this paper is restricted to nets indexed by subsets of Baire space (as in Definition 2.4), as such nets suffice to obtain our main results. We shall study (more) general index sets in Appendix A. In particular, we obtain full n-th order arithmetic from a realiser (aka witnessing functional) for the monotone convergence theorem for nets indexed by sets expressible in the language of n-th order arithmetic. Appendix A is meant as illustration: we believe that this kind of study should be further developed in a set theoretic framework. Nonetheless, index sets beyond Baire space do occur ‘in the wild’, namely in fuzzy mathematics and the iterated limit theorems, as discussed in Remark A.1.

Finally, some initial RM-results on nets, in particular certain theorems from Sections 3.1.1, 3.1.2, 3.2.1, and Sections 4.2, 4.3, and A.2 can be found in [93,94] as part of LNCS conference proceedings. All other results in this paper are new, while the below proofs are the most elementary to date. It goes without saying that this paper constitutes a spin-off from the joint project with Dag Normann on the Reverse Mathematics and computability theory of the uncountable. The interested reader may consult [84] for an introduction to this endeavour.

1.3. Motivation

We provide some motivation for the RM-study of nets in this section. In light of the previous section, the answer to the question in item (d) is positive: the Bolzano–Weierstrass theorem for nets implies both sequential and (uncountable) open-cover compactness.

Nets were introduced5

⁵
On a historical note, Vietoris introduces the notion of oriented set in [108, p. 184], which is exactly the notion of ‘directed set’. He proceeds to prove (among others) a version of the Bolzano–Weierstrass theorem, and also mentions that these results are part of his dissertation, written in the period 1913–1919, i.e. during his army service for the Great War.

about a century ago [71,73,108] and many basic theorems have since been generalised to nets, i.e. nets should count as ‘ordinary mathematics’ in Simpson’s sense, as discussed in [98, I.1].

Nets provide an elegant equivalent formulation of compactness; the latter has been studied in remarkable detail in RM (see e.g. [26,27]). This paper can therefore be viewed as a continuation of this study, based on nets.

Filters are studied in the RM of topology (see e.g. [75–77]), and it is well-known that nets and filters provide an equivalent framework (see [7]).

Sequential compactness and open-cover compactness are classified in quite different² RM categories. It is a natural, if somewhat outlandish, question if there is one concept that ‘unifies’ these different notions of compactness.

The weak-∗-topology, including the Banach–Alaoglu theorem, is studied in RM (see [98, X.2] for an overview) and this topology has an elegant formulation in terms of nets. Moreover, Alaoglu makes use of nets in [2] to prove the general version of the aforementioned theorem.

Domain theory and associated topologies are studied in RM [64,78], and nets take central stage in domain theory in [44,45,47].

Nets are used in topological dynamics [41], which is studied in the proof mining program [43,60]. More generally, ergodic theory is also studied in RM [32] and proof theory [5], and it is therefore a natural question how strong basic results regarding nets are.

In general, sequences do not suffice for describing topologies, and nets are needed instead (see the Arens–Fort space in [100, p. 54]). As it turns out, even for basic spaces like $R$ where sequences do suffice to describe the topology over strong systems like $ZFC$ , sequences no longer suffice to describe the topology over weak systems like ${RCA}_{0}^{ω}$ , but nets do suffice (see Section 4).

We discuss these and related conceptual motivations in more detail in the body of the paper, namely in Remarks 3.1, 3.2, 3.3, and A.1. We stress that item (h) elevates the RM-study of nets beyond that of a mere curiosity: nets are in fact needed to described topologies in weak systems like

{RCA}_{0}^{ω}

, even if the topology can be described by sequences assuming strong systems like

ZFC

. In fact, countable choice plays an essential role, as discussed in Section 4.1.

2. Preliminaries

We introduce Reverse Mathematics in Section 2.1, as well as its generalisation to higher-order arithmetic, and the associated base theory ${RCA}_{0}^{ω}$ . We introduce some essential axioms in Section 2.2. We provide a brief introduction to nets and related concepts in Section 2.3. As noted in Section 1, to obtain our main results it suffices to study nets indexed by subsets of Baire space, i.e. part of third-order arithmetic; the associated bit of set theory shall be represented in ${RCA}_{0}^{ω}$ as in Definition 2.4.

2.1. Reverse mathematics

Reverse Mathematics is a program in the foundations of mathematics initiated around 1975 by Friedman [37,38] and developed extensively by Simpson [98]. 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 [101] for a basic introduction to RM and to [97,98] for an overview of RM. We expect basic familiarity with RM, but do sketch some aspects of Kohlenbach’s higher-order RM [59] essential to this paper, including the base theory ${RCA}_{0}^{ω}$ (Definition 2.1). As will become clear, the latter is officially a type theory but can accommodate (enough) set theory via Definition 2.4.

First of all, in contrast to ‘classical’ RM based on second-order arithmetic $Z_{2}$ , higher-order RM uses $L_{ω}$ , the richer language of higher-order arithmetic. Indeed, while the latter 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 T, defined by the two clauses: $\begin{array}{l} (i) 0 \in T and (ii) If σ, τ \in T then (σ \to τ) \in T, \end{array}$ 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 functions from numbers to numbers, and where $n + 1 \equiv n \to 0$ . Viewing sets as given by characteristic functions, we note that $Z_{2}$ only includes objects of type 0 and 1.

Secondly, the language $L_{ω}$ includes variables $x^{ρ}, y^{ρ}, z^{ρ}, \dots$ of any finite type $ρ \in T$ . Types may be omitted when they can be inferred from context. The constants of $L_{ω}$ 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 $\begin{matrix} (2.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}], \end{matrix}$ if the type τ is composed as $τ \equiv (τ_{1} \to \dots \to τ_{k} \to 0)$ . Furthermore, $L_{ω}$ also includes the recursor constant $R_{0}$ , which allows for iteration on type 0-objects as in (2.2). Formulas and terms are defined as usual. One obtains the sub-language $L_{n + 2}$ by restricting the above type formation rule to produce only type $n + 1$ objects (and related types of similar complexity).

Definition 2.1.
The base theory ${RCA}_{0}^{ω}$ consists of the following axioms.
Basic axioms expressing that 0, 1, $<_{0}$ , $+_{0}$ , $\times_{0}$ form an ordered semi-ring with equality $=_{0}$ .

Basic axioms defining the well-known Π and Σ combinators (aka K and S in [6]), which allow for the definition of λ-abstraction.

The defining axiom of the recursor constant $R_{0}$ : For $m^{0}$ and $f^{1}$ : $\begin{matrix} (2.2) & R_{0} (f, m, 0) : = m and R_{0} (f, m, n + 1) : = f (n, R_{0} (f, m, n)) . \end{matrix}$

The axiom of extensionality: for all $ρ, τ \in T$ , we have: $\begin{array}{l} (E_{ρ, τ}) & (\forall x^{ρ}, y^{ρ}, φ^{ρ \to τ}) [x =_{ρ} y \to φ (x) =_{τ} φ (y)] . \end{array}$

The induction axiom for quantifier-free6
⁶
To be absolutely clear, variables (of any finite type) are allowed in quantifier-free formulas of the language $L_{ω}$ : only quantifiers are banned.

formulas of $L_{ω}$ .

${QF-AC}^{1, 0}$ : The quantifier-free Axiom of Choice as in Definition 2.2.

Definition 2.2.
The axiom $QF-AC$ consists of the following for all $σ, τ \in T$ : $\begin{array}{l} ({QF-AC}^{σ, τ}) & (\forall x^{σ}) (\exists y^{τ}) A (x, y) \to (\exists Y^{σ \to τ}) (\forall x^{σ}) A (x, Y (x)), \end{array}$ for any quantifier-free formula A in the language of $L_{ω}$ .

We let $IND$ be the induction axiom for all formulas in $L_{ω}$ . The system ${RCA}_{0}^{ω} + IND$ has the same first-order strength as Peano arithmetic.

As discussed in [59, §2], ${RCA}_{0}^{ω}$ and ${RCA}_{0}$ prove the same sentences ‘up to language’ as the latter is set-based and the former function-based. Recursion as in (2.2) is also called primitive recursion. One can generalise $R_{0}$ to any finite type and the class of functionals obtained from $R_{ρ}$ for all $ρ \in T$ is called Gödel’s system T of all (higher-order) primitive recursive functionals.

We use the usual notations for natural, rational, and real numbers, and the associated functions, as introduced in [59, p. 288–289].
Definition 2.3 (Real numbers and related notions in ${RCA}_{0}^{ω}$ ).

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.

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

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.

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} | ⩽ 2^{- n + 1})$ . Inequality ‘ $<_{R}$ ’ is defined similarly. We sometimes omit the subscript ‘ $R$ ’ if it is clear from context.

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

The relation ‘ $x ⩽_{τ} y$ ’ is defined as in (2.1) but with ‘ $⩽_{0}$ ’ instead of ‘ $=_{0}$ ’. Binary sequences are denoted ‘ $f^{1}, g^{1} ⩽_{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}$ ’.

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

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

The following special case of item (h) is singled out, as it will be used frequently.

Definition 2.4 ( ${RCA}_{0}^{ω}$ ).

A ‘subset D of $N^{N}$ ’ is given by its characteristic function $F_{D}^{2} ⩽_{2} 1$ , i.e. we write ‘ $f \in D$ ’ for $F_{D} (f) = 1$ for any $f \in N^{N}$ . A ‘binary relation ⪯ on a subset D of $N^{N}$ ’ is given by the associated characteristic function $G_{⪯}^{(1 \times 1) \to 0}$ , i.e. we write ‘ $f ⪯ g$ ’ for $G_{⪯} (f, g) = 1$ and any $f, g \in D$ . Assuming extensionality on the reals as in item (e), we obtain characteristic functions that represent subsets of $R$ and relations thereon. Using pairing functions, it is clear we can also represent sets of finite sequences (of reals), and relations thereon.

Finally, we mention the highly useful $ECF$ -interpretation.

Remark 2.1 (The $ECF$ -interpretation).

The technical definition of $ECF$ may be found in [106, p. 138, §2.6]. Intuitively speaking, the $ECF$ -interpretation ${[A]}_{ECF}$ of a formula $A \in L_{ω}$ is just A with all variables of type two and higher replaced by countable representations of continuous functionals. Such representations are also (equivalently) called ‘associates’ or ‘codes’ (see [58, §4]). The $ECF$ -interpretation connects ${RCA}_{0}^{ω}$ and ${RCA}_{0}$ (see [59, Prop. 3.1]) in that if ${RCA}_{0}^{ω}$ proves A, then ${RCA}_{0}$ proves ${[A]}_{ECF}$ , again ‘up to language’, as ${RCA}_{0}$ is formulated using sets, and ${[A]}_{ECF}$ is formulated using types, namely only using type zero and one objects.

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

Notation 2.1 (Finite sequences).

We assume a dedicated type for ‘finite sequences of objects of type ρ’, namely $ρ^{*}$ . Since the usual coding of pairs of numbers goes through in ${RCA}_{0}^{ω}$ , we shall not always distinguish between 0 and $0^{*}$ . Similarly, 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 sequence $s^{ρ^{*}} = ⟨ s_{0}^{ρ}, s_{1}^{ρ}, \dots, s_{n - 1}^{ρ} ⟩$ , where $| ⟨ ⟩ | = 0$ , i.e. the empty sequence has length zero. For sequences $s^{ρ^{*}}$ , $t^{ρ^{*}}$ , 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 | ⩽ j < | s | + | t |$ . For a sequence $s^{ρ^{*}}$ , we define $\overline{s} N : = ⟨ s (0), s (1), \dots, s (N - 1) ⟩$ for $N^{0} < | s |$ . For $α^{0 \to ρ}$ , we also write $\overline{α} 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.

2.2. Some axioms of higher-order RM

We introduce some functionals which constitute the counterparts of second-order arithmetic $Z_{2}$ , and some of the Big Five systems, in higher-order RM. We use the formulation from [59,84].

First of all, Feferman’s search operator $μ^{2}$ [6] is defined as follows: $\begin{array}{l} (\exists μ^{2}) (\forall f^{1}) [(\exists n) (f (n) = 0) \\ (μ^{2}) & \to [f (μ (f)) = 0 \land (\forall i < μ (f)) (f (i) \neq 0) \land [(\forall n) (f (n) \neq 0) \to μ (f) = 0]]] . \end{array}$ The system ${ACA}_{0}^{ω} \equiv {RCA}_{0}^{ω} + (μ^{2})$ proves the same sentences as ${ACA}_{0}$ by [52, Theorem 2.5]. The (unique) functional $μ^{2}$ in $(μ^{2})$ is also called Feferman’s μ for short, and is discontinuous at $f =_{1} 11 \dots$ ; in fact, $(μ^{2})$ is equivalent to the existence of $F : R \to R$ such that $F (x) = 1$ if $x >_{R} 0$ , and 0 otherwise [59, §3], and to $\begin{array}{l} (\exists^{2}) & (\exists φ^{2} ⩽_{2} 1) (\forall f^{1}) [(\exists n) (f (n) = 0) \leftrightarrow φ (f) = 0] . \end{array}$ Secondly, the Suslin functional $S^{2}$ is defined as follows: $\begin{array}{l} (S^{2}) & (\exists S^{2} ⩽_{2} 1) (\forall f^{1}) [(\exists g^{1}) (\forall n^{0}) (f (\overline{g} n) = 0) \leftrightarrow S (f) = 0], \end{array}$ The system $Π_{1}^{1} {- CA}_{0}^{ω} \equiv {RCA}_{0}^{ω} + (S^{2})$ proves the same $Π_{3}^{1}$ -sentences as $Π_{1}^{1} {- CA}_{0}$ by [90, Theorem 2.2]. By definition, the Suslin functional $S^{2}$ can decide whether a $Σ_{1}^{1}$ -formula (as in the left-hand side of $(S^{2})$ ) is true or false. We similarly define the functional $S_{k}^{2}$ which decides the truth or falsity of $Σ_{k}^{1}$ -formulas; we also define the system $Π_{k}^{1} {- CA}_{0}^{ω}$ as ${RCA}_{0}^{ω} + (S_{k}^{2})$ , where $(S_{k}^{2})$ expresses that $S_{k}^{2}$ exists. Note that we allow formulas with function parameters, but not functionals here. In fact, Gandy’s Superjump [42] constitutes a way of extending $Π_{1}^{1} {- CA}_{0}^{ω}$ to parameters of type two.

Thirdly, full second-order arithmetic $Z_{2}$ is readily derived from $⋃_{k} Π_{k}^{1} {- CA}_{0}^{ω}$ , or from: $\begin{array}{l} (\exists^{3}) & (\exists E^{3} ⩽_{3} 1) (\forall Y^{2}) [(\exists f^{1}) Y (f) = 0 \leftrightarrow E (Y) = 0], \end{array}$ and we therefore define $Z_{2}^{Ω} \equiv {RCA}_{0}^{ω} + (\exists^{3})$ and $Z_{2}^{ω} \equiv ⋃_{k} Π_{k}^{1} {- CA}_{0}^{ω}$ , which are conservative over $Z_{2}$ by [52, Cor. 2.6]. Despite this close connection, $Z_{2}^{ω}$ and $Z_{2}^{Ω}$ can behave quite differently, as discussed in e.g. [84, §2.2]. The functional from $(\exists^{3})$ is also called ‘ $\exists^{3}$ ’, and we use the same convention for other functionals.

Finally, the Heine–Borel theorem states the existence of a finite sub-cover for an open cover of certain spaces. Now, a functional $Ψ : R \to R^{+}$ gives rise to the canonical cover $⋃_{x \in I} I_{x}^{Ψ}$ for $I \equiv [0, 1]$ , where $I_{x}^{Ψ}$ is the open interval $(x - Ψ (x), x + Ψ (x))$ . Hence, the uncountable cover $⋃_{x \in I} I_{x}^{Ψ}$ has a finite sub-cover by the Heine–Borel theorem; in symbols: $\begin{array}{l} (HBU) & (\forall Ψ : R \to R^{+}) (\exists ⟨ y_{1}, \dots, y_{k} ⟩) (\forall x \in I) (\exists i ⩽ k) (x \in I_{y_{i}}^{Ψ}) . \end{array}$ Note that $HBU$ is almost verbatim Cousin’s lemma (see [31, p. 22]), i.e. the Heine–Borel theorem restricted to canonical covers. The latter restriction does not make much of a big difference, as studied in [91]. By [81,84], $Z_{2}^{Ω}$ proves $HBU$ but $Z_{2}^{ω} + {QF-AC}^{0, 1}$ cannot, and many basic properties of the gauge integral [74,102] are equivalent to $HBU$ . Although strictly speaking incorrect, we sometimes use set-theoretic notation, like reference to the cover $⋃_{x \in I} I_{x}^{Ψ}$ inside ${RCA}_{0}^{ω}$ , to make proofs more understandable. Such reference can in principle be removed in favour of formulas of higher-order arithmetic.

2.3. Introducing nets

We introduce the notion of net and associated concepts. We first consider the following standard definition (see e.g. [55, Ch. 2]).

Definition 2.5 (Nets).

A set $D \neq \emptyset$ with a binary relation ‘⪯’ is directed if

The relation ⪯ is transitive, i.e. $(\forall x, y, z \in D) ([x ⪯ y \land y ⪯ z] \to x ⪯ z)$ .

For $x, y \in D$ , there is $z \in D$ such that $x ⪯ z \land y ⪯ z$ .

The relation ⪯ is reflexive, i.e. $(\forall x \in D) (x ⪯ x)$ .

For such

(D, ⪯)

and topological space X, any mapping

x : D \to X

is a net in X. We denote

λ d . x (d)

as ‘

x_{d}

’ or ‘

x_{d} : D \to X

’ to suggest the connection to sequences. The directed set

(D, ⪯)

is not always explicitly mentioned together with a net

x_{d}

In this paper, we only study directed sets that are subsets of Baire space, i.e. as given by Definition 2.4. Similarly, we only study nets $x_{d} : D \to R$ where D is a subset of Baire space. Thus, a net $x_{d}$ in $R$ is just a type $1 \to 1$ functional with extra structure on its domain D provided by ‘⪯’ as in Definition 2.4. We shall allow for additional input variables over $R$ in Section 3.2 in the study of nets of functions.

The definitions of convergence and increasing net have the usual form in this setting.

Definition 2.6 (Convergence of nets).

If $x_{d}$ is a net in X, we say that $x_{d}$ converges to the limit ${lim}_{d} x_{d} = y \in X$ if for every neighbourhood U of y, there is $d_{0} \in D$ such that for all $e ⪰ d_{0}$ , $x_{e} \in U$ .

Definition 2.7 (Increasing nets).

A net $x_{d} : D \to R$ is increasing if $a ⪯ b$ implies $x_{a} ⩽_{R} x_{b}$ for all $a, b \in D$ .

Definition 2.8.
A point $x \in X$ is a cluster point for a net $x_{d}$ in X if every neighbourhood U of x contains $x_{u}$ for some $u \in D$ .

The previous definition yields the following nice equivalence: a toplogical space is compact if and only if every net therein has a cluster point [7, Prop. 3.4]. All the below results can be formulated using cluster points only, but such an approach does not address the question of what the counterpart of ‘sub-sequence’ for nets is. Indeed, an obvious next step following Definition 2.8 is to take smaller and smaller neighbourhoods around the cluster point x and (somehow) say that the associated points $x_{u}$ net-converge to x. To this end, we consider the following definition, first introduced by Moore in [72], and used by Kelley in [55]. Alternative definitions involve extra requirements (see [96, §7.14]), i.e. our definition is the weakest.
Definition 2.9 (Sub-nets).

A sub-net of a net $x_{d}$ with directed set $(D, ⪯_{D})$ , is a net $y_{b}$ with directed set $(B, ⪯_{B})$ such that there is a function $ϕ : B \to D$ such that:

the function ϕ satisfies $y_{b} = x_{ϕ (b)}$ ,

$(\forall d \in D) (\exists b_{0} \in B) (\forall b ⪰_{B} b_{0}) (ϕ (b) ⪰_{D} d)$ .

We point out that the distinction between ‘ $⪯_{B}$ ’ and ‘ $⪯_{D}$ ’ is not always made in the literature (see e.g. [7,55]). Finally, $N$ with its usual ordering yields a directed set, i.e. convergence results about nets do apply to sequences. Of course, a sub-net of a sequence is not necessarily a sub-sequence, i.e. some care is advisable in these matters. Nonetheless, the Bolzano–Weierstrass theorem for nets will be seen to imply the monotone convergence theorem for sequences in Section 3.1.1.

3. Main results I

We study the generalisation to nets of theorems pertaining to the sequential compactness of the unit interval in Section 3.1. We study theorems pertaining to nets of functions in Section 3.2. In each case, we obtain $HBU$ from Section 2.2, and sometimes even an equivalence over a reasonable base theory.

3.1. Sequential compactness and nets

In this section, we study the generalisation to nets of theorems pertaining to the sequential compactness of the unit interval, like the Bolzano–Weierstrass (Section 3.1.1) and the monotone convergence theorem (Section 3.1.2). These generalisations imply the sequential compactness of the unit interval, but also the Heine–Borel compactness for uncountable covers as in $HBU$ . Hence, nets provide a ‘unified’ approach to compactness that captures both sequential and (uncountable) open-cover compactness. We also study the ‘anti-Specker property’ from constructive mathematics in Section 3.1.3, which can be (equivalently) viewed as the study of isolated points of nets. Basic theorems pertaining to Cauchy nets are studied in Section 3.1.4. Finally, we discuss unordered sums in Section 3.1.5 as the study of such sums by Moore in [70] was the first step towards the Moore–Smith theory of convergence in [73].

3.1.1. The Bolzano–Weierstrass theorem for nets

We study the Bolzano–Weierstrass theorem for nets, ${BW}_{net}$ for short, i.e. the statement that a net in the unit interval $I \equiv [0, 1]$ has a convergent sub-net. This theorem is one of the standard results pertaining to nets, and can even be found in mathematical physics, namely in [87, p. 98]. As discussed in Section 2.3, ${BW}_{net}$ is limited to nets indexed by subsets of $N^{N}$ .

Theorem 3.1.
The system ${RCA}_{0}^{ω} + {BW}_{net}$ proves $HBU$ .
Proof.
Note that ${BW}_{net}$ implies the monotone convergence theorem for sequences, as the latter are nets. Indeed, if a sub-net $x_{ϕ (b)}$ of an increasing sequence $x_{n}$ converges to $x = {lim}_{b} x_{ϕ (b)}$ , then also ${lim}_{n \to \infty} x_{n} = x$ . Hence, we have access to ${ACA}_{0}$ by [98, III.2.2]. Now, in case $\neg (\exists^{2})$ , all functions on $R$ are continuous by [59, Prop. 3.12], and $HBU$ reduces to $WKL$ by [58, §4]. We now prove $HBU$ in case $(\exists^{2})$ , which finishes the proof using the law of excluded middle. Thus, suppose $\neg HBU$ and fix some $Ψ : I \to R^{+}$ for which $⋃_{x \in I} I_{x}^{Ψ}$ does not have a finite sub-cover. Let D be the set of all finite sequences of reals in the unit interval, and define ‘ $v ⪯_{D} w$ ’ for $w, v \in D$ if $⋃_{i < | v |} I_{v (i)}^{ψ} \subseteq ⋃_{i < | w |} I_{w (i)}^{ψ}$ , i.e. the cover generated by w includes the cover associated to v. Note that $(\exists^{2})$ suffices to define $⪯_{D}$ . Clearly, the latter is transitive and reflexive, and item (b) in Definition 2.5 is satisfied by noting that $(v * w) ⪰ w$ and $(v * w) ⪰ v$ . To define a net, consider $\begin{matrix} (3.1) & (\forall w^{1^{}} \in D) (\exists q \in Q \cap [0, 1]) \underline{(q \notin \cup_{i < | w |} I_{w (i)}^{Ψ})}, \end{matrix}$ which again holds by assumption. Note that the underlined formula in (3.1) is decidable thanks to $(\exists^{2})$ . Applying ${QF-AC}^{1, 0}$ to (3.1), we obtain a net $x_{w}$ in $[0, 1]$ , which has a convergent (say to $z_{0} \in I$ ) sub-net $y_{b} = x_{ϕ (d)}$ for some directed set $(B, ⪯_{B})$ and $ϕ : B \to D$ , by ${BW}_{net}$ . By definition, the neighbourhood $U_{0} = I_{z_{0}}^{Ψ}$ contains all $y_{b}$ for $b ⪰_{B} b_{1}$ for some $b_{1} \in B$ . However, taking $d = ⟨ z_{0} ⟩ \in D$ in the second item in Definition 2.9, there is also $b_{0} \in B$ such that $(\forall b ⪰_{B} b_{0}) (ϕ (b) ⪰_{D} ⟨ y_{0} ⟩)$ . By the definition of ‘ $⪯_{D}$ ’, $ϕ (b)$ is hence such that $⋃_{i < | ϕ (b) |} I_{ϕ (b) (i)}^{Ψ}$ contains $U_{0}$ , for any $b ⪰_{B} b_{0}$ . Now use item (b) from Definition 2.5 (for the directed set $(B, ⪯_{B})$ ) to find $b_{2} \in B$ satisfying $b_{2} ⪰_{B} b_{0}$ and $b_{2} ⪰_{B} b_{1}$ . Hence, $y_{b_{2}} = x_{ϕ (b_{2})}$ is in $U_{0}$ , but $⋃_{i < | ϕ (b_{2}) |} I_{ϕ (b_{2}) (i)}^{Ψ}$ also contains $U_{0}$ , i.e. $x_{ϕ (b_{2})}$ must be outside* of $U_{0}$ by the definition of $x_{w}$ , a contradiction. In this way, we also obtain $HBU$ in case $(\exists^{2})$ . □

We cannot expect a reversal in the previous theorem, as ${BW}_{net}$ implies ${ACA}_{0}$ , while ${RCA}_{0}^{ω} + HBU$ is conservative over ${WKL}_{0}$ , which readily follows from applying the $ECF$ -translation from Remark 2.1. Furthermore, the theorem suggests a realiser (aka witnessing functional) for ${BW}_{net}$ would compute a realiser for the Bolzano–Weierstrass theorem, and hence $\exists^{2}$ , as well as a realiser for $HBU$ , called Θ in [82–84]. By the results in the latter, a realiser for ${BW}_{net}$ therefore would compute a realiser for ${ATR}_{0}$ . We obtain much stronger results in Section 3.1.2.
3.1.2. The monotone convergence theorems for nets

We study the monotone convergence theorem for nets in the unit interval. To this end, let ${MCT}_{net}^{0}$ state that every increasing net in the unit interval converges. As discussed in Section 2.3, ${MCT}_{net}^{0}$ is restricted to nets that are indexed by subsets of Baire space.

We show ${MCT}_{net}^{0} \to HBU$ in Theorem 3.2, but Corollary 3.3 is of more importance, as it establishes that ${MCT}_{net}^{0}$ is provable without the Axiom of Choice, i.e. the ‘hardness’ of the former theorem has nothing to do with the latter. We obtain a relative computability result in Corollary 3.7, the foundation for Appendix A. We also obtain the equivalence ${MCT}_{net}^{0} \leftrightarrow HBU$ over a fairly nice base theory.

As to the provenance of ${MCT}_{net}^{0}$ , this theorem can be found in e.g. [25, p. 103], but is also implicit in domain theory [44,45]. Indeed, the main objects of study of domain theory are dcpos, i.e. directed-complete posets, and every monotone net converges to its supremum in any dcpo.

Theorem 3.2.
The system ${RCA}_{0}^{ω} + {MCT}_{net}^{0}$ proves $HBU$ .
Proof.
We make use of $(\exists^{2}) \lor \neg (\exists^{2})$ as in the proof of Theorem 3.1. The first part involving $\neg (\exists^{2})$ is identical. For the second part, fix some $Ψ : I \to R^{+}$ and use $(\exists^{2})$ to define D as the set of finite sequences of reals $w^{1^{}}$ such that $0 \in w$ and the cover $⋃_{i < | w |} I_{w (i)}^{Ψ}$ has ‘no holes’, i.e. any point between two intervals of this cover, is also in the cover. We define ‘ $v ⪯ w$ ’ as $(\forall i < | v |) (\exists j < | w |) (v (i) =_{R} w (j))$ . Clearly, $(D, ⪯)$ is a directed set and we define the net $x_{w} : D \to [0, 1]$ as the right end-point of the right-most interval in $⋃_{i < | w |} I_{w (i)}^{Ψ}$ , capped by 1 if necessary.

Since $x_{w}$ is increasing by definition, let $x \in [0, 1]$ be the limit provided by ${MCT}_{net}^{0}$ . If $x =_{R} 1$ , then apply $lim x_{d} = x$ for $ε = Ψ (1)$ to find a finite sub-cover for the canonical cover associated to Ψ. In case $x <_{R} 1$ , apply ${lim}_{d} x_{d} = x$ for $ε_{0} = min (Ψ (x), | x - 1 | / 2)$ , i.e. there is $w_{0} \in D$ such that for all $v ⪰ w_{0}$ , we have $| x_{v} - x | < ε_{0}$ , implying $x_{v} \in I_{x}^{Ψ}$ . Fix such $w_{0}$ and consider $v_{0} : = w_{0} ⟨ x ⟩$ . The latter is in D and satisfies $v_{0} ⪰ w_{0}$ . Hence, $x_{v_{0}}$ must be in $I_{x}^{Ψ}$ by the aforementioned convergence, but $x_{v_{0}} \notin I_{x}^{Ψ}$ by definition of the net $x_{w}$ . Hence, we have obtained a contradiction in case $x <_{R} 1$ , and we are done. □

The previous proof is counter-intuitive as it does not go through for a sequence defined as $x_{0} : = 0$ and $x_{n + 1} : = x_{n} + Ψ (x_{n})$ . In fact, Borel’s original proof of the Heine–Borel theorem [18] is based on transfinite iteration of these kinds of sequences. Of course, one could define $x_{n + 1}$ as the right end-point of the ‘largest’ interval covering $x_{n}$ , but this requires $\exists^{3}$ . In this light, the proof of the theorem involving nets is ‘more constructive’ than a proof involving sequences and $\exists^{3}$ .

On one hand, the previous implies that nets indexed by subsets of Baire space already give rise to $HBU$ . On the other hand, the proof of the following corollary suggests that such nets are ‘all we can handle’ in $Z_{2}^{Ω}$ .
Corollary 3.3.
The system $Z_{2}^{Ω}$ proves ${MCT}_{net}^{0}$ , while $Z_{2}^{ω} + {QF-AC}^{0, 1}$ does not.
Proof.
The negative result follows from [81, Theorem 4.3]. For the remaining result, note that $HBU$ is available thanks to [81, Theorem 4.2]. Suppose $\neg {MCT}_{net}^{0}$ , i.e. there is some increasing net $x_{d}$ in I that does not converge to any point in I. Hence, for every $x \in I$ there is $n \in N$ such that for all $d \in D$ there is $e ⪰ d$ such that $| x - x_{e} | ⩾ \frac{1}{2^{n}}$ . Since $\exists^{3}$ is given, we may use ${QF-AC}^{1, 0}$ to obtain $Φ : I \to R$ such that $Φ (x)$ is the least such $n \in N$ . Define $Ψ (x) : = \frac{1}{2^{Φ (x)}}$ and use $HBU$ to find $y_{1}, \dots, y_{k} \in I$ such that $⋃_{i ⩽_{k}} I_{y_{i}}^{Ψ}$ covers I. By definition, for any $i ⩽ k$ , either $x_{d}$ is ‘below’ $I_{y_{i}}^{Ψ}$ for all $d \in D$ or there is $d_{i} \in D$ such that $x_{e}$ is ‘above’ $I_{y_{i}}^{Ψ}$ for all $e ⪰ d_{i}$ . Let $d_{i_{1}}, \dots, d_{i_{m}} \in D$ be all such numbers from the second case. There is $e_{0} ⪰ d_{i_{j}}$ for $j ⩽ m$ by Definition 2.5, but $x_{e_{0}}$ cannot be in I, a contradiction. □

The previous theorem also implies that ${MCT}_{net}^{0}$ has the same first-order strength as ${ACA}_{0}$ using the above ‘excluded middle trick’ and the ‘splitting’ of $(\exists^{3})$ as $[(κ_{0}^{3}) + (\exists^{2})] \leftrightarrow (\exists^{3})$ , where $(κ_{0}^{3})$ may be found in [92, §3.1].

Nonetheless, it remains desirable to derive ${MCT}_{net}^{0}$ from ‘more constructive’ axioms than $(\exists^{3})$ , preferably involving $HBU$ . To this end, recall the neighbourhood function principle $NFP$ , a choice principle in the intersection of both classical and intuitionistic mathematics, as discussed in [107, p. 215]. The proof of the Lindelöf lemma for $R$ in $Z_{2}^{Ω} + {QF-AC}^{0, 1}$ in [84] makes use of $NFP$ . We use the following special case of $NFP$ not involving RM codes.
Definition 3.4 ( ${NFP}_{0}$ ).

For any $Π_{\infty}^{1}$ -formula A with any type two parameter: $\begin{matrix} (\forall f^{1}) (\exists n^{0}) A (\overline{f} n) \to (\exists Φ^{2}) (\forall f^{1}) A (\overline{f} Φ (f)) . \end{matrix}$

Note that $NFP$ states the existence of an RM code for Φ as in ${NFP}_{0}$ . Thus, the $ECF$ -translation of ${NFP}_{0}$ yields $NFP$ restricted to $L_{2}$ -formulas. Assuming ${RCA}_{0}^{ω} + {NFP}_{0}$ is consistent, it therefore cannot prove e.g. $(\exists^{2})$ , while (second-order) comprehension follows by the results in [107, p. 245]. We now have the following theorem.

Theorem 3.5.
The system ${RCA}_{0}^{ω} + IND + {NFP}_{0} + HBU$ proves ${MCT}_{net}^{0}$ .
Proof.
Let $x_{d} : D \to I$ be an increasing net that does not converge, i.e. $\begin{matrix} (3.2) & (\forall y \in I) (\exists k^{0}) (\forall d \in D) (\exists e ⪰ d) (| x_{e} - y | ⩾ \frac{1}{2^{k}}) . \end{matrix}$ Recall that $[x] (k)$ is the k-th approximation of the real x; (3.2) implies $\begin{matrix} (3.3) & (\forall y \in I) (\exists k^{0}) \underline{(\forall d \in D) (\exists e ⪰ d) (| x_{e} - [y] (2^{k + 1}) | ⩾ \frac{1}{2^{k}})} . \end{matrix}$ The underlined formula in (3.3) can be written $A (\overline{y} k)$ with only slight abuse of notation. Applying ${NFP}_{0}$ to (3.3), there is $Φ^{2}$ such that $\begin{matrix} (\forall y \in I) (\forall d \in D) (\exists e ⪰ d) (| x_{e} - y | ⩾ \frac{1}{2^{Φ (y)}}) . \end{matrix}$ The canonical cover $⋃_{x \in [0, 1]} I_{x}^{Ψ}$ of $[0, 1]$ for Ψ defined as $Ψ (x) : = \frac{1}{2^{Φ (x)}}$ has a finite sub-cover $y_{0}, \dots, y_{k}$ by $HBU$ , i.e. $⋃_{i ⩽ k} I_{y_{i}}^{Ψ}$ covers $[0, 1]$ . Now for $y_{i_{0}}$ such that $0 \in I_{y_{i_{0}}}^{Ψ}$ and some $d_{0} \in D$ , there is $e_{0} ⪰ d_{0}$ such that $x_{e_{0}} \notin I_{y_{i_{0}}}^{Ψ}$ , which implies $x_{e_{0}} ⩾ Ψ (y_{i_{0}})$ . Repeat the previous for $y_{i_{1}}$ such that $Ψ (y_{0}) \in I_{y_{i_{1}}}^{Ψ}$ and $e_{0}$ , yielding $x_{e_{1}} ⩾ Ψ (y_{i_{0}}) + Ψ (y_{i_{1}})$ for some $e_{1} ⪰ e_{0}$ . After at most k steps, we find $x_{d}$ that falls outside of $[0, 1]$ , a contradiction. Note that this k-step process can be performed in ${RCA}_{0}^{ω} + IND$ . □
Corollary 3.6.
The system ${RCA}_{0}^{ω} + IND + {NFP}_{0}$ proves $HBU \leftrightarrow {MCT}_{net}^{0}$ .

The axiom ${NFP}_{0}$ is clearly much too strong for the above and we study weaker axioms in [95]. While the previous proof proceeds via contradiction, a ‘direct’ proof is available for the case of the anti-Specker property in Section 3.1.3.

Next, it is well-known that $\exists^{2}$ computes a realiser for the monotone convergence theorem for sequences via a term of Gödel’s T, and vice versa (see [90, §4]). Inspired by this observation, we obtain an elegant ‘one type up’ generalisation in Corollary 3.7. A realiser for ${MCT}_{net}^{0}$ is a functional taking as input $(D, ⪯_{D}, x_{d})$ and outputting the real $x = {lim}_{d} x_{d}$ if the inputs satisfy the conditions of ${MCT}_{net}^{0}$ .
Corollary 3.7.
A realiser for ${MCT}_{net}^{0}$ computes $\exists^{3}$ via a term of Gödel’s T, and vice versa.
Proof.
For the ‘vice versa’ direction, one uses the usual ‘interval halving technique’ where $\exists^{3}$ is used to decide whether there is $d \in D$ such that $x_{d}$ is in the relevant interval. Indeed, define $𝕣 : C \to [0, 1]$ as $𝕣 (f) : = \sum_{n = 0}^{\infty} \frac{f (n)}{2^{n + 1}}$ and define $f_{0} \in C$ as follows: $f_{0} (0) = 1$ if and only if $(\exists d \in D) (x_{d} ⩾ \frac{1}{2})$ and $f_{0} (n + 1) = 1$ if and only if $(\exists d \in D) (x_{d} ⩾ 𝕣 (\overline{f_{0}} n * 00 \dots))$ . Then ${lim}_{d} x_{d} = 𝕣 (f_{0})$ , as required.

For the other direction, fix $Y^{2}$ , let D be Baire space, and define ‘ $f ⪯ g$ ’ by $Y (f) ⩾_{0} Y (g)$ for any $f, g \in D$ . It is straightforward to show that $(D, ⪯)$ is a directed set. Define the net $x_{d} : D \to I$ by 0 if $Y (d) > 0$ , and 1 if $Y (d) = 0$ , which is increasing by definition. Hence, $x_{d}$ converges, say to $y_{0} \in I$ , and if $y_{0} >_{R} 1 / 3$ , then there must be $f^{1}$ such that $Y (f) = 0$ , while if $y_{0} <_{R} 2 / 3$ , then $(\forall f^{1}) (Y (f) > 0)$ . Clearly, this provides a term of Gödel’s T that computes $\exists^{3}$ . □

The previous two corollaries show that ${MCT}_{net}^{0}$ is extremely hard to prove (in terms of the usual hierarchy of comprehension axioms), the limit therein similarly hard to compute. We establish in Appendix A that generalisations of ${MCT}_{net}^{0}$ to ‘larger’ index sets have yet more extreme properties, even compared to e.g. $\exists^{3}$ .

Finally, ${BW}_{net}$ implies ${MCT}_{net}^{0}$ , but the reversal seems to need the following theorem, which is restricted as in Definition 2.4; the general case is in e.g. [49, §2].
Definition 3.8 ( ${ADS}_{net}$ ).

A net in $R$ has a monotone sub-net.

We conjecture ${ADS}_{net}$ does not follow from ${MCT}_{net}^{0}$ and is connected to $ADS$ from the RM zoo (see [51]). The usual proof of ${ACA}_{0} \to ADS$ provides a proof of $[(\exists^{3}) + {QF-AC}^{1, 1}] \to {ADS}_{net}$ , and we believe that the Axiom of Choice is essential. We finish this section with a conceptual remark.

Remark 3.1 (Filters versus nets).

For completeness, we discuss the intimate connection between filters and nets. Now, a topological space X is compact if and only if every filter base has a refinement that converges to some point of X (see [7, Prop. 3.4]). Whatever the meaning of the italicised notions, the similarity with the Bolzano–Weierstrass theorem for nets is obvious, and not a coincidence: for every net $r$ , there is an associated filter base $B (r)$ such that if the erstwhile converges, so does the latter to the same point; one similarly associates a net $r (B)$ to a given filter base $B$ with the same convergence properties (see [7, §2]). Hence, one can reformulate ${BW}_{net}$ using filters and obtain the same result as in Theorem 3.1. We choose nets over filters in this paper for the following reasons.

Nets have a greater intuitive clarity compared to filters, in our opinion, due to the similarity between nets and sequences.

Nets are ‘more economical’ in terms of ontology: consider the aforementioned filter base $B (r)$ associated to the net $r$ . By [7, Prop. 2.1], the base has strictly higher type than the net. The same holds for $r (B)$ versus $B$ .

The notion of refinement mirrors the notion of sub-net by [7, §2]. The former is studied in [91] in the context of paracompactness and the associated results suggest that the notion of sub-net works better in weak systems.

On a historical note, G. Birkhoff introduces what we nowadays call ‘convergence of a filter base’ in [15], but switched to nets for [16]. Despite Birkhoff’s aforementioned work, Cartan is generally credited with pioneering the use of filters in topology in [29], and the latter are unsurprisingly also the lingua franca of Bourbaki [19,20]. On a conceptual note, the well-known notion of ultrafilter corresponds to the equivalent notion of universal net [7, §3].

3.1.3. Isolated points and nets

We study a theorem pertaining to isolated points, i.e. any net convergent to such a point must be eventually constant. Indeed, the proof of Theorem 3.10 deals with $[0, 1] \cup {2}$ , which has an obvious isolated point. There is a ‘constructive’ dimension to this section, as discussed in Remark 3.2, where we also explain the name of the following definition.

Definition 3.9 (Anti-Specker property).

We say that the net $x_{d} : D \to R$ is eventually bounded away from the point $x \in R$ if $(\exists δ > 0, d \in D) (\forall e ⪰ d) (| x - x_{e} | ⩾ δ)$ .

We say that the net $x_{d} : D \to R$ is eventually bounded away from the set $[0, 1]$ if $(\exists δ > 0, d \in D) (\forall e ⪰ d) (\forall x \in [0, 1]) (| x - x_{e} | ⩾ δ)$ .

The theorem ${AS}_{net}$ states that any net that is eventually bounded away from every $x \in [0, 1]$ , is eventually bounded away from $[0, 1]$ .

As discussed in Section 2.3, ${AS}_{net}$ is restricted to nets that are indexed by Baire space. Note that we avoid the (explicit) use of one-point extensions in our version of the anti-Specker property ${AS}_{net}$ .

Theorem 3.10.
The system ${RCA}_{0}^{ω}$ proves ${AS}_{net} \to HBU$ .
Proof.
Since sequences are nets, it is straightforward to derive the monotone convergence theorem for sequences from ${AS}_{net}$ , and hence ${ACA}_{0}$ by [98, III.2.2]. Thus, in case $\neg (\exists^{2})$ , we have $HBU$ as the latter reduces to $WKL$ . In case $(\exists^{2})$ , define D and ⪯ as in the proof of Theorem 3.1. Fix $Ψ : I \to R^{+}$ and define the net $x_{w}$ as 2 if $⋃_{i < | w |} I_{w (i)}^{Ψ}$ covers all rationals in $[0, 1]$ , and otherwise use $μ^{2}$ to find some $q \in [0, 1] \cap Q$ not in $⋃_{i < | w |} I_{w (i)}^{Ψ}$ . For any $x \in [0, 1]$ and $w ⪰ ⟨ x ⟩$ , we have $| x - x_{w} | ⩾ min (1, Ψ (x))$ , i.e. $x_{w}$ is eventually bounded away from any point in $[0, 1]$ . By ${AS}_{net}$ , $x_{w}$ is eventually bounded away from $[0, 1]$ , i.e. there is $w_{0} \in D$ such that for $v ⪰ w_{0}$ we have $x_{v} = 2$ . Clearly, this yields a finite sub-cover for the rationals in $[0, 1]$ , which becomes a finite sub-cover for all reals in $[0, 1]$ by including in the former cover all the end-points and associated intervals. □

We could weaken ${AS}_{net}$ to reflect the ‘limited’ anti-Specker property from [23]; we would still obtain $HBU$ as it suffices for the above proof that there is one $w \in D$ such that $x_{w} = 2$ , which is the content of the ‘limited’ anti-Specker property (for sequences). We could also derive ${MCT}_{net}^{0}$ from ${AS}_{net}$ and use Theorem 3.2, but the previous proof is more elegant. An equivalence in Theorem 3.10 seems difficult, in light of the type one quantifiers in the definitions of (net) convergence and related notions. The following corollary does follow in the same way as Corollary 3.3.
Corollary 3.11.
The system $Z_{2}^{Ω}$ proves ${AS}_{net}$ , while $Z_{2}^{ω} + {QF-AC}^{0, 1}$ does not.

In light of the ‘constructive’ status of the anti-Specker property (see Remark 3.2), a more ‘constructive’ proof of ${AS}_{net}$ is desirable.
Theorem 3.12.
The system ${RCA}_{0}^{ω} + IND + {NFP}_{0} + HBU$ proves ${AS}_{net}$ .
Proof.
Let $x_{d} : D \to R$ be a net that is eventually bounded away from I, i.e. $\begin{matrix} (3.4) & (\forall x \in I) (\exists n^{0}) (\exists d \in D) (\forall e ⪰ d) (| x - x_{e} | ⩾ \frac{1}{2^{n}}) . \end{matrix}$ By the definition of $[x] (k)$ the k-th approximation of x, we have $\begin{matrix} (3.5) & (\forall x \in I) (\exists n^{0}) [(\exists d \in D) (\forall e ⪰ d) (| [x] (2^{n + 1}) - x_{e} | ⩾ \frac{1}{2^{n + 1}})] . \end{matrix}$ The formula in square brackets in (3.5) can be written $A (\overline{x} n)$ with only slight abuse of notation. To finish the proof, apply ${NFP}_{0}$ to (3.5) and follow the final part of the proof of Theorem 3.5. □
Corollary 3.13.
The system ${RCA}_{0}^{ω} + IND + {NFP}_{0}$ proves $HBU \leftrightarrow {AS}_{net}$ .

The previous result can be sharpened by introducing ${AS}_{net}^{-}$ , which is ${AS}_{net}$ where the antecedent states the existence of $F : R \to R$ such that $F (x)$ is the number $δ > 0$ as in the first item of Definition 3.9, i.e. F is a ‘bounded away’ modulus.
Theorem 3.14.
The system ${RCA}_{0}^{ω} + IND$ proves $HBU \leftrightarrow {AS}_{net}^{-}$ .
Proof.
The forward direction follows as in the second part of the proof of Theorem 3.5. The reverse direction follows from the proof of Theorem 3.10 by noting that $min (1, Ψ (x))$ is the modulus required by the antecedent of ${AS}_{net}^{-}$ . □

We note that ${AS}_{net}$ is remarkably robust, i.e. we do not know of any reasonable weakening. Similar to item (h) in Section 1.3, there are basic spaces with a sequence that is bounded away from every point, but not from the entire space, i.e. the anti-Specker property for sequences does not capture the topology.

We finish this section with a discussion of the provenance of the anti-Specker property. To fully appreciate the following remark, one requires some basic familiarity with Bishop’s Constructive Analysis [17] and the associated RM-development [53]. Nonetheless, all of the results in this section are part of classical mathematics/logic and can be read without any knowledge of constructive mathematics. Remark 3.2.
The sequential compactness of the unit interval is rejected in constructive mathematics as this property implies some fragment of the law of excluded middle [54]. A more constructive notion of sequential compactness was formulated in [12] by considering the ‘antithesis’ of Specker’s theorem (see [24, p. 58]); the latter theorem provides a recursive counterexample to the monotone convergence theorem. The associated general ‘anti-Specker property’ was later introduced, intuitively expressing that if a sequence is eventually bounded away from any point in a space, then it is eventually bounded away (uniformly) from the entire space. The anti-Specker property (of certain spaces) is equivalent to (certain versions of) Brouwer’s fan theorem, a ‘semi-constructive’ principle accepted in intuitionistic mathematics (see e.g. [10]). The classical contraposition of weak König’s lemma is often referred to as ‘the’ fan theorem (for decidable bars).

3.1.4. Cauchy nets

In this section, we study basic theorems pertaining to Cauchy nets (see e.g. [55, p. 190]), defined as follows for $R$ . It goes without saying that such nets are the generalisation of the notion of Cauchy sequence to directed sets.

Definition 3.15 (Cauchy net).

A net $x_{d} : D \to R$ is Cauchy if $(\forall ε > 0) (\exists d \in D) (\forall e, f ⪰_{D} d) (| x_{e} - x_{f} | < ε)$ .

Our motivation is two-fold: one one hand, the convergence of Cauchy sequences in the unit interval is equivalent to ${ACA}_{0}$ by [98, III.2.2]. One the other hand, ${MCT}_{net}^{0}$ obviously follows from the combination of the following two theorems.

Definition 3.16 ( ${CAU}_{net}$ ).

A Cauchy net in $[0, 1]$ converges to a limit.

Definition 3.17 ( ${CAU}_{net}^{'}$ ).

An increasing net in $[0, 1]$ is a Cauchy net.

It is readily shown that $Z_{2}^{Ω} + {QF-AC}^{0, 1}$ or ${RCA}_{0}^{ω} + IND + {NFP}_{0} + HBU$ proves ${CAU}_{net}$ , while ${RCA}_{0}^{ω} + IND$ proves ${CAU}_{net}^{'}$ . As it turns out, both ‘Cauchy net theorems’ have interesting properties, as follows.

Theorem 3.18.
The system ${RCA}_{0}^{ω} + IND + {CAU}_{net}$ proves $HBU$ .
Proof.
We make use of $(\exists^{2}) \lor \neg (\exists^{2})$ as in the proof of Theorem 3.1. The first part involving $\neg (\exists^{2})$ is identical. For the second part, let the net $x_{w}$ be as in the proof of Theorem 3.2. In case $x_{w}$ is Cauchy, the proof of the latter theorem goes through. In case $x_{w}$ is not Cauchy, there is $k_{0}^{0}$ such that $(\forall d \in D) (\exists e, f ⪰_{D} d) (| x_{e} - x_{f} | ⩾ \frac{1}{2^{k_{0}}})$ . Applying the latter at most $2^{k}$ times, we obtain a finite sub-cover by the definition of $x_{w}$ . For this final step, it seems $IND$ is needed. □

Secondly, by Corollary 3.7, the functional $\exists^{3}$ computes a realiser for the monotone convergence theorem for nets via a term of Gödel’s T, and vice versa. We now obtain similar results for ${CAU}_{net}$ and ${CAU}_{net}^{'}$ . The latter is the most interesting.

Now, a realiser for ${CAU}_{net}^{'}$ takes as input $(D, ⪯_{D}, x_{d})$ and outputs $Φ^{1 \to 1}$ such that $(\forall ε > 0) (\forall e, f ⪰_{D} Φ (ε)) (| x_{e} - x_{f} | < ε)$ if the inputs are as in ${CAU}_{net}^{'}$ .
Corollary 3.19.
A realiser for ${CAU}_{net}^{'}$ together with $\exists^{2}$ , computes $\exists^{3}$ via a term of Gödel’s T.
Proof.
Let D be the set of finite sequences in Baire space and define $w ⪯_{D} v$ for $w, v \in D$ as $(\forall i < | w |) (\exists j < | v |) (w (i) =_{1} v (j))$ using $\exists^{2}$ . Now fix $Y^{2}$ and define the net $x_{w} : D \to I$ as $1 - \frac{1}{2^{| w |}}$ if $(\exists i < | w |) (Y (w (i)) = 0)$ , and 0 otherwise. Clearly, $x_{w}$ is increasing, and let Φ be a modulus of Cauchy-ness. Note that $(\exists f \in Φ (1 / 2)) (Y (f) = 0) \leftrightarrow (\exists g^{1}) (Y (g) = 0)$ , and we are done. □

On a related note, to derive ${BW}_{net}$ from ${CAU}_{net}$ , one requires ${COH}_{net}$ , i.e. the statement any net in the unit interval contains a Cauchy sub-net. The associated property for sequences is equivalent to $COH$ from the RM zoo (see [61]). A realiser for ${COH}_{net}$ clearly computes $\exists^{3}$ by Corollary 3.19. Moreover, in light of the proof of Corollary 3.19, a realiser for ${CAU}_{net}^{'}$ also provides a witness $g^{1}$ such that $Y (g) = 0$ if such exists, i.e. ${QF-AC}^{0, 1}$ is involved, in contrast to Corollaries 3.7 and 3.20.

We now study realisers for ${CAU}_{net}$ , which are tame by comparison (to the above). A realiser for ${CAU}_{net}$ is a functional taking as input $(D, ⪯_{D}, x_{d})$ and outputting the limit $x = {lim}_{d} x_{d}$ if the inputs satisfy the conditions of ${CAU}_{net}$ . Corollary 3.20.
A realiser for ${CAU}_{net}$ together with $\exists^{2}$ computes $\exists^{3}$ via a term of Gödel’s T, and vice versa.
Proof.
For the ‘vice versa’ direction, the limit exists and one uses the usual ‘interval halving technique’ to locate it, where $\exists^{3}$ is used to decide whether there is a limit in the relevant half-interval. For the other direction, let $x_{w}$ be as in the proof of Corollary 3.19. In case $(\forall g^{1}) (Y (g) > 0)$ , $x_{w}$ is always 0 and hence Cauchy. In case there is some $g_{0}^{1}$ such that $Y (g_{0}) = 0$ , $x_{w}$ is also Cauchy, which is seen by considering long enough w containing $g_{0}$ . Clearly, ${lim}_{d} x_{d} = 1 \leftrightarrow (\exists g^{1}) (Y (g) = 0)$ . □

3.1.5. Unordered sums

We discuss unordered sums, the generalisation of sums to possibly uncountable index sets (see e.g. [9, §5.2], [48, Ch. 1, §7]. [55, p. 76], [56, Ch. 0], or [103, §3.3]). Historically, the study of such sums by Moore in [70] was the first step toward the Moore–Smith theory of convergence in [73]. Moreover, unordered sums allow for an alternative formulation of measure theory (see [55, p. 79]).

For $D \subseteq N^{N}$ and any $a_{d} : D \to R$ , we want to provide meaning to ‘the uncountable sum $\sum_{d \in D} a_{d}$ ’. To this end, let $D^{*}$ be the set of finite subsets of elements of D, which is a directed set if $⪯_{D^{*}}$ is inclusion on $D^{*}$ . The net $(\sum_{i \in d} a_{i}) : D^{*} \to R$ then behaves as in the following (most) basic permutation theorem.

Definition 3.21 ( $PERM$ ).

For any $D \subseteq N^{N}$ and any $a_{d} : D \to R$ , if $\begin{matrix} (3.6) & (\forall ε > 0) (\exists d \in D^{*}) (\forall e, f ⪰_{D^{*}} d) (| \sum_{i \in e} a_{i} - \sum_{j \in f} a_{j} | < ε), \end{matrix}$ then the net $(\sum_{i \in d} a_{i}) : D^{*} \to R$ converges to some $a \in R$ .

The above limit $a \in R$ bestows meaning onto ‘the uncountable sum $\sum_{d \in D} a_{d}$ ’. A realiser for $PERM$ takes as input $D \subseteq N^{N}$ and $a_{d} : D \to R$ and outputs the limit $a \in R$ if (3.6) is satisfied. Following the definitions in [98, V.2], a realiser for ${ATR}_{0}$ is any functional that outputs Y as in $H_{θ} (X, Y)$ on input $f^{1}$ such that $θ (n, Z) \equiv (\forall k^{0}) (f (\overline{Z} k, n) = 0)$ and any countable well-ordering X.

Theorem 3.22.
A realiser for $PERM$ computes $\exists^{2}$ and a realiser for ${ATR}_{0}$ via a term of Gödel’s T.
Proof.
First of all, to obtain $\exists^{2}$ , consider $f^{1}$ and define the sequence $a_{n}$ as 1 if n is the least number such that $f (n) = 0$ , and 0 otherwise. Clearly, $a_{n}$ satisfies (3.6) and the limit $a \in R$ is such that $a =_{R} 1 \leftrightarrow (\exists n^{0}) (f (n) = 0)$ .

Secondly, consider [98, V.5.2] which shows that ${ATR}_{0}$ is equivalent to $\begin{matrix} (3.7) & (\forall n^{0}) (\exists at most one X) φ (n, X) \to (\exists Z) (\forall m^{0}) (m \in Z \leftrightarrow (\exists X) φ (m, X)), \end{matrix}$ for any arithmetical φ and over ${RCA}_{0}$ . The proof of [98, V.5.2] yields that a realiser for ${ATR}_{0}$ is readily defined in terms of any functional that outputs Z as in (3.7) on input $f^{1}$ such that $φ (n, X) \equiv (\forall k^{0}) (f (\overline{X} k, n) = 0)$ satisfying the uniqueness in (3.7). Now let D be Cantor space, fix some $n^{0}$ , and define $a_{d} : D \to R$ as 1 if $φ (n, d)$ , and zero otherwise. Clearly, $a_{d}$ satisfies (3.6) and the limit $a \in R$ is such that $a =_{R} 1 \leftrightarrow (\exists d \in D) φ (n, d)$ , if φ satisfies uniqueness as in (3.7). □

3.2. Compactness and nets of functions

In this section, we study theorems pertaining to nets of continuous functions, like Dini’s theorem (Section 3.2.1) and Arzelà’s theorem (Section 3.2.2). It goes without saying that for nets of functions $f_{d} : (D \times [0, 1]) \to R$ , properties of $f_{d} (x)$ like continuity pertain to the variable x, while the net is indexed by $d \in D$ . For instance, an increasing net is as follows.

Definition 3.23 (Increasing net).

A net of functions $f_{d} : (D \times I) \to R$ is increasing if $a ⪯ b$ implies $f_{a} (x) ⩽_{R} f_{b} (x)$ for all $x \in I$ and $a, b \in D$ .

We remind the reader that we restrict ourselves to nets that are indexed by subsets of Baire space.

3.2.1. Dini’s theorem

We study a version of Dini’s theorem for nets, which may be found in many places: [3,8,55,63,73,79,104,105,111].

By Corollary 3.26, the following version of Dini’s theorem for nets is equivalent to $HBU$ . We say that $f_{d} : (D \times I) \to R$ converges uniformly if the net $λ d . f_{d} (x)$ converges, and $d_{0} \in D$ as in Definition 2.6 does not depend on the choice of $x \in I$ .

Definition 3.24 ( ${DIN}_{net}$ ).

For continuous $f_{d} : (D \times I) \to R$ forming an increasing net and converging to continuous $f : I \to R$ , the convergence is uniform.

Theorem 3.25.
The system ${RCA}_{0}^{ω} + {DIN}_{net}$ proves $HBU$ .
Proof.
The ‘classical’ Dini’s theorem (for sequences) is equivalent to $WKL$ by [13, Theorem 21], i.e. we have access to the latter. Now, in case $\neg (\exists^{2})$ , all functions on $R$ are continuous by [59, Prop. 3.12], and $HBU$ reduces to $WKL$ by [58, §4]. We now prove $HBU$ in case $(\exists^{2})$ , which finishes the proof using the law of excluded middle.

Fix some $Ψ : I \to R$ and let D be the set of finite sequences of reals in I and define ‘ $v ⪯ w$ ’ for $w, v \in D$ if $(\forall i < | v |) (\exists j < | w |) (v (i) =_{R} w (j))$ , i.e. as in the proof of Theorem 3.2. Now define $f_{w} : I \to R$ as follows: if $w = ⟨ x ⟩$ for some $x \in I$ , then $f_{w}$ is 0 outside of $I_{x}^{Ψ}$ , while inside the latter, $f_{w} (x)$ is the piecewise linear function that is 1 at x, and 0 in $x \pm Ψ (x)$ . Note that these objects have the required basic properties (of directed set, net, et cetera). Moreover, $f_{w}$ is also increasing (in the sense of nets) and converges to the constant one function (in the sense of nets), as for any $v ⪰ ⟨ x ⟩$ , we have $f_{v} (x) = 1$ . Now apply ${DIN}_{net}$ and conclude that the convergence is uniform. Hence, applying the erstwhile theorem for $ε = 1 / 2$ , there is $w_{0}$ such that for all $x \in I$ , $f_{w_{0}} (x) > 0$ . However, the latter implies that every $x \in I$ is in $⋃_{i < | w_{0} |} I_{w_{0} (i)}^{Ψ}$ , i.e. we found a finite sub-cover, yielding $HBU$ for Ψ. □

Since Dini’s theorem is equivalent to $WKL$ in classical RM, we expect the following result. Using the continuity properties of the functions in the net, one can get by with ${QF-AC}^{0, 1}$ , but the latter axiom does seem essential. Moreover, using the above ‘excluded middle’ trick, one could omit $(\exists^{2})$ .
Corollary 3.26.
The system ${ACA}_{0}^{ω} + {QF-AC}^{1, 1}$ proves $HBU \leftrightarrow {DIN}_{net}$ .
Proof.
We only have to prove the forward direction. As in the usual proof of Dini’s theorem, we may assume that the net $f_{d}$ is decreasing and converges pointwise to the constant zero function. Fix $ε_{0} > 0$ and apply ${QF-AC}^{1, 1}$ to $(\forall z \in I) (\exists d \in D) (0 ⩽ f_{d} (z) < ε_{0})$ , to obtain $Φ^{1 \to 1}$ yielding $d \in D$ from $z \in I$ . Since $λ x . f_{Φ (z)} (x)$ is continuous for any fixed z, $(\exists^{2})$ yields a modulus of continuity g as in the proof of [58, Prop. 4.7], i.e. we have: $\begin{matrix} (3.8) & (\forall ε > 0) (\forall x, y \in I) (| x - y | < g (x, ε, z) \to | f_{Φ (z)} (x) - f_{Φ (z)} (y) | < ε), \end{matrix}$ for all $z \in I$ . Define $Ψ : I \to R^{+}$ as $Ψ (x) : = g (x, ε_{0}, x)$ and note that $(0 ⩽ f_{Φ (x)} (y) < ε_{0})$ for all $y \in I_{x}^{Ψ}$ by (3.8) and the definition of Φ. Now let $y_{1}, \dots, y_{k}$ be the associated finite sub-cover provided by $HBU$ . By item (b) of Definition 2.5, there is $d_{0} \in D$ such that $d_{0} ⪰ Φ (y_{i})$ for all $i ⩽ k$ . Since $f_{d}$ is a decreasing net and $[0, 1] \subset ⋃_{i ⩽ k} I_{y_{i}}^{Ψ}$ , we have $(0 ⩽ f_{d} (y) < ε_{0})$ for all $y \in I$ and $d ⪰ d_{0}$ , i.e. uniform convergence as required. □

A detailed study of the proof of [58, Prop. 4.10] shows that one can avoid the use of $(\exists^{2})$ to obtain the modulus of continuity in the previous proof; indeed, by the aforementioned result, it suffices to have $WKL$ , which follows from $HBU$ . We could weaken the conclusion of Dini’s theorem to convergence in measure or convergence of integrals, and the resulting theorems would be equivalent to weak compactness as in Vitali’s covering theorem; see [85] for details.
3.2.2. Arzelà’s theorem

We show that Arzelà’s theorem for nets (see7

⁷
Note that [30] includes an historical overview pertaining to Arzelà’s theorem (for nets).

e.g. [8,22,30,73]) implies

HBU

. This theorem deals with quasi-uniform convergence, a notion apparently first introduced by Arzelà himself in [4, Def. 2.1].

Definition 3.27 (Quasi-uniform convergence of nets).

A net $f_{d} : (D \times I) \to R$ converges quasi-uniformly to $f : I \to R$ if f is the limit of the net $f_{d}$ and $\begin{matrix} (\forall ε > 0, d \in D) (\exists d_{0}, \dots, d_{k} ⪰ d) (\forall x \in I) (\exists j ⩽ k) (| f_{d_{j}} (x) - f (x) | < ε) . \end{matrix}$

Arzelà’s theorem now has the following generalisation to nets.

Definition 3.28 ( ${ARZ}_{net}$ ).

For continuous $f_{d} : (D \times I) \to R$ forming a net convergent to a continuous $f : I \to R$ , the convergence is quasi-uniform.

Theorem 3.29.
The system ${RCA}_{0}^{ω} + {ARZ}_{net}$ proves $HBU$ .
Proof.
The proof of the theorem is similar to the proof of Theorem 3.25. Indeed, for $f_{w}$ as in the latter, quasi-uniform convergence for $ε = 1 / 2$ and $d = ⟨ 0 ⟩$ , yields $w_{0}, \dots, w_{k} ⪰ ⟨ 0 ⟩$ such that for each $x \in [0, 1]$ , there is $j ⩽ k$ such that $| f_{w_{j}} (x) - f (x) | < 1 / 2$ . As in the proof of Theorem 3.25, this implies that $w_{0} * \dots * w_{k}$ yields a finite sub-cover of the canonical cover associated to Ψ, and we are done. □

The Ascoli–Arzelà theorem for nets (see e.g. [47, p. 247]) similarly implies $HBU$ , since it implies the Bolzano–Weierstrass theorem for nets.

We finish this section with a conceptual remark regarding quasi-convergence. Remark 3.3 (Quasi-convergence and the weak-∗-topology).

Dual spaces and the associated weak-∗-topology are studied in RM (see e.g. [98, X.2]). Moreover, it has been known for more than half a century that quasi-uniform convergence for nets is related to the weak and weak-∗-topologies (see [8,21,22,109]). For instance, quasi-convergence for nets yields an equivalent formulation of the weak-∗-topology for a large class of spaces by [21, Theorem 3.1]. In this light, the study of net convergence, and ${ARZ}_{net}$ in particular, in (higher-order) RM is quite natural.

4. Main results II

As suggested by item h in Section 1.3, sequences do not suffice for describing topologies in general, and nets are needed instead. Intuitively speaking, we show in this section that even for spaces like $R$ where sequences do suffice to describe the topology (say working in $ZFC$ ), the absence of countable choice (say over ${RCA}_{0}^{ω}$ ) implies that sequences no longer suffice to describe the topology, but nets do suffice.

On a historical note, Root, a student of E.H. Moore, already studied when limits from Moore’s General Analysis [71] can be replaced by limits given by sequences [89]. Thus, the idea of replacing nets by sequences goes back more than a century.

4.1. Introduction

Nets are generalisations of sequences, and it is therefore a natural question ‘how hard’ it is to replace the former by the latter. In Section 4.2, we study such an ‘sequentialisation’ principle, called $SUB$ , from Bourbaki’s general topology [20]; we show that despite its highly elementary nature, $SUB$ implies the Lindelöf lemma for $R$ , a close relative of $HBU$ . We also show that ${SUB}_{0}$ , a special case of $SUB$ , is equivalent to ${QF-AC}^{0, 1}$ , assuming (natural) extra axioms. Thus, in the absence of countable choice, nets are more general than sequences in terms of convergence on $R$ . In general, it should be noted that such sequentialisation theorems are only valid/possible for first-countable spaces.

Inspired by the previous paragraph, it is a natural question whether ‘upgrading’ sequential continuity with nets has any noteworthy effects. In Section 4.3, we prove the local equivalence of the resulting ‘net-continuity’ and ‘epsilon-delta’ continuity in ${RCA}_{0}^{ω}$ . Note that the local equivalence between sequential continuity and epsilon-delta continuity cannot be proved in $ZF$ [36], while ${QF-AC}^{0, 1}$ suffices [58,59].

Similarly, we show in Section 4.4 that $R$ is a sequential space, i.e. that ‘sequentially closed’ sub-sets of $R$ are closed, over ${RCA}_{0}^{ω} + {QF-AC}^{0, 1}$ ; this result cannot be proved in $ZF$ by [50, p. 73], i.e. ${QF-AC}^{0, 1}$ is essential, as in the case of sequential continuity. By contrast, we also prove that the generalisation from sequences to nets does not require the Axiom of Choice: ‘net-closed’ sets are closed over ${RCA}_{0}^{ω}$ .

We stress that the previous is not merely spielerei: the definition of closed sets in [45] and the definition of continuity in [45,47] are given in terms of nets. In other words, nets are central to domain theory and are used to define the notions of closed set and continuous function. Moreover, our results show that using nets instead of sequence obviates the need for the Axiom of Choice, a foundational concern in domain theory by the quotes from Section 1.1. We remind the reader that we restrict ourselves to nets indexed by Baire space.

4.2. Nets and sequentialisation

By the above, basic theorems regarding nets imply $HBU$ and therefore require rather strong comprehension axioms for a proof. In line with the coding practise of RM, one may therefore want to replace limits involving nets by ‘countable’ limits, i.e. if a net converges to some limit, then there should be a sequence in the net that also converges to the same limit. In this section, we show that such ‘sequentialisation’ theorems imply ${QF-AC}^{0, 1}$ (Theorem 4.5) and the Lindelöf lemma (Theorem 4.3), and obtain a nice spin-off result (Theorem 4.8) regarding the RM zoo [33]. In general, it should be noted that such sequentialisation theorems are only valid/possible for first-countable spaces.

First of all, we show that even an highly elementary version of the aforementioned sequentialisation theorem implies the Lindelöf lemma for $R$ from [84], as follows.

Definition 4.1 ( $LIN$ ).

For every $Ψ : R \to R^{+}$ , there is a sequence of open intervals $⋃_{n \in N} (a_{n}, b_{n})$ covering $R$ such that $(\forall n \in N) (\exists x \in R) [(a_{n}, b_{n}) = I_{x}^{Ψ}]$ .

Lindelöf proved the Lindelöf lemma in 1903 [65], while Young and Riesz proved a similar theorem in 1902 and 1905 [88,112]; $LIN$ expresses that an open cover of $R$ has a countable sub-cover, and is very close to Lindelöf’s original lemma.8

⁸
Lindelöf formulates his lemma in [65, p. 698] as follows: Let P be any set in $R^{n}$ and construct for every point of P a sphere $S_{P}$ with x as center and radius $ρ_{P}$ , where the latter can vary from point to point; there exists a countable infinity $P^{'}$ of such spheres such that every point in P is interior to at least one sphere in $P^{'}$ .

By [84, Theorem 3.13], $HBU$ is equivalent to $[LIN + WKL]$ , i.e. $LIN$ is extremely hard to prove, while a connection between $LIN$ and some theorem about nets is expected by the previous. In particular, $SUB$ fulfils that role by Theorem 4.3.

Definition 4.2 (SUB).

For $f_{d} : (D \times I) \to R$ an increasing net of continuous functions converging to continuous $f = {lim}_{d} f_{d}$ , there is $Φ : N \to D$ such that $f_{Φ (n)}$ is increasing (in the variable n) and ${lim}_{n \to \infty} f_{Φ (n)} = f$ .

Note $SUB$ ’s narrow scope, i.e. it only seems to apply to ${DIN}_{net}$ and ${MCT}_{net}$ . Nonetheless, $SUB$ occurs in Bourbaki’s general topology, namely [20, p. 337].

Theorem 4.3.
The system ${RCA}_{0}^{ω} + SUB$ proves $LIN$ .
Proof.
In case $\neg (\exists^{2})$ , all functions on $R$ are continuous by [59, Prop. 3.12]. The countable sub-cover required for $LIN$ is then given by $Q$ . In case $(\exists^{2})$ , suppose $\neg LIN$ and let $Ψ : R \to R^{+}$ be such that the associated canonical cover does not have a countable sub-cover. We let D be the set of sequences of real numbers and we define the relation between such sequences ‘ $λ n . x_{n} ⪯ λ n . y_{n}$ ’ as $\begin{matrix} (4.1) & (\forall n \in N) (\exists m \in N) (x_{n} =_{R} y_{m}) \end{matrix}$ Clearly, this relation yields a directed set. Now define $f_{w} : I \to R$ as follows: If $w = ⟨ x ⟩$ for some $x \in I$ , then $f_{w}$ is 0 outside of $I_{x}^{Ψ}$ , while inside the latter, $f_{w} (x)$ is the piecewise linear function that is 1 at x, and 0 in $x \pm Ψ (x)$ . If w is a sequence, then $f_{w} (x) = {sup}_{n \in N} f_{⟨ w (n) ⟩} (x)$ . Clearly, $f_{w}$ is increasing (in the sense of nets) and converges to the constant one function (in the sense of nets), as for any $v ⪰ (x, x, x, \dots)$ , we have $f_{v} (x) = 1$ . Now let $Φ^{0 \to 1}$ be as in $SUB$ and create a ‘master sequence’ of reals $λ n . z_{n}$ containing the sequences $Φ (1)$ , $Φ (2)$ , $Φ (3)$ et cetera. By $SUB$ , for any $x \in R$ , there is $n_{0}$ such that $| f_{Φ (n_{0})} (x) - 1 | < \frac{1}{2}$ , i.e. there is $m \in N$ such that $x \in I_{Φ (n_{0}) (m_{0})}^{Ψ}$ . Since the real $Φ (n_{0}) (m_{0})$ is part of the master sequence $z_{n}$ , we obtain $LIN$ . □

It is possible to obtain an equivalence in the previous theorem by considering the more general ‘Borel–Schoenflies’ version of $LIN$ from [81, §5.3] and ${QF-AC}^{0, 1}$ for real quantifiers. The proofs are however similar, so we do not go into details. We do prove the equivalence between ${QF-AC}^{0, 1}$ and a special case of $SUB$ as follows.
Definition 4.4 ( ${SUB}_{0}$ ).

For $x_{d} : D \to I$ an increasing net converging to $x \in I$ , there is $Φ : N \to D$ such that $λ n . x_{Φ (n)}$ is increasing and ${lim}_{n \to \infty} x_{Φ (n)} =_{R} x$ .

Recall that $IND$ is the induction schema for all formulas of $L_{ω}$ .

Theorem 4.5.
The system ${RCA}_{0}^{ω} + IND$ proves ${SUB}_{0} \to {QF-AC}^{0, 1}$ .
Proof.
In case $\neg (\exists^{2})$ , all functions on Baire space are continuous by [59, Prop. 3.7], and ${QF-AC}^{0, 1}$ clearly reduces to ${QF-AC}^{0, 0}$ , included in ${RCA}_{0}^{ω}$ . For the case $(\exists^{2})$ , note that we also have $(μ^{2})$ . Let $𝕓^{1 \to 1^{}}$ be the inverse of a pairing function defined as $| 𝕓 (f) | = f (0) + 1$ and $𝕓 (f) (i)$ for $i < | 𝕓 (f) |$ is the sequence $f (1 + i), f (1 + i + | 𝕓 (f) |), f (1 + i + 2 | 𝕓 (f) |), \dots$ , which is definable in ${RCA}_{0}^{ω}$ . Fix some $F^{(0 \times 1) \to 0}$ satisfying the antecedent of ${QF-AC}^{0, 1}$ , i.e. $(\forall n^{0}) (\exists f^{1}) (F (n, f) = 0)$ , and use $IND$ to prove $(\forall n^{0}) (\exists f^{1}) \underline{(\forall i ⩽ n) (F (i, 𝕓 (⟨ n ⟩ f) (i)) = 0)}$ . The underlined formula is also written ‘ $G (n, f) = 0$ ’ and if there is $f_{0}^{1}$ such that $(\forall n^{0}) (G (n, f_{0}) = 0)$ , then $Y (n) : = 𝕓 (⟨ n ⟩ * f_{0}) (n)$ is as required for the consequent of ${QF-AC}^{0, 1}$ .

Otherwise, i.e. in case $(\forall f^{1}) (\exists n^{0}) (G (n, f) \neq 0)$ , define the set $D : = {f^{1} : (\exists n^{0}) G (n, f) = 0}$ and define the predicate ‘⪯’ as: $f ⪯ g$ if and only if $\begin{matrix} (4.2) & (μ n) (G (n, f) \neq 0) ⩽ (μ m) (G (m, g) \neq 0), \end{matrix}$ which is well-defined by assumption. Note that D with ⪯ forms a directed set by assumption. Define the increasing net $x_{d} : = 1 - 2^{- (μ n) (G (n, d) \neq 0)}$ and note that ${lim}_{d} x_{d} = 1$ by assumption and (4.2). By ${SUB}_{0}$ , there is some $Φ^{0 \to 1}$ such that ${lim}_{n \to \infty} x_{Φ (n)} = 1$ , i.e. $(\forall ε > 0) (\exists m^{0}) (\forall k^{0} ⩾ m) (| x_{Φ (k)} - 1 | < ε)$ , and use $μ^{2}$ to find $Ψ^{2}$ computing such $m^{0}$ from ε. Then the functional $Y (n) : = Φ (Ψ (\frac{1}{2^{n + 1}}))$ provides the witness as required for the conclusion of ${QF-AC}^{0, 1}$ . □

Let $ADS$ be the $L_{2}$ -sentence from the RM zoo (see [51, Def. 9.1]) that every infinite linear order has an infinite ascending or descending sequence.
Corollary 4.6.
The system ${RCA}_{0}^{ω} + IND + ADS$ proves ${SUB}_{0} \leftrightarrow {QF-AC}^{0, 1}$ .
Proof.
We only need to prove the reverse implication. To this end, let $x_{d} : D \to I$ be an increasing net converging to some $x \in I$ . This convergence trivially implies: $\begin{matrix} (4.3) & (\forall k \in N) (\exists d \in D) (| x - x_{d} | < \frac{1}{2^{k}}), \end{matrix}$ and applying ${QF-AC}^{0, 1}$ to (4.3) yields $Φ : N \to D$ such that the sequence $λ k^{0} . x_{Φ (k)}$ also converges to x as $k \to \infty$ . Since $ADS$ is equivalent to the statement that every sequence in $R$ has a monotone sub-sequence (see [62, §3]), ${SUB}_{0}$ now follows. □

As is clear from the previous two proofs, it is straightforward to omit the two occurrences of ‘increasing’ in ${SUB}_{0}$ . It is a natural RM-question, posed previously by Hirschfeldt (see [67, §6.1]), whether the extra axioms are needed in the base theory of Corollary 4.6.

Finally, inspired by the proof of Theorem 4.5, we show that $ADS$ generalised to uncountable linear orders9
⁹
The prototypical uncountable linear order is given by $(R, ⩽_{R})$ , where ‘ $x =_{R} y$ ’ is equivalent to $x ⩽_{R} y \land y ⩽_{R} x$ (see [98, II.4]). Hence, we implicitly assume that an uncountable linear order $(D, ⩽_{D})$ has an equality relation $x =_{D} y$ equivalent to $x ⩽_{D} y \land y ⩽_{D} x$ .

is not provable in $ZF$ . We restrict ourselves as in Definition 2.4, i.e. a linear order $(D, ⩽_{D})$ is given by a subset D of Baire space with a binary relation $⩽_{D}$ thereon, satisfying the usual properties.
Definition 4.7 ( ${ADS}_{2}$ ).

For $(D, ⩽_{D})$ an infinite linear order, there is an ascending or descending sequence $x_{n}$ , i.e. $(\forall n \in N) (x_{n} <_{D} x_{n + 1}) \lor (\forall n \in N) (x_{n} >_{D} x_{n + 1})$ .

Theorem 4.8.
The system ${RCA}_{0}^{ω} + IND + {ADS}_{2}$ proves ${QF-AC}^{0, 1}$ .
Proof.
In case $\neg (\exists^{2})$ , all functions on Baire space are continuous by [59, Prop. 3.7], and ${QF-AC}^{0, 1}$ clearly reduces to ${QF-AC}^{0, 0}$ , included in ${RCA}_{0}^{ω}$ . For the case $(\exists^{2})$ , note that we also have $(μ^{2})$ . Let $𝕓^{1 \to 1^{}}$ be as in the proof of Theorem 4.5. Fix some $F^{(0 \times 1) \to 0}$ satisfying the antecedent of ${QF-AC}^{0, 1}$ , i.e. $(\forall n^{0}) (\exists f^{1}) (F (n, f) = 0)$ , and use $IND$ to prove $(\forall n^{0}) (\exists f^{1}) \underline{(\forall i ⩽ n) (F (i, 𝕓 (⟨ n ⟩ f) (i)) = 0)}$ . The underlined formula is also written ‘ $G (n, f) = 0$ ’ and if there is $f_{0}^{1}$ such that $(\forall n^{0}) (G (n, f_{0}) = 0)$ , then $Y (n) : = 𝕓 (⟨ n ⟩ * f_{0}) (n)$ is as required for the consequent of ${QF-AC}^{0, 1}$ .

In case $(\forall f^{1}) (\exists n^{0}) (G (n, f) \neq 0)$ , an equality on $D = N^{N}$ is as follows: ‘ $f =_{D} g$ ’ is $(μ n) (G (n, f) \neq 0) =_{0} (μ m) (G (m, g) \neq 0)$ . Now define the order ‘ $f ⩽_{D} g$ ’ as $(μ n) (G (n, f) \neq 0) ⩽_{0} (μ m) (G (m, g) \neq 0)$ . Clearly, $(D, ⩽_{D})$ is a linear order and applying ${ADS}_{2}$ , there is an ascending sequence $x_{n}$ in D, i.e. $x_{n} <_{D} x_{n + 1}$ for all $n \in N$ . Since $(μ m) G (m, x_{n + 1}) ⩾ n + 2$ , we have $G (n, x_{n + 1}) = 0$ , as required. □
Corollary 4.9.
The system $ZF$ cannot prove ${ADS}_{2}$ .

In conclusion, we note that the power of ${ADS}_{2}$ seems to stem from the ordering relation $⩽_{D}$ : the latter is a true third-order object, as is clear from the proof. Moreover, if one demands that the relation ‘ $f ⩽_{D} g$ ’ is given by $φ (f, g)$ for some $φ \in L_{2}$ (and the same for ‘ $f \in D$ ’), the associated restriction of ${ADS}_{2}$ is of course provable using some fragment of dependent choice in $Z_{2}$ [98, VII.6.1].
4.3. Nets and continuity

We establish that ‘net-continuity’ as in Definition 4.10 and ‘epsilon-delta’ continuity are locally equivalent over ${RCA}_{0}^{ω}$ . As discussed in [59, Rem. 3.13], $ZF$ cannot prove the local10

¹⁰
By [59, Prop. 3.6], ${RCA}_{0}^{ω}$ can prove the global equivalence of sequential continuity and epsilon-delta continuity on $N^{N}$ , i.e. when those continuity properties hold everywhere on the latter.

equivalence of sequential and epsilon-delta continuity [36], while

{QF-AC}^{0, 1}

suffices to establish the general case.

Definition 4.10 (Net-continuity).

A function $f : R \to R$ is net-continuous at $x \in R$ if for any net $x_{d}$ in $R$ converging to x, the net $f (x_{d})$ also converges to $f (x)$ .

Note that net-continuity is equivalent to the topological definition of continuity by [7, Example 2.7]. As it happens, the definition of continuity in [45, p. 45] is the definition of net-continuity. It should be noted that Scott continuity is a much more important/central notion than net-continuity in domain theory.

Theorem 4.11 ( ${RCA}_{0}^{ω}$ ).

For any $f : R \to R$ and $x \in R$ , the following are equivalent:

the function $f : R \to R$ is net-continuous at x,

$(\forall ε > 0) (\exists δ > 0) (\forall y \in R) (| x - y | < δ \to | f (x) - f (y) | < ε)$ .

Proof.
The implication $(b) \to (a)$ is immediate. For the remaining implication, note that in case of $\neg (\exists^{2})$ , all $f : R \to R$ are continuous by [59, Prop. 3.12]. In case $(\exists^{2})$ , fix $x \in R$ , $f : R \to R$ and suppose f is net-continuous at x, but not epsilon-delta continuous at x, i.e. there is $ε_{0} > 0$ such that $\begin{matrix} (4.4) & (\forall k \in N) (\exists y \in R) (| x - y | <_{R} \frac{1}{2^{k}} \land | f (x) - f (y) | ⩾_{R} ε_{0}) . \end{matrix}$ Using $(\exists^{2})$ , let D be the set of all $y \in R$ such that $| f (x) - f (y) | ⩾_{R} ε_{0}$ and define ‘ $y_{1} ⪯ y_{2}$ ’ for $y_{1}, y_{2} \in D$ by $| x - y_{1} | ⩾_{R} | x - y_{2} |$ . Clearly, the relation ⪯ yields a directed set. Now define a net $x_{d} : D \to R$ by $x_{d} : = d$ and note that $x_{d}$ converges to x by (4.4). By the net-continuity of f, $f (x_{d})$ then converges to $f (x)$ , which yields a clear contradiction. □

The previous proof highlights a conceptual advantage of nets compared to sequences: to define a sequence $λ n^{0} . x_{n}$ , one has to list the members one by one. In this light, to get a sequence from (4.4), ${QF-AC}^{0, 1}$ seems unavoidable. By contrast, to define a net $x_{d}$ , one only needs to satisfy Definition 2.5, i.e. show that there always exist ‘bigger’ (in the sense of ⪯) elements in the net without listing them.

Now, a modulus-of-continuity functional computes a modulus of continuity for functionals in a certain class. Various results exist on the minimal complexity of the former (see e.g. [10,35,106]). Theorem 4.11 implies that a modulus-of-net-continuity functional is readily computed from a modulus-of-continuity functional (in ${RCA}_{0}^{ω}$ ). The former takes as input f and a modulus of convergence for ${lim}_{d} x_{d} = x$ (and also $x_{d}$ and x), and outputs a modulus of convergence for ${lim}_{d} f (x_{d}) = f (x)$ .

The following corollary is similar to Theorem 4.3, as the ‘strong’ version of the Lindelöf lemma implies ${QF-AC}^{0, 1}$ by [81, §5].
Corollary 4.12.
The system $ZF$ cannot prove the local equivalence between net-continuity and sequential continuity on $R$ .

In conclusion, nets have the advantage that the associated notion of net-continuity is locally equivalent to the usual epsilon-delta definition without the use of the Axiom of Choice as in ${QF-AC}^{0, 1}$ .
4.4. Nets and closed sets

The results in the previous section are not the only example of nets obviating the need for the Axiom of Choice. Indeed, we discuss another example involving closed sets, and the notion of ‘sequential space’ in particular. These results are of historical interest, as Engelking writes in [34, p. 55]:

Sequential spaces and Fréchet spaces belonged to the folklore almost since the origin of general topology, […]

We now introduce our notion of open and closed set in Definition 4.13. As to compatibility with classical RM, note that if

Y : R \to R

is continuous, it represents an open set for which ‘

x \in Y

’ has the same complexity (with parameters) as a code for an open set in RM (see [98, II.5.6]). Also note that the notion ‘sequentially closed’ is similar to that of ‘separably closed’ (see e.g. [46]).

Definition 4.13 (Open and closed sets).

We let $Y : R \to R$ represent subsets of $R$ by writing ‘ $x \in Y$ ’ for ‘ $| Y (x) | >_{R} 0$ ’.

We call Y ‘open’ if for $x \in Y$ , there is an open ball $B (x, r) \subset Y$ with $r^{0} > 0$ .

We define ‘ $Y^{c}$ ’ as the complement of Y, i.e. $x \in Y^{c} \leftrightarrow \neg (x \in Y)$ .

We call a set F ‘closed’ if its complement $F^{c}$ is open.

We call a set F ‘sequentially closed’ if for any sequence $x_{n}$ and x in $R$ , we have $[(\forall n \in N) (x_{n} \in F) \land {lim}_{n \to \infty} x_{n} = x] \to x \in F$ .

A space is sequential if ‘sequentially closed’ and ‘closed’ coincide for subsets.

Trivially, a closed set in $R$ is sequentially closed, but the reverse direction cannot be proved in $ZF$ by [50, p. 73]. We prove that ${QF-AC}^{0, 1}$ suffices over ${RCA}_{0}^{ω}$ .

Theorem 4.14.
The system ${RCA}_{0}^{ω} + {QF-AC}^{0, 1}$ proves that $R$ is a sequential space.
Proof.
We prove the theorem in case $(\exists^{2})$ and in case $\neg (\exists^{2})$ , and let the law of excluded middle finish the proof. For the first case, let Y be a sequentially closed sub-set of $R$ and suppose that Y is not closed, i.e. there is $x \in Y^{c}$ such that $\begin{matrix} (4.5) & (\forall n \in N) (\exists y \in R) [| x - y | < \frac{1}{2^{n}} \land y \notin Y^{c}] . \end{matrix}$ The formula in square brackets is arithmetical, and ${QF-AC}^{0, 1}$ and $(\exists^{2})$ yield a sequence $y_{n}^{0 \to 1}$ in $[0, 1]$ such that $(\forall n \in N) (| x - y_{n} | < \frac{1}{2^{n}} \land y_{n} \in Y)$ . Clearly, $y_{n}$ converges to x, implying that $x \in Y$ , a contradiction. In case $\neg (\exists)$ , all $R \to R$ -functions are continuous by [59, Prop. 3.7]. Hence, (4.5) immediately implies: $\begin{matrix} (\forall n \in N) (\exists q \in [0, 1] \cap Q) [| x - q | < \frac{1}{2^{n}} \land q \in Y], \end{matrix}$ and ${QF-AC}^{0, 0}$ now provides the required sequence in Y as in the previous case. □

We call a set F ‘net-closed’ if for any net $x_{d} : D \to R$ and $x \in R$ , we have that: $\begin{matrix} (4.6) & [(\forall d \in D) (x_{d} \in F) \land {lim}_{d} x_{d} = x] \to x \in F . \end{matrix}$ Note that the definition of closed set in domain theory [45, p. 45] is that of net-closed. It should be noted that Scott open/Scott closed is a much more important/central notion than net-open/net-closed in domain theory. As in Section 4.3, the upgrade to nets obviates the need for ${QF-AC}^{0, 1}$ .
Theorem 4.15.
The system ${RCA}_{0}^{ω}$ proves that any net-closed set in $R$ is closed.
Proof.
We prove the theorem in case $(\exists^{2})$ and in case $\neg (\exists^{2})$ , and let the law of excluded middle finish the proof. In case $(\exists^{2})$ , fix $F : R \to R$ and suppose F is net-closed and not closed, i.e. there is $x \in F^{c}$ such that $\begin{matrix} (4.7) & (\forall k \in N) (\exists y \in R) (| x - y | <_{R} \frac{1}{2^{k}} \land y \notin F^{c}) . \end{matrix}$ Using $(\exists^{2})$ , let D be the set of all $y \in R$ such that $y \in F$ (which is exactly ‘ $y \notin F^{c}$ ’) and define ‘ $y_{1} ⪯ y_{2}$ ’ for $y_{1}, y_{2} \in D$ by $| x - y_{1} | ⩾_{R} | x - y_{2} |$ . Clearly, the relation ⪯ yields a directed set. Now define a net $x_{d} : D \to R$ by $x_{d} : = d$ and note that $x_{d}$ converges to x by (4.7). By (4.6) and $(\forall d \in D) (x_{d} \in D)$ , we have $x \in F$ , a contradiction. Hence, F is closed and this case is finished. The remaining case is treated as in the proof of Theorem 4.6, i.e. using ${QF-AC}^{0, 0}$ . □

Intuitively, a space is sequential if the topology can be described using sequences only, i.e. nets are not needed (see [34, p. 53]). Since all first-countable spaces are sequential [34, 1.6.14], the latter property is fairly weak. It is therefore somewhat ironic that ${QF-AC}^{0, 1}$ is required to prove that $R$ is sequential, while the base theory can establish this result for sequences replaced by nets. Due to the classical equivalence, the same holds for the anti-Specker property from Section 3.1.3.

Finally, other results can be obtained in the same way: on one hand, ${QF-AC}^{0, 1}$ is needed to show that every accumulation point of a set in $R$ has a sequence converging to that point [50, p. 73]. On the other hand, ${RCA}_{0}^{ω}$ can prove that every accumulation point of a set in $R$ has a net converging to that point.
4.5. Nets and sub-continuity

As suggested by its name, sub-continuity is a notion of continuity (based on nets) that is strictly weaker than continuity. Sub-continuity was introduced in [40] as in Definition 4.16 below. Now, in [81, §4.2], it is shown that sub-continuity involving sequences, as found in e.g. [80], implies local boundedness using ${QF-AC}^{0, 1}$ . We believe the use of countable choice to be necessary in the case of sequences; we show in Theorem 4.17 that sub-continuity formulated with nets implies local boundedness over ${RCA}_{0}^{ω}$ .

Definition 4.16 (Sub-continuity).

A function $f : R \to R$ is sub-continuous if for any net $x_{d} : D \to I$ convergent to $x \in R$ , $f (x_{d})$ has a convergent sub-net.

Note that ${lim}_{d} f (x_{d})$ need not be $f (x)$ in the previous definition. Recall that a function is locally bounded if for every point there is a neighbourhood in which the functions is bounded.

Theorem 4.17.

The system ${RCA}_{0}^{ω}$ proves that a function $f : R \to R$ is locally bounded if it is sub-continuous.

Proof.

We establish the theorem in ${RCA}_{0}^{ω}$ in two steps: first we prove it assuming $(\exists^{2})$ and then prove it again assuming $\neg (\exists^{2})$ . The law of excluded middle as in $(\exists^{2}) \lor \neg (\exists^{2})$ then yields the theorem. Hence, assume $(\exists^{2})$ and suppose $f : R \to R$ is sub-continuous on I but not locally bounded. The latter assumption implies that there is $y_{0} \in R$ such that $\begin{matrix} (4.8) & (\forall n^{0}) (\exists x \in R) (| x - y_{0} | <_{R} \frac{1}{n + 1} \land | f (x) | >_{R} n) . \end{matrix}$ Using $(\exists^{2})$ , let D be the set of all pairs $x \in R$ and $n \in N$ such that $0 < | x - y_{0} | <_{R} \frac{1}{n + 1} \land | f (x) | >_{R} n$ . Also define ‘ $(y_{1}, n_{1}) ⪯_{D} (y_{2}, n_{2})$ ’ by $n_{1} ⩽_{0} n_{2}$ for elements of D. Clearly, the relation $⪯_{D}$ yields a directed set. Now define a net $x_{d} : D \to R$ by $x_{d} : = y$ if $d = (y, n)$ and note that ${lim}_{d} x_{d} = y_{0}$ by (4.8). Hence the net $f (x_{d})$ has a convergent sub-net by sub-continuity, which is impossible as $f (x_{d})$ grows arbitrarily large by definition: $| f (x_{d}) | > n$ if $d = (y, n)$ in particular.

Finally, in case that $\neg (\exists^{2})$ , any function $f : R \to R$ is everywhere sequentially continuous and everywhere ε-δ-continuous by [59, Prop. 3.12]. Hence, any $f : R \to R$ is also sub-continuous on I and locally bounded on I, and the implication from the theorem is then trivially true. □

Footnotes

Acknowledgements

Our research was supported by the John Templeton Foundation via the grant a new dawn of intuitionism with ID 60842. We express our gratitude towards this institution. We thank Dag Normann, Thomas Streicher, and Anil Nerode for their valuable advice. Opinions expressed in this paper do not necessarily reflect those of the John Templeton Foundation.

General index sets

Nets and the Gödel hierarchy

We discuss the foundational implications of our results, esp. as they pertain to the Gödel hierarchy. Now, the latter is a collection of logical systems ordered via consistency strength. This hierarchy is claimed to capture most systems that are natural or have foundational import, as follows.

It is striking that a great many foundational theories are linearly ordered by <. Of course it is possible to construct pairs of artificial theories which are incomparable under <. However, this is not the case for the “natural” or non-artificial theories which are usually regarded as significant in the foundations of mathematics. [99]

Burgess and Koellner corroborate this claim in [28, §1.5] and [57, §1.1]. The Gödel hierarchy is a central object of study in mathematical logic, as e.g. argued by Simpson in [99, p. 112] or Burgess in [28, p. 40]. Precursors to the Gödel hierarchy may be found in the work of Wang [110] and Bernays (see [11,14]). Friedman [39] studies the linear nature of the Gödel hierarchy in detail. Moreover, the Gödel hierarchy exhibits some remarkable robustness: we can perform the following modifications and the hierarchy remains largely unchanged:

Instead of the consistency strength ordering, we can order via inclusion: Simpson claims that inclusion and consistency strength yield the same11

¹¹

Simpson mentions in [99] the caveat that e.g. $PRA$ and ${WKL}_{0}$ have the same first-order strength, but the latter is strictly stronger than the former.

Gödel hierarchy as depicted in [99, Table 1]. Some exceptional (semi-natural) statements12

¹²

There are some examples (predating $HBU$ and [84]) that fall outside of the Gödel hierarchy based on inclusion, like special cases of Ramsey’s theorem and the axiom of determinacy from set theory [51,68]. These are far less natural than e.g. Heine–Borel compactness, in our opinion.

do fall outside of the inclusion-based Gödel hierarchy.

We can replace the systems with their higher-order (eponymous but for the ‘ω’) counterparts. The higher-order systems are generally conservative over their second-order counterpart for (large parts of) $L_{2}$ . Hunter’s dissertation contains a number of such general results [52, Ch. 2].

Now, if one accepts the modifications (inclusion ordering and higher types) described in the previous two items, then an obvious question is where e.g.

HBU

fits into the (inclusion-based) Gödel hierarchy. Indeed, the Heine–Borel theorem has a central place in analysis and a rich history predating set theory (see [66]).

The answer to this question may come as a surprise: starting with the results in [81,84,85], Dag Normann and the author have identified a large number of natural theorems of third-order arithmetic, including $HBU$ , forming a branch independent of the medium range of the Gödel hierarchy based on inclusion. Indeed, none of the systems $Π_{k}^{1} {- CA}_{0}^{ω} + {QF-AC}^{0, 1}$ can prove $HBU$ , while $Z_{2}^{Ω}$ can. We stress that both $Π_{k}^{1} {- CA}_{0}^{ω} + {QF-AC}^{0, 1}$ and $HBU$ are part of the language of third-order arithmetic, i.e. expressible in the same language.

In more detail, results pertaining to ‘local-global’ theorems are obtained in [81]. Measure theory is studied in [85], while results pertaining to $HBU$ and the gauge integral may be found in [84]. In this paper and [85,93,94], we have shown that a number of basic theorems about nets similarly fall outside of the Gödel hierarchy including the monotone convergence theorem for nets of continuous functions and the Riemann integral ( ${MCT}_{net}$ ; see [85]).

We recall that convergence theorems concerning nets are old and well-established, starting with Moore, Smith, and Vietoris more than a century ago [71,73,108]. Our results highlight a fundamental difference between second-order and higher-order arithmetic. Such differences are discussed in detail in [92, §4], based on helpful discussion with Steve Simpson, Denis Hirschfeldt, and Anil Nerode. The associated results concerning nets are summarised in Fig. 1 below.

We first discuss some the technical details concerning Fig. 1.

In conclusion, in light of the results in this paper and [81,84,85,93,94], we observe a serious challenge to the linear nature of the Gödel hierarchy (with a caveat provided by the above items (i) and (ii)), as well as Feferman’s claim that the mathematics necessary for the development of physics can be formalised in relatively weak logical systems (see e.g. [84, p. 24]).

References

Abramsky and

Jung , Domain theory, in: Handbook of Logic in Computer Science, Vol. 3, Handb. Log. Comput. Sci., Vol. 3, Oxford Univ. Press, 1994, pp. 1–168.

Alaoglu , Weak topologies of normed linear spaces, Ann. of Math. (2) 41 (1940), 252–267. doi:10.2307/1968829.

C.D.

Aliprantis and

K.C.

Border , Infinite Dimensional Analysis, 3rd edn, Springer, Berlin, 2006, A hitchhiker’s guide.

Arzelà , Intorno alia continuitd delta somma d’infinitd di funzioni continue, Rend. dell’Accad. di Bologna (1883–1884), 79–84.

Avigad , The metamathematics of ergodic theory, Ann. Pure Appl. Logic 157(2–3) (2009), 64–76. doi:10.1016/j.apal.2008.09.001.

Avigad and

Feferman , Gödel’s functional (“Dialectica”) interpretation, in: Handbook of Proof Theory, Stud. Logic Found. Math., Vol. 137, 1998, pp. 337–405.

R.G.

Bartle , Nets and filters in topology, Amer. Math. Monthly 62 (1955), 551–557. doi:10.1080/00029890.1955.11988688.

R.G.

Bartle , On compactness in functional analysis, Trans. Amer. Math. Soc. 79 (1955), 35–57. doi:10.1090/S0002-9947-1955-0073938-2.

A.F.

Beardon , Limits, Undergraduate Texts in Mathematics, Springer-Verlag, New York, 1997, A new approach to real analysis.

10.

M.J.

Beeson , Foundations of Constructive Mathematics, Ergebnisse der Mathematik und Ihrer Grenzgebiete, Vol. 6, Springer, 1985, Metamathematical studies.

11.

Benacerraf and

Putnam , Philosophy of Mathematics: Selected Readings, 2nd edn, Cambridge University Press, 1984.

12.

Berger and

Bridges , A fan-theoretic equivalent of the antithesis of Specker’s theorem, Indag. Math. (N.S.) 18(2) (2007), 195–202. doi:10.1016/S0019-3577(07)00012-2.

13.

Berger and

Schuster , Dini’s theorem in the light of reverse mathematics, in: Logicism, Intuitionism, and Formalism, Synth. Libr., Vol. 341, Springer, 2009, pp. 153–166.

14.

Bernays , Sur le Platonisme Dans les Mathématiques, L’Enseignement Mathématique 34 (1935), 52–69.

15.

Birkhoff , Abstract 355: A new definition of limit, Bull. Amer. Math. Soc. 41 (1935), 636.

16.

Birkhoff , Moore–Smith convergence in general topology, Ann. of Math. (2) 38(1) (1937), 39–56. doi:10.2307/1968508.

17.

Bishop , Foundations of Constructive Analysis, McGraw-Hill, 1967.

18.

Borel , Sur quelques points de la théorie des fonctions, Ann. Sci. École Norm. Sup. (3) 12 (1895), 9–55. doi:10.24033/asens.406.

19.

Bourbaki , Elements of Mathematics. General Topology. Part 1, Addison-Wesley, 1966.

20.

Bourbaki , Elements of Mathematics. General Topology. Part 2, Addison-Wesley, 1966.

21.

J.W.

Brace , Almost uniform convergence, Portugal. Math. 14 (1956), 99–104.

22.

J.W.

Brace , The topology of almost uniform convergence, Pacific J. Math. 9 (1959), 643–652. doi:10.2140/pjm.1959.9.643.

23.

Bridges ,

Dent and

McKubre-Jordens , Constructive connections between anti-Specker, positivity, and fan-theoretic properties, New Zealand J. Math. 44 (2014).

24.

Bridges and

Richman , Varieties of Constructive Mathematics, London Mathematical Society Lecture Note Series, Vol. 97, Cambridge University Press, Cambridge, 1987.

25.

Brown and

Pearcy , An Introduction to Analysis, Graduate Texts in Mathematics, Vol. 154, Springer, 1995.

26.

D.K.

Brown , Functional Analysis in Weak Subsystems of Second-order Arithmetic, PhD Thesis, The Pennsylvania State University, ProQuest LLC, 1987.

27.

D.K.

Brown , Notions of compactness in weak subsystems of second order arithmetic, in: Reverse Mathematics 2001, Lect. Notes Log., Vol. 21, Assoc. Symbol. Logic, 2005, pp. 47–66.

28.

J.P.

Burgess , Fixing Frege, Princeton Monographs in Philosophy, Princeton University Press, 2005.

29.

Cartan , Théorie des filtres and Filtres et ultrafiltres, C. R. Acad. Sc. Paris 205 (1937), 595–598 and 777–779.

30.

Caserta ,

Di Maio and

Ľ.

Holá , Arzelà’s theorem and strong uniform convergence on bornologies, J. Math. Anal. Appl. 371(1) (2010), 384–392. doi:10.1016/j.jmaa.2010.05.042.

31.

Cousin , Sur les fonctions de n variables complexes, Acta Math. 19 (1895), 1–61. doi:10.1007/BF02402869.

32.

A.R.

Day , On the strength of two recurrence theorems, J. Symb. Log. 81(4) (2016), 1357–1374. doi:10.1017/jsl.2016.9.

33.

D.D.

Dzhafarov , Reverse Mathematics Zoo. http://rmzoo.uconn.edu/.

34.

Engelking , General Topology, 2nd edn, Sigma Series in Pure Mathematics, Vol. 6, Heldermann, 1989.

35.

Escardó and

Xu , The inconsistency of a Brouwerian continuity principle with the Curry–Howard interpretation, in: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 38, 2015, pp. 153–164.

36.

Felgner , Models of ZF-Set Theory, Lecture Notes in Mathematics, Vol. 223, Springer-Verlag, Berlin–New York, 1971.

37.

Friedman , Some systems of second order arithmetic and their use, in: Proceedings of the International Congress of Mathematicians (Vancouver, B. C., 1974), Vol. 1, 1975, pp. 235–242.

38.

Friedman , Systems of second order arithmetic with restricted induction, I & II (Abstracts), Journal of Symbolic Logic 41 (1976), 557–559.

39.

Friedman , Interpretations, According to Tarski, Interpretations of Set Theory in Discrete Mathematics and Informal Thinking, The Nineteenth Annual Tarski Lectures, Vol. 1 (2007), pp. 42. http://u.osu.edu/friedman.8/files/2014/01/Tarski1052407-13do0b2.pdf.

40.

R.V.

Fuller , Relations among continuous and various non-continuous functions, Pac. J. Math. 25 (1968), 495–509. doi:10.2140/pjm.1968.25.495.

41.

Furstenberg and

Weiss , Topological dynamics and combinatorial number theory, J. Analyse Math. 34 (1978), 61–85.

42.

Gandy , General recursive functionals of finite type and hierarchies of functions, Ann. Fac. Sci. Univ. Clermont-Ferrand No. 35 (1967), 5–24.

43.

Gerhardy , Proof mining in topological dynamics, Notre Dame J. Form. Log. 49(4) (2008), 431–446. doi:10.1215/00294527-2008-022.

44.

Gierz ,

K.H.

Hofmann ,

Keimel ,

J.D.

Lawson ,

Mislove and

D.S.

Scott , A Compendium of Continuous Lattices, Springer, 1980.

45.

Gierz ,

K.H.

Hofmann ,

Keimel ,

J.D.

Lawson ,

Mislove and

D.S.

Scott , Continuous Lattices and Domains, Encyclopedia of Mathematics and Its Applications, Vol. 93, Cambridge University Press, 2003.

46.

Giusto and

S.G.

Simpson , Located sets and reverse mathematics, J. Symbolic Logic 65(3) (2000), 1451–1480. doi:10.2307/2586708.

47.

Goubault-Larrecq , Non-Hausdorff Topology and Domain Theory, New Mathematical Monographs, Vol. 22, Cambridge University Press, 2013.

48.

P.R.

Halmos , Introduction to Hilbert Space and the Theory of Spectral Multiplicity, AMS Chelsea Publishing, 1998, Reprint of the second (1957) edition.

49.

R.W.

Hansell , Monotone subnets in partially ordered sets, Proc. Amer. Math. Soc. 18 (1967), 854–858. doi:10.1090/S0002-9939-1967-0215759-7.

50.

Herrlich , Axiom of Choice, Lecture Notes in Mathematics, Vol. 1876, Springer, 2006.

51.

D.R.

Hirschfeldt , Slicing the Truth, Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore, Vol. 28, World Scientific Publishing, 2015.

52.

Hunter , Higher-Order Reverse Topology, ProQuest LLC, Ann Arbor, MI, 2008, Thesis (Ph.D.) – The University of Wisconsin–Madison.

53.

Ishihara , Reverse mathematics in Bishop’s constructive mathematics, Philosophia Scientiae (Cahier Spécial) 6 (2006), 43–59.

54.

Ishihara and

Schuster , Compactness under constructive scrutiny, MLQ Math. Log. Q. 50(6) (2004), 540–550. doi:10.1002/malq.200310119.

55.

J.L.

Kelley , General Topology, Springer-Verlag, 1975, Reprint of the 1955 edition; Graduate Texts in Mathematics, No. 27.

56.

J.L.

Kelley and

T.P.

Srinivasan , Measure and Integral. Vol. 1, Graduate Texts in Mathematics, Vol. 116, Springer-Verlag, New York, 1988.

57.

Koellner , Large cardinals and determinacy, in: The Stanford Encyclopedia of Philosophy, 2014. https://plato.stanford.edu/archives/spr2014/entries/large-cardinals-determinacy/.

58.

Kohlenbach , Foundational and mathematical uses of higher types, in: Reflections on the Foundations of Mathematics, Lect. Notes Log., Vol. 15, ASL, 2002, pp. 92–116.

59.

Kohlenbach , Higher order reverse mathematics, in: Reverse Mathematics 2001, Lect. Notes Log., Vol. 21, ASL, 2005, pp. 281–295.

60.

Kohlenbach , Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, Springer-Verlag, Berlin, 2008.

61.

A.P.

Kreuzer , The cohesive principle and the Bolzano–Weierstraß principle, MLQ Math. Log. Q. 57(3) (2011), 292–298. doi:10.1002/malq.201010008.

62.

A.P.

Kreuzer , Primitive recursion and the chain antichain principle, Notre Dame J. Form. Log. 53(2) (2012), 245–265. doi:10.1215/00294527-1715716.

63.

Kupka , A generalised uniform convergence and Dini’s theorem, New Zealand J. Math. 27(1) (1998), 67–72.

64.

Li ,

Ru and

Wu , Rudin’s lemma and reverse mathematics, Ann. Japan Assoc. Philos. Sci. 25 (2017), 57–66.

65.

Lindelöf , Sur Quelques Points De La Théorie Des Ensembles, Comptes Rendus (1903), 697–700.

66.

F.A.

Medvedev , Scenes from the History of Real Functions, Science Networks. Historical Studies, Vol. 7, Birkhäuser Verlag, Basel, 1991.

67.

Montalbán , Open questions in reverse mathematics, Bull. Symb. Logic 17(3) (2011), 431–454. doi:10.2178/bsl/1309952320.

68.

Montalbán and

R.A.

Shore , The limits of determinacy in second-order arithmetic, Proc. Lond. Math. Soc. (3) 104(2) (2012), 223–252. doi:10.1112/plms/pdr022.

69.

E.H.

Moore , On a form of general analysis with aplication to linear differential and integral equations, Atti IV Cong. Inter. Mat. (Roma,1908) 2 (1909), 98–114.

70.

E.H.

Moore , Introduction to a Form of General Analysis, Yale University Press, 1910.

71.

E.H.

Moore , Definition of limit in general integral analysis, Proceedings of the National Academy of Sciences of the United States of America 1(12) (1915), 628–632. doi:10.1073/pnas.1.12.628.

72.

E.H.

Moore , General Analysis. Part I. The Algebra of Matrices, Memoirs of the American Philosophical Society, Vol. 1, Philadelphia, 1935.

73.

E.H.

Moore and

Smith , A general theory of limits, Amer. J. Math. 44 (1922), 102–121. doi:10.2307/2370388.

74.

Muldowney , A General Theory of Integration in Function Spaces, Including Wiener and Feynman Integration, Vol. 153, Longman Scientific & Technical, Harlow; John Wiley, 1987.

75.

Mummert , On the Reverse Mathematics of General Topology, ProQuest LLC, Ann Arbor, MI, 2005, Thesis (Ph.D.) – The Pennsylvania State University.

76.

Mummert , Reverse mathematics of MF spaces, J. Math. Log. 6(2) (2006), 203–232. doi:10.1142/S0219061306000578.

77.

Mummert and

S.G.

Simpson , Reverse mathematics and

Π_{2}^{1}

comprehension, Bull. Symb. Logic 11(4) (2005), 526–533. doi:10.2178/bsl/1130335208.

78.

Mummert and

Stephan , Topological aspects of poset spaces, Michigan Math. J. 59(1) (2010), 3–24. doi:10.1307/mmj/1272376025.

79.

S.A.

Naimpally and

J.F.

Peters , Preservation of continuity, Sci. Math. Jpn. 76(2) (2013).

80.

Noiri , Sequentially subcontinuous functions, Accad. Naz. dei Lincei 58 (1975), 370–373.

81.

Normann and

Sanders , Pincherle’s theorem in Reverse Mathematics and computability theory. Submitted (2018). https://arxiv.org/abs/1808.09783.

82.

Normann and

Sanders , Nonstandard Analysis, Computability Theory, and their connections, Journal of Symbolic Logic. To appear (2019). https://arxiv.org/abs/1702.06556.

83.

Normann and

Sanders , The strength of compactness in computability theory and nonstandard analysis, Annals of Pure and Applied Logic. To appear (2019). http://arxiv.org/abs/1801.08172.

84.

Normann and

Sanders , On the mathematical and foundational significance of the uncountable, Journal of Mathematical Logic 19(1) (2019). doi:10.1142/S0219061319500016.

85.

Normann and

Sanders , Representations in measure theory. Submitted (2019). https://arxiv.org/abs/1902.02756.

86.

P.M.

Pu and

Y.M.

Liu , Fuzzy topology. I. Neighborhood structure of a fuzzy point and Moore–Smith convergence, J. Math. Anal. Appl. 76(2) (1980), 571–599. doi:10.1016/0022-247X(80)90048-7.

87.

Reed and

Simon , Methods of Modern Mathematical Physics. I. Functional Analysis, Academic Press, 1981.

88.

Riesz , Sur un théorème de M. Borel, Comptes rendus de l’Académie des Sciences, Paris, Gauthier-Villars 140 (1905), 224–226.

89.

R.E.

Root , Limits in terms of order, with example of limiting element not approachable by a sequence, Trans. Amer. Math. Soc. 15(1) (1914), 51–71. doi:10.1090/S0002-9947-1914-1500965-1.

90.

Sakamoto and

Yamazaki , Uniform versions of some axioms of second order arithmetic, MLQ Math. Log. Q. 50(6) (2004), 587–593. doi:10.1002/malq.200310122.

91.

Sanders , Reverse Mathematics of topology: Dimension, paracompactness, and splittings. Submitted (2018), pp. 17. https://arxiv.org/abs/1808.08785.

92.

Sanders , Splittings and disjunctions in Reverse Mathematics, Notre Dame Journal for Formal Logic. To appear (2019). https://arxiv.org/abs/1805.11342.

93.

Sanders , Nets and Reverse Mathematics: Initial Results, LNCS 11558, Proceedings of CiE19, Springer, 2019, p. 12.

94.

Sanders , Reverse Mathematics and Computability Theory of Domain Theory, LNCS 11541, Proceedings of WoLLIC19, Springer, 2019, p. 20.

95.

Sanders , Bootstraps, nets, and hierarchies. Submitted (2019), pp. 29. https://arxiv.org/abs/1908.05676.

96.

Schechter , Handbook of Analysis and Its Foundations, Academic Press, Inc., San Diego, CA, 1997.

97.

S.G.

Simpson (ed.), Reverse Mathematics 2001, Lecture Notes in Logic, Vol. 21, ASL, La Jolla, CA, 2005.

98.

S.G.

Simpson , Subsystems of Second Order Arithmetic, 2nd edn, Perspectives in Logic, CUP, 2009.

99.

S.G.

Simpson , The Gödel hierarchy and reverse mathematics, in: Kurt Gödel. Essays for His Centennial, Cambridge University Press, 2010, pp. 109–127. doi:10.1017/CBO9780511750762.008.

100.

Steen and

Seebach , Counterexamples in Topology, Dover, 1995.

101.

Stillwell , Reverse Mathematics, Proofs from the Inside Out, Princeton Univ. Press, 2018.

102.

Swartz , Introduction to Gauge Integrals, World Scientific, 2001.

103.

Thomson ,

Bruckner and

Bruckner , Elementary Real Analysis, Prentice Hall, 2001.

104.

Timofte and

Timofte , Generalized Dini theorems for nets of functions on arbitrary sets, Positivity 20(1) (2016), 171–185. doi:10.1007/s11117-015-0348-2.

105.

Toma , Strong convergence and Dini theorems for non-uniform spaces, Ann. Math. Blaise Pascal 4(2) (1997), 97–102. doi:10.5802/ambp.100.

106.

A.S.

Troelstra , Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, Vol. 344, Springer, Berlin, 1973.

107.

A.S.

Troelstra and

van Dalen , Constructivism in Mathematics. Vol. I, Studies in Logic and the Foundations of Mathematics, Vol. 121, North-Holland, 1988.

108.

Vietoris , Stetige mengen, Monatsh. Math. Phys. 31(1) (1921), 173–204. doi:10.1007/BF01702717.

109.

von Neumann , On complete topological spaces, Trans. Amer. Math. Soc. 37(1) (1935), 1–20. doi:10.1090/S0002-9947-1935-1501776-7.

110.

Wang , Eighty years of foundational studies, Dialectica 12 (1958), 466–497. doi:10.1111/j.1746-8361.1958.tb01476.x.

111.

E.S.

Wolk , Continuous convergence in partially ordered sets, General Topology and Appl. 5(3) (1975), 221–234. doi:10.1016/0016-660X(75)90022-7.

112.

W.H.

Young , Overlapping intervals, Bulletin of the London Mathematical Society 35 (1902), 384–388.

113.

L.A.

Zadeh , Fuzzy sets, Information and Control 8 (1965), 338–353. doi:10.1016/S0019-9958(65)90241-X.

Nets and reverse mathematics

Abstract

Keywords

1. Aim and motivation

1.1. Introduction

1 Nets can have uncountable index sets, and the latter are called directed sets.

2.1. Reverse mathematics

Definition 2.4 ( RCA 0 ω ).

Remark 2.1 (The ECF -interpretation).

Notation 2.1 (Finite sequences).

2.2. Some axioms of higher-order RM

2.3. Introducing nets

Definition 2.5 (Nets).

Definition 2.6 (Convergence of nets).

Definition 2.7 (Increasing nets).

3. Main results I

3.1. Sequential compactness and nets

3.1.1. The Bolzano–Weierstrass theorem for nets

Remark 3.1 (Filters versus nets).

3.1.3. Isolated points and nets

Definition 3.9 (Anti-Specker property).

Definition 3.15 (Cauchy net).

Definition 3.16 ( CAU net ).

Definition 3.17 ( CAU net ′ ).

Definition 3.21 ( PERM ).

Definition 3.23 (Increasing net).

3.2.1. Dini’s theorem

Definition 3.24 ( DIN net ).

7 Note that [30] includes an historical overview pertaining to Arzelà’s theorem (for nets).

Definition 3.28 ( ARZ net ).

4. Main results II

4.1. Introduction

4.2. Nets and sequentialisation

Definition 4.1 ( LIN ).

10 By [59, Prop. 3.6], RCA 0 ω can prove the global equivalence of sequential continuity and epsilon-delta continuity on N N , i.e. when those continuity properties hold everywhere on the latter.

Theorem 4.11 ( RCA 0 ω ).

Definition 4.13 (Open and closed sets).

Definition 4.16 (Sub-continuity).

Footnotes

Acknowledgements

General index sets

Nets and the Gödel hierarchy

References

¹
Nets can have uncountable index sets, and the latter are called directed sets.

Definition 2.4 ( ${RCA}_{0}^{ω}$ ).

Remark 2.1 (The $ECF$ -interpretation).

Definition 3.16 ( ${CAU}_{net}$ ).

Definition 3.17 ( ${CAU}_{net}^{'}$ ).

Definition 3.21 ( $PERM$ ).

Definition 3.24 ( ${DIN}_{net}$ ).

⁷
Note that [30] includes an historical overview pertaining to Arzelà’s theorem (for nets).

Definition 3.28 ( ${ARZ}_{net}$ ).

Definition 4.1 ( $LIN$ ).

¹⁰
By [59, Prop. 3.6], ${RCA}_{0}^{ω}$ can prove the global equivalence of sequential continuity and epsilon-delta continuity on $N^{N}$ , i.e. when those continuity properties hold everywhere on the latter.

Theorem 4.11 ( ${RCA}_{0}^{ω}$ ).