The strength of compactness for countable complete linear orders

TL;DR

This paper explores the logical strength of compactness in countable complete linear orders within reverse mathematics, showing it varies with the formulation of open covers, and establishes equivalences with well-known subsystems.

Contribution

It clarifies how the formulation of compactness affects its logical strength, providing a nuanced understanding in reverse mathematics.

Findings

Compactness with uniform open covers is equivalent to WKL_0.

Without uniformity, compactness is equivalent to ACA_0.

Answers a question posed by François Dorais.

Abstract

We investigate the statement "the order topology of every countable complete linear order is compact" in the framework of reverse mathematics, and we find that the statement's strength depends on the precise formulation of compactness. If we require that open covers must be uniformly expressible as unions of basic open sets, then the compactness of complete linear orders is equivalent to $\mathsf{WKL}_0$ over $\mathsf{RCA}_0$. If open covers need not be uniformly expressible as unions of basic open sets, then the compactness of complete linear orders is equivalent to $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$. This answers a question of Fran\c{c}ois Dorais.

Equations

$$(a,\infty )$$

$$(-\infty ,b)$$

$$(a,b)$$

$$(\forall x\in A^{-})(\forall y\in A^{+})(x\prec y),$$

$$[\phi (0)\wedge \forall n(\phi (n)\to \phi (n+1))]\to \forall n\phi (n),$$

$$\forall n(\phi (n)\leftrightarrow \psi (n))\to \exists X\forall n(n\in X\leftrightarrow \phi (n)),$$

$$\exists n\phi (n)\to \exists n[\phi (n)\wedge (\forall m<n)(\neg \phi (m))],$$

$$\forall a[(\forall n<a)(\exists m)\phi (n,m)\to \exists b(\forall n<a)(\exists m<b)\phi (n,m)],$$

$$\forall b\exists X\forall n[n\in X\leftrightarrow (n<b\wedge \phi (n))],$$

$$\exists X\forall n(n\in X\leftrightarrow \phi (n)),$$

$$\forall x[(\exists n)(x\in \hat{h}(n))\leftrightarrow (\exists n)(\exists i\in h(n))(x\in U_i)].$$

$$g(⟨m,n,s⟩)=\{\begin{array}{ll}\text{the (s+1)textsuperscriptth smallest member of h(m,n)}& \text{if ∣h(m,n)∣≥s+1}\\ i_0& \text{otherwise}.\end{array}$$

$$U_{⟨0,n⟩}$$

$$U_{⟨1,⟨n,s⟩⟩}$$

$$U_{⟨2,s⟩}$$

$$\exists s(f(s)=n)\iff \exists m\exists s(h(m)=⟨1,⟨n,s⟩⟩)\iff \forall m(h(m)\ne ⟨0,n⟩).$$

$$D=\{x<n:(\exists ⟨n_i:i<k⟩)[\text{((ani,bni):i<k) is a linkage containing both 0 and x}]\}.$$

$$\sigma \supseteq \tau \vee (\exists n<\min (|\sigma |,|\tau |))[\sigma (n)<\tau (n)\wedge (\forall i<n)(\sigma (i)=\tau (i))].$$

$$\ell (\sigma )=\{\begin{array}{ll}\text{σ’s <KB-immediate predecessor}& \text{if σ is not <KB-least}\\ -\infty & \text{if σ is <KB-least}.\end{array}$$

$$r(\sigma )=\{\begin{array}{ll}\text{σ’s <KB-immediate successor}& \text{if σ=∅}\\ \infty & \text{if σ=∅}.\end{array}$$

$$\sigma \in A^{+}\wedge (\forall i<|\sigma |)(\forall n<\sigma (i))[(\sigma \upharpoonright i{)}^{⌢}n\notin A^{+}].$$

Full text

1. Introduction

Every linear order $(L,\prec)$ can be equipped with its order topology, where the basic open sets are the open intervals

[TABLE]

Call a linear order $(L,\prec)$ complete if whenever $L$ is partitioned as $L=A^{-}\cup A^{+}$ with

[TABLE]

it is the case that either $A^{-}$ has a greatest element or $A^{+}$ has a least element. It is well-known (see for example [Munkres, Theorem 27.1]) that the order topology of a non-empty linear order is compact if and only if the linear order is complete in the above sense. Our goal is to characterize the logical strength of this fact when restricting to countable linear orders.

This work is an example of reverse mathematics, which is the project of classifying mathematical theorems phrased in second-order arithmetic by the strengths of the axiom systems that are required to prove the theorems. Reverse mathematics was introduced by H. Friedman [Friedman], and the standard reference is Simpson’s [SimpsonSOSOA]. Formally, the only mathematical objects that second-order arithmetic allows are natural numbers and sets of natural numbers. Nevertheless, straightforward coding techniques available in weak background theories allow us to discuss tuples and sequences of natural numbers; functions $f\colon\mathbb{N}^{m}\rightarrow\mathbb{N}^{n}$; countable algebraic or combinatorial objects such as countable groups, rings, fields, graphs, trees, partial orders, linear orders; and more. By coding a real number as a rapidly converging Cauchy sequence of rational numbers and by coding a basic open subset of $\mathbb{R}^{n}$ as an $(n+1)$-tuple of rational numbers (representing an open ball of rational radius whose center has rational coordinates), we may discuss $\mathbb{R}^{n}$, its topology, continuous functions $f\colon\mathbb{R}^{m}\rightarrow\mathbb{R}^{n}$, and so forth. We may even discuss arbitrary complete separable metric spaces by specifying a space’s countable dense set and a metric on that dense set. To date, most work in reverse mathematics involving topology has been confined to complete separable metric spaces. Few attempts have been made to study general topology in second-order arithmetic. One excellent example is Mummert’s and Simpson’s work on filter spaces [MummertMF, MummertSimpson]. Here we take up Dorais’s framework of countable second-countable topological spaces [Dorais].

Dorais’s idea is to study general topology in second-order arithmetic by restricting to the topological spaces that can be straightforwardly represented in second-order arithmetic. These are the countable second-countable spaces: the topological spaces with countably many points and with countable bases. The countable second-countable spaces framework of course comes with its own limitations (it is not a good approach to studying connectivity, for example), but it has the advantage of representing topological notions directly, and it works well for analyzing theorems whose proofs largely concern the combinatorics of open sets and closed sets. This framework was used in [NoetherianSpaces] to analyze topological spaces arising from quasi-orders, for example. Here we study countable linear orders and their order topologies. This could be done in a completely ad hoc manner, as a linear order’s order topology is easy to describe. However, the order topologies of countable linear orders fit very nicely into the countable second-countable spaces framework, as shown by the many examples in [Dorais].

In [Dorais], Dorais considers a notion of compactness in which the open sets of an open cover are explicitly presented as unions of basic open sets. We call this notion compactness with respect to honest open covers. The idea is that a sequence of open sets is honest if it comes with an explanation of how each open set in the sequence can be written as a union of basic open sets. Dorais observes that the base theory $\mathsf{RCA}_{0}$ proves that if the order topology of a countable linear order is compact with respect to honest open covers, then that linear order is complete (see Lemma 3.12 below). He then asks for the axiomatic strength of the converse, that is, for the strength of the statement “the order topology of every countable complete linear order is compact with respect to honest open covers.” Dorais shows that $\mathsf{RCA}_{0}$ does not suffice to prove this statement. In fact, he shows that, over $\mathsf{RCA}_{0}$, the statement implies that there is no set of maximum Turing degree [Dorais, Example 7.8]. We answer Dorais’s question by showing that the statement “the order topology of every countable complete linear order is compact with respect to honest open covers” is equivalent to $\mathsf{WKL}_{0}$ over $\mathsf{RCA}_{0}$.

Dorais also considers a stronger notion of compactness, here simply called compactness, where the open sets of an open cover need not be uniformly presentable as unions of basic open sets [DoraisPC]. We show that with this notion of compactness, the statement “the order topology of every countable complete linear order is compact” is equivalent to $\mathsf{ACA}_{0}$ over $\mathsf{RCA}_{0}$.

2. Preliminaries for working in second-order arithmetic

We remind the reader of the axiom systems $\mathsf{RCA}_{0}$, $\mathsf{WKL}_{0}$, and $\mathsf{ACA}_{0}$. Simpson’s [SimpsonSOSOA] provides many more details concerning these and other systems, including many examples of theorems that can be proven in them.

The language of second-order arithmetic contains two sorts of variables: first-order variables intended to range over the natural numbers and second-order variables intended to range over sets of natural numbers. Typically, but not always, lower-case letters $a$, $b$, $c$, $x$, $y$, $z$, etc. denote first-order variables, and capital letters $A$, $B$, $C$, $X$, $Y$, $Z$, etc. denote second-order variables. The symbol $\mathbb{N}$ is notational shorthand for the first-order part of whatever structure is implicitly under consideration.

The language of second-order arithmetic contains constant symbols [math] and $1$, binary function symbols $+$ and $\times$, and binary relation symbols $=$, $<$, and $\in$. The constants [math] and $1$ name numbers, and the functions and relations $+$, $\times$, $=$, and $<$ only apply to numbers. The relation $\in$ relates numbers to sets, and equality between sets is defined in terms of $\in$.

$\mathsf{RCA}_{0}$ (standing for recursive comprehension axiom) is an axiom system designed to capture computable mathematics. Roughly speaking, to prove that some set exists when working in $\mathsf{RCA}_{0}$, one must show how to compute that set, possibly using as an oracle some other set that has already been shown to exist. The axioms of $\mathsf{RCA}_{0}$ consist of

• •

a first-order sentence expressing that the numbers form a discretely ordered commutative semi-ring with identity;

• •

the $\Sigma^{0}_{1}$ induction scheme (denoted $\mathsf{I}\Sigma^{0}_{1}$), which consists of the universal closures (by both number and set quantifiers) of all formulas of the form

[TABLE]

where $\varphi$ is $\Sigma^{0}_{1}$; and

• •

the $\Delta^{0}_{1}$ comprehension scheme, which consists of the universal closures (by both number and set quantifiers) of all formulas of the form

[TABLE]

where $\varphi$ is $\Sigma^{0}_{1}$, $\psi$ is $\Pi^{0}_{1}$, and $X$ is not free in $\varphi$.

$\mathsf{RCA}_{0}$ is the usual base system or background theory in reverse mathematics. Many theorems in reverse mathematics have the form $\mathsf{RCA}_{0}\vdash\varphi\leftrightarrow\psi$, where $\varphi$ and $\psi$ are two well-known mathematical statements. If $\mathsf{RCA}_{0}\vdash\varphi\leftrightarrow\psi$, we say that $\varphi$ and $\psi$ are equivalent over $\mathsf{RCA}_{0}$, and we interpret this as meaning that $\varphi$ and $\psi$ have equivalent logical strength. The ‘[math]’ in ‘$\mathsf{RCA}_{0}$’ refers to the restriction of the induction scheme to $\Sigma^{0}_{1}$ formulas.

$\mathsf{RCA}_{0}$ proves several induction schemes, least element principles, bounding schemes, and bounded comprehension principles in addition to $\mathsf{I}\Sigma^{0}_{1}$. Here the relevant schemes are the $\Pi^{0}_{1}$ induction scheme (denoted $\mathsf{I}\Pi^{0}_{1}$), the $\Sigma^{0}_{1}$ least element principle, the $\Sigma^{0}_{1}$ bounding scheme (denoted $\mathsf{B}\Sigma^{0}_{1}$), and the bounded $\Sigma^{0}_{1}$ comprehension scheme. The $\Pi^{0}_{1}$ induction scheme is as the $\Sigma^{0}_{1}$ induction scheme, but the formula $\varphi$ is required to be $\Pi^{0}_{1}$. The $\Sigma^{0}_{1}$ least element principle consists of the universal closures of all formulas of the form

[TABLE]

where $\varphi$ is $\Sigma^{0}_{1}$. The $\Sigma^{0}_{1}$ bounding scheme consists of the universal closures of all formulas of the form

[TABLE]

where $\varphi$ is $\Sigma^{0}_{1}$ and $a$ and $b$ are not free in $\varphi$. The $\Sigma^{0}_{1}$ bounded comprehension scheme consists of the universal closures of all formulas of the form

[TABLE]

where $\varphi$ is $\Sigma^{0}_{1}$ and $X$ is not free in $\varphi$. See [HajekPudlak, Section I.2] and [SimpsonSOSOA, Section II.3] for further details.

$\mathsf{RCA}_{0}$ suffices to code a finite set of numbers as a single number and a finite sequence of numbers as a single number in the usual way. In $\mathsf{RCA}_{0}$, we can thus code the set $\mathbb{N}^{<\mathbb{N}}$ of all finite sequences as well as its subset $2^{<\mathbb{N}}$ of all finite binary sequences. We now fix our notation and terminology for (coded) sequences. For $\sigma,\tau\in\mathbb{N}^{<\mathbb{N}}$, $|\sigma|$ denotes the length of $\sigma$, $\sigma\subseteq\tau$ denotes that $\sigma$ is an initial segment of $\tau$, and $\sigma^{\smallfrown}\tau$ denotes the concatenation of $\sigma$ and $\tau$. For $\sigma\in\mathbb{N}^{<\mathbb{N}}$ and $n\leq|\sigma|$, $\sigma{\restriction}n=\langle\sigma(0),\dots,\sigma(n-1)\rangle$ denotes the initial segment of $\sigma$ of length $n$. Likewise, if $f\colon\mathbb{N}\rightarrow\mathbb{N}$ is a function and $n\in\mathbb{N}$, $f{\restriction}n=\langle f(0),\dots,f(n-1)\rangle$ denotes the sequence consisting of the first $n$ values of $f$.

In $\mathsf{RCA}_{0}$, we define a tree to be a set $T\subseteq\mathbb{N}^{<\mathbb{N}}$ that is closed under initial segments: $\forall\sigma\forall\tau[(\sigma\in T\wedge\tau\subseteq\sigma)\rightarrow\tau\in T]$. A function $f\colon\mathbb{N}\rightarrow\mathbb{N}$ is an infinite path through a tree $T$ if every initial segment of $f$ is in $T$: $\forall n(f{\restriction}n\in T)$. We can now define weak König’s lemma to be the statement “every infinite subtree of $2^{<\mathbb{N}}$ has an infinite path.” The system $\mathsf{WKL}_{0}$ is obtained by adding weak König’s lemma to the axioms of $\mathsf{RCA}_{0}$.

Lastly, the system $\mathsf{ACA}_{0}$ (standing for arithmetical comprehension axiom) is obtained by augmenting $\mathsf{RCA}_{0}$ by the arithmetical comprehension scheme, which consists of the universal closures of all formulas of the form

[TABLE]

where $\varphi$ is an arithmetical formula in which $X$ is not free.

$\mathsf{WKL}_{0}$ is strictly stronger than $\mathsf{RCA}_{0}$, and $\mathsf{ACA}_{0}$ is strictly stronger than $\mathsf{WKL}_{0}$ (see [SimpsonSOSOA, Remark I.10.2 and Section VIII.2]). A helpful characterization of $\mathsf{ACA}_{0}$ is that, over $\mathsf{RCA}_{0}$, it is equivalent to the statement “every injection has a range.”

Lemma 2.1** ([SimpsonSOSOA, Lemma III.1.3]).**

The following are equivalent over $\mathsf{RCA}_{0}$.

1. (i)

$\mathsf{ACA}_{0}$. 2. (ii)

If $f\colon\mathbb{N}\rightarrow\mathbb{N}$ is an injection, then there is a set $X$ such that $\forall n(n\in X\leftrightarrow\exists s(f(s)=n))$.

Thus to show that some statement implies $\mathsf{ACA}_{0}$ over $\mathsf{RCA}_{0}$, it suffices to show that the statement implies that every injection has a range.

We make use of König’s lemma and bounded König’s lemma in addition to weak König’s lemma. Call a tree $T\subseteq\mathbb{N}^{<\mathbb{N}}$ finitely-branching if every $\sigma\in T$ has at most finitely many immediate successors: $(\forall\sigma\in T)(\exists n)(\forall m)[\sigma^{\smallfrown}\langle m\rangle\in T\rightarrow m<n]$. Furthermore, call a finitely-branching tree $T\subseteq\mathbb{N}^{<\mathbb{N}}$ bounded if it comes equipped with a function bounding its branching, i.e., if there is a function $g\colon\mathbb{N}\rightarrow\mathbb{N}$ such that $(\forall\sigma\in T)(\forall n<|\sigma|)[\sigma(n)<g(n)]$. König’s lemma is the statement “every infinite finitely-branching subtree of $\mathbb{N}^{<\mathbb{N}}$ has an infinite path,” and bounded König’s lemma is the statement “every infinite bounded subtree of $\mathbb{N}^{<\mathbb{N}}$ has an infinite path.”

Theorem 2.2**.**

1. (i)

König’s lemma is equivalent to $\mathsf{ACA}_{0}$ over $\mathsf{RCA}_{0}$ (see [SimpsonSOSOA, Theorem III.7.2]). 2. (ii)

Bounded König’s lemma is equivalent to $\mathsf{WKL}_{0}$ over $\mathsf{RCA}_{0}$ (see [SimpsonSOSOA, Lemma IV.1.4]).

3. Countable second-countable topological spaces

We introduce the countable second-countable topological spaces framework from [Dorais].

Definition 3.1** ($\mathsf{RCA}_{0}$; [Dorais, Definition 2.1]).**

A strong base (or simply base) for a topology on a set $X$ is an indexed sequence $\mathcal{U}=(U_{i})_{i\in I}$ of subsets of $X$ together with a function $k\colon X\times I\times I\rightarrow I$ such that the following properties hold.

• •

If $x\in X$, then $x\in U_{i}$ for some $i\in I$.

• •

If $x\in U_{i}\cap U_{j}$, then $x\in U_{k(x,i,j)}\subseteq U_{i}\cap U_{j}$.

Definition 3.2** ($\mathsf{RCA}_{0}$; [Dorais, Definition 2.2]).**

A strong countable second-countable space (or simply countable second-countable space) is a triple $(X,\mathcal{U},k)$ where $\mathcal{U}=(U_{i})_{i\in I}$ and $k\colon X\times I\times I\rightarrow I$ form a base for a topology on the set $X$.

We have no use for the empty space, so we always assume that a countable second-countable space is non-empty.

Dorais also defines the notion of a weak base for a topology on a set $X$ and the corresponding notion of a weak countable second-countable space [DoraisPC]. The distinction is that a weak base for a topology on $X$ is a uniformly enumerable sequence of subsets of $X$ rather than a sequence of literal subsets of $X$. So in a weak base, membership in a basic open set is a $\Sigma^{0}_{1}$ property, whereas in a strong base, membership in a basic open set is a $\Delta^{0}_{1}$ property. It is natural and straightforward to define a strong base for the order topology of a countable linear order in $\mathsf{RCA}_{0}$ (see Definition 3.11 below), so in this work we need only consider strong bases and strong countable second-countable spaces.

Open subsets of countable second-countable spaces are coded by enumerations of indices of basic open sets. Thus we must first define coded enumerable sets.

Definition 3.3** ($\mathsf{RCA}_{0}$).**

Let $A\subseteq\mathbb{N}$, and let $\mathcal{P}_{\mathrm{f}}(A)$ denote the set of finite subsets of $A$.

• •

An enumerable subset of $A$ is coded by a function $h\colon\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(A)$, where $h$ codes $A_{h}=\bigcup_{n\in\mathbb{N}}h(n)$.

• •

A sequence of uniformly enumerable subsets of $A$ is coded by a function $h\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(A)$, where, for each $m$, $h(m,\cdot)$ codes the $m$th set in the sequence: $A_{g(m,\cdot)}=\bigcup_{n\in\mathbb{N}}h(m,n)$. Denote this sequence by $(A_{h(m,\cdot)}:m\in\mathbb{N})$.

In general, $\mathsf{ACA}_{0}$ is required to prove that $A_{h}=\bigcup_{n\in\mathbb{N}}h(n)$ exists as a set for every $A\subseteq\mathbb{N}$ and every $h\colon\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(A)$. Thus the expressions ‘$a\in A_{h}$’ and ‘$a\in\bigcup_{n\in\mathbb{N}}h(n)$’ must be interpreted as abbreviations for the formula ‘$\exists n(a\in h(n))$.’ The reason we consider functions $h\colon\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(A)$ rather than functions $h\colon\mathbb{N}\rightarrow A$ is that with functions $h\colon\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(A)$, we may easily represent $\emptyset$ by the function with constant value $\emptyset$.

Definition 3.4** ($\mathsf{RCA}_{0}$; [Dorais, Definitions 2.3 and 2.4]).**

Let $(X,\mathcal{U},k)$ be a countable second-countable space, where $\mathcal{U}=(U_{i})_{i\in I}$. An effectively open subset of $X$ is coded by an enumerable subset of $I$, i.e., by a function $h\colon\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$. An $x\in X$ is a member of the effectively open subset of $X$ coded by $h$ if there are an $n\in\mathbb{N}$ and an $i\in h(n)$ such that $x\in U_{i}$. Let $G_{h}=\bigcup_{n\in\mathbb{N}}\bigcup_{i\in h(n)}U_{i}$ denote the open subset of $X$ coded by $h$.

Again, $\mathsf{ACA}_{0}$ is required to show that $G_{h}$ exists as a set for every countable second-countable space $(X,\mathcal{U},k)$ and function $h\colon\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$. Thus the expression ‘$x\in G_{h}$’ must be interpreted as an abbreviation for the formula ‘$(\exists n)(\exists i\in h(n))(x\in U_{i})$.’

Let $(X,\mathcal{U},k)$ be a countable second-countable space. Every open subset of $X$ is an enumerable subset of $X$, meaning that for every $h\colon\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$, there is an $\hat{h}\colon\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(X)$ such that $X_{\hat{h}}=G_{h}$:

[TABLE]

Furthermore, we may interpret any double-sequence $h\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$ as a sequence $(G_{h(m,\cdot)}:m\in\mathbb{N})$ of open sets, where the $m$th open set in the sequence is $G_{h(m,\cdot)}=\bigcup_{n\in\mathbb{N}}\bigcup_{i\in h(m,n)}U_{i}$. Each such sequence may also be thought of as a uniformly enumerable sequence of subsets of $X$. That is, there is an $\hat{h}\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(X)$ such that, for all $m\in\mathbb{N}$, $X_{\hat{h}(m,\cdot)}=G_{h(m,\cdot)}$. However, there may be sequences $(X_{\ell(m,\cdot)}:m\in\mathbb{N})$ of uniformly enumerable subsets of $X$ where each individual $X_{\ell(m,\cdot)}$ is open, but there is no uniform way to code each $X_{\ell(m,\cdot)}$ as a union of basic open sets. That is, it could be that for every $m$ there is an $h\colon\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$ such that $X_{\ell(m,\cdot)}=G_{h}$, but there is no $h\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$ such that for every $m$, $X_{\ell(m,\cdot)}=G_{h(m,\cdot)}$. We call a sequence of open subsets of $X$ honest if each set in the sequence is uniformly coded as a union of basic open sets.

Definition 3.5** ($\mathsf{RCA}_{0}$).**

Let $(X,\mathcal{U},k)$ be a countable second-countable space, where $\mathcal{U}=(U_{i})_{i\in I}$. A sequence $(X_{\ell(m,\cdot)}:m\in\mathbb{N})$ of uniformly enumerable subsets of $X$ is an honest sequence of open subsets of $X$ if there is a function $h\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$ such that for all $m$, $X_{\ell(m,\cdot)}=G_{h(m,\cdot)}$.

Dorais gives two notions of compactness for countable second-countable spaces, corresponding to whether or not we require open covers to be honest. We warn the reader that Dorais’s original definition of compactness [Dorais, Definition 3.1] considers only honest open covers, so the definition of ‘compact’ in [Dorais, NoetherianSpaces] corresponds to the definition of ‘compact with respect to honest open covers’ here.

Definition 3.6** ($\mathsf{RCA}_{0}$).**

Let $(X,\mathcal{U},k)$ be a countable second-countable space.

• •

A sequence $(X_{h(m,\cdot)}:m\in\mathbb{N})$ of uniformly enumerable subsets of $X$ is an open cover of $X$ if $X_{h(m,\cdot)}$ is an open subset of $X$ for each $m$ and if $X=\bigcup_{m\in\mathbb{N}}X_{h(m,\cdot)}$ (i.e., $(\forall x\in X)(\exists m)(x\in X_{h(m,\cdot)})$).

• •

An open cover $(X_{h(m,\cdot)}:m\in\mathbb{N})$ of $X$ is honest if $(X_{h(m,\cdot)}:m\in\mathbb{N})$ is an honest sequence of open subsets of $X$.

• •

The space $(X,\mathcal{U},k)$ is compact if for every open cover $(X_{h(m,\cdot)}:m\in\mathbb{N})$ of $X$ there is an $M\in\mathbb{N}$ such that $X=\bigcup_{m<M}X_{h(m,\cdot)}$.

• •

The space $(X,\mathcal{U},k)$ is compact with respect to honest open covers if for every honest open cover $(X_{h(m,\cdot)}:m\in\mathbb{N})$ of $X$ there is an $M\in\mathbb{N}$ such that $X=\bigcup_{m<M}X_{h(m,\cdot)}$.

In terms of basic open sets, an honest open cover of $(X,\mathcal{U},k)$ is an open cover of the form $X=\bigcup_{m\in\mathbb{N}}\bigcup_{n\in\mathbb{N}}\bigcup_{i\in h(m,n)}U_{i}$ for a function $h\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$. Thus $(X,\mathcal{U},k)$ is compact w.r.t. honest open covers if and only if whenever $h\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$ is such that $X=\bigcup_{m\in\mathbb{N}}\bigcup_{n\in\mathbb{N}}\bigcup_{i\in h(m,n)}U_{i}$, there is an $M\in\mathbb{N}$ such that $X=\bigcup_{m<M}\bigcup_{n\in\mathbb{N}}\bigcup_{i\in h(m,n)}U_{i}$. A double-sequence of basic open sets may be rewritten as a single sequence of basic open sets, which means that a countable second-countable space is compact w.r.t. honest open covers if and only if it is compact w.r.t. honest open covers by basic open sets.

Proposition 3.7** ($\mathsf{RCA}_{0}$).**

Let $(X,\mathcal{U},k)$ be a countable second-countable space with $\mathcal{U}=(U_{i})_{i\in I}$. Then $(X,\mathcal{U},k)$ is compact w.r.t. honest open covers if and only if for every $g\colon\mathbb{N}\rightarrow I$ such that $X=\bigcup_{m\in\mathbb{N}}U_{g(m)}$, there is an $M\in\mathbb{N}$ such that $X=\bigcup_{m<M}U_{g(m)}$.

Proof.

Every open cover of the form $X=\bigcup_{m\in\mathbb{N}}U_{g(m)}$ is an honest open cover. So if $(X,\mathcal{U},k)$ is compact w.r.t. honest open covers, then for every $g\colon\mathbb{N}\rightarrow I$ such that $X=\bigcup_{m\in\mathbb{N}}U_{g(m)}$, there is an $M\in\mathbb{N}$ such that $X=\bigcup_{m<M}U_{g(m)}$.

For the converse, suppose that $X=\bigcup_{m\in\mathbb{N}}\bigcup_{n\in\mathbb{N}}\bigcup_{i\in h(m,n)}U_{i}$ for some function $h\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$. Fix $m_{0}$ and $n_{0}$ such that $h(m_{0},n_{0})\neq\emptyset$, and fix an $i_{0}\in h(m_{0},n_{0})$. For the purposes of this argument, let $\langle\cdot,\cdot,\cdot\rangle\colon\mathbb{N}^{3}\rightarrow\mathbb{N}$ denote a bijection. Define $g\colon\mathbb{N}\rightarrow I$ by

[TABLE]

Then $X=\bigcup_{p\in\mathbb{N}}U_{g(p)}$, so there is a $P\in\mathbb{N}$ such that $X=\bigcup_{p<P}U_{g(p)}$. For every $p<P$ there are $m$ and $n$ such that $g(p)\in h(m,n)$. By $\mathsf{B}\Sigma^{0}_{1}$, there is an $M\in\mathbb{N}$ such that for every $p<P$, there is an $m<M$ and an $n$ such that $g(p)\in h(m,n)$. Therefore $X=\bigcup_{m<M}\bigcup_{n\in\mathbb{N}}\bigcup_{i\in h(m,n)}U_{i}$. ∎

In light of the above proposition, we typically think of compactness w.r.t. honest open covers in terms of covers of the form $X=\bigcup_{m\in\mathbb{N}}U_{g(m)}$ for functions $g\colon\mathbb{N}\rightarrow I$. Equivalently, we may also think of compactness w.r.t. honest open covers in terms of covers of the form $X=\bigcup_{n\in\mathbb{N}}\bigcup_{i\in h(n)}U_{i}$ for functions $h\colon\mathbb{N}\rightarrow\mathcal{P}_{\mathrm{f}}(I)$, as was (implicitly) done in Dorais’s original definition [Dorais, Definition 3.1] and in [NoetherianSpaces].

When working with compactness in $\mathsf{RCA}_{0}$, there is the added wrinkle that it may or may not be possible to uniformly determine whether or not a given finite collection of basic open sets covers the whole space. If it is possible, then we say that the space’s base has a finite cover relation.

Definition 3.8** ($\mathsf{RCA}_{0}$; [Dorais, Definition 2.13]).**

Let $(X,\mathcal{U},k)$ be a countable second-countable space with $\mathcal{U}=(U_{i})_{i\in I}$. $\mathcal{U}$ has a finite cover relation if there is a set $C\subseteq\mathcal{P}_{\mathrm{f}}(I)$ such that, for all $\{i_{0},\dots,i_{n-1}\}\subseteq I$, $\{i_{0},\dots,i_{n-1}\}\in C$ if and only if $X=\bigcup_{j<n}U_{i_{j}}$.

Every honest open cover of a countable second-countable space is also an open cover of the space, so $\mathsf{RCA}_{0}$ proves that a compact countable second-countable space is also compact w.r.t. honest open covers. Unsurprisingly, $\mathsf{ACA}_{0}$ is required to prove that every countable second-countable space that is compact w.r.t. honest open covers is compact. This fact follows from [Dorais, Example 5.4], but we find it instructive to present a similar yet somewhat more straightforward proof. It is convenient to first introduce notions of discreteness.

Definition 3.9** ($\mathsf{RCA}_{0}$; [Dorais, Definition 5.1]).**

Let $(X,\mathcal{U},k)$ be a countable second-countable space with $\mathcal{U}=(U_{i})_{i\in I}$.

• •

$(X,\mathcal{U},k)$ is discrete if for every $x\in X$ there is an $i\in I$ such that $U_{i}=\{x\}$.

• •

$(X,\mathcal{U},k)$ is effectively discrete if there is a function $d\colon X\rightarrow I$ such that, for every $x\in X$, $U_{d(x)}=\{x\}$.

We readily see that an infinite discrete countable second-countable space is not compact and that an infinite effectively discrete countable second-countable space is not compact w.r.t. honest open covers.

Proposition 3.10**.**

The statement “every countable second-countable space that is compact w.r.t. honest open covers is compact” is equivalent to $\mathsf{ACA}_{0}$ over $\mathsf{RCA}_{0}$.

Proof.

For the forward direction, when working in $\mathsf{ACA}_{0}$ it is routine to show that every sequence of open subsets of a countable second-countable space is honest. Thus $\mathsf{ACA}_{0}$ proves that compactness and compactness w.r.t. honest open covers are equivalent.

For the reverse direction, let $f\colon\mathbb{N}\rightarrow\mathbb{N}$ be an injection. We appeal to Lemma 2.1 and show that the range of $f$ exists. Define a countable second-countable space $(X,\mathcal{U},k)$ by $X=\mathbb{N}$, $I=\{0,1,2\}\times\mathbb{N}$, and

[TABLE]

The function $k$ is computed as follows. To check that $k$ behaves as intended, it is helpful to observe that if $x\in U_{\langle 0,n\rangle}$ but $x\neq n$, then $U_{\langle 2,x\rangle}\subseteq U_{\langle 0,n\rangle}$.

• •

For $k(x,\langle 0,m\rangle,\langle 0,n\rangle)$:

• –

If $m=n$, then output $\langle 0,m\rangle$.

• –

If $m\neq n$ and either $x=m$ or $x=n$, then check if there is an $s\leq x$ such that $f(s)=x$. If so, output $\langle 2,x\rangle$. If not, output $\langle 0,x\rangle$.

• –

If $m\neq n$, $x\neq m$, and $x\neq n$, then output $\langle 2,x\rangle$.

• •

For $k(x,\langle 0,m\rangle,\langle 1,\langle n,s\rangle\rangle)$ and $k(x,\langle 1,\langle n,s\rangle\rangle,\langle 0,m\rangle)$: Output $\langle 1,\langle n,s\rangle\rangle$.

• •

For $k(x,\langle 0,m\rangle,\langle 2,s\rangle)$ and $k(x,\langle 2,s\rangle,\langle 0,m\rangle)$:

• –

If $x=m$, check if there is a $t\leq x$ such that $f(t)=x$. If so, output $\langle 2,x\rangle$. If not, output $\langle 0,x\rangle$.

• –

If $x\neq m$, output $\langle 2,x\rangle$.

• •

For $k(x,\langle 1,\langle m,s\rangle\rangle,\langle 1,\langle n,t\rangle\rangle)$, output $\langle 1,\langle m,s\rangle\rangle$.

• •

For $k(x,\langle 1,\langle m,s\rangle\rangle,\langle 2,t\rangle)$ and $k(x,\langle 2,t\rangle,\langle 1,\langle m,s\rangle\rangle)$, output $\langle 1,\langle m,s\rangle\rangle$.

• •

For $k(x,\langle 2,s\rangle,\langle 2,t\rangle)$, output $\langle 2,\max\{s,t\}\rangle$.

The space $(X,\mathcal{U},k)$ is discrete because for every $n$, either $U_{\langle 0,n\rangle}=\{n\}$ or there is an $s$ such that $U_{\langle 1,\langle n,s\rangle\rangle}=\{n\}$. Thus $(X,\mathcal{U},k)$ is not compact, and therefore it is not compact w.r.t. honest open covers. Let $h\colon\mathbb{N}\rightarrow I$ be such that $X=\bigcup_{m\in\mathbb{N}}U_{h(m)}$, but such that there is no $M\in\mathbb{N}$ for which $X=\bigcup_{m<M}U_{h(m)}$. Notice that every basic open set is either finite or cofinite. If $U_{h(m)}$ is cofinite for some $m$, then by using $\mathsf{B}\Sigma^{0}_{1}$ and the assumption $X=\bigcup_{m\in\mathbb{N}}U_{h(m)}$, we may conclude that there is an $M\in\mathbb{N}$ such that $X=\bigcup_{m<M}U_{h(m)}$, which is a contradiction. Thus $U_{h(m)}$ is finite for every $m$. Consider an $n\in X$. There must be an $m$ such that $n\in U_{h(m)}$. If there is an $s$ such that $f(s)=n$, then the only finite basic open set that contains $n$ is $U_{\langle 1,\langle n,s\rangle\rangle}$, so in this case it must be that $h(m)=\langle 1,\langle n,s\rangle\rangle$. If instead there is no $s$ such that $f(s)=n$, then the only finite basic open set that contains $n$ is $U_{\langle 0,n\rangle}$, so in this case it must be that $h(m)=\langle 0,n\rangle$. Therefore

[TABLE]

Thus the range of $f$ exists by $\Delta^{0}_{1}$-comprehension. ∎

Dorais’s [Dorais, Example 5.4] shows that, over $\mathsf{RCA}_{0}$, $\mathsf{ACA}_{0}$ is equivalent to the statement “every infinite countable second-countable space that is compact w.r.t. honest open covers and whose base has a finite cover relation is not discrete.” The proof of Proposition 3.10 may also be seen as a proof of this fact, as one may check that the constructed $\mathcal{U}$ has a finite cover relation.

This work concerns the order topologies of countable linear orders, which give natural examples of (strong) countable second-countable spaces.

Definition 3.11** ($\mathsf{RCA}_{0}$; [Dorais, Definition 7.1]).**

Let $(L,\prec)$ be a linear order. The base for the order topology on $L$ is given by $\mathcal{U}=(U_{i})_{i\in I}$ and $k:L\times I\times I\rightarrow I$, where

• •

$I=(L\cup\{-\infty,\infty\})\times(L\cup\{-\infty,\infty\})$,

• •

$U_{\langle a,b\rangle}=(a,b)=\{x\in L:a\prec x\prec b\}$, for $\langle a,b\rangle\in I$, and

• •

$k(x,\langle a_{0},b_{0}\rangle,\langle a_{1},b_{1}\rangle)=\langle\max(a_{0},a_{1}),\min(b_{0},b_{1})\rangle$ for $x\in L$ and $\langle a_{0},b_{0}\rangle,\langle a_{1},b_{1}\rangle\in I$.

The ordered space associated with $L$ is the countable second-countable space $(L,\mathcal{U},k)$.

In the above definition, $-\infty$ and $\infty$ are (codes for) two distinct fresh symbols not in $L$. We extend $\prec$ to $L\cup\{-\infty,\infty\}$ by setting $-\infty\prec x\prec\infty$ for all $x\in L$. Note that, as a matter of convenience, we allow $\langle a,b\rangle\in I$ even when $b\prec a$, in which case $U_{\langle a,b\rangle}=\emptyset$. As the basic open subsets of $L$ are particularly easy to describe, we dispense with the notational encumbrances of Definition 3.4 and simply write an enumeration of basic open sets as $((a_{n},b_{n}):n\in\mathbb{N})$, with the understanding that $a_{n},b_{n}\in L\cup\{-\infty,\infty\}$ for each $n$. Notice that the base of an ordered space always has a finite cover relation [Dorais, Proposition 7.5].

As mentioned above, Dorais observes that $\mathsf{RCA}_{0}$ proves that if the order topology of $(L,\prec)$ is compact w.r.t. honest open covers, then $(L,\prec)$ is complete.

Lemma 3.12** ([Dorais, Section 7]).**

$\mathsf{RCA}_{0}$* proves the statement “for every countable linear order $(L,\prec)$, if the order topology of $(L,\prec)$ is compact w.r.t. honest open covers, then $(L,\prec)$ is complete.” It follows that $\mathsf{RCA}_{0}$ also proves the statement “for every countable linear order $(L,\prec)$, if the order topology of $(L,\prec)$ is compact, then $(L,\prec)$ is complete.”*

Proof.

We prove the contrapositive. Suppose that $(L,\prec)$ is not complete, and let $A^{-}\cup A^{+}=L$ be a partition where $(\forall x\in A^{-})(\forall y\in A^{+})(x\prec y)$, but is such that $A^{-}$ has no maximum element and $A^{+}$ has no minimum element. Then any enumeration of the basic open sets of the form $(-\infty,b)$ for $b\in A^{-}$ and $(a,\infty)$ for $a\in A^{+}$ is an honest open cover of $L$ by basic open sets that has no finite subcover. Thus the order topology of $(L,\prec)$ is not compact w.r.t. honest open covers. ∎

We show the following in the next section.

• •

The statement “for every countable linear order $(L,\prec)$, if $(L,\prec)$ is complete, then the order topology of $(L,\prec)$ is compact w.r.t. honest open covers” is equivalent to $\mathsf{WKL}_{0}$ over $\mathsf{RCA}_{0}$.

• •

The statement “for every countable linear order $(L,\prec)$, if $(L,\prec)$ is complete, then the order topology of $(L,\prec)$ is compact” is equivalent to $\mathsf{ACA}_{0}$ over $\mathsf{RCA}_{0}$.

4. The strength of compactness for complete linear orders

First, we show that $\mathsf{WKL}_{0}$ proves that the order topology of a complete linear order is compact w.r.t. honest open covers. It follows that $\mathsf{ACA}_{0}$ proves that the order topology of a complete linear order is compact. The proof is essentially an implementation of the usual argument as found, for example, in the proof of [Munkres, Theorem 27.1].

Lemma 4.1**.**

$\mathsf{WKL}_{0}$* proves the statement “for every countable linear order $(L,\prec)$, if $(L,\prec)$ is complete, then the order topology of $(L,\prec)$ is compact w.r.t. honest open covers.”*

Proof.

We prove the contrapositive of the statement in $\mathsf{WKL}_{0}$. Suppose that the order topology of $(L,\prec)$ is not compact w.r.t. honest open covers, and let $((a_{n},b_{n}):n\in\mathbb{N})$ be an open cover of $L$ by basic open sets with no finite subcover. Assume that [math] is the minimum element of $L$ and that $1$ is the maximum element of $L$, for if either $L$ has no minimum or $L$ has no maximum, then $(L,\prec)$ is not complete, as desired.

Define a linkage in $L$ to be a finite sequence $((a_{n_{i}},b_{n_{i}}):i<k)$ of intervals from the cover such that $(\forall i<k-1)(a_{n_{i+1}}\prec b_{n_{i}}\prec b_{n_{i+1}})$. Say that an $\ell\in L$ is in a linkage $((a_{n_{i}},b_{n_{i}}):i<k)$ if $(\exists i<k)(a_{n_{i}}\prec\ell\prec b_{n_{i}})$ (i.e., if $\ell\in\bigcup_{i<k}(a_{n_{i}},b_{n_{i}})$). Notice that no linkage contains both [math] and $1$ because such a linkage would be a finite subcover of $((a_{n},b_{n}):n\in\mathbb{N})$. A straightforward application of $\Pi^{0}_{1}$ induction on the length of a linkage shows that the union of a linkage is an interval, meaning that if $((a_{n_{i}},b_{n_{i}}):i<k)$ is a linkage, if $x$ and $y$ are both in the linkage, and if $x\prec y$, then every $z\in(x,y)$ is also in the linkage.

We define the tree $T\subseteq 2^{<\mathbb{N}}$ consisting of all sequences $\sigma$ that look like initial segments of sets that contain [math], do not contain $1$, are $\prec$-downward-closed, and are closed under linkages. Let $T$ be the set of all $\sigma\in 2^{<\mathbb{N}}$ satisfying the following conditions.

• •

If $|\sigma|>0$, then $\sigma(0)=1$.

• •

If $|\sigma|>1$, then $\sigma(1)=0$.

• •

For all $x<|\sigma|$, if $x\notin L$, then $\sigma(x)=0$.

• •

For all $x,y<|\sigma|$, if $x,y\in L$, $x\prec y$, and $\sigma(y)=1$, then $\sigma(x)=1$.

• •

For all $x,y<|\sigma|$ and for all finite sequences $\langle n_{i}:i<k\rangle<|\sigma|$, if $x,y\in L$, if $((a_{n_{i}},b_{n_{i}}):i<k)$ is a linkage containing both $x$ and $y$, and if $\sigma(y)=1$, then $\sigma(x)=1$.

$T$ is $\Delta^{0}_{1}$ relative to $(L,\prec)$ and hence exists by $\Delta^{0}_{1}$ comprehension. It is easy to see that $T$ is closed under initial segments and hence is a tree. We show that $T$ is infinite. To this end, let $n\in\mathbb{N}$, and let

[TABLE]

The set $D$ exists by bounded $\Sigma^{0}_{1}$ comprehension. Let $\sigma\in 2^{<\mathbb{N}}$ be the sequence of length $n$ where, for all $x<n$, $\sigma(x)=1$ if $x\in D$ and $\sigma(x)=0$ if $x\notin D$. Then $\sigma\in T$, which can be seen by noticing that $0\in D$ (if $n>0$); that $1\notin D$ because [math] and $1$ are not in a linkage together; and that $D$ is $\prec$-downwards closed in $L\cap\{0,1,\dots,n-1\}$ because the union of any linkage containing [math] is an initial segment of $L$. Therefore, for every $n$ there is a $\sigma\in T$ with $|\sigma|=n$. Hence $T$ is infinite.

Thus $T$ is an infinite subtree of $2^{<\mathbb{N}}$. Apply weak König’s lemma to $T$ to get an infinite path, and view that path as the characteristic function of a set $X\subseteq L$. $X$ contains [math], does not contain $1$, is $\prec$-downward-closed, and is closed under linkages. By setting $A^{-}=X$ and $A^{+}=L\setminus X$, we obtain a partition $L=A^{-}\cup A^{+}$ where $0\in A^{-}$, $1\in A^{+}$, and $(\forall x\in A^{-})(\forall y\in A^{+})(x\prec y)$.

We show that $A^{-}$ has no maximum element and that $A^{+}$ has no minimum element. First, suppose for a contradiction that $A^{-}$ has a maximum element $\ell$. As $((a_{n},b_{n}):n\in\mathbb{N})$ is a cover, let $(a_{n_{0}},b_{n_{0}})$ be such that $\ell\in(a_{n_{0}},b_{n_{0}})$. We cannot have that $b_{n_{0}}=\infty$, for otherwise $\ell$ and $1$ are both in the linkage $(a_{n_{0}},b_{n_{0}})$, which implies that $1\in A^{-}$ because $A^{-}$ is linkage-closed. Thus $b_{n_{0}}\in L$, so let $(a_{n_{1}},b_{n_{1}})$ be such that $b_{n_{0}}\in(a_{n_{1}},b_{n_{1}})$. Then $(a_{n_{0}},b_{n_{0}}),(a_{n_{1}},b_{n_{1}})$ is a linkage containing both $\ell$ and $b_{n_{0}}$. Thus $b_{n_{0}}\succ\ell$ is in $A^{-}$ because $A^{-}$ is linkage-closed. This contradicts that $\ell$ is the maximum of $A^{-}$. Now suppose for a contradiction that $A^{+}$ has a minimum element $\ell$. Again by the fact that $((a_{n},b_{n}):n\in\mathbb{N})$ is a cover, let $(a_{m_{1}},b_{m_{1}})$ be such that $\ell\in(a_{m_{1}},b_{m_{1}})$. We cannot have that $a_{m_{1}}=-\infty$, for otherwise [math] and $\ell$ are both in the linkage $(a_{m_{1}},b_{m_{1}})$, which implies that $\ell\in A^{-}$ because $0\in A^{-}$ and $A^{-}$ is linkage-closed. Thus $a_{m_{1}}\in L$, so let $(a_{m_{0}},b_{m_{0}})$ be such that $a_{m_{1}}\in(a_{m_{0}},b_{m_{0}})$. Then either $b_{m_{0}}\prec b_{m_{1}}$, in which case $(a_{m_{0}},b_{m_{0}}),(a_{m_{1}},b_{m_{1}})$ is a linkage containing both $\ell$ and $a_{m_{1}}$; or $b_{m_{0}}\succeq b_{m_{1}}$, in which case $(a_{m_{0}},b_{m_{0}})\supseteq(a_{m_{1}},b_{m_{1}})$ is a linkage containing both $\ell$ and $a_{m_{1}}$. Thus $a_{m_{1}}$ is in a linkage with $\ell$. However, $a_{m_{1}}\in A^{-}$ because $a_{m_{1}}\prec\ell$ and $\ell$ is the minimum element of $A^{+}$. This contradicts that $A^{-}$ is linkage-closed. Thus $A^{-}$ has no maximum element, and $A^{+}$ has no minimum element. So $A^{-}$ and $A^{+}$ witness that $(L,\prec)$ is not complete. ∎

Corollary 4.2**.**

$\mathsf{ACA}_{0}$* proves the statement “for every countable linear order $(L,\prec)$, if $(L,\prec)$ is complete, then the order topology of $(L,\prec)$ is compact.”*

Proof.

$\mathsf{ACA}_{0}$ proves $\mathsf{WKL}_{0}$ and that a countable second-countable space is compact if and only if it is compact w.r.t. honest open covers. ∎

We now give the reversals. The strategy is as follows. First, recall the Kleene-Brouwer ordering of finite sequences: $\sigma\leq_{\mathrm{KB}}\tau$ if either $\sigma$ is an extension of $\tau$ or $\sigma$ is to the left of $\tau$. That is, $\sigma\leq_{\mathrm{KB}}\tau$ if

[TABLE]

Now, let $T\subseteq\mathbb{N}^{<\mathbb{N}}$ be an infinite finitely-branching tree. In the case of $\mathsf{ACA}_{0}$, we show that the order topology of $(T,<_{\mathrm{KB}})$ is discrete, hence not compact. In the case of $\mathsf{WKL}_{0}$, we additionally assume that $T$ is bounded, and we show that the order topology of $(T,<_{\mathrm{KB}})$ is effectively discrete, hence not compact w.r.t. honest open covers. In both cases, we conclude that $(T,<_{\mathrm{KB}})$ is not complete, which lets us extract an infinite path through $T$ from a witnessing partition. The idea of last step of this this strategy, to use a certain partition of a linear order on $T$ to find a path through $T$, also appears in Simpson and Yokoyama’s analysis of Peano categoricity [SimpsonYokoyama].

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

Let $T\subseteq\mathbb{N}^{<\mathbb{N}}$ be an infinite, finitely-branching tree, and for each $\sigma\in T$, let $T_{\sigma}=\{\tau\in T:\tau\supseteq\sigma\}$ denote the full subtree of $T$ above $\sigma$. Assume that every $T_{\sigma}$ has a $<_{\mathrm{KB}}$-least element. Then the order topology of $(T,<_{\mathrm{KB}})$ is discrete. Moreover, if $T$ is bounded, then the order topology of $(T,<_{\mathrm{KB}})$ is effectively discrete.

Proof.

The lemma follows from two claims.

Claim**.**

If $\sigma\in T$ is not $<_{\mathrm{KB}}$-least, then $\sigma$ has a $<_{\mathrm{KB}}$-immediate predecessor. If $T$ is bounded, then the $<_{\mathrm{KB}}$-immediate predecessor can be found effectively. That is, if $T$ is bounded, then there is a function $\ell\colon T\rightarrow T\cup\{-\infty\}$ such that

[TABLE]

Proof of claim.

Consider a $\sigma\in T$ that is not $<_{\mathrm{KB}}$-least. If $\sigma$ is not a leaf, then its rightmost child is its $<_{\mathrm{KB}}$-immediate predecessor. In this case, the rightmost child exists because $T$ is finitely-branching.

Suppose that $\sigma$ is a leaf. Let $i<|\sigma|$ be greatest such that for some $m<\sigma(i)$, $(\sigma{\restriction}i)^{\smallfrown}m\in T$. Such an $i$ exists by the assumption that $\sigma$ is not $<_{\mathrm{KB}}$-least (and that $\sigma$ is a leaf). Given this greatest $i$, let $m<\sigma(i)$ be greatest such that $(\sigma{\restriction}i)^{\smallfrown}m\in T$. Then this $\tau=(\sigma{\restriction}i)^{\smallfrown}m$ is $\sigma$’s $<_{\mathrm{KB}}$-immediate predecessor. To see this, suppose that $\alpha<_{\mathrm{KB}}\sigma$ for some $\alpha\in T$. Let $j$ be such that $\alpha{\restriction}j=\sigma{\restriction}j$ and $\alpha(j)<\sigma(j)$. Then $j\leq i$ by the maximality of $i$. If $j=i$, then $\alpha\leq_{\mathrm{KB}}\tau$ by the maximality of $m$. If $j<i$, then $\alpha<_{\mathrm{KB}}\tau$ because $\alpha{\restriction}j=\sigma{\restriction}j=\tau{\restriction}j$ but $\alpha(j)<\sigma(j)=\tau(j)$.

If $T$ is bounded by $f$, then $f$ can be used to determine whether or not $\sigma$ is a leaf and, if not, determine $\sigma$’s rightmost child. If $\sigma$ is a leaf, no further use of $f$ is required to produce the $<_{\mathrm{KB}}$-immediate predecessor $\tau$ because in this case $\sigma$ itself provides the necessary bounds. ∎

Claim**.**

If $\sigma\in T$ is not $<_{\mathrm{KB}}$-greatest (i.e., if $\sigma\neq\emptyset$), then $\sigma$ has a $<_{\mathrm{KB}}$-immediate successor. If $T$ is bounded, then the $<_{\mathrm{KB}}$-immediate successor can be found effectively. That is, if $T$ is bounded, then there is a function $r\colon T\rightarrow T\cup\{\infty\}$ such that

[TABLE]

Proof of claim.

Here we use the ad hoc notation ‘$\alpha\operatorname{{!}}i$’ to denote the sequence obtained by changing the last entry of $\alpha\neq\emptyset$ to $i$.

Consider a $\sigma\in T$ that is not $\emptyset$. If there is no $m>\sigma(|\sigma|-1)$ such that $\sigma\operatorname{{!}}m\in T$, then $\sigma{\restriction}(|\sigma|-1)$ is $\sigma$’s $<_{\mathrm{KB}}$-immediate successor.

If there is an $m>\sigma(|\sigma|-1)$ such that $\sigma\operatorname{{!}}m\in T$, then let $m$ be the least such $m$. Then $\sigma$’s $<_{\mathrm{KB}}$-immediate successor is the $<_{\mathrm{KB}}$-least element $\tau$ of $T_{\sigma\operatorname{{!}}m}$, which exists by assumption. To see this, suppose that $\alpha>_{\mathrm{KB}}\sigma$ for some $\alpha\in T$. If $\alpha\subsetneq\sigma$, then $\alpha\subsetneq\sigma\operatorname{{!}}m\subseteq\tau$, so $\alpha>_{\mathrm{KB}}\tau$. Otherwise, there is a $j$ such that $\alpha{\restriction}j=\sigma{\restriction}j$ and $\alpha(j)>\sigma(j)$. If $j<|\sigma|-1$, then $\alpha>_{\mathrm{KB}}\sigma\operatorname{{!}}m\geq_{\mathrm{KB}}\tau$. If $j=|\sigma|-1$, then either $\alpha(j)>m$ or $\alpha(j)=m$. If $\alpha(j)>m$, then again $\alpha>_{\mathrm{KB}}\sigma\operatorname{{!}}m\geq_{\mathrm{KB}}\tau$. If $\alpha(j)=m$, then $\alpha\in T_{\sigma\operatorname{{!}}m}$, so $\alpha\geq_{\mathrm{KB}}\tau$ by the choice of $\tau$.

If $T$ is bounded by $f$, then $f$ can be used to determine whether or not there is an $m>\sigma(|\sigma|-1)$ with $\sigma\operatorname{{!}}m\in T$. Furthermore, $f$ can be used to find the $<_{\mathrm{KB}}$-least element of any subtree $T_{\eta}$. The $<_{\mathrm{KB}}$-least element of $T_{\eta}$ is the leftmost leaf of $T_{\eta}$, which can be found by starting at $\eta$ and following the leftmost child until reaching a leaf. The bound $f$ can be used to determine whether or not a given element of $T$ is a leaf, so this search is effective. ∎

Consider now the order topology of $(T,<_{\mathrm{KB}})$, and consider a $\sigma\in T$. If $\sigma$ is neither $<_{\mathrm{KB}}$-least nor $<_{\mathrm{KB}}$-greatest, then $\sigma$ has a $<_{\mathrm{KB}}$-immediate predecessor $\tau$ and a $<_{\mathrm{KB}}$-immediate successor $\eta$. In this case, $\{\sigma\}=(\tau,\eta)$ is a basic open set. If $\sigma$ is $<_{\mathrm{KB}}$-least, then $\sigma$ has a $<_{\mathrm{KB}}$-immediate successor $\eta$. In this case, $\{\sigma\}=(-\infty,\eta)$ is a basic open set. If $\sigma$ is $<_{\mathrm{KB}}$-greatest, then $\sigma$ has a $<_{\mathrm{KB}}$-immediate predecessor $\tau$. In this case $\{\sigma\}=(\tau,\infty)$ is a basic open set. Thus the order topology of $(T,<_{\mathrm{KB}})$ is discrete. Furthermore, if $T$ is bounded, then $\{\sigma\}=(\ell(\sigma),r(\sigma))$ for every $\sigma\in T$. Thus the order topology of $(T,<_{\mathrm{KB}})$ is effectively discrete via the function $d(\sigma)=\langle\ell(\sigma),r(\sigma)\rangle$. ∎

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

Let $T\subseteq\mathbb{N}^{<\mathbb{N}}$ be an infinite finitely-branching tree. If the linear order $(T,<_{\mathrm{KB}})$ is not complete, then $T$ has an infinite path.

Proof.

Let $A^{-}$ and $A^{+}$ witness that $(T,<_{\mathrm{KB}})$ is not complete. Notice that $A^{+}$ is non-empty (because $\emptyset\in A^{+}$, as otherwise it would be the greatest element of $A^{-}$) and that $A^{+}$ is closed under initial segments (because it is $<_{\mathrm{KB}}$-upward closed). Define a set $X\subseteq\mathbb{N}^{<\mathbb{N}}$ by putting $\sigma\in X$ if and only if

[TABLE]

For every $n$, the set $X$ contains at most one sequence of length $n$, which can be seen from the definition of $X$ and the fact that $A^{+}$ is closed under initial segments. Using $\mathsf{I}\Sigma^{0}_{1}$, we show that, for every $n$, $X$ contains at least one sequence of length $n$. For the base case, $\emptyset$ is a sequence in $X$ of length [math]. For the inductive case, suppose that $X$ contains a sequence $\sigma$ of length $n$. Then $\sigma\in A^{+}$ and, as $A^{+}$ has no $<_{\mathrm{KB}}$-least element, there must be a sequence $\tau\in A^{+}$ with $\tau<_{\mathrm{KB}}\sigma$. The sequence $\tau$ cannot be to the left of $\sigma$ because this would contradict $\sigma\in X$. Therefore it must be that $\tau\supseteq\sigma$. It follows that there is an $m$ such that $\sigma^{\smallfrown}m\in A^{+}$. Let $m$ be least such that $\sigma^{\smallfrown}m\in A^{+}$. Then $\sigma^{\smallfrown}m$ is in $X$ and has length $n+1$. This completes the induction.

The set $X$ thus contains exactly one sequence of each length. As $X$ is closed under initial segments, it follows that if $\sigma,\tau\in X$ are such that $|\sigma|\leq|\tau|$, then $\sigma\subseteq\tau$. Thus if we let $\sigma_{i}$ be the sequence in $X$ of length $i$, then $\sigma_{0}\subseteq\sigma_{1}\subseteq\sigma_{2}\subseteq\cdots$ defines an infinite path through $T$. ∎

Theorem 4.5**.**

1. (i)

The statement “for every countable linear order $(L,\prec)$, if $(L,\prec)$ is complete, then the order topology of $(L,\prec)$ is compact w.r.t. honest open covers” is equivalent to $\mathsf{WKL}_{0}$ over $\mathsf{RCA}_{0}$. 2. (ii)

The statement “for every countable linear order $(L,\prec)$, if $(L,\prec)$ is complete, then the order topology of $(L,\prec)$ is compact” is equivalent to $\mathsf{ACA}_{0}$ over $\mathsf{RCA}_{0}$.

Proof.

The forward direction of item (i) is Lemma 4.1, and the forward direction of item (ii) is Corollary 4.2.

For the reversal of item (ii), let $T\subseteq\mathbb{N}^{<\mathbb{N}}$ be an infinite finitely-branching tree. By Theorem 2.2 item (i), it suffices to show that $T$ has an infinite path. Recall that, for $\sigma\in T$, $T_{\sigma}=\{\tau\in T:\tau\supseteq\sigma\}$ denotes the full subtree of $T$ above $\sigma$. Suppose that there is a $\sigma\in T$ such that $T_{\sigma}$ has no $<_{\mathrm{KB}}$-least element. Then setting $A^{-}=\emptyset$ and $A^{+}=T_{\sigma}$ gives a partition of $T_{\sigma}$ witnessing that the linear order $(T_{\sigma},<_{\mathrm{KB}})$ is not complete. By Lemma 4.4, there is an infinite path through $T_{\sigma}$, which is an infinite path through $T$. Suppose instead that $T_{\sigma}$ has a $<_{\mathrm{KB}}$-least element for every $\sigma\in T$. Then the order topology of $(T,<_{\mathrm{KB}})$ is discrete by Lemma 4.3. Therefore the order topology of $(T,<_{\mathrm{KB}})$ is not compact. We assume that the order topology of a complete linear order is compact, so $(T,<_{\mathrm{KB}})$ is not complete. Therefore $T$ has an infinite path by Lemma 4.4.

The reversal of item (i) is analogous. Let $T\subseteq\mathbb{N}^{<\mathbb{N}}$ be an infinite bounded tree. By Theorem 2.2 item (ii), it suffices to show that $T$ has an infinite path. As above, if there is a $\sigma\in T$ such that $T_{\sigma}$ has no $<_{\mathrm{KB}}$-least element, then the linear order $(T_{\sigma},<_{\mathrm{KB}})$ is not complete, so $T_{\sigma}$, and therefore $T$, has an infinite path by Lemma 4.4. If $T_{\sigma}$ has a $<_{\mathrm{KB}}$-least element for every $\sigma\in T$, then the order topology of $(T,<_{\mathrm{KB}})$ is effectively discrete by Lemma 4.3. Therefore the order topology of $(T,<_{\mathrm{KB}})$ is not compact w.r.t. honest open covers. Therefore the linear order $(T,<_{\mathrm{KB}})$ is not complete. Therefore $T$ has an infinite path by Lemma 4.4. ∎

Acknowledgments

We thank François Dorais and Giovanni Soldà for helpful discussions. This project was partially supported by a grant from the John Templeton Foundation (“A new dawn of intuitionism: mathematical and philosophical advances” ID 60842). The opinions expressed in this work are those of the author and do not necessarily reflect the views of the John Templeton Foundation.