Condition to guarantee that an inhabited and bounded set of reals has a supremum

Question

This question is about constructive mathematics (without Choice), such as in the internal logic of a topos with natural numbers object, or in IZF. The “reals” (and the symbol $\mathbb{R}$) refer to the Dedekind real numbers.

Classically, if $S$ is an inhabited ($\exists x\in S.\top$) set of reals that has an upper bound ($\exists x\in\mathbb{R}.\forall y\in S.(y\leq x)$), then it has a supremum (i.e., an upper bound $x$ such that additionally $\forall\delta>0.\exists y\in S.(y\geq x-\delta)$). Constructively, this can no longer be asserted.

[Edit: also, it is worth noting that “supremum” is a constructively stronger notion than “least upper bound”: see comment by Jean Abou Samra below, and my reply to it. So, to be clear, I am asking about “supremum”, and this is why I recalled the definition.]

Question: What nice additional conditions can we add to “inhabited” and “bounded above” to guarantee that $S$ has a supremum? Specifically, can we find one of “topological” nature?

Discussion about locatedness:

One notion relevant here is “locatedness”. However, there is an entire maze of subtly different notations that go under some variation of this term.

The most standard definition of “locatedness” of $S \subseteq \mathbb{R}$ seems to be that for all $z\in\mathbb{R}$ the distance $d(z,S)$ exits, but this is not at all topological, and also, since the distance is defined as the infemum of $|z-y|$ for $y\in S$, applying this with $z$ being an upper bound of $S$ does guarantee that $S$ has a supremum… but in an absolutely trivial way, so something less circular is desirable.

One form of locatedness that I had incorrectly believed to be sufficient (in conjunction with “inhabited” and “bounded above” to guarantee that the set has a supremum), and which [1] calls “pointwise almost located” is:

$$ \begin{aligned} \forall x\in\mathbb{R}.\forall \delta>0.(&(\exists y\in S.(|x-y|<\delta))\\ \lor\;&(\exists \eta>0.\neg\exists y\in S.(|x-y|<\eta))) \end{aligned} \tag{*} $$

that is, in topological terms,

$$ \begin{aligned} \forall x\in\mathbb{R}.\forall U\,\text{open}\ni x.(&S\cap U\;\text{inhabited}\\ \lor\;&(\exists V\,\text{open}\ni x.(S\cap V=\varnothing))) \end{aligned} \tag{*} $$

(In [2], definition 1.2.1(iv) this is called “located”, and naïve me was thus led into believing that what one paper calls “located” might be equivalent to what another paper calls “located”. Ha, ha, silly me.)

In the latter form, this is the sort of condition I am after. However, it is not sufficient, as the following counterexample slightly adapted from [1] shows: let $(s_n)$ be a Specker sequence in $[0,1]$, i.e., an increasing sequence of rational numbers in $[0,1]$ that is bounded away from any real (meaning: $\forall x\in\mathbb{R}.\exists\eta>0.\exists N.\forall n\geq N.(|x-s_n|\geq\eta)$). Let $(b_n)$ be a binary sequence at most one term of which equals $1$. Let $S := \{-1\} \cup \{s_n : b_n=1\}$. Then $S$ is inhabited (by $-1$), bounded above (by $1$), satisfies (*) (as is easy to see from the property of $(s_n)$), but if it has a supremum $x$ then either $\forall n.(b_n=0)$ (this is implied by $x<0$) or $\exists n.(b_n=1)$ (this is implied by $x>-\frac{1}{2}$). So if there exists a Specker sequence and if every inhabited bounded above subset of $\mathbb{R}$ satisfying (*) has a supremum, then LPO holds; and in the effective topos, a Specker sequence exists and LPO fails, so (*) is not sufficient.

The following condition, which [1] calls “almost located”, however, is sufficient by [1], corollary 5:

$$ \begin{aligned} \forall \delta>0.\exists \eta>0.\forall x\in\mathbb{R}.(&(\exists y\in S.(|x-y|<\delta))\\ \lor\;&\neg\exists y\in S.(|x-y|<\eta)) \end{aligned} \tag{†} $$

But this notion (†) does not appear to be expressible in topological terms as I did for (*): it is a uniform notion and, indeed, [1] expresses it in the context of uniform spaces.

There may be some reason (which escapes me) why we really need some kind of uniformity to express locatedness, but note that I am not demanding locatedness, I am just demanding the existence of a supremum, and maybe locatedness is uselessly strong.

References:

1. Douglas Bridges, Hajime Ishihara, Ray Mines, Fred Richman, Peter Schuster & Luminiţa Vîţă, “Almost locatedness in uniform spaces”, Czechoslovak Math. J. 57 (2007) 1‒12

2. Robin J. Grayson, “Concepts of general topology in constructive mathematics and in sheaves. II”, Ann. Math. Logic 23 (1982) 55–98

Answer 1

The following (somewhat strong) property seems to be sufficient:

For any open sets $U,V \subseteq \mathbb{R}$, if $\forall x \in \mathbb{R}.\; x \in U \vee x \in V$, then either $S \subseteq U$ or $S \cap V$ is inhabited.

Let's see that this is sufficient. Let $a$ be a given element of $S$ and let $b$ be a given upper bound of $S$. Define the sets $L = \{x \in \mathbb{Q} : \exists y \in S.\;x < y\}$ and $R = \{x \in \mathbb{Q} : \exists z \in \mathbb{Q}.\; z < x \wedge \forall y \in S.\; y < z\}$. First we need to verify that $(L,R)$ is a Dedekind real (following the definition on nLab here), and then we need to verify that it is the supremum of $S$.

• First note that for any rational $a' < a$, we have that $a' \in L$. Moreover, for any rational $b' > b$, we have that $b' \in R$, so $L$ and $R$ are both inhabited.

• Suppose that $x \in L$. By definition, this implies that there is a $y \in S$ such that $x < y$. Since $y$ is a Dedekind real, this means we can find an $x' \in \mathbb{Q}$ such that $x < x' < y$, whereby $x' \in L$.

• Suppose that $x \in R$. By definition, this implies that there is a $z \in \mathbb{Q}$ such that $z < x$ and $\forall y \in S.\; y < z$. We then have that $x' = \frac{x + z}{2}$ satisfies that $z < x' < x$, whereby $x' \in R$.

• Suppose that $x \in L$ and $x' \in R$. We have that there is a $y \in S$ such that $x < y$ and there is a $z \in \mathbb{Q}$ such that $z < x'$ and $z > y$. Therefore $x < y < z < x'$.

• Finally, we need to use our assumption about $S$ to show the third bullet point in the nLab definition. Suppose that $c < d$ are rational numbers. By the definition of the Dedekind reals, we have that for all $x \in \mathbb{R}$, either $x \in \left(-\infty,\frac{c+2d}{3}\right)$ or $x \in \left(\frac{2c+d}{3},\infty\right)$. Therefore $U = \left(-\infty,\frac{c+2d}{3}\right)$ and $V = \left(\frac{2c+d}{3},\infty\right)$ is a pair of open sets satisfying the condition on our assumed property of $S$. Applying the assumed property gives that either $S \subseteq U$ or $S \cap V$ is inhabited. If $S \subseteq U$, then $\frac{c+3d}{4}$ witnesses that $d \in R$. If $S \cap V$ is inhabited by some $x$, then we have that $c < x$ and so $c \in L$. (Note that this is the only bullet that actually uses our extra condition.)

Okay so $(L,R)$ is a Dedekind real. Let's call it $x$. We need to argue that $x$ is the supremum of $S$. Since $L$ is the union of the lower cuts of the elements of $S$ and $R$ is contained in the intersection of the upper cuts of the elements of $S$, we clearly have that $x$ is an upper bound of $S$. For any $y \in L$, we have by definition that there is a $z \in S$ such that $y < z$, which is enough to imply the supremum condition. (It should be a general fact that if $S$ has a supremum, then the definitions I gave of $L$ and $R$ specify it.)

---

I said that this property is strong, although I think it is a relatively natural property one would expect from '(pre-)compact' sets. (Although note of course that classically all sets satisfy this.) For any finite set $X$ and any $f: X \to \mathbb{R}$, the image of $X$ under $f$ satisfies this condition. It is also reminiscent of the omniscience property Escardó studied in the JSL paper Infinite sets that Satisfy the Principle of Omniscience in any Variety of Constructive Mathematics. I think some kind of effective compactness should be enough to entail it (although this might need something like Markov's principle, depending on how things are stated). We could weaken the condition to just talk about $U$ of the form $(-\infty,d)$ and $V$ of the form $(c,\infty)$ with rational $c$ and $d$, since this is all we really used in the proof, but this makes it feel a bit more like 'smuggling' in the construction of a Dedekind real directly and less like a 'purely topological' notion.

Answer 2

There is a topological analogue of locatedness, called overtness.

First let's consider how we obtain the supremum $a$ of $S$ as a Dedekind Cut, $$ (u\in U) \quad\equiv\quad a< u \quad\equiv\quad \forall x\in S.x< u$$ $$ (d\in D) \quad\equiv\quad d< a \quad\equiv\quad \exists x\in S.d< x.$$

Subsets of the form $U\equiv\{u\|a<u\}$ and $D\equiv\{ d\| d< a\}$ are open, so to turn this into a constructive logic, we define a calculus of open predicates.

The atomic open predicates are $\top$, $\bot$ and $x<y$.

We can add $\lor$, $\land$ and certain restricted quantifiers to this calculus:

It was, I think, first observed by Nachbin in the 1950s that Compact unions of closed subsets are closed and compact intersections of open subsets are open.

For the universal quantifier, if $\phi(x,y)$ is an open predicate, so is $\forall x\in K.\phi(x,y)$, when $K$ is compact.

An overt subspace is one that gives rise to an analogous existential quantifier.

However, it's not good trying to define this in terms of points, because any such subspace is trivially overt.

It was done for locales in the early 1980s by Joyal, Tierney and Johnstone. They used the word open, but sublocales with this property have a habit of being closed, so another word is needed.

These ideas were developed in my Lambda Calculus for Real Analysis, in particular Section 12 considers the supremum (maximum) of an inhabited compact overt subspace.