On the necessity of some topological spaces

Abstract

Topological models are sometimes used to prove independence results in constructive mathematics. Here we show that some of the topologies that have been used are necessary for those results.

Keywords

Constructive mathematics topological models

1. Introduction

The motivation behind reverse math is the foundational question whether, if a certain method, broadly understood, is used to prove a theorem, that method is in some sense necessary. The cleanest kind of result, when the “method” is a hypothesis, is that the theorem implies the hypothesis. A similar kind of result obtains when the “method” in question is the use of a certain object, and you show that any procedure which ends in that theorem must use that object. That is the goal of this work.

The framework we will be using is topological models for constructive mathematics. (A brief introduction to topological models, with references, is given in a sub-section at the end of this introduction.) If you want an independence result, like ϕ does not imply ψ, then you could show this by developing a topological space $T$ such that the model built over $T$ satisfies ϕ and not ψ. What we would like to show here is that if the model built over any space $U$ similarly satisfies ϕ and not ψ then $U$ in some sense induces $T$ . This is familiar from forcing: if G is $P$ -generic, and $H \in V [G]$ is $Q$ -generic, then (the complete Boolean algebra generated by) $Q$ is a sub-algebra of (the cBa generated by) $P$ (see for instance [10], 15.42–15.45). What corresponds to a cBa $P$ in our setting is the complete Heyting algebra of the open sets of $U$ . So the way $T$ sits inside of $U$ should be so that the opens of $T$ are a sub-cHa of those of $U$ .

One way this could happen is if $U$ is $T \times V$ . (That could be the case for instance if ϕ is made true by the existence of an object generic over $T$ . A generic for $U$ is a pair of generics for $T$ and $V$ .) Then $T$ is a quotient space of $U$ . Or if $U$ is the disjoint union $T ⊎ V$ (which could be the case if forcing with $V$ also satisfies ϕ), in which case $T$ is a subspace of $U$ .

A limitation of the efforts here is that we consider only topological models. A slight extension would include arbitrary Heyting-valued models, accounting for Heyting algebras that are not spatial. More broadly than that, there are other constructions of constructive models, such as realizability and Kripke models. Moreover, these various methods can be mixed and matched, such as a Kripke model built using cHa extensions of a realizability model. They are all instances of Krivine’s classical realizability [11,12], a construction method that covers all of those mentioned thus far, classical forcing included. That could be a setting in which one could hope to show that any construction which has a given property must of necessity contain a certain core. It is not clear that such will always be possible. For instance, the two known models separating Decidable Fan from c-Fan [1,16] are very different from each other, making it unclear that in that case there is a common core to that separation. No doubt in other cases there is a common core. This is all left for future work.

Regarding the meta-theory used here, if push comes to shove it is taken to be ZFC. To illustrate why, at one point we come up with an ultrafilter, which is known to require a certain amount of Choice. There are constructive work-arounds to ultrafilters, so no doubt matters could be re-formulated and done more carefully to stay within constructive set theory. That is not the purpose of this paper.

This section continues with a brief introduction to topological models in general, and a summary of the principles we will be analyzing. Each of the next three sections extracts a topological consequence from a separation of those principles. The penultimate section examines the separation of the Cauchy and Dedekind reals. The final section suggests some possibilities for future work along these lines, especially in connection with BD-N.

This article is an extension of [17]. The only significant difference is the inclusion here of Section 5, the study of the reals. Thanks are to be given to Matt Hendtlass, who was the inspiration for this work. He came up with the idea for this project, and proved the chronologically first theorem, Theorem 2 here. May he come back!

1.1. Topological models

Forcing in set theory can be described as Boolean-valued models, built over complete Boolean algebras. The reason that Boolean algebras are used here is that they exactly characterize classical logic. If what you want is instead constructive logic, the appropriate structures are Heyting algebras. Heyting-valued models, built over complete Heyting algebras (cHa’s), can be developed just like Boolean-valued models. The open sets of a topological space form a cHa; the Heyting-valued model built over such a cHa is called a topological model. The opens of a topological space form what is called a spatial Heyting algebra; not every cHa is spatial. Although there is a prior history of topological semantics, Heyting-valued semantics for set theory were fully developed in [4]; a more recent and perhaps more accessible account for topological models is given in [5], which also contains most of the independence proofs referenced in this paper. To help make this current work more self-contained, the basic definitions of these models from the latter paper are given below.

Topological models are Heyting valued models where the complete Heyting algebra is the lattice of opens $O_{T}$ of a topological space $T$ . (By way of notation, we take $T$ to be the set of points of the space, i.e. the largest open set, or $⋃_{O \in O_{T}} O$ . Strictly speaking, most authors might take the space to be $⟨ T, O_{T} ⟩$ .) Meet and join in $O_{T}$ are given by intersection and union respectively, while the pseudo-complement → is defined by $\begin{matrix} U \to V \equiv {(- U \cup V)}^{\circ}, \end{matrix}$ where $- U$ denotes the complement of $U$ in $T$ and $W^{\circ}$ denotes the interior of $W$ . The full topological model over $T$ consists of the class of names or terms, defined inductively by $\begin{aligned} V_{α} (T) = P (⋃ {V_{ν} (T) \times O_{T} : ν \in α}), \\ V (T) = ⋃_{α \in ORD} V_{α} (T) . \end{aligned}$ Given $σ \in V_{α} (T)$ , the meaning of $⟨ τ, U ⟩ \in σ$ is that $U$ is the degree of truth, or truth-value, of τ being in σ. (Of course, the ultimate value of $τ \in σ$ might be greater than $U$ , depending on what else is in σ.) The idea of the full model is to throw in absolutely everything you can. We will have occasion to look at sub-models of the full model. An embedding $\overset{ˇ}{\cdot}$ of the ground model V into $V (T)$ is defined inductively by $\begin{matrix} \overset{ˇ}{a} = {⟨ \overset{ˇ}{b}, T ⟩ : b \in a} . \end{matrix}$

The truth value of any proposition A, with parameters from $V (T)$ , is an open subset of $T$ and is denoted by $⟦ A ⟧$ . To say that a proposition A is true, or satisfied, in a topological model $M_{T}$ over $T$ means $⟦ A ⟧ = T$ , otherwise A is said to fail in $M_{T}$ . Being false in $M_{T}$ is a stronger property: A is said to be false in $M_{T}$ if $M_{T}$ satisfies $\neg A$ , or equivalently $⟦ A ⟧ = \emptyset$ . We freely switch between truth value notation $⟦ \cdot ⟧$ for topological models and forcing notation: a point $x \in T$ forces a formula A, written $x ⊩ A$ , if and only if $x \in ⟦ A ⟧$ , and, for an open subset $U$ of $T$ , $U ⊩ A$ if and only if $U \subset ⟦ A ⟧$ .

A particularly important object, the generic, in a topological model $M_{T}$ is described by the name $\begin{matrix} G = {⟨ \overset{ˇ}{U}, U ⟩ : U \in O_{T}} . \end{matrix}$ Strictly speaking, the generic contains as its members open sets from the ground model, being characterised by $\begin{matrix} U ⊩ \overset{ˇ}{U} \in G \end{matrix}$ for all $U \in O_{T}$ . In practice though, it is more useful to think of the generic as a new element of the topological space over which we are forcing. A point in a Hausdorff space is determined by its open neighborhoods, and so could be thought of as the set consisting of all of those neighborhoods. Similarly, in the other direction, $\overset{ˇ}{U} \in G$ can fruitfully be thought of as $G \in U$ . Of course, since G is not in the ground model, $G \in \overset{ˇ}{U}$ is just false. Instead, one may think of $U$ as being given by a description, and then $“ G \in U$ ” would mean that G satisfies this description, as interpreted in the extension. For instance, if $T$ is the reals, then $U$ might be the interval $(p, q)$ with rational endpoints; G could be thought of as a generic real number, and $\overset{ˇ}{U} \in G$ could be read as meaning $p < G < q$ .

IZF, Intuitionistic ZF, is a ZF-style axiomatization of set theory using constructive logic, which is equivalent with ZF under classical logic.

Theorem 1 (Grayson).

Topological models preserve IZF; that is, IZF proves that the full topological model $V (T)$ satisfies the axioms of IZF.

1.2. Summary of constructive principles

BD-N: Every countable, pseudo-bounded set of natural numbers is bounded. (See the last section for the definition of pseudo-boundedness.)

LLPO, the Lesser Limited Principle of Omniscience: Every binary sequence with at most one 1 has either all the even slots 0 or all the odds 0.

LPO, the Limited Principle of Omniscience: Every binary sequence is either all 0s or has a 1 in it.

MP, Markov’s Principle: If it is impossible for every value in a binary sequence to be 0, then there is one value which is 1.

WLEM, the Weak Law of the Excluded Middle: For any proposition A, either $\neg A$ or $\neg \neg A$ .

WLEM $_{ω}$ : For any countable sequence of propositions, if it is impossible that for any distinct pair of them both are true, then one of them must be false; $\neg ⋁_{i, j \in ω, i \neq j} A_{i} \land A_{j} \to ⋁_{i} \neg A_{i}$ .

WMP, Weak Markov’s Principle: $\begin{matrix} \forall γ [\forall β (\neg \neg \exists n (β (n) = 1) \lor \neg \neg \exists n (γ (n) = 1 \land β (n) = 0)) \to \exists n γ (n) = 1] . \end{matrix}$

For the convenience of the reader, these principles are repeated where they are used.

2. The coarse topology on $ω^{+}$

The first example we will consider may as well be the simplest. Let $ω^{+}$ be $ω \cup {*}$ . We extend the discrete topology on ω (under which every set is open) in the coarsest possible way to $ω^{+}$ by letting the entire space be the only open neighborhood of ∗. When we refer to $ω^{+}$ as a topological space, we mean this coarse topology.

The Limited Principle of Omniscience, LPO, states that every binary sequence is either all 0s or has a 1 in it. A weakening of the Weak Law of the Excluded Middle, WLEM $_{ω}$ is the assertion that, for any countable sequence of propositions, if it is impossible that for any distinct pair of them both are true, then one of them must be false.

It is shown in [5], Theorem 4.1, that LPO does not imply WLEM $_{ω}$ , by showing that in the topological model over $ω^{+}$ LPO holds while ∗ does not force WLEM $_{ω}$ (meaning no neighborhood of ∗ forces as much). We show that any topological space with a point not forcing WLEM $_{ω}$ induces $ω^{+}$ .

Theorem 2.
If $x \in T$ and $x ⊮$ WLEM $_{ω}$ then a quotient space of $T$ is isomorphic to $ω^{+}$ .
Proof.
By the failure of WLEM $_{ω}$ at x, there is a neighborhood $O$ of x and a sequence of $A_{i}$ ( $i \in ω$ ) of propositions such that $O$ forces that no pair $A_{i}$ , $A_{j}$ ( $i \neq j$ ) are both true, but $O$ does not force that one is false. Without loss of generality we take each open set $⟦ A_{i} ⟧$ , which is best thought of as the truth value of $A_{i}$ , to be a subset of $O$ , since we could replace $⟦ A_{i} ⟧$ by $⟦ A_{i} ⟧ \cap O$ . Since $O$ forces no pair to be true, $⟦ A_{i} ⟧ \cap ⟦ A_{j} ⟧ = \emptyset$ . Since $O$ does not force one to be false, the union $⋃_{i} ⟦ \neg A_{i} ⟧$ is not all of $O$ . So there is some point, let’s call it ∞, which is in no $⟦ \neg A_{i} ⟧$ . That means that ∞ is in the closure of each $⟦ A_{i} ⟧$ . Furthermore, ∞ is in no $⟦ A_{i} ⟧$ , since the closure of $⟦ A_{j} ⟧$ is the smallest closed set containing $⟦ A_{j} ⟧$ , and one such closed set is the complement of $⟦ A_{i} ⟧$ . So ∞ is in the boundary of each $⟦ A_{i} ⟧$ . Take the quotient space that sends all of $⟦ A_{i} ⟧$ to one point, call it i, and everything not in any $⟦ A_{i} ⟧$ to ∗. Notice that ∞ goes to ∗. In the quotient topology, each i is open, because its inverse image is $⟦ A_{i} ⟧$ . Now consider a set X containing ∗ and missing some i. The inverse image of X contains ∞, which is in the boundary of $⟦ A_{i} ⟧$ , yet is disjoint from $⟦ A_{i} ⟧$ , and so is not open. That yields that the only possible open neighborhood of ∗ cannot miss any i. Trivially, the inverse image of the entire quotient is all of $T$ , and so the quotient space is open. Hence the quotient space is $ω^{+}$ . □

3. The necessity of ultrafilters

Theorem 5.1 of [5] is that WLEM does not imply WMP, Weak Markov’s Principle. The topological model that is used for this is based on a non-principal ultrafilter of ω. This is unsettling, because the existence of ultrafilters needs some amount of Choice, but the independence of WMP from WLEM should not depend on Choice. Are the ultrafilters just a trick which happens to work? Or are they somehow fundamental to the questions at hand?

In the following, we will work with LLPO, which follows from WLEM, and LPO, from which WMP follows. LLPO, the Lesser Limited Principle of Omniscience, states that every binary sequence with at most one 1 has either all the even slots 0 or all the odds 0. The construction that WLEM does not imply WMP yields trivially that LLPO does not imply LPO.

Lemma 1.
A point x in a topological space $T$ does not force LPO if and only if there exists a sequence ${(C_{n})}_{n \in ω}$ of clopen subsets of $T$ such that $\begin{matrix} x \notin {(⋂_{n \in ω} C_{n})}^{\circ} \cup ⋃_{n \in ω} - C_{n} . \end{matrix}$
Proof.
Let α be a counterexample to LPO at x. (Without loss of generality, $T ⊩ α \in 2^{ω}$ .) Let $C_{n}$ be $⟦ α (n) = 0 ⟧$ . Then ${(⋂_{n \in ω} C_{n})}^{\circ} ⊩ \forall n α (n) = 0$ , while $⋃_{n \in ω} - C_{n} ⊩ \exists n α (n) = 1$ ; whence x is in neither of these sets.

In the other direction, given such a sequence $C_{n}$ , define α to be the term such that $⟦ α (n) = 0 ⟧ = C_{n}$ . □

We will call a topological space an ultrafilter topology on ω if (up to homeomorphism) the underlying set is $ω \cup {}$ ( $ \notin ω$ ), the subspace ω carries the discrete topology, and for some ultrafilter $U$ , the neighborhoods of ∗ are of the form ${} \cup u$ where $u \in U$ .
Theorem 3.
If $x \in T$ forces LLPO and not LPO, then a subset of* $T$ has a quotient space with an ultrafilter topology on ω.
Proof.
Since x does not force LPO, let $C_{n}$ be a sequence of clopens as in the previous lemma. Without loss of generality we can take $C_{0}$ to be $T$ and the sequence to be strictly decreasing: $C_{0} ⊋ C_{1} ⊋ \dots$ . Of course, $⋂_{n \in ω} C_{n}$ has a non-empty boundary, because it contains x in particular. In the following construction, anything else in the boundary might be trouble (an example follows the proof). So consider the subspace of $T$ with those other points removed. In other words, we want $⋂_{n \in ω} C_{n} ∖ {x}$ to be open. We recycle notation, and call this subspace $T$ also.

Let $O_{n}$ be $C_{n} ∖ C_{n + 1}$ . Notice $⋃_{n \in ω} O_{n} = T ∖ ⋂_{n \in ω} C_{n}$ . Let f send $O_{n}$ to n and $⋂_{n \in ω} C_{n}$ to ∗. We claim that the induced quotient topology on $ω \cup {}$ is an ultrafilter topology.

For starters, ω carries the discrete topology, because each $O_{n}$ is (clopen and therefore in particular) open. As for neighborhoods of ∗, first, ${} \cup ω$ is open because its inverse image is all of $T$ . Also, ${}$ is not open because its inverse image is $⋂_{n \in ω} C_{n}$ , which contains x as a member, but x is not in the interior. As for closure under intersection, if the inverse images of both ${} \cup u$ and ${} \cup v$ are open, then the inverse image of ${} \cup (u \cap v)$ is open, being the intersection of two open sets.

Finally, suppose $v = ω ∖ u$ . We must show the inverse image of either ${} \cup u$ or ${} \cup v$ is open. We can safely assume both u and v are infinite. Let g and h enumerate u and v respectively. Let α be such that $⟦ α (2 n) = 1 ⟧ = O_{g (n)}$ and $⟦ α (2 n + 1) = 1 ⟧ = O_{h (n)}$ . Since x forces LLPO, some neighborhood of x, say $N$ , forces either all of α’s even entries or all of α’s odds to be 0. Say it’s the evens. Then $N$ is a subset of the inverse image of ${} \cup v$ . Hence the latter set is itself open, being the union of $N$ with the open sets $O_{h (n)}$ and ${(⋂_{n \in ω} C_{n})}^{\circ}$ . □

To see why we had to throw the boundary points away, consider the following variant of the ultrafilter topology on ω. The underlying set is $ω \cup {, ⊥}$ , the neighborhoods of ∗ are as before, and the neighborhoods of ⊥ include ∗ and a cofinite subset of ω. If ⊥ is not thrown away, the ultrafilter is obscured.
4. The necessity of non-ultra filters

While the previous section focused on ultrafilters, some of the constructions of [5], while being based on filters, pointedly do not use maximal filters. This is clearest in the one model of Theorem 5.6 (WMP does not imply MP $_{ω}^{\lor}$ ) which uses the Fréchet filter. There are, however, other models presented there, namely in Theorems 5.2, 5.7, and 5.8, which look a bit different from each other, while all ultimately using non-maximal (a.k.a. non-ultra) filters, even though that latter fact is not flagged there. Is there a commonality that binds them all together?

In the following, we will need:

MP (Markov’s Principle): If it is impossible for all terms of α to be zero, then there exists an n such that $α (n) = 1$ .

We will also need:

WMP (Weak Markov’s Principle): $\begin{matrix} \forall γ [\forall β (\neg \neg \exists n (β (n) = 1) \lor \neg \neg \exists n (γ (n) = 1 \land β (n) = 0)) \to \exists n γ (n) = 1] . \end{matrix}$

(The aforementioned MP $_{ω}^{\lor}$ is a weakening of MP which we will not use here.)

Theorem 4.
At a point ∞ in a topological space $T$ , if $\infty ⊩$ WMP and $\infty ⊮$ MP then it is dense at ∞ that there is a quotient space which is homeomorphic to a non-principal non-ultra filter topology on ω.

(To say that property P holds densely at point x means that every open set containing x has an open subset satisfying P. For $F$ a filter on ω, the induced filter topology on $ω \cup {}$ is discrete on ω and has as neighborhoods of ∗ all sets of the form $u \cup {}$ for $u \in F$ .) Proof.
$\infty ⊮$ MP iff for all $O$ containing ∞, $O ⊮$ MP. Unpacking the definition of ⊩, we get that for some $\hat{O} \subseteq O$ and α, $\hat{O} ⊩ α$ is a binary sequence, $\hat{O} ⊩ \neg \forall n α (n) = 0$ , yet $\hat{O} ⊮ \exists n α (n) = 1$ . Working within $\hat{O}$ , let $C_{n}$ be $⟦ α (n) = 0 ⟧$ . Since α is forced not to be the 0 sequence, $⋂_{n \in ω} C_{n}$ has an empty interior. At the same time, $⋂_{n \in ω} C_{n}$ is non-empty, as follows. If that intersection were empty, then each $x \in \hat{O}$ is in the complement of some $C_{n}$ . The complement of $C_{n}$ is $⟦ α (n) = 1 ⟧$ . Therefore x is in an open set forcing $\exists n α (n) = 1$ . Hence $\hat{O}$ is covered by open sets each forcing $\exists n α (n) = 1$ , and so $\hat{O}$ forces the same. This contradicts the choice of $\hat{O}$ and α.

Let $O_{n}$ be $(\hat{O} ∖ C_{n}) ∖ (⋃_{k < n} O_{k})$ . Because each $C_{n}$ is clopen, so is each $O_{n}$ . Notice that $O_{n}$ is the truth-value of “n is the first place where α is 1;” as is often the case, once we have an occurrence of 1 in α our work is done, and it’s easier to focus on the first such occurrence. If only finitely many of the $O_{n}$ ’s were non-empty, then their union $⋃_{n} O_{n}$ would be a union of finitely many clopen sets, hence itself clopen. That would make the complement of $⋃_{n} O_{n}$ also clopen. But that complement is $⋂_{n} C_{n}$ , which we have seen is non-empty with empty interior, and so cannot be clopen. We conclude that infinitely many of the $O_{n}$ ’s are non-empty. By thinning the sequence of $O_{n}$ ’s by eliminating those that are empty, we can assume without loss of generality that each $O_{n}$ is non-empty.

Consider the function f which sends each point in $O_{n}$ to n and the rest of $\hat{O}$ to ∗. This epimorphism induces a corresponding quotient space topology on $ω \cup {}$ . Because each $O_{n}$ is clopen, the quotient topology on ω is the discrete topology. We need only concern ourselves with neighborhoods of ∗.

Toward this end, let $F$ be ${u \subseteq ω | u \cup {}$ is open in the quotient topology}, meaning that its inverse image under f is open in $\hat{O}$ . We will show first that $F$ is a non-principal filter.

For starters, $\emptyset \notin F$ , because the inverse image of ∗ is $⋂_{n} C_{n}$ , which is not open. Also, $F$ is closed upwards: if $v \supseteq u \in F$ , then the inverse image of $v \cup {}$ is the union of the inverse image of $u \cup {}$ with some open sets. Furthermore, $F$ is closed under intersections, because the inverse image of an intersection is the intersection of the inverse images, and the intersection of open sets is open. Hence $F$ is a filter. Because each $O_{n}$ is clopen, $F$ contains each co-finite set, and so is not principal.

The construction above could be applied to any open $O^{'} \subseteq \hat{O}$ as long as $O^{'}$ contains some point from $⋂_{n} C_{n}$ (by considering the sequence $O^{'} \cap O_{n}$ ). If there is some such $O^{'}$ where the induced filter $F$ is not an ultrafilter then we are done. Hence assume there is no such, which we will call the ultrafilter assumption, toward a contradiction.

Let γ be such that $⟦ γ (n) = 1 ⟧ = O_{n}$ . Effectively, γ is α up until the first 1, and then 0 thereafter. Because WMP was forced by $O$ , we can apply WMP to γ. We will show that $\hat{O}$ forces the hypothesis of WMP, so that $\hat{O}$ forces γ to have a 1 somewhere. Then $\hat{O}$ will force α to have a 1 somewhere, the desired contradiction.

So let $\bar{O} \subseteq \hat{O}$ force β to be a binary sequence. Let $\bar{β}$ be such that $⟦ \bar{β} (n) = 1 ⟧ = ⟦ β (n) = 1 ⟧ \cap O_{n}$ . The purpose of $\bar{β}$ is that, if anything, it is even more difficult to verify the hypothesis of WMP on $\bar{β}$ than it is on β. After all, the value at any n of $⟦ \bar{β} (n) = 1 ⟧$ is a subset of that of $⟦ β (n) = 1 ⟧$ , so it is more difficult to make the first disjunct true for $\bar{β}$ than for β. Regarding the second disjunct, the value $⟦ β (n) = 1 \land \bar{β} (n) = 0 ⟧$ is disjoint from $O_{n}$ , meaning $⟦ β (n) = 1 \land \bar{β} (n) = 0 ⟧ ⊩ γ (n) = 0$ , hence if the second disjunct holds for $\bar{β}$ then it also does for β. We conclude that if we can show $\bar{O}$ forces the hypothesis of WMP on $\bar{β}$ , we will have shown the same for β.

There are two cases to consider: $\bar{O}$ is disjoint from $⋂_{n} C_{n}$ , or it’s not. In the former case, $\bar{O}$ is covered by the disjoint clopens $\bar{O} \cap O_{n}$ , each of which itself is the disjoint union of the clopens $\bar{O} \cap O_{n} \cap ⟦ \bar{β} (n) = 1 ⟧$ and $\bar{O} \cap O_{n} \cap ⟦ \bar{β} (n) = 0 ⟧$ . The former set forces $\exists n \bar{β} (n) = 1$ , and the latter $\exists n γ (n) = 1 \land β (n) = 0$ , which suffices.

For the second case, we get to use the ultrafilter hypothesis. Work within $\bar{O}$ . (That means, for instance, reference to $O_{n}$ implicitly means $O_{n} \cap \bar{O}$ .) Let $N_{0}$ be ${n | O_{n} ⊩ \bar{β} (n) = 0}$ , $N_{1}$ be ${n | O_{n} ⊩ \bar{β} (n) = 1}$ , and $N_{2}$ be the naturals in neither $N_{0}$ nor $N_{1}$ . The $N_{i}$ ’s form a partition of the natural numbers, hence one is in the ultrafilter. That means the inverse image $U_{i}$ of some $N_{i} \cup {*}$ is open. Suppose first that is the case for $i = 0$ . Notice that the inverse image of $N_{0}$ forces $\exists n γ (n) = 1 \land β (n) = 0$ . Let x be any other point of $U_{0}$ , meaning x is in $⋂_{n} C_{n}$ . If $V$ is an open set containing x, then $V \cap U_{0}$ must contain a point in some $O_{n}$ with $n \in N_{0}$ , lest $V \subseteq ⋂_{n} C_{n}$ , whereas the latter set has empty interior. Hence $V \cap U_{0}$ forces the second disjunct (in the hypothesis of WMP). Similarly if $i = 1$ or 2. □

5. Cauchy and Dedekind reals

There are many known constructions of the reals from the rationals: Dedekind cuts, equivalence classes of Cauchy sequences, regular Cauchy sequences (with a fixed modulus of convergence), continued fractions, decimal or binary representations, to name some. An obvious question is whether these constructions are equivalent constructively. The first observation along these lines was that every Cauchy sequence induces a corresponding Dedekind cut, and that the generic for the topological model over the reals is a Dedekind cut which is not a Cauchy sequence of rationals [3]. (For separations among various kinds of Cauchy sequences, see [13].) It is the goal of this section to determine what topological models separate Dedekind and Cauchy reals. Note that we take a real to be a Dedekind cut, since that is the most general common definition of a real, and since it has nice closure properties, mostly the idempotency of the construction: a Dedekind cut of reals which are themselves Dedekind cuts of rationals can be reduced to a Dedekind cut of rationals, whereas a Cauchy sequence of Cauchy sequences of rationals may not be a Cauchy sequence of rationals [13].

5.1. Dedekind reals

Because every Dedekind cut in a classical ground model is already a Cauchy sequence, we explore first when there is even a new Dedekind cut.

Theorem 5.
$T ⊩$ “There is a real which is not in the ground model.” iff locally there is a continuous function to the reals such that the inverse image of any point has an empty interior. (By a property holding locally, we mean that the collection of open sets on which the property holds covers the space.)

This is called here a theorem, because it is of such central importance, being the translation of a forcing statement into a purely topological one. The proof though is more like that of a proposition, being a straightforward unpacking of the forcing semantics. Proof.
We use the well-established fact that a Dedekind cut in a topological model comes down to a continuous function to the reals [3].

$T ⊩$ “There is a real which is not in the ground model.” iff

$T ⊩ “ \exists r \in R r \notin R^{V}$ ” iff

$T$ is covered by open sets $O$ such that there is a term $σ_{O}$ with $O ⊩ “ σ_{O} \in R \land σ_{O} \notin R^{V}$ ” iff

locally there is a term $σ_{O}$ with $O ⊩ “ σ_{O} \in R \land σ_{O} \notin R^{V}$ ” iff

locally there is a continuous function $f : O \to R$ such that $O ⊩ “ f \notin R^{V}$ ” iff

locally there is a continuous function f to the reals such that for all $r \in R$ $O ⊩ “ f \neq r$ ” iff

locally there is a continuous function f to the reals such that for all $r \in R$ and all open $U \subseteq O$ $U ⊮ “ f = r$ ” iff

locally there is a continuous function f to the reals such that for all $r \in R$ and all open $U \subseteq O$ f is not constant on $U$ with value r iff

locally there is a continuous function f to the reals such that for all $r \in R$ and all open $U \subseteq O$ $U ⊈ f^{- 1} (r)$ iff

locally there is a continuous function f to the reals such that, for any real number r, the inverse image $f^{- 1} (r)$ does not contain an open set iff

locally there is a continuous function to the reals such that the inverse image of any point has an empty interior. □
Definition 1.
$T$ is functionally Hausdorff if, for every distinct $x, y \in T$ , there is a continuous function f from $T$ to the reals such that $f (x) \neq f (y)$ .
Theorem 6.
For every $T$ there is a unique quotient space $T^{fH}$ which is functionally Hausdorff and universal in the sense that every continuous $f : T \to U$ to a functionally Hausdorff space $U$ factors through the quotient map.
Proof.
Say $x \sim y$ iff for every continuous $f : T \to R f (x) = f (y)$ . It is easy to check that ∼ is an equivalence relation. Modding out by ∼ gives the desired quotient space. □
Lemma 2.
Let $T$ be functionally Hausdorff and $X = {x_{0}, x_{1}, \dots}$ a countable subset of $T$ . Then there is a continuous function from $T$ to the reals which is one-to-one on X.
Proof.
For convenience, take the $x_{i}$ s to be pairwise distinct. Let $f_{0}$ be the constant function 1, and $d_{0}$ the number 1. Suppose inductively we have $f_{n}$ continuous to the positive reals which is one-to-one on ${x_{0}, \dots, x_{n}}$ , and $d_{n} > 0$ . If $f_{n}$ is also one-to-one on ${x_{0}, \dots, x_{n + 1}}$ , then let $f_{n + 1}$ be $f_{n}$ , and $d_{n + 1}$ be $d_{n}$ . Else $f_{n} (x_{n + 1}) = f_{n} (x_{i})$ for a unique $i ⩽ n$ . Let c be the minimum of $d_{n}$ and $| f_{n} (x_{j}) - f_{n} (x_{k}) |$ as j and k take on all distinct values from 0 to n. Let $d_{n + 1}$ be $c / 3$ . By functional Hausdorffness, let g be continuous to [0, $d_{n + 1}$ ] with $g (x_{i}) = 0$ and $g (x_{n + 1}) = d_{n + 1}$ . Let $f_{n + 1}$ be $f_{n} + g$ . It is easy to see that $f_{n + 1}$ satisfies the inductive hypothesis.

Let f be the pointwise limit of the $f_{n}$ s. First off, notice that f is defined, in that the sequence $f_{n} (x)$ always converges, being monotonically non-decreasing and bounded above by the convergent series $\sum 1 / 3^{n}$ .

To see that f is one-to-one on X, consider $x_{j}$ and $x_{k}$ with $j < k$ . In going from $f_{k}$ to $f_{k + 1}$ , the distance between the images of $x_{j}$ and $x_{k}$ shrinks the most when the smaller of the two increases by the most possible, namely $d_{k + 1}$ , and the larger doesn’t change at all; also, $d_{k + 1}$ is at most a third of the distance between those images. Similarly, at all future stages $n ⩾ k + 1$ , the distance between the images of $x_{j}$ and $x_{k}$ will shrink by at most $d_{n}$ , and the sequence of ds always shrinks by a factor of at least 1/3. So in the limit the distance between the images will have shrunk by a factor of at most $\sum_{1}^{\infty} 1 / 3^{n}$ , which is 1/2.

Finally, we must check the continuity of f. It suffices to show that for all $ϵ > 0$ and $x \in T$ there is an open set $O$ containing x such that $f^{″} O \subseteq (f (x) - ϵ, f (x) + ϵ)$ . Let m be large enough so that $\sum_{n = m}^{\infty} 1 / 3^{n} < ϵ / 2$ . Let $O$ be the inverse image of $(f (x) - ϵ, f (x) + ϵ / 2)$ under $f_{m}$ . This $O$ suffices. □
Theorem 7.
Suppose $T$ is separable. Then $T ⊩$ “There is a real which is not in the ground model.” iff each equivalence class $[x]$ of the quotient map $[\cdot] : T \to T^{fH}$ has an empty interior.
Proof.
First we show the left-to-right direction, which does not use separability. Letting $x \in T$ be arbitrary, by Theorem 5 let $O$ be a neighborhood of x and $f : O \to R$ continuous such that, for all reals r, the pre-image $f^{- 1} (r)$ has empty interior. By Theorem 6, since $R$ is (trivially) functionally Hausdorff, f factors through the quotient map to $T^{fH}$ : $f = g \circ [\cdot]$ . Then $[x] \subseteq f^{- 1} (f (x))$ , and so itself has empty interior.

For the other direction, let X be a countable dense subset of $T$ . Then the image $[X]$ of X in $T^{fH}$ under the quotient map $[\cdot]$ is also a countable dense subset of $T^{fH}$ . By Lemma 2, let $f : T^{fH} \to R$ be continuous and one-to-one on $[X]$ . It suffices to show that for $f \circ [\cdot]$ the inverse image of any point has an empty interior. Toward this end, let r be in the range of f. Let $O$ be the interior of ${(f \circ [\cdot])}^{- 1} (r)$ . We need only show that $O$ is empty. If not, then by density there is an $x \in X \cap O$ , and, by the choice of f, $X \cap O \subseteq [x]$ . By hypothesis, $[x]$ has an empty interior; in particular, $[x]$ is not a superset of $O$ . So there is a $y \in O$ not in $[x]$ . That means that in $T^{fH} [x] \neq [y]$ . Let g separate $[x]$ and $[y]$ ; that is, $g : T^{fH} \to R$ is continuous and $g ([x]) \neq g ([y])$ . Choosing two open sets which separate $g ([x])$ and $g ([y])$ , their inverse images under g are two open sets in $T^{fH}$ separating $[x]$ and $[y]$ . And their inverse images under $[\cdot]$ are two open sets, say $U$ and $V$ , separating x and y. Moreover, $[x] \subseteq U$ . Intersecting $U$ and $V$ with $O$ yields two disjoint non-empty open subsets of $O$ . By density, $V \cap O$ contains a point from X. But as has already been observed, $X \cap O \subseteq [x] \subseteq U$ . By this contradiction, $O$ is empty. □
Corollary 1.
If $T$ is locally separable, then $T ⊩$ “There is a real which is not in the ground model.” iff each equivalence class $[x]$ of the quotient map $[\cdot] : T \to T^{fH}$ has an empty interior.
Proof.
Each property in the iff is a local property. □
Corollary 2.
Suppose $T$ is separable and functionally Hausdorff. Then $T ⊩$ “There is a real which is not in the ground model.” iff points are not open.
Proof.
If $T$ is functionally Hausdorff, then each equivalence class $[x]$ is just ${x}$ . □

5.2. Regular Cauchy sequences

We now turn our attention to Cauchy sequences.

Constructively there are two basic kinds of Cauchy sequences: those with and those without a modulus of convergence. In more detail, for ${⟨ q_{n} ⟩}_{n \in ω}$ to be a Cauchy sequence (of rationals) means that $\forall ϵ > 0 \exists N \forall m$ , $n ⩾ N | q_{m} - q_{n} | < ϵ$ . It suffices to consider only rational ϵ, or rationals of the form $1 / k$ or $1 / 2^{k}$ , which helps by keeping the type level of the assertion down. Using this last formulation, a modulus of convergence is a function f giving N as a function of k: $\forall k \forall m, n ⩾ f (k) | q_{m} - q_{n} | < 1 / 2^{k}$ . (It is easy to see that from a modulus of convergence for some choice of $ϵ (k)$ , here taken to be $1 / 2^{k}$ , one can construct a modulus for any other choice of $ϵ (k)$ . We choose to work with $1 / 2^{k}$ for convenience.) It is consistent with constructive set theory that there is a Cauchy sequence with no modulus of convergence [13]. A Cauchy sequence that has a modulus of convergence is often called a regular Cauchy sequence.

In this paper we describe what it is for a real (i.e. Dedekind cut) in a topological model to be represented by a regular Cauchy sequence. We leave for future work the study of arbitrary Cauchy sequences.

5.2.1. Topology

Before turning to the connection with constructivity and topological models, we develop the topology proper. First we repeat some well-known notions and properties, to help make this paper self-contained for those with varied backgrounds in topology. Instead of providing specific references for most of it, we refer the reader to [2] for a full exposition. Then we will introduce the particular notions we will need here, and discuss their connections with the more common definitions already introduced.

Definition 2.
A topological space $T$ is $T_{1}$ if points are closed: for every $x \in T$ , ${x}$ is closed. A space has small inductive dimension zero if it has a base of clopens. It has (Lebesgue) covering dimension zero if every open cover has a refinement which is a cover of disjoint clopens. (Note that sometimes in the covering dimension finiteness is taken: that every finite open cover has a finite disjoint clopen refinement. We prefer the more general definition, and the distinction will play no role here anyway.)
Proposition 1.
For a $T_{1}$ space $T$ , if $T$ has covering dimension zero then it has small inductive dimension zero.
Proof.
We need to show that every open set of $T$ is the union of its clopen subsets. Let $O$ be an open set and $x \in O$ . Consider the open cover consisting of the two sets $O$ and $T ∖ {x}$ . By hypothesis, that cover has a refinement of disjoint clopens. The clopen in that refinement which contains x is a subset of $O$ . □
Definition 3.
A topological space $T$ is functional covering dimension zero if, for every continuous $g : T \to R$ and every open cover ${U_{i} | i \in I}$ of $R$ , ${g^{- 1} (U_{i}) | i \in I}$ (which note is an open cover of $T$ ) has a refinement of disjoint clopens which also covers $T$ .

By way of comparison with the literature, in [2] a space $T$ is defined as $T_{3 \frac{1}{2}}$ , or Tychonoff, or completely regular if points and closed sets can be separated by continuous functions to the reals, i.e. for every $x \in T$ and every closed set $C$ not containing x there is a continuous function f to the reals with $f (x) = 0$ and $f^{″} C \subseteq {1}$ (allowing here for the possibility that C is empty). A set is functionally open resp. closed if it is the inverse image under a continuous function to the reals of an open resp. closed set. A non-empty Tychonoff space is taken to be strongly zero-dimensional if every finite cover consisting of functionally open sets has a refinement of finitely many disjoint clopens which is also a cover. This is a lot like functional covering dimension zero as defined above. A detailed comparison of the two notions would take us too far afield.

Trivially, every space of covering dimension zero has functional covering dimension zero. This notion can be contrasted with other notions of functionality in topology. Typically, the functional version of a property is a strengthening. For instance, functionally Hausdorff spaces are Hausdorff but not conversely, and functionally (better know as completely) regular spaces are regular but not conversely. In this case the implication seems to be going in the other direction.

For Tychonoff spaces, having functional covering dimension zero implies having small inductive dimension zero, as follows. Let x be a member of an open set $O$ . Let $f : T \to [0, 1]$ separate x and $T ∖ O$ . Consider the open cover of $T$ consisting of the inverse images of [0, 2/3) and (1/3, 1]. In its clopen refinement given by functional covering dimension zero, the clopen set containing x is a subset of $O$ , which suffices.
Definition 4.
$T$ is of local functional covering dimension zero if for every continuous $g : T \to R$ there is an open cover ${O_{j} | j \in J}$ of $T$ such that, for any open cover ${U_{i} | i \in I}$ of $R$ and any $j \in J$ , ${g^{- 1} (U_{i}) | i \in I}$ has a refinement of disjoint clopens (in $O_{j}$ ’s subspace topology) which covers $O_{j}$ .

Having local functional covering dimension zero is strictly weaker than having functional covering dimension zero. For an example, see Dowker’s example, 6.2.20 in [2]. It is easy enough to see that the property of being of local functional covering dimension zero can be amalgamated; that is, if a space has an open cover of sets of local functional covering dimension zero, then that space is itself of local functional covering dimension zero. This is not true for the functional covering dimension, by the same example 6.2.20 of [2]. Simplifications of these definitions under additional hypotheses, and discussion of when these dimensional properties are inherited by subspaces, are discussed in Section 7.1 of [2].

Can we get an even better handle on when a space has local functional dimension zero? On the one hand, straight from the definition itself it looks like there would have to be a lot of clopen sets. One extreme is a discrete space, in which every set is clopen: every discrete space trivially is of local function covering dimension zero (by considering covers consisting of singletons, either for the original cover or the refinement). The other extreme is a space that has as few clopen sets as possible, namely the entire space and the empty set, such as the reals $R$ . In fact, if for a continuous $g : R \to R$ there is such an open cover, then g must be constant, as follows. Without loss of generality, we can take the open cover ${O_{j} | j \in J}$ in the definition to consist of intervals. If g is not constant on $R$ , then g is not constant on some $O_{j}$ , say $O$ . Say g on $O$ takes on (at least) the two values $r_{0} < r_{1}$ . Consider the open cover of $R$ consisting of $(- \infty, r_{1})$ and $(r_{0}, \infty)$ . The inverse image of that open cover consists of two sets, neither of which is all of $O$ . Therefore their only clopen subsets are both empty, the union of which is not $O$ . Of course, there are many continuous $g : R \to R$ which are not constant. In short, being of local functional covering dimension zero seems from these examples to come down to having many clopens.

On the other hand though, it could instead come down to having very few continuous functions. Consider for instance the following Hausdorff space which is not functionally Hausdorff [6]. The underlying set is the positive integers. A basic open set is an equivalence class ${[a]}_{b}$ of those integers equivalent to a mod b, whenever a and b are relatively prime. It can be shown that ${[b]}_{b}$ is a subset of the closure of ${[a]}_{b}$ . Hence, for the two basic open sets ${[a]}_{b}$ and ${[c]}_{d}$ , $b d$ is in the closure of each of those sets. Therefore, the closures of any two non-empty open sets are not disjoint. This has two important consequences. For one, the only clopen sets are once again the empty set and the whole space. For another, the only continuous functions to $R$ are the constant ones, as follows. If g took on two distinct values $r_{0} < r_{1}$ , let $O_{0}$ and $O_{1}$ be neighborhoods of $r_{0}$ and $r_{1}$ respectively, with disjoint closures $C_{0}$ and $C_{1}$ . Observe that the closure of $g^{- 1} (O_{i})$ is contained in $g^{- 1} (C_{i})$ . Since $g^{- 1} (C_{0})$ and $g^{- 1} (C_{1})$ are disjoint, so are the closures of $g^{- 1} (O_{0})$ and $g^{- 1} (O_{1})$ , contradicting the property just shown. Since every continuous function to $R$ is constant, it is easy to check the local functional covering dimension property: each $g^{- 1} (U_{i})$ is either the empty set or the entire space. The import of this example is that it is a non-trivial space (infinite and Hausdorff) with as few clopen sets as possible, yet still of local functional covering dimension zero, because there are as few continuous functions as possible. So it is not clear (yet) how to characterize these spaces.
5.2.2. Implications for the reals

The importance and naturality of having local functional covering dimension zero is brought out by the following.

Theorem 8.
$T ⊩ R^{d} = R^{c} = R^{rc}$ (i.e. the Dedekind, Cauchy, and regular Cauchy reals are all the same) iff each open set of $T$ is of local functional covering dimension zero.

In the following, we will drop the descriptor of the dimension being the covering dimension, and refer merely to spaces of (local, functional) dimension zero.

By way of foreshadowing, it gets used at the end of this section that the proof below is local: for a continuous $g : O \to R$ , which gives a Dedekind real, $O ⊩ g \in R^{rc}$ iff g is a confirming instance of $O$ (possibly) having local functional covering dimension zero.
Proof.
For the left-to-right direction, let $O$ be an open set of $T$ , and $g : O \to R$ be continuous. Then $O ⊩ “ g$ is a Dedekind real,” so by hypothesis $O ⊩ “ g$ is a regular Cauchy real.” That means that $O$ is covered by open sets $O_{j}$ each of which forces a particular regular Cauchy sequence to have limit g, i.e. $O_{j} ⊩ “ {⟨ ρ_{n} ⟩}_{n \in ω}$ is a regular Cauchy sequence with limit g.” Let ${U_{i} | i \in I}$ be an open cover of $R$ . It suffices to find a refinement of ${g^{- 1} (U_{i}) | i \in I}$ consisting of disjoint clopens which covers $O_{j}$ , for any fixed j.

Consider the statements of the form $ρ_{0} = q$ , as q ranges over the rationals. Each truth-value $⟦ ρ_{0} = q ⟧$ is an open set, different values of q give disjoint sets, and, because $O_{j}$ forces the entire sequence $⟨ ρ_{n} ⟩$ to be defined, $O_{j}$ forces $ρ_{0}$ to be some rational number, meaning that the sets $⟦ ρ_{0} = q ⟧$ cover $O_{j}$ . In short, the family $⟦ ρ_{0} = q ⟧$ is a partition of $O_{j}$ into countably many open sets. Furthermore, each of those open sets is clopen, because its complement is the union of all the other open sets, hence open itself. (There is no further restriction. For instance, some of these clopens may be empty. In fact, it is possible that all are empty except for one.)

For the next step, work within any one of the clopens $⟦ ρ_{0} = q ⟧$ . We would like to consider sets of the form $⟦ ρ_{1} = r ⟧$ (as r ranges over the rationals). By regularity, $⟦ ρ_{0} = q ⟧ ⊩ q - 1 < ρ_{1} < q + 1$ . So it suffices to consider rs from the interval $(q - 1, q + 1)$ . (It does no harm to allow r to be from outside that interval, it’s just that the corresponding sets will then be empty.) As in the previous step, we get a partition of our starting set $⟦ ρ_{0} = q ⟧$ into countably many clopens $⟦ ρ_{1} = r ⟧$ (or, more accurately, $⟦ ρ_{0} = q \land ρ_{1} = r ⟧$ ).

Continuing in this way, each clopen on level n gets partitioned into countably many clopens on level $n + 1$ .

Visually the picture can be thought of this way. We have a countably branching tree, as in the construction of Baire space. The root, level −1, stands for the entire open set $O_{j}$ . The nodes on level 0 are indexed by the rationals and each node has an associated clopen set, which jointly form a partition of $O_{j}$ . For notational convenience, we identify the node indexed by q with the sequence $⟨ q ⟩$ . Furthermore, any descendant of the node $⟨ q ⟩$ can be indexed only by rationals r from the interval $(q - 1, q + 1)$ . We identify the child of node $⟨ q ⟩$ indexed by r with the sequence $⟨ q, r ⟩$ . Inductively, the children of a node σ on level n are indexed by rationals s from $(σ (n) - 1 / 2^{n}, σ (n) + 1 / 2^{n})$ , subject perhaps to other constrains coming from other ancestors; we identify the child indexed by s with the sequence $σ^{⌢} s$ . Furthermore, these children each have an associated clopen set, which jointly form a partition of σ’s clopen set. The clopen set associated with σ is actually $⟦ \forall k ⩽ length (σ) ρ_{k} = σ (k) ⟧$ ; for notational convenience we write this set as $⟦ σ ⟧$ .

Each (infinite) path through this countably branching tree produces a sequence $⟨ q_{0}, q_{1}, \dots ⟩$ of rationals, namely the indices of the nodes on the path. By the restriction on the indexing, this sequence is Cauchy, in fact regular Cauchy. By intersecting the nested clopens along this path, we get a closed set. (Note that this closed set might well be empty, even if all the clopens along the way are non-empty, since there is no assumption of compactness.) Because the clopens on any fixed level are a partition of $O_{j}$ , these closed sets are also a partition of $O_{j}$ . This induces a function from $O_{j}$ to $R$ : each $t \in O_{j}$ is in each clopen along a unique path through the tree, which path has an associated Cauchy sequence of rationals, so send t to the limit of that sequence. Since $O_{j} ⊩ lim ρ_{n} = g$ , this function is just g itself.

Note that we did not use g in the construction of the tree. The only role g played was in identifying the function induced by the tree. Hence if $O_{j} ⊩ “ ⟨ ρ_{n} ⟩$ is a regular Cauchy sequence” then we can build a tree as above and extract its induced function. It is easy to see that this function is continuous, hence represents a real in the topological model, namely the limit of the given Cauchy sequence. This is no surprise, as it is easy to show in constructive set theory that every regular Cauchy sequence induces a Dedekind cut.

Although it was not phrased this way, it is easy to see the existence of such a tree is equivalent to $O_{j}$ forcing the existence of a regular Cauchy sequence with limit the tree-induced function. That is, from the tree one can construct a term in the forcing language which $O_{j}$ forces to be a regular Cauchy sequence. The tree is the externalization of the internal Cauchy sequence.

To return to the proof, let $⟨ q_{0}, q_{1}, \dots ⟩$ be a path through the tree, with limit r. For some i, $r \in U_{i}$ . For any such i there is a smallest n such that $[r - 1 / 2^{n}, r + 1 / 2^{n}] \subseteq U_{i}$ . For that i and n, $⟦ ⟨ q_{0}, \dots, q_{n + 1} ⟩ ⟧ \subseteq g^{- 1} (U_{i})$ . Let S be the set of nodes σ in the tree such that for some i $⟦ σ ⟧ \subseteq g^{- 1} (U_{i})$ and for all proper initial segments of σ there is no such i. Then ${⟦ σ ⟧ | σ \in S}$ is the desired refinement.

For the reverse direction, assume that each open set $O$ of $T$ is of local functional dimension zero. It is easy enough in constructive set theory to show that $R^{rc} \subseteq R^{c} \subseteq R^{d}$ . So we need only show $T ⊩ R^{d} \subseteq R^{rc}$ . Toward this end, assume $O ⊩ g \in R^{d}$ . So g is a continuous function from $O$ to $R$ . Let ${O_{j} | j \in J}$ be an open cover of $O$ as given by the hypothesis of $O$ being of local functional dimension zero. For an arbitrary j it suffices to find a term ρ such that $O_{j} ⊩ “ ρ$ is a regular Cauchy sequence with limit g.”

Consider the open cover of $R$ of intervals of the form ( $q -$ 1/2, $q + 1 / 2$ ): = $q_{1}$ as q ranges over the rationals. Let $C_{k}$ (as k ranges over some index set K) be a refinement of ${g^{- 1} (q_{1}) | q \in Q}$ consisting of disjoint clopens which covers $O_{j}$ , which exists by hypothesis. It is safe to assume that for each k there is a distinguished $q^{k}$ with $C_{k} \subseteq g^{- 1} (q_{1}^{k})$ , as such a $q^{k}$ can be chosen canonically (as say the first such q in a well-ordering of $Q$ ). Let $ρ_{0}$ be a term such that $⟦ ρ_{0} = q ⟧ = ⋃ {C_{k} | q^{k} = q}$ .

Similarly, for each n and rational q, let $q_{n}$ be the interval ( $q - 1 / 2^{n}, q + 1 / 2^{n}$ ). Recycling notation here, let $C_{k}, k \in K$ be a refinement of ${g^{- 1} (q_{n}) | q \in Q}$ consisting of disjoint clopens which covers $O_{j}$ . Again reusing notation, for each k, $q^{k}$ is such that $C_{k} \subseteq g^{- 1} (q_{n}^{k})$ . Let $ρ_{n}$ be a term such that $⟦ ρ_{n} = q ⟧ = ⋃ {C_{k} | q^{k} = q}$ . Then ρ is as desired. □
Corollary 3.
$T ⊩ R^{d} \neq R^{rc}$ iff the open sets of $T$ which are not of local functional covering dimension zero are dense, i.e. every open set has an open subset which is not of local functional covering dimension zero.
Proof.
This comes down to unraveling the forcing semantics. $T ⊩ R^{d} \neq R^{rc}$ iff no open set forces $T ⊩ R^{d} = R^{rc}$ , i.e. for all open sets $O$ , $O ⊮ R^{d} = R^{rc}$ . By the previous theorem, that is equivalent to saying that all open sets $O$ have open subsets not of local functional covering dimension zero. □

As is well understood, constructively there is a difference between two sets being unequal and the existence of a member of one which is not a member of the other. So to get a witness to the Dedekind and regular Cauchy reals being unequal, we need a stronger property. Definition 5.
A continuous function $g : T \to R$ witnesses that $T$ is not of local functional covering dimension zero if for every open cover ${O_{j} | j \in J}$ of $T$ there is an open cover ${U_{i} | i \in I}$ of $R$ and a $j \in J$ such that ${g^{- 1} (U_{i}) | i \in I}$ has no refinement of disjoint clopens of $O_{j}$ which covers $O_{j}$ . ghereditarily witnesses that $T$ is not of local functional covering dimension zero if g witnesses that each open set of $T$ is not of local functional covering dimension zero.
Remark 1.
As has already been observed, the proof of the previous theorem was local: what was actually shown was that for each continuous $g : T \to R$ , $T ⊩ g \in R^{rc}$ iff g is a confirming instance of $T$ (potentially) being of local functional covering dimension zero, or, to use the terminology above, that g is not a witness that $T$ is not of local functional covering dimension zero.
Theorem 9.
$T ⊩ \exists r \in R^{d} ∖ R^{rc}$ iff $T$ has an open cover of which each member $O$ has a hereditary witness that $O$ is not of local functional covering dimension zero.
Proof.
$T ⊩ \exists r \in R^{d} ∖ R^{rc}$ iff $T$ has an open cover, and for each member $O$ of that cover there is a g such that $O ⊩ g \in R^{d} ∖ R^{rc}$ . Since $O ⊩ g \in R^{d}$ , g is a continuous function from $O$ to $R$ , hence of the right type to be a hereditary witness for $O$ . The proof will be complete if we show that g is a hereditary witness for $O$ iff $O ⊩ g \notin R^{rc}$ .

$O ⊩ g \notin R^{rc}$ iff

for every open $O^{} \subseteq O$ , $O^{} ⊮ g \in R^{rc}$ iff, by the remark above,

for every such $O^{}$ , g witnesses that $O^{}$ is not of local functional covering dimension zero iff

g is a hereditary witness for $O$ . □

6. BD-N and future directions

The principles studied above, although about sequences, are really logical principles, because they are about binary sequences. A natural extension is to include similar analyses for analytic principles. Examples abound: whether the Cauchy and Dedekind reals are equal [3], the Fundamental Theorem of Algebra [3,14], the Fan Theorem [3,16], BD-N [15]. As it turns out, this is more difficult than the current study of logical principles. Perhaps that is only to be expected, since principles of analysis are more complicated. Be that as it may, the following is a summary of what is known in one case, namely BD-N. The purpose of discussing these failed attempts is to convey to the interested reader a sense of the difficulties, and to provide a springboard for future researchers. This section then concludes with some other open questions.

By way of background, a set (of natural numbers) is pseudo-bounded if every sequence $(a_{n})$ of its members is eventually bounded by the identity sequence (i.e. for n large enough $a_{n} < n$ ). BD-N is the principle that every countable pseudo-bounded set is bounded [7–9]. In [15], it was shown that the model built over the space $T$ of bounded sequences, suitably topologized, falsifies BD-N: $T ⊩ G$ is pseudo-bounded yet unbounded (where G is the generic). This failure is strong in that there is one counter-example that works for the whole space, and that this counter-example is not merely not forced to be bounded, which would ultimately come down to a single point, but rather that it is positively forced to be unbounded, and that, again, by the whole space.

To get a model in which BD-N fails, it would seem as though some kind of completeness is necessary, because if you take either the space of eventually constant sequences, or the space of bounded but never eventually constant sequences, the generic is no longer pseudo-bounded. (The sequence that picks out the next pair of identical entries, or the next change in the sequence, can be leveraged to contradict pseudo-boundedness.) On the other hand, in the successful space in [15], if you remove just one point, you violate completeness, but what’s left is covered by open sets of the original space, each of which forces ¬BD-N. So the role of completeness is unclear.

It is easy to find ways to change the space so it is no longer precisely the bounded sequences, but it may as well be, in that the bounded sequences are easily recovered from the space. For instance, take the set of always positive bounded sequences – don’t allow 0 as a value. Trivially, by shifting everything down one, you re-create the bounded sequences. Or the space of bounded sequences in which every entry indexed by an odd number is equal to the entry just before (i.e. $α (2 n) = α (2 n + 1)$ ). By identifying each odd entry with its predecessor, again one re-captures the bounded sequences. Clearly one could come up with more complicated variants of these. What’s not so clear is just how they would be identified and how one could give a general procedure to extract exactly the bounded sequences. Or, for that matter, since it’s not exactly the bounded sequences we need, how to give the general property of a space which would make it violate BD-N.

This then leads to a general project: find a good theorem about topological spaces violating, or for that matter satisfying, BD-N; more generally, find such for other principles of analysis.

Even for logical principles, there is still more to be done. For instance, analyze some principles not studied here. Even for the ones in this paper, the theorems could be improved. For instance, the theorems proved here are implications; it would be nice to see iff’s, perhaps of course calling for a tighter property.

Some logical principles, given about binary sequences, have real number correlates. For instance, assuming for instance DC, LPO is equivalent with the decidability of equality on the reals. Also, again under DC, LLPO is equivalent with the linearity of the ordering of the reals. It would be interesting to compare the requirements and restrictions on topological spaces for corresponding pairs of principles.

References

Diener and

Lubarsky, Separating the Fan Theorem and its weakenings, Journal of Symbolic Logic79(3) (2014), 792–813. doi:10.1017/jsl.2014.9.

Engelking, General Topology, Heldermann Verlag, Berlin, 1989.

M.P.

Fourman and

J.M.E.

Hyland, Sheaf models for analysis, in: Applications of Sheaves,

M.P.

Fourman,

C.J.

Mulvey and

D.S.

Scott, eds, Lecture Notes in Mathematics, Vol. 753, Springer-Verlag, Berlin, Heidelberg, New York, 1979, pp. 280–301. doi:10.1007/BFb0061823.

R.J.

Grayson, Heyting-valued semantics, in: Logic Colloquium ’82, Studies in Logic and the Foundations of Mathematics, Vol. 112, North Holland, 1984, pp. 181–208. doi:10.1016/S0049-237X(08)71817-2.

Hendtlass and

Lubarsky, Separating fragments of WLEM, LPO, and MP, Journal of Symbolic Logic81(4) (2016), 1315–1343. doi:10.1017/jsl.2016.38.

https://planetmath.org/hausdorffspacenotcompletelyhausdorff.

Ishihara, Continuity and nondiscontinuity in constructive mathematics, Journal of Symbolic Logic56 (1991), 1349–1354. doi:10.2307/2275479.

Ishihara, Continuity properties in constructive mathematics, Journal of Symbolic Logic57 (1992), 557–565. doi:10.2307/2275292.

Ishihara and

Schuster, A continuity principle, a version of Baire’s theorem and a boundedness principle, Journal of Symbolic Logic73 (2008), 1354–1360. doi:10.2178/jsl/1230396924.

10.

Jech, Set Theory, 3rd edn, Springer Monographs in Mathematics, Springer, 2006.

11.

J.-L.

Krivine, Typed lambda-calculus in classical Zermelo–Fraenkel set theory, Archive for Mathematical Logic40(3) (2001), 189–205. doi:10.1007/s001530000057.

12.

J.-L.

Krivine, Dependent choice, ‘quote’ and the clock, Theoretical Computer Science308 (2003), 259–276. doi:10.1016/S0304-3975(02)00776-4.

13.

Lubarsky, On the Cauchy completeness of the constructive Cauchy reals, Mathematical Logic Quarterly53(4–5) (2007), 396–414. doi:10.1002/malq.200710007.

14.

Lubarsky, Geometric spaces with no points, Journal of Logic and Analysis2(6) (2010), 1–10, http://logicandanalysis.org/ . doi:10.4115/jla.2010.2.6a.

15.

Lubarsky, On the failure of BD-N and BD, and an application to the anti-Specker property, Journal of Symbolic Logic78(1) (2013), 39–56. doi:10.2178/jsl.7801030.

16.

Lubarsky, Separating the Fan Theorem and its weakenings II, Journal of Symbolic Logic84 (2019), 1484–1509. doi:10.1017/jsl.2019.1.

17.

Lubarsky, On the necessity of some topological spaces, in: Revolutions and Revelations in Computability. Proceedings of CiE 2022, Lecture Notes in Computer Science, Vol. 13359, Springer, 2022, pp. 162–171.