Apartness, sharp elements, and the Scott topology of domains

Abstract

Working constructively, we study continuous directed complete posets (dcpos) and the Scott topology. Our two primary novelties are a notion of intrinsic apartness and a notion of sharp elements. Being apart is a positive formulation of being unequal, similar to how inhabitedness is a positive formulation of nonemptiness. To exemplify sharpness, we note that a lower real is sharp if and only if it is located. Our first main result is that for a large class of continuous dcpos, the Bridges–Vîţǎ apartness topology and the Scott topology coincide. Although we cannot expect a tight or cotransitive apartness on nontrivial dcpos, we prove that the intrinsic apartness is both tight and cotransitive when restricted to the sharp elements of a continuous dcpo. These include the strongly maximal elements, as studied by Smyth and Heckmann. We develop the theory of strongly maximal elements highlighting its connection to sharpness and the Lawson topology. Finally, we illustrate the intrinsic apartness, sharpness, and strong maximality by considering several natural examples of continuous dcpos: the Cantor and Baire domains, the partial Dedekind reals, the lower reals and, finally, an embedding of Cantor space into an exponential of lifted sets.

1. Introduction

Domain theory (Abramsky and Jung 1995) is rich with applications in semantics of programming languages (Plotkin 1977; Scott 1982, 1993), topology and algebra (Gierz et al. 2003), and higher-type computability (Longley and Normann 2015). The basic objects of domain theory are directed complete posets (dcpos), although we often restrict our attention to algebraic or continuous dcpos which are generated by so-called compact elements or, more generally, by the so-called way-below relation (Section 2). We examine the Scott topology on dcpos using an apartness relation and a notion of sharp elements. Our work is constructive in the sense that we do not assume the principle of excluded middle or choice axioms, but we do use impredicativity and powersets in particular, see Section 1.1 for more details on our foundational setup.

Classically, that is, when assuming excluded middle, a dcpo with the Scott topology satisfies $T_0$-separation: if two points have the same Scott open neighborhoods, then they are equal. This holds constructively if we restrict to continuous dcpos. A classically equivalent formulation of $T_0$-separation is: if $x \neq y$, then there is a Scott open separating x and y, that is, containing x but not y or vice versa. This second formulation is equivalent to excluded middle. This brings us to the first main notion of this paper (Section 3). We say that x and y are intrinsically apart, written $x \mathrel{\#} y$, if there is a Scott open containing x but not y or vice versa. Then $x \mathrel{\#} y$ is a positive formulation of $x \neq y$, similar to how inhabitedness (i.e., $\exists\,{x \in X}$) is a positive formulation of nonemptiness (i.e., $X \neq \emptyset$).

This definition works for any dcpo, but the intrinsic apartness is mostly of interest to us for continuous dcpos. In fact, the apartness really starts to gain traction for continuous dcpos that have a basis satisfying certain decidability conditions. For example, we prove that for such continuous dcpos, the apartness topology (Bridges and Vîţǎ 2011) and the Scott topology coincide (Section 4). Thus, our work may be regarded as showing that the constructive framework by Bridges and Vîţǎ is applicable to domain theory. It should be noted that these decidability conditions are satisfied by the major examples in applications of domain theory to topology and computation. Moreover, these conditions are stable under products of dcpos and, in the case of bounded complete algebraic dcpos, under exponentials (Section 2).

In Bridges and Richman (1987, p. 7), Mines et al. (1988, p. 8), and Bridges and Vîţǎ (2011, p. 8), an irreflexive and symmetric relation is called an inequality (relation) and the symbol ${\neq}$ is used to denote it. In Bishop and Bridges (1985, Definition 2.1), an inequality is moreover required to be cotransitive:

The latter is called a preapartness in Troelstra and vanDalen (1988, Section 8.1.2) and the symbol ${\mathrel{\#}}$ is used to denote it, reserving ${\neq}$ for the logical negation of equality and the word apartness for a relation that is also tight: if $\lnot(x \mathrel{\#} y)$, then $x = y$.

Warning 1. We deviate from the above and use the word apartness and the symbol ${\mathrel{\#}}$ for an irreflexive and symmetric relation, so we do not require it to be cotransitive or tight.

The reasons for our choice of terminology and notations are as follows: (i) we wish to reserve $\neq$ for the negation of equality as in Troelstra and van Dalen (1988, Section 8.1.2); (ii) the word inequality is confusingly also used in the context of posets to refer to the partial order; and finally, (iii) the word inequality seems to suggest that the negation of the inequality relation is an equivalence relation, but, in the absence of cotransitivity, it need not be.

Actually, we prove that no apartness on a nontrivial dcpo can be cotransitive or tight unless (weak) excluded middle holds. However, there is a natural collection of elements for which the intrinsic apartness is both tight and cotransitive: the sharp elements (Section 5). Sharpness is slightly involved in general, but it is easy to understand for algebraic dcpos: an element x is sharp if and only if for every compact element it is decidable whether it is below x. Moreover, the notion is quite natural in many examples. For instance, the sharp elements of a powerset are exactly the decidable subsets and the sharp lower reals are precisely the located ones.

An import class of sharp elements is given by the strongly maximal elements (Section 6). These were studied in a classical context in Smyth (2006) and Heckmann (1998), because of their desirable properties. For instance, while the subspace of maximal elements may fail to be Hausdorff, the subspace of strongly maximal elements is both Hausdorff (two distinct points can be separated by disjoint Scott opens) and regular (every neighborhood contains a Scott closed neighborhood). As shown by Smyth (2006), strong maximality is closely related to the Lawson topology. Specifically, Smyth proved that a point x is strongly maximal if and only if every Lawson neighborhood of x contains a Scott neighborhood of x. Using sharpness, we offer a constructive proof of this.

Finally, in Section 7 we illustrate the above notions by presenting natural examples of continuous dcpos, many of which embed well-known spaces as the strongly maximal elements. Specifically, we consider the Cantor and Baire domains, the partial Dedekind reals, the lower reals, and an embedding of Cantor space into an exponential of lifted sets.

1.1 Foundations

We work informally in an impredicative set theory with intuitionistic logic. If we wish to pin down a particular formal system, then we could choose IZF (Friedman 1973), which has models in Grothendieck and realizability toposes (Fourman 1980; Hayashi 1981; Joyal and Moerdijk 1995). In particular, we have powersets and allow for the usual impredicative definitions of interior and closure in topology. Functions, as is standard in set theory, are encoded as single-valued and total relations. We stress that our work is fully compatible with classical logic.

1.2 Contributions

Our primary objective is to explore the Scott topology of continuous dcpos in a constructive setting where we do not rely on excluded middle or the axiom of choice. This leads us to study an apartness relation, as well as the subsets of sharp and strongly maximal elements, as explained in the Section 1.

We list some main results: Theorem 51 says the framework of Bridges and Vîţǎ (2011) is applicable to constructive domain theory; Theorem 68 shows that the intrinsic apartness is tight and cotransitive for sharp elements. We have a supply of sharp elements, thanks to Theorems 61 and 67, as well as Proposition 71 which tells us that strongly maximal elements are sharp. Finally, the examples of Section 7 provide important illustrations of the theory. For example, Theorem 105 shows that the real line is homeomorphic to the subspace of strongly maximal elements in the continuous domain of partial Dedekind reals, and moreover, that the homeomorphism reflects and preserves apartness.

Some notions, such as sharpness, trivialize in a classical setting. However, our simplification of Smyth’s definition of strong maximality (Section 6) and Proposition 79 are new contributions in a classical setting as well. Moreover, our constructive treatment could possibly inform a classical, but effective treatment of domain theory (Smyth 1977).

1.3 Related work

There are numerous accounts of basic domain theory in several constructive systems, such as Sambin et al. (1996), Negri (1998, 2002), Maietti and Valentini (2004), Kawai (2017, 2021) in the predicative setting of formal topology (Coquand et al. 2003; Sambin 1987), as well as works in various type theories: (Hedberg 1996) in (a version of) Martin-Löf Type Theory, (Lidell 2020) in Agda, (Benton et al. 2009; Dockins 2014) in Coq and our previous work, and (de Jong and Escardó 2021a; de Jong 2022) in univalent foundations. Besides that, the papers (Bauer and Kavkler 2009; Pattinson and Mohammadian 2021) are specifically aimed at program extraction.

Our work is not situated in formal topology and we work informally in impredicative set theory without using excluded middle or choice axioms. We also consider completeness with respect to all directed subsets and not just $\omega$-chains as is done in Bauer and Kavkler (2009), Pattinson and Mohammadian (2021) The principal contributions of our work are the aforementioned notions of intrinsic apartness and sharp elements, although the idea of sharpness also appears in formal topology: an element of a continuous dcpo is sharp if and only if its filter of Scott open neighborhoods is located in the sense of Spitters (2010) and Kawai (2017).

If, as advocated in Abramsky (1987), Vickers (1989), and Smyth (1993), we think of (Scott) opens as observable properties, then this suggests that we label two points as apart if we have made conflicting observations about them, that is, if there are disjoint opens separating the points. Indeed, (an equivalent formulation of) this notion is used in Smyth (2006, p. 362). While these notions are certainly useful, both in the presence and absence of excluded middle, our apartness serves a different purpose: It is a positive formulation of the negation of equality used when reasoning about the Scott topology on a dcpo, which (classically) is only a $T_0$-space that is not Hausdorff in general. By contrast, an apartness based on disjoint opens would supposedly perform a similar job for a Hausdorff space, such as a dcpo with the Lawson topology.

Finally, von Plato (2001) gives a constructive account of so-called positive partial orders: sets with a binary relation ${\not\leq}$ that is irreflexive and cotransitive (i.e., if $x \not\leq y$, then $x \not\leq z$ or $y \not\leq z$ for any elements x, y and z). Our notion ${\mathrel{\;\not\!\not{\!\leq}}}$ from Definition 33 bears some similarity, but our work is fundamentally different for two reasons. Firstly, ${\mathrel{\;\not\!\not{\!\leq}}}$ is not cotransitive. Indeed, we cannot expect such a cotransitive relation on nontrivial dcpos, cf. Theorem 57. Secondly, in von Plato (2001) equality is a derived notion from ${\not\leq}$, while equality is primitive for us.

2. Preliminaries

We give the basic definitions and results in the theory of (continuous) dcpos. It is not adequate to simply refer the reader to classical texts on domain theory (Abramsky and Jung 1995; Gierz et al. 2003), because two classically equivalent definitions need not be constructively equivalent, and hence we need to make choices here. For example, while classically every Scott open subset is the complement of a Scott closed subset, this does not hold constructively (Lemma 10).

The results presented here are all provable constructively. Constructive proofs of standard order-theoretic results, such as Lemma 4 and Proposition 18 (the interpolation property), can be found in de Jong and Escardó (2021a), or alternatively, the author’s PhD thesis (de Jong 2022), and will not be repeated here. Since the Scott topology is not treated in the above references, the proofs of any results involving topology (such as Proposition 17) are spelled out in full.

Finally, in Section 2.3 we introduce and study some decidability conditions on bases of dcpos that will make several appearances throughout the paper. These decidability conditions always hold if excluded middle is assumed.

Definition 2 (Directed complete poset (dcpo)).

1. (1) A subset S of a poset $(X,\mathrel{\sqsubseteq})$ is directed if it is inhabited (meaning there exists $s \in S$) and semidirected: for every two points $x,y \in S$ there exists $z \in S$ with $x \mathrel{\sqsubseteq} z$ and $y \mathrel{\sqsubseteq} z$.

2. (2) A directed complete poset (dcpo) is a poset where every directed subset S has a supremum, denoted by $\bigsqcup S$.

3. (3) A dcpo is pointed if it has a least element, typically denoted by $\bot$.

Notice that a poset is a pointed dcpo if and only if it has suprema for all semidirected subsets. In fact, given a pointed dcpo D and a semidirected subset $S \,\subseteq\, D$, we can consider the directed subset $S \cup \{{\bot}\}$ of D whose supremum is also the supremum of S.

Definition 3 (Way-below relation ${\ll}$). An element x of a dcpo D is way below an element $y \in D$, denoted $x \ll y$, if for every directed subset S with $y \mathrel{\sqsubseteq} \bigsqcup S$ there exists $s \in S$ such that $x \mathrel{\sqsubseteq} s$ already.

Lemma 4. The way-below relation enjoys the following properties:

1. (1) it is transitive;

2. (2) if $x \mathrel{\sqsubseteq} y \ll z$, then $x \ll z$ for every x, y, and z;

3. (3) if $x \ll y \mathrel{\sqsubseteq} z$, then $x \ll z$ for every x, y, and z.

Definition 5 (Continuity of a dcpo). A dcpo D is continuous if for every element $x \in D$, the subset is directed and its supremum is x.

Definition 6 (Companctness and algebraicity). An element of a dcpo is compact if it is way below itself. A dcpo D is algebraic if for every element $x \in D$, the subset $\{{c \in D \mid c \mathrel{\sqsubseteq} x \text{ and }\textit{c} \, \text{is compact}}\}$ is directed with supremum x.

Proposition 7. Every algebraic dcpo is continuous.

2.1 The Scott topology

We stress that constructively it is necessary to define Scott closed and Scott open subsets independently, see Lemma 10.

Definition 8 (Scott topology).

1. (1) A subset C of a dcpo D is Scott closed if it is closed under directed suprema and a lower set: if $x \mathrel{\sqsubseteq} y \in C$, then $x \in C$ too.

2. (2) A subset U of a dcpo D is Scott open if it is an upper set and for every directed subset $S \,\subseteq\, D$ with $\bigsqcup S \in U$, there exists $s \in S$ such that $s \in U$ already.

Example 9. For any element x of a dcpo D, the subset $\,\downarrow\, x := \{{y \in D \mid y \mathrel{\sqsubseteq} x}\}$ is Scott closed. If D is continuous, then the subset is Scott open. (One proves this using the interpolation property, which is Proposition 18 below.) Moreover, if D is continuous, then the set is a basis for the Scott topology on D.

Lemma 10. The complement of a Scott open subset is Scott closed. The converse holds if and only if excluded middle does, as we prove in Proposition 41.

Proof. Let $U \,\subseteq\, D$ be a Scott open of a dcpo D. We show that $C := D \setminus U$ is Scott closed. If $x \mathrel{\sqsubseteq} y$ with $y \in C$, then $x \in C$, for assuming $x \in U$ leads to $y \in U$ as U is Scott open, contradicting that $y \in C$. Now suppose that $S \,\subseteq\, C$ is directed and assume for a contradiction that $\bigsqcup S \in U$. By Scott openness of U, there exists $s \in S$ such that $s \in U$, but this contradicts $S \,\subseteq\, C$.

Definition 11 (Interior and closure). In a topological space X, the interior of a subset $S \,\subseteq\, X$ is the largest open of X contained in S, that is, the interior of S is $\bigcup\{{U \in \mathcal P({X}) \mid U \,\subseteq\, S, U \text{ is open}}\}$. Dually, the closure of a subset $S \,\subseteq\, X$ is the smallest closed subset of X that contains S.

2.2 (Abstract) bases

Ideal completions of abstract bases provide a source of continuous (and algebraic) dcpos. In general, the notion of a basis is constructively quite interesting, as explained in the next subsection.

Definition 12 (Basis for a dcpo). A basis for a dcpo D is a subset $B \,\subseteq\, D$ such that for every element $x \in D$, the subset is directed with supremum x.

Lemma 13. A dcpo is continuous if and only if it has a basis and a dcpo is algebraic if and only if it has a basis of compact elements. Moreover, if B is a basis for an algebraic dcpo D, then B must contain every compact element of D. Hence, an algebraic dcpo has a unique smallest basis consisting of compact elements.

Example 14 (Kuratowski finite subsets). The powerset $\mathcal P({X})$ of any set X ordered by inclusion and with suprema given by unions is a pointed algebraic dcpo. Its compact elements are the Kuratowski finite subsets of X. A set X is Kuratowski finite if it is finitely enumerable, that is, there exists a surjection $\{{0,\dots,n-1}\} \twoheadrightarrow X$ for some number $n \in \mathbb{N}$.

Definition 15 (Sierpiński domain $\mathbb{S}$). The Sierpiński domain $\mathbb{S}$ is the free pointed dcpo on a single generator. We can realize $\mathbb{S}$ as the set of truth values, that is, as the powerset $\mathcal P({\{{*}\}})$ of a singleton. The compact elements of $\mathbb{S}$ are exactly the elements $\bot := \emptyset$ and $\top := \{{*}\}$.

Lemma 16. For every continuous dcpo D, if a subset $B \,\subseteq\, D$ is a basis for the dcpo D, then is a basis for the Scott topology on D.

Proof. Suppose that B is a basis of the continuous dcpo D and let $U \,\subseteq\, D$ be an arbitrary Scott open. We claim that which would finish the proof. If $b \in B \cap U$, then because U is upper closed. Conversely, if $x \in U$, then, since B is a basis, x is the directed supremum $\bigsqcup \{{b \in B \mid b \ll x}\}$. Because U is Scott open, there must exist $b \in B$ with $b \ll x$ such that $b \in U$. Hence, $b \in B \cap U$ and , as desired.

Proposition 17. Every basis of a continuous dcpo is dense with respect to the Scott topology in the following (classically equivalent) ways:

1. (1) the Scott closure of the basis is the whole dcpo;

2. (2) every inhabited Scott open contains a point in the basis.

Proof. Suppose that B is a basis of a continuous dcpo D. (1): Let C be an arbitrary Scott closed subset of D containing B. We wish to show that $D \,\subseteq\, C$, so let $x \in D$ be arbitrary. Since B is a basis, we have . Note that , so C must also contain x because Scott closed subsets are closed under directed suprema. (2): If U is a Scott open containing a point x, then from and the fact that U is Scott open, we see that U must contain an element of B.

Proposition 18 (Interpolation). If $x \ll y$ are elements of a continuous dcpo D, then there exists $b \in D$ with $x \ll b \ll y$. Moreover, if D has a basis B, then there exists such an element b in B.

Lemma 19. For every two elements x and y of a continuous dcpo D, we have

$$ x \mathrel{\sqsubseteq} y \iff \forall_{z \in D}\,({z \ll x \to z \ll y}) \iff \forall_{z \in D}\,({z \ll x \to z \mathrel{\sqsubseteq} y}).$$

Moreover, if D has a basis B, then

$$ x \mathrel{\sqsubseteq} y \iff \forall_{b \in B}\,({b \ll x \to b \ll y}) \iff \forall_{b \in B}\,({b \ll x \to b \mathrel{\sqsubseteq} y}).$$

Definition 20 (Abstract basis and ideal completion $\textrm{Idl}(B,\prec)$). An abstract basis is a pair $(B,\prec)$ such that $\prec$ is transitive and interpolative: for every $b \in B$, the subset $\,\downarrow\, b := \{{a \in B \mid a \prec b}\}$ is directed. The rounded ideal completion $\textrm{Idl}(B,\prec)$ of an abstract basis $(B,\prec)$ consists of directed lower sets of $(B,\prec)$, known as (rounded) ideals, ordered by subset inclusion. It is a continuous dcpo with basis $\{{\,\downarrow\, b \mid b \in B}\}$ and directed suprema given by unions.

Lemma 21. If the relation $\prec$ of an abstract basis $(B,\prec)$ is reflexive, then $\textrm{Idl}(B,\prec)$ is algebraic and its compact elements are exactly those of the form $\,\downarrow\, b$ for $b \in B$.

2.3 Decidability conditions

Every continuous dcpo D has a basis, namely D itself. Our interest in bases lies in the fact that we can ask a dcpo to have a basis satisfying certain decidability conditions that we could not reasonably impose on the entire dcpo. For instance, the basis $\{{\bot,\top}\}$ of the Sierpiński domain $\mathbb{S}$ has decidable equality, but decidable equality on all of $\mathbb{S}$ is equivalent to excluded middle.

The first decidability condition that we will consider is for bases B of a pointed continuous dcpo:

\begin{equation}\tag{$\delta_\bot$} \text{For every } b \in B, \text{ it is decidable whether } b = \bot.\end{equation}

The second and third decidability conditions are for bases of any continuous dcpo:

\begin{gather}\tag{$\delta_{\ll}$} \text{For every } a,b \in B, \text{ it is decidable whether } a \ll b. \\ \tag{$\delta_{\mathrel{\sqsubseteq}}$} \text{For every } a,b \in B, \text{ it is decidable whether } a \mathrel{\sqsubseteq} b.\end{gather}

Observe that each of and implies for pointed dcpos, because $\bot$ is compact. In general, neither of the conditions and implies the other, at least as far as we know. However, in some cases, for example, when B is Kuratowski finite, is a stronger condition, because of Lemma 19. Moreover, if the dcpo is algebraic, then conditions and are equivalent for the unique basis of compact elements.

Finally, we remark that many natural examples in domain theory satisfy the decidability conditions. In particular, this holds for all examples in Section 7.

Again, we stress that these decidability conditions are necessarily restricted to the basis, as the following proposition shows.

Proposition 22. Let D be any pointed dcpo that is nontrivial in the sense that there exists $x \in D$ with $x \neq \bot$. If $y = \bot$ is decidable for every $y \in D$, then weak excluded middle follows.

Proof. For any proposition P, observe that $\lnot P$ holds if and only if $\bigsqcup \{{x \mid P}\} = \bot$. Hence, if $y = \bot$ is decidable for every $y \in D$, then so is $\lnot P$ for every proposition P.

Moreover, if the order relation of a dcpo is decidable, then, by antisymmetry, the dcpo must have decidable equality, but we showed in de Jong and Escardó (2021b, Corollary 39) that this implies (weak) excluded middle, unless the dcpo is trivial.

For understanding these results, it is important to recall that the two-element poset with $\bot \mathrel{\sqsubseteq} \top$ cannot be shown to be directed complete, constructively.

We now show that the decidability conditions , and are preserved by taking products and exponentials (function spaces) of dcpos.

Definition 23 (Product of dcpos $D \times E$). The product $D \times E$ of two dcpos D and E is given by their Cartesian product ordered pairwise. The supremum of a directed subset $S \,\subseteq\, D \times E$ is given by the pair of suprema $\bigsqcup \{{x \in D \mid \exists_{y \in E}\, (x,y) \in S}\}$ and $\bigsqcup \{{y \in D \mid \exists_{x \in D}\, (x,y) \in S}\}$.

Proposition 24. If D and E are continuous dcpos with bases $B_D$ and $B_E$, then $B_D \times B_E$ is a basis for the product $D \times E$. Also, if $B_D$ and $B_E$ both satisfy , then so does $B_D \times B_E$, and similarly for and .

Definition 25 (Scott continuity). A function between dcpos is Scott continuous if it preserves directed suprema.

Definition 26 (Exponential of dcpos $E^D$). The exponential $E^D$ of two dcpos D and E is given by the set of Scott continuous functions from D to E ordered pointwise, that is, $f \mathrel{\sqsubseteq} g$ if $\forall_{x \in D}\,f(x) \mathrel{\sqsubseteq} g(x)$ for $f,g\colon D \to E$. Suprema of directed subsets are also given pointwise.

We use the name “exponential” for $E^D$, because this construction (together with the product) witnesses that the category of dcpos is Cartesian closed. In the (bounded complete) algebraic case, a basis for the exponential can be constructed using step functions which we recall now.

Definition 27 (Step function). Given an element x of a dcpo D and an element y of a pointed dcpo E, the single-step function is defined as . A step-function is the supremum of a Kuratowski finite (recall Example 14) subset of single-step functions.

Lemma 28. If x is a compact element of D and y is any element of a pointed dcpo E, then the single-step function is Scott continuous. If y is also compact, then is a compact element of the exponential $E^D$.

Lemma 29. For every element x of a dcpo D, element y of a pointed dcpo E and Scott continuous function $f \colon D \to E$, we have if and only if $y \mathrel{\sqsubseteq} f(x)$.

Lemma 30. The compact elements of a dcpo are closed under existing Kuratowski finite suprema.

Definition 31 (Bounded completeness). A subset S of a poset $(X,\mathrel{\sqsubseteq})$ is bounded if there exists $x \in X$ such that $s \mathrel{\sqsubseteq} x$ for every $s \in S$. A poset $(X,\mathrel{\sqsubseteq})$ is bounded complete if every bounded subset $S \,\subseteq\, X$ has a supremum $\bigsqcup S$ in X.

Proposition 32. If D is an inhabited algebraic dcpo with basis of compact elements $B_D$ and E is a pointed bounded complete algebraic dcpo with basis of compact elements $B_E$, then

is the basis of compact elements for the algebraic exponential $E^D$. Moreover, if $B_E$ satisfies , then so does B. Finally, if $B_D$ and $B_E$ both satisfy (or equivalently, ), then B satisfies and too.

Proof. Firstly, notice that B is well-defined as suprema are given pointwise and E is bounded complete. Secondly, B consists of compact elements by Lemmas 28 and 30. Next, we show that B is indeed a basis for $E^D$. So suppose that $f \colon D \to E$ is Scott continuous. We show that is directed. Observe that this set is indeed semidirected: if S and T are Kuratowski finite subsets of single-step functions bounded by f, then so is $S \cup T$ and its supremum is above those of S and T. Moreover, the set is inhabited, because D is inhabited, so there must exist some $b \in B_D$ and then is a single-step function way below f. Hence, $B \cap \,\downarrow\, f$ is directed, as desired. Next, we prove that f equals the supremum of $B \cap \,\downarrow\, f$, which exists because $B \cap \,\downarrow\, f$ is bounded by f. So let $x \in D$ be arbitrary. We must show that $f(x) \mathrel{\sqsubseteq} ({\bigsqcup({B \cap \,\downarrow\, f})})(x)$. Using continuity of f, it suffices to prove that $f(a) \mathrel{\sqsubseteq} ({\bigsqcup({B \cap \,\downarrow\, f})})(x)$ for every $a \in B_D$ with $a \mathrel{\sqsubseteq} x$. So fix $a \in B_D$ with $a \mathrel{\sqsubseteq} x$. Since $B_E$ is a basis for E, it is enough to prove that $b \mathrel{\sqsubseteq} ({\bigsqcup({B \cap \,\downarrow\, f})})(x)$ for every $b \in B_E$ with $b \mathrel{\sqsubseteq} f(a)$. But if we have $b \in B_E$ with $b \mathrel{\sqsubseteq} f(a)$, then by Lemma 29, so , as desired.

Now suppose that $B_E$ satisfies and let $\bigsqcup S \in B$. Notice that the least element of $E^D$ is given by $x \mapsto \bot$. We wish to show that it is decidable whether $\bigsqcup S = ({x \mapsto \bot})$. Since S is Kuratowski finite, it is enough to show that is decidable for every . By Lemma 29, this inequality reduces to $b = \bot$, which is indeed decidable as $B_E$ is assumed to satisfy .

Finally, assume that both $B_D$ and $B_E$ satisfy and suppose that $\bigsqcup S, \bigsqcup T \in B$. We must prove that $\bigsqcup S \mathrel{\sqsubseteq} \bigsqcup T$ is decidable. Since S is Kuratowski finite, it is enough to prove that is decidable for every . By Lemma 29, this inequality reduces to $b \mathrel{\sqsubseteq} ({\bigsqcup T})(a)$. Write T as a Kuratowski finite set of single-step functions: . Then $({\bigsqcup T})(a) = \bigsqcup\{{\chi_1(a),\chi_2(a),\dots,\chi_n(a)}\}$ where

\[ \chi_i(a) := \begin{cases} b_i &\text{if } a_i \mathrel{\sqsubseteq} a; \\ \bot &\text{else}; \end{cases} \]

using that $B_D$ satisfies . Hence, since $B_E$ is closed under finite bounded suprema by Lemma 30, we see that $({\bigsqcup T})(a) \in B_E$. But then $b \mathrel{\sqsubseteq} ({\bigsqcup T})(a)$ is decidable because $B_E$ satisfies by assumption.

3. The Intrinsic Apartness

Definition 33 (Specialization preorder $\leq$ and $\mathrel{\;\not\!\not{\!\leq}}$). The specialization preorder on a topological space X is the preorder ${\leq}$ on X given by putting $x \leq y$ if every open neighborhood of x is an open neighborhood of y. Given $x,y\in X$, we write $x \mathrel{\;\not\!\not{\!\leq}} y$ if there exists an open neighborhood of x that does not contain y.

Observe that $x \mathrel{\;\not\!\not{\!\leq}} y$ is classically equivalent to $x \nleq y$, the logical negation of $x \leq y$. We also write $x \not\mathrel{\sqsubseteq} y$ for the logical negation of $x \mathrel{\sqsubseteq} y$, where ${\mathrel{\sqsubseteq}}$ is the partial order on a dcpo.

Definition 34 (Apartness). An apartness on a set X is a binary relation ${\mathrel{\#}}$ on X satisfying

1. (1) irreflexivity: $x \mathrel{\#} x$ is false for every $x \in X$;

2. (2) symmetry: if $x \mathrel{\#} y$, then $y \mathrel{\#} x$ for every $x,y \in X$.

If $x \mathrel{\#} y$ holds, then x and y are said to be apart.

Notice that we do not require cotransitivity or tightness, cf. Warning 1 on p. 2. Also note that irreflexivity implies that if $x \mathrel{\#} y$, then $x \neq y$, so $\mathrel{\#}$ is a strengthening of inequality.

Definition 35 (Intrinsic apartness ${\mathrel{\#}}$). Given two points x and y of a topological space X, we say that x and y are intrinsically apart, written $x \mathrel{\#} y$, if $x \mathrel{\;\not\!\not{\!\leq}} y$ or $y \mathrel{\;\not\!\not{\!\leq}} x$. Thus, x is intrinsically apart from y if there is an open neighborhood of x that does not contain y or vice versa. It is clear that the relation ${\mathrel{\#}}$ is an apartness in the sense of Definition 34.

With excluded middle, one can show that the specialization preorder for the Scott topology on a dcpo coincides with the partial order of the dcpo. In particular, the specialization preorder is in fact a partial order. Constructively, we still have the following result.

Lemma 36. If $x \mathrel{\sqsubseteq} y$ in a dcpo D, then $x \leq y$, where ${\leq}$ is the specialization order of the Scott topology on D. If D is continuous, then the converse holds too, so ${\mathrel{\sqsubseteq}}$ and ${\leq}$ coincide in that case.

Proof. The first claim follows because Scott opens are upper sets. Now assume that D is continuous and that $x \leq y$. Then by Example 9 and hence, $x \mathrel{\sqsubseteq} y$ by Lemma 19.

Lemma 37. For a continuous dcpo D, we have $x \mathrel{\;\not\!\not{\!\leq}} y$ if and only if there exists $b \in D$ such that $b \ll x$, but $b \not\mathrel{\sqsubseteq} y$. Moreover, if D has a basis B, then there exists such an element b in B.

Proof. Suppose that B (which may be all of D) is a basis for D. If we have $b \in B$ with $b \ll x$ and $b \not\mathrel{\sqsubseteq} y$, then is a Scott open containing x, but not y, so $x \mathrel{\;\not\!\not{\!\leq}} y$. Conversely, if there exists a Scott open U with $x \in U$ and $y \not\in U$, then by Lemma 16, there exists $b \in B$ such that . Hence, $b \ll x$, but $b \not\mathrel{\sqsubseteq} y$, for if $b \mathrel{\sqsubseteq} y$, then $y \in U$ as U is an upper set, contradicting our assumption.

The condition in Lemma 37 appears in a remark right after (Gierz et al. 2003, Definition I-1.6), as a classically equivalent reading of $x \not\mathrel{\sqsubseteq} y$.

Example 38. Consider the powerset $\mathcal P({X})$ of a set X as a pointed algebraic dcpo. Using Lemma 37, we see that a subset $A \in \mathcal P({X})$ is intrinsically apart from the empty set if and only if A is inhabited. More generally, for $A,B \in \mathcal P({X})$, we have $A \mathrel{\;\not\!\not{\!\leq}} B$ if and only if $B \setminus A$ is inhabited.

Proposition 39.

1. (1) For any elements x and y of a dcpo D, we have that $x \mathrel{\;\not\!\not{\!\leq}} y$ implies $x \not\mathrel{\sqsubseteq} y$.

2. (2) The converse of (1) holds if and only if excluded middle holds. In particular, if the converse of (1) holds for all elements of the Sierpiński domain $\mathbb{S}$, then excluded middle follows.

3. (3) For any elements x and y of a dcpo D, we have that $x \mathrel{\#} y$ implies $x \neq y$.

4. (4) The converse of (3) holds if and only if excluded middle holds. In particular, if the converse of (3) holds for all elements of the Sierpiński domain $\mathbb{S}$, then excluded middle follows.

5. (5) If c is a compact element of a dcpo D and $x \in D$, then $c \not\mathrel{\sqsubseteq} x$ implies $c \mathrel{\;\not\!\not{\!\leq}} x$, without the need to assume excluded middle.

Proof. (1): This is just the contrapositive of the first claim in Lemma 36. (2): It is straightforward to prove the implication if excluded middle holds. For the converse, assume that $x \not\mathrel{\sqsubseteq} y$ implies $x \mathrel{\;\not\!\not{\!\leq}} y$ for every $x,y \in \mathbb{S}$. We are going to show that $\lnot\lnot P \to P$ for every proposition P, which is equivalent to excluded middle. So let P be an arbitrary proposition and assume that $\lnot\lnot P$ holds. Then the element $\chi_P := \{{* \mid P}\} \in \mathbb{S}$ satisfies $\chi_P \not\mathrel{\sqsubseteq} \bot$. So $\chi_P \mathrel{\;\not\!\not{\!\leq}} \bot$ by assumption. By Lemma 37 and Example 14, there exists $b \in \{{\bot,\top}\}$ such that $b \ll \chi_P$ and $b \neq \bot$. The latter implies $b = \top = \{{*}\}$, which means that $\chi_P$ must be inhabited, which is equivalent to P holding. (3): Since the intrinsic apartness is irreflexive. (4): Similar to (2). (5): If c is compact and $c \not\mathrel{\sqsubseteq} x$, then is a Scott open containing c, but not x.

With excluded middle, complements of Scott closed subsets are Scott open. In particular, the subset $\{{x \in D \mid x \not\mathrel{\sqsubseteq} y}\}$ is Scott open for any element y of a dcpo D. Constructively, we have the following result:

Lemma 40. For any element y of a dcpo D, the Scott interior of $\{{x \in D \mid x \not\mathrel{\sqsubseteq} y}\}$ is given by the subset $\{{x \in D \mid x \mathrel{\;\not\!\not{\!\leq}} y}\}$, where we recall that $x \mathrel{\;\not\!\not{\!\leq}} y$ means that there exists a Scott open containing x but not y.

Proof. Notice that $\{{x \in D \mid x \mathrel{\;\not\!\not{\!\leq}} y}\}$ is the same thing as $\bigcup\{{U \,\subseteq\, D \mid U \text{ is Scott open and } y \not\in U}\}$, which is a union of opens and therefore open itself. Moreover, $\{{x \in D \mid x \mathrel{\;\not\!\not{\!\leq}} y}\}$ is contained in $\{{x \in D \mid x \not\mathrel{\sqsubseteq} y}\}$ by Proposition 39. Finally, if V is a Scott open contained in $\{{x \in D \mid x \not\mathrel{\sqsubseteq} y}\}$, then $y \not\in V$, since $y \not\mathrel{\sqsubseteq} y$ is false. Hence, $V \,\subseteq\, \bigcup\{{U \,\subseteq\, D\mid U \text{ is Scott open and } y \not\in U}\} = \{{x \in D \mid x \mathrel{\;\not\!\not{\!\leq}} y}\}$, completing the proof.

Proposition 41. If the complement of every Scott closed subset of the Sierpiński domain $\mathbb{S}$ is Scott open, then excluded middle follows.

Proof. If the complement of every Scott closed subset of $\mathbb{S}$ is Scott open, then $x \not\mathrel{\sqsubseteq} y$ implies $x \mathrel{\;\not\!\not{\!\leq}} y$ for every two points $x,y \in \mathbb{S}$ by Lemma 40. Hence, excluded middle would follow by Proposition 39.

An element x of a pointed dcpo may be said to be nontrivial if $x \neq \bot$. Given our notion of apartness, we might consider the constructively stronger $x \mathrel{\#} \bot$. We show that this is related to Johnstone’s notion of positivity (Johnstone 1984, p. 98). In de Jong and Escardó (2021b, Definition 25), we adapted Johnstone’s notion of positivity from locales to a general class of posets that includes dcpos. Here we give an equivalent, but simpler, definition just for pointed dcpos.

Definition 42 (Positivity) An element x of a pointed dcpo D is positive if every semidirected subset $S \,\subseteq\, D$ satisfying $x \mathrel{\sqsubseteq} \bigsqcup S$ is inhabited (and hence directed).

Proposition 43. For every element x of a pointed dcpo, if $x \mathrel{\#} \bot$, then x is positive. In the other direction, if D is a continuous pointed dcpo with a basis satisfying , then every positive element of D is apart from $\bot$.

Proof. Suppose first that x is an element of a pointed dcpo D and that $x \mathrel{\#} \bot$. Then we have a Scott open U containing x but not $\bot$. Now suppose that $S \,\subseteq\, D$ is semidirected with $x \mathrel{\sqsubseteq} \bigsqcup S$. Scott opens are upper sets, so $\bigsqcup S \in U$. Now $S' := S \cup \{{\bot}\}$ is a directed subset of D with the same supremum as S. In particular, $\bigsqcup S' \in U$. But then there exists $y \in S'$ such that $y \in U$ already, because U is Scott open. By construction of S’, we have $y = \bot$ or $y \in S$. As the former is impossible, we are done.

For the other claim, assume that D is continuous with a basis B satisfying and that $x \in D$ is positive. Consider the subset $S := \{{b \in B \mid b \ll x , b \neq \bot}\}$ and note that it is semidirected because is. If we can show that S is inhabited, then we see that $x \mathrel{\#} \bot$ by Lemma 37, which would finish the proof. As x is positive, it suffices to prove that $x \mathrel{\sqsubseteq} \bigsqcup S$. Since B is a basis, it is enough to prove that $b \mathrel{\sqsubseteq} \bigsqcup S$ for every $b \in B$ with $b \ll x$. So suppose that we have $b \in B$ with $b \ll x$. By the decidability condition either $b = \bot$ or $b \neq \bot$. In the first case, we get $b = \bot \mathrel{\sqsubseteq} \bigsqcup S$, as desired; in the second case, we get $b \mathrel{\sqsubseteq} \bigsqcup S$ because $b \in S$.

4. The Apartness Topology

In Bridges and Vîţǎ (2011, Section 2.2), the authors start with a topological space X equipped with an apartness relation ${\mathrel{\#}}$ and, using the topology and apartness, define a second topology on X, known as the apartness topology. A natural question is whether the original topology and the apartness topology coincide. For example, if X is a metric space and we set two points of X to be apart if their distance is strictly positive, then the Bridges-Vîţǎ apartness topology and the topology induced by the metric coincide (Proposition 2.2.10 in ibid). We show, assuming a modest $\lnot\lnot$-stability condition that holds in examples of interest, that the Scott topology on a continuous dcpo with the intrinsic apartness relation coincides with the apartness topology.

We start by repeating some basic definitions and results of Bridges and Vîţǎ. Recalling Warning 1 on p. 2, we remind the reader familiar with (Bridges and Vîţǎ 2011) that they write $\neq$ and use the word inequality for what we denote by $\mathrel{\#}$ and call apartness.

In constructive mathematics, positively defined notions are usually more useful than negatively defined ones. We already saw examples of this: ${\mathrel{\#}}$ versus ${\neq}$ and ${\mathrel{\;\not\!\not{\!\leq}}}$ versus ${\not\mathrel{\sqsubseteq}}$. We now use an apartness to give a positive definition of the complement of a set.

Definition 44 ((Logical) complement; Bridges and Vîţă 2011, pp. 19–20). Given a subset A of a set X with an apartness $\mathrel{\#,}$ we define the logical complement and the complement, respectively, as

1. (1) ${\lnot}\hspace{0.12em} A := \{{x \in X \mid x \not\in A}\} = \{{x \in X \mid \forall_{y \in A}\, x \neq y}\}$, and

2. (2) ${\sim} A := \{{x \in X \mid \forall_{y \in A}\,x \mathrel{\#} y}\}$.

Recall that, classically, a topological space is a $T_0$ or Kolmogorov space if $x \neq y$ implies that there exists an open U such that $x \in U$ and $y \not\in U$. This explains the name for the following definition of Bridges and Vîţǎ.

Definition 45 (Topological reverse Kolmogorov property; p. 29 in ibid). A topological space X equipped with an apartness ${\mathrel{\#}}$ satisfies the (topological) reverse Kolmogorov property if for every open U and points $x,y \in X$ with $x \in U$ and $y \not\in U$, we have $x \mathrel{\#} y$.

Lemma 46 (Proposition 2.2.2 in ibid). If a topological space X equipped with an apartness $\mathrel{\#}$ satisfies the reverse Kolmogorov property, then for every subset $A \,\subseteq\, X$, we have $({{\lnot}\hspace{0.12em} A})^\circ = ({{\sim} A})^\circ$, where $Y^\circ$ denotes the interior of Y in X.

Definition 47 (Apartness complement and topology, nearly open subset; pp. 20, 28 and 31 in ibid). For an element x of a topological space X with an apartness $\mathrel{\#}$ and a subset $A \,\subseteq\, X$, we write $x \mathrel{\bowtie} A$ if $x \in ({{\sim} A})^\circ$. This gives rise to the apartness complement: $- A := \{{x \in X \mid x \bowtie A}\}$. Subsets of the form $- A$ are called nearly open. The apartness topology on X is the topology whose basic opens are the nearly open subsets of X.

While the name “nearly open” may suggest otherwise, the apartness topology is coarser than the original topology:

Lemma 48 (Proposition 2.2.7 in ibid). Every nearly open subset of X is open in the original topology of X.

The following are original contributions.

Definition 49 ($\lnot\lnot$-stable basis). We say that a basis B for a topological space X is $\lnot\lnot$-stable if $U = ({\lnot\lnot U})^\circ$ for every open $U \in B$. Note that $U \,\subseteq\, ({\lnot\lnot U})^\circ$ holds for every open U, so the relevant condition is that $({\lnot\lnot U})^\circ \,\subseteq\, U$ for every basic open U.

Examples of such bases will be provided by Theorem 51 below.

Lemma 50. If a topological space X equipped with an apartness $\mathrel{\#}$ satisfies the reverse Kolmogorov property and has a $\lnot\lnot$-stable basis, then the original topology on X and the apartness topology on X coincide, that is, a subset of X is open (in the original topology) if and only if it is nearly open.

Proof. By Lemma 48, every nearly open subset of X is open in the original topology. So it remains to prove the converse. For this it suffices to prove that every basic open of X is nearly open. So let U be an arbitrary basic open of X. We are going to show that $U = -({{\lnot}\hspace{0.12em} U})$, which proves the claim, as the latter is nearly open. To this end, observe that

\begin{align*} -({{\lnot}\hspace{0.12em} U}) &= \{{x \in X \mid x \mathrel{\bowtie} {{\lnot}\hspace{0.12em} U}}\} &&\text{(by definition)} \\ &= \{{x \in X \mid x \in ({{\sim}({{\lnot}\hspace{0.12em} U})})^\circ}\} &&\text{(by definition)} \\ &= \{{x \in X \mid x \in ({{\lnot}\hspace{0.12em}{{\lnot}\hspace{0.12em} U}})^\circ}\} &&\text{(by Lemma 46)} \\ &= \{{x \in X \mid x \in U}\} &&\text{(by $\lnot\lnot$-stability of the basis)}, \end{align*}

so that $U = -({{\lnot}\hspace{0.12em} U})$, as desired.

Theorem 51. Let D be a continuous dcpo with a basis B. Each of the following conditions on the basis B implies that is a $\lnot\lnot$-stable basis for the Scott topology on D:

1. (1) For every $a,b\in B$, if $\lnot\lnot(a \ll b)$, then $({a \ll b})$.

2. (2) For every $a,b\in B$, if $\lnot\lnot(a \mathrel{\sqsubseteq} b)$, then $({a \mathrel{\sqsubseteq} b})$.

3. (3) B satisfies

4. (4) B satisfies

Hence, if one of these conditions holds, then the Scott topology on D coincides with the apartness topology on D with respect to the intrinsic apartness, that is, a subset of D is Scott open if and only if it is nearly open.

Proof. The final claim follows from Lemma 50 and the fact that the intrinsic apartness satisfies the reverse Kolmogorov property (by definition). Moreover, (3) implies (1) and (4) implies (2). So it suffices to show that if (1) or (2) holds, then is a $\lnot\lnot$-stable basis for the Scott topology on D, viz. that for every $a \in B$. Let $a \in B$ be arbitrary and suppose that . Using Scott openness and continuity of D, there exists $b \in B$ such that $b \ll x$ and . The latter just says that $\lnot\lnot (a \ll b)$. So if condition (1) holds, then we get $a \ll b$, so $a \ll x$ and , as desired. Now suppose that condition (2) holds. From $\lnot\lnot(a \ll b)$, we get $\lnot\lnot(a \mathrel{\sqsubseteq} b)$ and hence, $a \mathrel{\sqsubseteq} b$ by condition (2). So $a \mathrel{\sqsubseteq} b \ll x$ and , as wished.

5. Tightness, Cotransitivity, and Sharpness

We show that, in general, the intrinsic apartness will not be tight or cotransitive. In fact, we cannot expect any tight or cotransitive apartness relation on nontrivial dcpos. To remedy this, we introduce the notion of sharpness and we show (Theorem 68) that the sharp elements do satisfy tightness and cotransitivity for the intrinsic apartness.

Definition 52 (Tightness and cotransitivity). An apartness relation $\mathrel{\sharp}$ on a set X is tight if $\lnot(x \mathrel{\sharp} y)$ implies $x = y$ for every $x,y \in X$. The apartness is cotransitive if $x\mathrel{\sharp} y$ implies the disjunction of $x \mathrel{\sharp} z$ and $x \mathrel{\sharp} y$ for every $x,y,z \in X$.

Lemma 53. If X is a set with a tight apartness, then X is $\lnot\lnot$-separated, viz. $\lnot\lnot(x=y)$ implies $x = y$ for every $x,y \in X$.

Proof. For any apartness ${\mathrel{\sharp}}$ on X we have that $x \mathrel{\sharp} y$ implies $\lnot(x = y)$. Hence, $\lnot\lnot(x=y)$ implies $\lnot(x\mathrel{\sharp} y)$, so if ${\mathrel{\sharp}}$ is tight, then X is $\lnot\lnot$-separated.

It will be helpful to employ the following positive (but classically equivalent) formulation of $({x \mathrel{\sqsubseteq} y}) \land ({x \neq y})$ from de Jong and Escardó (2021b, Definition 20).

Definition 54 (Strictly below $\mathrel{\sqsubset}$). An element x of a dcpo D is strictly below an element y, written $x \mathrel{\sqsubset} y$, if $x \mathrel{\sqsubseteq} y$ and for every $z \mathrel{\sqsupseteq} y$ and proposition P, the equality $z = \bigsqcup({\{{x}\} \cup \{{z \mid P}\}})$ implies P.

We can relate the above notion to the intrinsic apartness, but, although we do not have a counterexample, we believe $x \mathrel{\sqsubset} y$ to be weaker than $x \mathrel{\#} y$ in general. However, if x is a sharp element of a continuous dcpo, then $x \mathrel{\sqsubset} y$ does imply $x \mathrel{\#} y$, as shown in Proposition 64.

Proposition 55. If $x \mathrel{\sqsubseteq} y$ are elements of a dcpo D with $x \mathrel{\#} y$, then $x \mathrel{\sqsubset} y$.

Proof. Suppose we have $x \mathrel{\sqsubseteq} y$ and $x \mathrel{\#} y$. Then $y \mathrel{\;\not\!\not{\!\leq}} x$ and hence by Lemma 37, there exists $b \in D$ with $b \ll y$ but $b \not\mathrel{\sqsubseteq} x$. Now let $z \mathrel{\sqsupseteq} y$ be arbitrary and P be a proposition with $z = \bigsqcup({\{{x}\} \cup \{{z \mid P}\}})$. We must prove that P holds. Since $b \ll y \mathrel{\sqsubseteq} z$, we have $b \ll z = \bigsqcup({\{{x}\} \cup \{{z \mid P}\}})$ and hence $b \mathrel{\sqsubseteq} x$ or $b \mathrel{\sqsubseteq} y$ and P holds. But $b \not\mathrel{\sqsubseteq} x$, so P must hold, as desired.

Example 56. In the Sierpiński domain $\mathbb{S}$ we have $\bot \mathrel{\sqsubset} \top$. In the powerset $\mathcal P({X})$ of some set X, the empty set is strictly below a subset A of X if and only if A is inhabited. More generally, if $A \,\subseteq\, B$ are subsets of some set, then $A \mathrel{\sqsubset} B$ holds if $B \setminus A$ is inhabited, and if A is a decidable subset and $A \mathrel{\sqsubset} B$, then $B \setminus A$ is inhabited.

The following shows that we cannot expect any tight or cotransitive apartness relations on nontrivial dcpos.

Theorem 57. Let D be a dcpo with an apartness relation ${\mathrel{\sharp}}$.

1. (1) If D has elements $x \mathrel{\sqsubset} y$, then tightness of ${\mathrel{\sharp}}$ implies excluded middle.

2. (2) If D has elements $x \mathrel{\sqsubseteq} y$ with $x \mathrel{\sharp} y$, then cotransitivity of ${\mathrel{\sharp}}$ implies weak excluded middle.

Proof. (1): If ${\mathrel{\sharp}}$ is tight, then D is $\lnot\lnot$-separated by Lemma 53, which, since D has elements $x \mathrel{\sqsubset} y$, implies excluded middle by de Jong and Escardó (2021b, Theorem 38). (2): For a proposition P, consider the supremum $s_P$ of the directed subset $\{{x}\} \cup \{{y \mid P}\}$. If ${\mathrel{\sharp}}$ is cotransitive, then either $x \mathrel{\sharp} s_P$ or $y \mathrel{\sharp} s_P$. In the first case, $x \neq s_P$, so that $\lnot\lnot P$ must be the case. In the second case, $y \neq s_P$, so that $\lnot P$ must be true. Hence, $\lnot P$ is decidable and weak excluded middle follows.

Theorem 57 works for any apartness relation. The following result specializes to the intrinsic apartness and derives full excluded middle from cotransitivity.

Theorem 58.

1. (1) If excluded middle holds, then the intrinsic apartness on any dcpo is tight. In the other direction, if D is a continuous dcpo with elements $x \mathrel{\sqsubseteq} y$ that are intrinsically apart, then tightness of the intrinsic apartness on D implies excluded middle.

2. (2) If excluded middle holds, then the intrinsic apartness on any dcpo is cotransitive. In the other direction, if D is a continuous dcpo and has elements $x \mathrel{\sqsubseteq} y$ that are intrinsically apart, then cotransitivity of the intrinsic apartness on D implies excluded middle.

3. (3) In particular, if the intrinsic apartness on the Sierpiński domain $\mathbb{S}$ is tight or cotransitive, then excluded middle follows.

Proof. (1): If excluded middle holds, then $\mathrel{\#}$ coincides with $\neq$ which is easily seen to be tight using excluded middle. Now suppose that D is continuous with elements $x \mathrel{\sqsubseteq} y$ such that $x \mathrel{\#} y$. By Theorem 57, it satisfies to show that $x \mathrel{\sqsubset} y$, but this follows from Proposition 55.

(2): If excluded middle holds, then $\mathrel{\#}$ coincides with $\neq$ which is easily seen to be cotransitive using excluded middle. Now suppose that D is continuous with elements $x \mathrel{\sqsubseteq} y$ such that $x \mathrel{\#} y$. As in the proof of Theorem 57, for any proposition P, consider the supremum $s_P$ of the directed subset $\{{x}\} \cup \{{y \mid P}\}$. If ${\mathrel{\#}}$ is cotransitive, then either $x \mathrel{\#} s_P$ or $y \mathrel{\#} s_P$. If $y \mathrel{\#} s_P$, then $\lnot P$ must be the case, as P implies that $y = s_P$. So suppose that $x \mathrel{\#} s_P$. Then $s_P \mathrel{\;\not\!\not{\!\leq}} x$, because $x \mathrel{\sqsubseteq} s_P$. By Lemma 37, there exists $d \in D$ with $d \ll s_P$ and $d \not\mathrel{\sqsubseteq} x$. Since $d \ll s_P$, there must exist $e \in \{{x}\}\cup\{{y \mid P}\}$ such that $d \mathrel{\sqsubseteq} e$. But $d \not\mathrel{\sqsubseteq} x$, so $e = y$ and P must be true. Hence, P is decidable.

(3): This follows from the above and the fact that the elements $\bot \mathrel{\sqsubseteq} \top$ of $\mathbb{S}$ are intrinsically apart.

We now isolate a collection of elements, which we call sharp elements, for which the intrinsic apartness is tight and cotransitive. The definition of a sharp element of a continuous dcpo may be somewhat opaque, but the algebraic case (Proposition 62) is easier to understand: an element x is sharp if and only if $c \mathrel{\sqsubseteq} x$ is decidable for every compact element c. Sharpness also occurs naturally in our examples in Section 7, for example, a lower real is sharp if and only if it is located.

Definition 59 (Sharpness). An element x of a dcpo D is sharp if for every $y,z\in D$ with $y \ll z$ we have $y \ll x$ or $z \not\mathrel{\sqsubseteq} x$.

Theorem 66 below provides many examples of sharp elements. Our first result is that sharpness in continuous dcpos is equivalent to a seemingly stronger condition.

Proposition 60. An element x of a continuous dcpo D is sharp if and only if for every $y,z \in D$ with $y \ll z$ we have $y \ll x$ or $z \mathrel{\;\not\!\not{\!\leq}} x$.

Proof. The right-to-left implication is clear, as $z \mathrel{\;\not\!\not{\!\leq}} x$ implies $z \not\mathrel{\sqsubseteq} x$. Now suppose that x is sharp and that we have $y \ll z$. Using interpolation twice, there exist $u,v \in D$ with $y \ll u \ll v \ll z$. By sharpness of x, we have $u \ll x$ or $v \not\mathrel{\sqsubseteq} x$. If $u \ll x$, then $y \ll x$ and we are done; if $v \not\mathrel{\sqsubseteq} x$, then $z \mathrel{\;\not\!\not{\!\leq}} x$ by Lemma 37.

As expected, it suffices to check sharpness condition for basis elements, and in the algebraic case, an even simpler criterion is available, as we show now.

Lemma 61. An element x of a continuous dcpo D with a basis B is sharp if and only if for every $a,b \in B$ with $a \ll b$ we have $a \ll x$ or $b \not\mathrel{\sqsubseteq} x$.

Proof. This is similar to the proof of Proposition 60, but we use that the interpolants can be found in the basis.

Proposition 62. An element x of an algebraic dcpo D is sharp if and only if for every compact $c \in D$ it is decidable whether $c \mathrel{\sqsubseteq} x$ holds.

Proof. Suppose that we sharp element x and let c be an arbitrary compact element. By compactness of c and sharpness of x, we have $c \ll x$ or $c \not\mathrel{\sqsubseteq} x$, so $c \mathrel{\sqsubseteq} x$ is decidable, as desired. Conversely, suppose that $c \mathrel{\sqsubseteq} x$ is decidable for every compact element $c \in D$. We use Lemma 61 applied to the basis of compact elements, so let $a \ll b$ be compact elements. By the decidability assumption, either $a \mathrel{\sqsubseteq} x$ or not. In the first case, we get $a \ll x$ as desired by compactness of a. In the second case, we get $b \not\mathrel{\sqsubseteq} x$, completing the proof.

Proposition 63. Assuming excluded middle, every element of any dcpo is sharp. The sharp elements of the Sierpiński domain $\mathbb{S}$ are exactly $\bot$ and $\top$. Hence, if every element of $\mathbb{S}$ is sharp, then excluded middle follows.

Proof. Let x be an arbitrary element of a dcpo D and suppose that y and z are elements of D with $y \ll z$. By excluded middle, we have $z \mathrel{\sqsubseteq} x$ or $z \not\mathrel{\sqsubseteq} x$. In the latter case, we are done. And if $z \mathrel{\sqsubseteq} x$, then $y \ll z \mathrel{\sqsubseteq} x$, so $y \ll x$. By Proposition 62, an element $x \in \mathbb{S}$ is sharp if and only if $\top = \{{*}\} \mathrel{\sqsubseteq} x$ is decidable, so the sharp elements of $\mathbb{S}$ are exactly the decidable subsets of $\{{\ast}\}$. Hence, the only sharp elements of $\mathbb{S}$ are $\bot = \emptyset$ and $\top$.

Sharpness also allows us to prove a converse to Proposition 55:

Proposition 64. If x is a sharp element of a continuous dcpo D, then $x \mathrel{\sqsubset} y$ implies $x \mathrel{\#} y$ for every element $y \in D$.

Proof. Suppose that x is a sharp element of a continuous dcpo D with $x \mathrel{\sqsubset} y$. We are going to show that $y \mathrel{\;\not\!\not{\!\leq}} x$ which implies $x \mathrel{\#} y$ by definition. By continuity of D and our assumption $x \mathrel{\sqsubset} y$, it suffices to prove that $d \mathrel{\sqsubseteq} \bigsqcup\{x\} \cup \{y \mid y \mathrel{\;\not\!\not{\!\leq}} x\}$ for every $d \ll y$. Given such $d \ll y$, we have $d \ll x$ or $y \mathrel{\;\not\!\not{\!\leq}} x$ by sharpness of x and Proposition 60. In either case, we get the desired inequality, completing the proof.

We can relate the notion of sharpness to a notion by Spitters (2010) and Kawai (2017, Definition 3.5) of a located subset: A subset V of a poset S is located if for every $s,t \in S$ with $s \ll t$, we have $t \in V$ or $s \not\in V$.

Proposition 65. An element x of a continuous dcpo is sharp if and only if the filter of Scott open neighborhoods of x is located in the poset of Scott opens of D.

Proof. Suppose first that $x \in D$ is sharp. We show that the filter $\mathcal{N} (x)$ of Scott open neighborhoods of x is located in the poset of Scott opens of D. So assume that we have Scott opens U and V with $U \ll V$. We must show that $x \in V$ or $x \not\in U$. Using continuity of D, interpolation, and Scott openness of V, we can prove that the inclusion holds. Hence, since also $U \ll V$, there are finitely many elements $d_1,d_2,\dots,d_n \in V$ and $e_1,e_2,\dots,e_n \in D$ with $d_1 \ll e_1 , \dots , d_n \ll e_n$ such that . For every $1 \leq i \leq n$, we have $d_i \ll x$ or $e_i \not\mathrel{\sqsubseteq} x$ by sharpness of x. We can distinguish two cases: either $d_j \ll x$ for some $1 \leq j \leq n$ or $e_i \not\mathrel{\sqsubseteq} x$ for every $1 \leq i \leq n$. If the former holds, then , so $x \in V$ and we are done. And if the latter is the case, then $x \not\in U$ as we had . Thus, $x \in V$ or $x \not\in U$, as desired.

Conversely, suppose that $\mathcal{N}(x)$ is located and let $u,v \in D$ with $u \ll v$. We must show that $u \ll x$ or $v \not\mathrel{\sqsubseteq} x$. By interpolation, there exists $d \in D$ with $u \ll d \ll v$. Then in the poset of Scott opens of D. Hence, by locatedness of $\mathcal{N}(x)$, we have or . Hence, $u \ll x$ or $\lnot (d \ll x)$. In the first case, we are done immediately. In the second case, assuming $v \mathrel{\sqsubseteq} x$ leads to $d \ll x$, contradicting $\lnot (d \ll x)$, so $v \not\mathrel{\sqsubseteq} x$ and we are finished too.

The following theorems give examples of sharp elements.

Theorem 66. Let D be a continuous dcpo with a basis B.

1. (1) Assuming that D is pointed, the least element of D is sharp if B satisfies .

2. (2) Every element of B is sharp if B satisfies or . particular, in these cases, the sharp elements are a Scott dense subset of D in the sense of Proposition 17.

   If D is algebraic, then we can reverse the implications for the basis of compact elements of D:.

3. (3) Assuming that D is pointed, the least element of D is sharp if and only if the set of compact elements of D satisfies .

4. (4) The compact elements of D are sharp if and only if the set of compact elements of D satisfies or .

Proof. (1): Suppose first that B satisfies and let $a,b\in B$ with $a \ll b$ be arbitrary. By assumption, either $a = \bot$ or $a \neq \bot$. If $a = \bot$, then $a \ll \bot$, by compactness of $\bot$ and we are done. If $a \neq \bot$, then $a \not\mathrel{\sqsubseteq} \bot$, so $b \not\mathrel{\sqsubseteq} \bot$ and we are finished too. (2): Suppose that $x \in B$ and let $a,b \in B$ with $a \ll b$. If B satisfies , then either $a \ll x$ or $\lnot (a\ll x)$. In the first case we are done. In the second case, we get $b \not\mathrel{\sqsubseteq} x$, for if $b \mathrel{\sqsubseteq} x$, then $a \ll b \mathrel{\sqsubseteq} x$, so $a \ll x$, contradicting our assumption. If B satisfies , then either $b \mathrel{\sqsubseteq} x$ or $b \not\mathrel{\sqsubseteq} x$. In the second case we are done. In the first case, we get $a \ll b \mathrel{\sqsubseteq} x$, so $a \ll x$ and we are done too. Scott density of the sharp elements now follows at once from Proposition 2.2.

(3): Suppose that $\bot$ is sharp and let $c \in D$ be compact. By Proposition 62, it is decidable whether $c \mathrel{\sqsubseteq} \bot$ holds, so the set of compact elements of D satisfies . (4): If every compact element is sharp, then the set of compact elements satisfies by Proposition 32.

Theorem 67.

1. (1) An element (x,y) of the product of two dcpos D and E is sharp if and only if x and y are sharp elements of D and E, respectively.

2. (2) An element $f \colon D \to E$ of the exponential of two bounded complete, algebraic dcpos D and E is sharp if and only if f(c) is sharp in E for every compact element $c : D$.

Proof. (1): Straightforward as the order is component-wise. (2): Suppose that $f \colon D \to E$ is sharp and let $c \in D$ be an arbitrary compact element. By Proposition 62, we have to show that $e \mathrel{\sqsubseteq} f(c)$ is decidable for every compact element $e \in E$. But $e \mathrel{\sqsubseteq} f(c)$ holds exactly when by Lemma 29, which is decidable by sharpness of f and Proposition 62 again. For the converse, it suffices, by Propositions 32 and 62, to show that is decidable for $a \in D$ and $b \in E$ compact elements. But again this reduces to decidability of $b \mathrel{\sqsubseteq} f(a)$ which is implied by the assumed sharpness of f(a).

Finally, we see that sharp elements are well-behaved with respect to the intrinsic apartness, because we get tightness and cotransitivity when restricting to sharp elements.

Theorem 68.

1. (1) If y is a sharp element of a continuous D, then $\lnot (x \mathrel{\;\not\!\not{\!\leq}} y)$ implies $x \mathrel{\sqsubseteq} y$ for every $x \in D$. In particular, the intrinsic apartness on a continuous dcpo D is tight on sharp elements.

2. (2) The intrinsic apartness on a continuous dcpo D is cotransitive with respect to sharp elements in the following sense: for every $x,y \in D$ and sharp element $z \in D$, we have $x \mathrel{\#} y \to ({x \mathrel{\#} z \vee y \mathrel{\#} z})$.

Proof. (1): Suppose that y is sharp with $\lnot (x \mathrel{\;\not\!\not{\!\leq}} y)$. We use Lemma 19 to prove $x \mathrel{\sqsubseteq} y$. So let $u \in D$ with $u \ll x$. Using interpolation, there exists $v \in D$ with $u \ll v \ll x$. So by sharpness of y, we have $u \ll y$ or $v \not\mathrel{\sqsubseteq} y$. If $u \ll y$, then we are done; if $v \not\mathrel{\sqsubseteq} y$, then $x \mathrel{\;\not\!\not{\!\leq}} y$, contradicting our assumption. Now if x and y are both sharp and $\lnot (x \mathrel{\#} y)$, then $\lnot (x \mathrel{\;\not\!\not{\!\leq}} y)$ and $\lnot (y \mathrel{\;\not\!\not{\!\leq}} x)$. Hence, $x \mathrel{\sqsubseteq} y$ and $y \mathrel{\sqsubseteq} x$ by the above, from which $x = y$ follows using antisymmetry.

(2): Let $x,y \in D$ be such that $x \mathrel{\#} y$ and $z \in D$ any sharp element. Assume without loss of generality that $x \mathrel{\;\not\!\not{\!\leq}} y$. By Lemma 37 and interpolation, there exist $u,v \in D$ with $u \ll v \ll x$ and $u \not\mathrel{\sqsubseteq} y$. Since z is sharp, we have $u \ll z$ or $v \not\mathrel{\sqsubseteq} z$. If $u \ll z$, then by Lemma 37, we have $z \mathrel{\;\not\!\not{\!\leq}} y$, so $z \mathrel{\#} y$ and we are done. If $v \not\mathrel{\sqsubseteq} z$, then $x \mathrel{\;\not\!\not{\!\leq}} z$ by Lemma 37, so $x \mathrel{\#} z$, finishing the proof.

By Theorem 61, the basis elements of a continuous dcpo are sharp in many examples of interest. The following section provides a very different source of sharp elements.

6. Strongly Maximal Elements

Smyth (2006) explored, in a classical setting, the notion of a constructively maximal element, adapted from Martin-Löf (1970). In an unpublished manuscript, Heckmann (1998) arrived at an equivalent notion, assuming excluded middle as noted in Smyth (2006, Section 8), and called it strong maximality. Whereas Smyth works directly with abstract bases and rounded ideal completions, we instead work with continuous dcpos. We use a simplification of Smyth’s definition but follow Heckmann’s terminology. We show that every strongly maximal element is sharp, compare strong maximality to maximality highlighting connections to sharpness, and study the subspace of strongly maximal elements.

Definition 69 (Hausdorff separation). Two points x and y of a dcpo D are Hausdorff separated if we have disjoint Scott open neighborhoods of x and y, respectively.

Definition 70 (Strong maximality). An element x of a continuous dcpo D is strongly maximal if for every $u,v \in D$ with $u \ll v$, we have $u \ll x$ or v and x are Hausdorff separated.

The following gives another source of examples of sharp elements.

Proposition 71. Every strongly maximal element of a continuous dcpo is sharp.

Proof. Let x be a strongly maximal element of a continuous dcpo D and let $u,v\in D$ be such that $u \ll v$. By strong maximality, we have $u \ll x$ or v and x are Hausdorff separated. In the first case we are done immediately. And if v and x are Hausdorff separated, then $v \not\mathrel{\sqsubseteq} x$, because Scott opens are upper sets. Hence, x is sharp, as desired.

Corollary 72.

1. (1) The intrinsic apartness on a continuous dcpo D is tight on strongly maximal elements.

2. (2) The intrinsic apartness on a continuous dcpo D is cotransitive with respect to strongly maximal elements in the following sense: for every $x,y \in D$ and strongly maximal element $z \in D$, we have ${x \mathrel{\#} y \to ({x \mathrel{\#} z \vee y \mathrel{\#} z})}$.

Proof. By Proposition 71 and Theorem 68.

Similarly to sharpness, the condition of Definition 11 can be restricted to the basis and simplifies in the case of algebraic dcpos:

Lemma 73. If a continuous dcpo D has a basis B, then an element $x \in D$ is strongly maximal if and only if for every $a,b \in B$ with $a \ll b$, we have $a \ll x$ or b and x are Hausdorff separated.

Proof. The left-to-right implication is immediate. Conversely, suppose that x satisfies the criterion in the lemma and let $u,v \in D$ with $u \ll v$. Using interpolation twice, there are $a,b \in B$ such that $u \ll a \ll b \ll v$. By assumption, we have $a \ll x$ or b and x are Hausdorff separated. If $a \ll x$, then $u \ll a \ll x$ and we are done. And if b and x are Hausdorff separated, then so are v and x, because Scott opens are upper sets.

Lemma 74. An element x of an algebraic dcpo D is strongly maximal if and only if for every compact element $c \in D$, either $c \mathrel{\sqsubseteq} x$ or c and x are Hausdorff separated.

Proof. The left-to-right implication is clear. So suppose that x satisfies the condition in the lemma. We use Lemma 73 on the basis B of compact elements. So suppose that we have $a,b\in B$ with $a \ll b$. By assumption and compactness of a, either $a \ll x$ or a and x are Hausdorff separated. If $a \ll x$, then we are done. And if a and x are Hausdorff separated, then so are b and x, because Scott opens are upper sets.

Smyth’s formulation of strong maximality (Smyth 2006, Definition 4.1) (called constructive maximality there) is somewhat more involved than ours, but it is equivalent, as Proposition 78 shows.

Definition 75 (Refinement ). We say that two elements x and y of a dcpo D can be refined, written , if there exists $z \in D$ with $x \ll z$ and $y \ll z$.

On Smyth (2006, p. 362), refinement is denoted by $x \mathrel{\uparrow} y$, but we prefer , because one might want to reserve $x \mathrel{\uparrow} y$ for the weaker statement that there exists $z \in D$ with $x,y \mathrel{\sqsubseteq} z$.

Lemma 76. Two elements x and y of a continuous dcpo D are Hausdorff separated if and only if there exist $a,b \in D$ with $a \ll x$ and $b \ll y$ such that . Moreover, if D has a basis B, then x and y are Hausdorff separated if and only if there exist such elements a and b in B.

Proof. Suppose that D has a basis B (which may be all of D) and let x and y be Hausdorff separated elements of D. Then there are two disjoint basic opens containing x and y, respectively. Hence, by Lemma 16, there exist $a,b \in B$ such that , and . The latter says exactly that . Conversely, if we have $a,b\in B$ with $a \ll x$, $b \ll y$ and , then and are disjoint Scott opens containing x and y, respectively.

In Smyth (2006, p. 362), the condition in Lemma 76 is taken as a definition (for basis elements) and such elements a and b are said to lie apart and this notion is denoted by $a \mathrel{\sharp} b$. We now translate Definition 4.1 of Smyth (2006) from ideal completions of abstract bases to continuous dcpos.

Definition 77 (Smyth maximality). An element x of a continuous dcpo D is Smyth maximal if for every $u,v \in D$ with $u \ll v$, there exists $d \ll x$ such that $u \ll d$ or the condition in Lemma 76 holds for v and d.

Proposition 78. An element x of a continuous D is strongly maximal if and only if x is Smyth maximal.

Proof. The right-to-left implication is straightforward, thanks to Lemma 76. So suppose that x is strongly maximal and that we have $u \ll v$. Then $u \ll x$ holds or v and x are Hausdorff separated. Suppose first that $u \ll x$. Then by interpolation there exists $d \in D$ with $u \ll d \ll x$ and we are done. Now suppose that v and x are Hausdorff separated. Then we have disjoint Scott opens V and U containing v and x, respectively. By continuity of D and Scott openness of U, there exists $d \ll x$ with $d \in U$. But the opens V and U then witness Hausdorff separation of v and d too, so that Lemma 76 finishes the proof.

Finally, we show strong maximality is preserved by taking products and exponentials.

Proposition 79.

1. (1) An element (x,y) of the product of two dcpos D and E is strongly maximal if and only if both x and y are strongly maximal elements of D and E, respectively.

2. (2) An element $f \colon D \to E$ of the exponential of two bounded complete, algebraic dcpos D and E is strongly maximal if f(c) is strongly maximal in E for every compact element $c : D$.

Proof. (1) is easily verified, so we only give the details for (2). Suppose that f(c) is strongly maximal for every compact element $c \in D$. We show that f is strongly maximal in the exponential $E^D$. By Lemma 74 and Proposition 32, it is enough to prove that for every two compact elements $a \in D$ and $b \in E$, we have or and f can be Hausdorff separated. Given such elements a and b, we have either $b \mathrel{\sqsubseteq} f(a)$ or b and f(a) can be Hausdorff separated by strong maximality of f(a). In the first case, we get by Lemma 29, as desired. In the second case, we get, using Lemma 16, compact elements $c,d \in E$ such that and while . But now and are disjoint open neighborhoods of respectively f and in $E^D$, finishing the proof.

Note that, unlike in Theorem 67, the converse to Item (2) of Proposition 79 does not hold: the identity on $\mathcal L(\mathbb{N})$ is strongly maximal, but $\bot$ is not. Here, $\mathcal L(\mathbb{N})$ denotes the free pointed dcpo on the set of natural numbers (see Section 7.4), which, classically, is simply the flat dcpo $\mathbb{N} \cup \{\bot\}$.

6.1 Maximality and strong maximality

The name strong maximality is justified by the following observation:

Proposition 80 (cf. Proposition 4.2 in Smyth 2006). Every strongly maximal element of a continuous dcpo D is maximal, that is, if $x \in D$ is strongly maximal, then $x \mathrel{\sqsubseteq} y$ implies $x = y$ for every element $y \in D$.

Proof. Let x be a strongly maximal element of a continuous D and suppose that we have $y \in D$ with $x \mathrel{\sqsubseteq} y$. We need to prove that $y \mathrel{\sqsubseteq} x$. We do so using Lemma 19. So let $u \in D$ be such that $u \ll y$. Our goal is to prove that $u \ll x$. By strong maximality of x, we have $u \ll x$ or x and y are Hausdorff separated. In the first case we are done, while the second case is impossible, because $x \mathrel{\sqsubseteq} y$ and Scott opens are upper sets.

In the presence of excluded middle, Smyth (2006, Corollary 4.4) tells us that the converse of Proposition 80 is true if and only if the Lawson condition (Smyth 2006; Lawson 1997) holds for the dcpo (the Scott and Lawson topologies coincide on the subset of maximal elements). Without excluded middle, the situation is subtler and involves sharpness, as we show in Theorem 84.

The following lemma is a technical device for constructing maximal elements that, constructively, fail to be strongly maximal. Besides Proposition 82, it also finds application in Propositions 91 and 103.

Lemma 81. Suppose that we have elements x and y of a continuous dcpo D such that

1. (1) x and y are both strongly maximal,

2. (2) x and y have a greatest lower bound $x \mathrel{\sqcap} y$ in D, and

3. (3) x and y are intrinsically apart.

Then, for any proposition P, the supremum $\bigsqcup S$ of the directed subset

\[ S := \{{x \mathrel{\sqcap} y}\} \cup \{{x \mid \lnot P}\} \cup \{{y \mid \lnot\lnot P}\} \]

is maximal, but $\bigsqcup S$ is sharp if and only if $\lnot P$ is decidable. Hence, $\bigsqcup S$ is maximal, but if $\bigsqcup S$ is strongly maximal, then $\lnot P$ is decidable.

Proof. We start by showing that $\bigsqcup S$ is maximal. Suppose that we have $z \in D$ with $\bigsqcup S \mathrel{\sqsubseteq} z$. We use Lemma 19 to show that $z \mathrel{\sqsubseteq} \bigsqcup S$. So let $u \in D$ be such that $u \ll z$. Our goal is to show that $u \mathrel{\sqsubseteq} \bigsqcup S$. By strong maximality of x, we have $u \ll x$ or z and x are Hausdorff separated. As y is also strongly maximal, we have $u \ll y$ or z and y are Hausdorff separated. We thus distinguish four cases:

• • ($u \ll x$ and $u \ll y$): In this case, $u \mathrel{\sqsubseteq} {x \mathrel{\sqcap} y}$ by assumption (2). Hence, $u \mathrel{\sqsubseteq} {x \mathrel{\sqcap} y} \mathrel{\sqsubseteq} \bigsqcup S$, and we are done in this case.

• • ($u \ll x$ and z and y are Hausdorff separated): We claim that $\lnot P$ must hold in this case. For suppose that P were true. Then $y = \bigsqcup S \mathrel{\sqsubseteq} z$, contradicting that z and y are Hausdorff separated. Thus, $\lnot P$ holds. But then $\bigsqcup S = x$ and $u \ll x = \bigsqcup S$, so $u \mathrel{\sqsubseteq} \bigsqcup S$, as wished.

• • (z and x are Hausdorff separated and $u \ll y$): This is similar to the above case, but now $\lnot\lnot P$ must hold, so that ${u \ll y = \bigsqcup S}$, so $u \mathrel{\sqsubseteq} \bigsqcup S$, as desired.

• • (z and x are Hausdorff separated as are z and y): This case is impossible, as it implies, using an argument similar to that used in the previous two cases, that both $\lnot P$ and $\lnot\lnot P$ must hold.

So in all cases, we get the desired $u \mathrel{\sqsubseteq} \bigsqcup S$ and $\bigsqcup S$ is seen to be maximal.

Now suppose that $\bigsqcup S$ is sharp. We show that we can decide $\lnot P$. By assumption, x and y are apart. We assume that $x \mathrel{\;\not\!\not{\!\leq}} y$; the case for $y \mathrel{\;\not\!\not{\!\leq}} x$ is similar. By Lemma 37, there exists $d \in D$ with $d \ll x$ and $d \not\mathrel{\sqsubseteq} y$. By assumed sharpness of $\bigsqcup S$, we have $d \ll \bigsqcup S$ or $x \not\mathrel{\sqsubseteq} \bigsqcup S$. If $d \ll \bigsqcup S$, then we claim that $\lnot P$ holds. For suppose for a contradiction that P holds, then $d \ll \bigsqcup S = y$, contradicting $d \not\mathrel{\sqsubseteq} y$. Now suppose that $x \not\mathrel{\sqsubseteq} \bigsqcup S$. Since $\lnot P$ implies $x = \bigsqcup S$, we see that $\lnot\lnot P$ must hold in this case. Hence, $\lnot P$ is decidable.

Conversely, suppose that $\lnot P$ is decidable. If $\lnot P$ holds, then $\bigsqcup S = x$, so $\bigsqcup S$ must be sharp since x is by Proposition 71. And if $\lnot\lnot P$ holds, then $\bigsqcup S = y$, and sharpness of $\bigsqcup S$ follows from Proposition 71 and strong maximality of y. The final claim follows from Proposition 71 and the fact that we just proved that sharpness of $\bigsqcup S$ implies decidability of $\lnot P$.

Proposition 82. Let P be the poset with exactly three elements $\bot \leq 0,1$ and 0 and 1 unrelated. If every maximal element of the algebraic dcpo $\textrm{Idl}(P)$ is strongly maximal, then weak excluded middle follows. In the other direction, if excluded middle holds, then every maximal element of $\textrm{Idl}(P)$ is strongly maximal.

Proof. We apply Lemma 81 with $x := \{{\bot,0}\}$ and $y := \{{\bot,1}\}$ in $\textrm{Idl}(P)$. Observe that x and y are apart and that they have a greatest lower bound, namely $\{{\bot}\}$. Thus, it remains to show that they are both strongly maximal. We do so for x; the proof for y is similar. We apply Lemma 74 with the basis of compact elements $\{{\,\downarrow\, p \mid p \in P}\}$ and so distinguish three cases:

• • ($p = \bot$): Note that $\,\downarrow\, \bot = \{{\bot}\} \ll x$.

• • ($p = 0$): Note that $\,\downarrow\, 0 = \{{\bot,0}\} = x \ll x$.

• • ($p = 1$): The elements $\,\downarrow\, 1 = \{{\bot,1}\} = y$ and x are Hausdorff separated, since and are disjoint Scott opens containing x and y, respectively.

Thus, x and y are both strongly maximal, so weak excluded middle follows by Lemma 81. If excluded middle holds, then we can easily prove that all maximal elements of $\textrm{Idl}(P)$ are strongly maximal.

Theorem 4.3 of Smyth (2006) states that an element x of a continuous dcpo is strongly maximal if and only if every Lawson neighborhood of x contains a Scott neighborhood of x. This requirement on neighborhoods is, assuming excluded middle, equivalent to the Lawson condition (the Scott topology and the Lawson topology coincide on the subset of maximal elements), as used in Smyth (2006, Corollary 4.4) and proved in Gierz et al. (2003, Lemma V-6.5). Inspecting the proof of Gierz et al. (2003), we believe that excluded middle is essential. However, we can still prove a constructive analogue of Smyth (2006, Theorem 4.3), but it requires a positive formulation of the subbasic opens of the Lawson topology, using the relation ${\mathrel{\;\not\!\not{\!\leq}}}$ rather than ${\not\mathrel{\sqsubseteq}}$.

Definition 83 (Lawson topology). The subbasic Lawson closed subsets of a dcpo D are the Scott closed subsets and the upper sets of the form $\uparrow x$ for $x \in D$. The subbasic Lawson opens are the Scott opens and the sets of the form $\{{y \in D \mid x \mathrel{\;\not\!\not{\!\leq}} y}\}$ for $x \in D$.

In the presence of excluded middle, the subset $\{{y \in D \mid x \mathrel{\;\not\!\not{\!\leq}} y}\}$ is equal to $D \setminus \uparrow x$, so with excluded middle the above definition is equivalent to the classical definition of the subbasic Lawson opens as in Gierz et al. (2003, pp. 211–212).

Theorem 84 (cf. Smyth 2006, Theorem 4.3). An element x of a continuous dcpo is strongly maximal if and only if x is sharp and every Lawson neighborhood of x contains a Scott neighborhood of x.

Proof. Let x be a strongly maximal element of a continuous dcpo D. Then x is sharp by Proposition 71. It remains to show that every Lawson neighborhood of x contains a Scott neighborhood of x. It suffices to do so for the subbasic Lawson open neighborhoods of x and in particular for those of the form $\{{d \in D \mid y \mathrel{\;\not\!\not{\!\leq}} d}\}$ for $y \in D$. So suppose that we have $y \in D$ with $y \mathrel{\;\not\!\not{\!\leq}} x$. Then there exists $u \ll y$ with $u \not\mathrel{\sqsubseteq} x$. By strong maximality of x, we have $u \ll x$ or y and x are Hausdorff separated. Since $u \not\mathrel{\sqsubseteq} x$, the first case $u \ll x$ is impossible. Hence, we have disjoint Scott opens U and V containing x and y, respectively. We claim that $U \,\subseteq\, \{{d \in D \mid y \mathrel{\;\not\!\not{\!\leq}} d}\}$, which would finish the proof. Since V is a Scott open neighborhood of y, we can use continuity of D to find $v \ll y$ with $v \in V$. Now if $u \in U$, then because U and V are disjoint and Scott opens are upper sets, we must have $v \not\mathrel{\sqsubseteq} u$. Hence, v witnesses that $y \mathrel{\;\not\!\not{\!\leq}} u$, so that $U \,\subseteq\, \{{d \in D \mid y \mathrel{\;\not\!\not{\!\leq}} d}\}$.

Conversely, suppose that x is a sharp element of a continuous dcpo D such that every Lawson neighborhood of x contains a Scott neighborhood of x. We prove that x is strongly maximal. So let $u,v\in D$ such that $u \ll v$. By interpolation, there exist $u',v' \in D$ with $u \ll u' \ll v' \ll v$. Because x is sharp, we have $u \ll x$ or $u' \not\mathrel{\sqsubseteq} x$. In the first case we are done, so assume that $u' \not\mathrel{\sqsubseteq} x$. Then u’ witnesses $v' \mathrel{\;\not\!\not{\!\leq}} x$. Hence, $\{{d \in D \mid v' \mathrel{\;\not\!\not{\!\leq}} d}\}$ is a Lawson neighborhood of x. So by assumption on x, there exists a Scott open neighborhood U of x contained in $\{{d \in D \mid v' \mathrel{\;\not\!\not{\!\leq}} d}\}$. But then U and are disjoint Scott opens containing x and v, respectively. So x and v are Hausdorff separated.

By Proposition 63, every element is sharp if excluded middle is assumed, so in that case, we can drop the requirement that x is sharp. Hence, in the presence of excluded middle, we recover (Smyth 2006, Theorem 4.3) from Theorem 84.

6.2 The subspace of strongly maximal elements

The classical interest in strong maximality comes from the fact that, while the subspace of maximal elements may fail to be Hausdorff (Heckmann 1998, Example 4), the subspace of strongly maximal elements with the relative Scott topology is both Hausdorff and regular (Smyth 2006, Theorem 4.6). We offer constructive proofs of these claims, with the proviso that the Hausdorff condition is formulated with respect to the intrinsic apartness.

Proposition 85. The subspace of strongly maximal elements of a continuous dcpo D with the relative Scott topology is Hausdorff, that is, if x and y are strongly maximal, then $x \mathrel{\#} y$ if and only if there are disjoint Scott opens U and V such that $x \in U$ and $y \in V$.

Proof. Let x and y be strongly maximal elements. The right-to-left implication is immediate by definition of the intrinsic apartness. Now suppose that $x \mathrel{\#} y$. Using Lemma 37, we can assume without loss of generality that we have $d \in D$ with $d \ll x$ and $d \not\mathrel{\sqsubseteq} y$. Since y is strongly maximal, we have $d \ll y$ or x and y are Hausdorff separated. But $d \ll y$ is impossible, because $d \not\mathrel{\sqsubseteq} y$. So x and y are Hausdorff separated, as desired.

Proposition 86. The subspace of strongly maximal elements of a continuous dcpo D with the relative Scott topology is regular, that is, every Scott neighborhood of a point $x \in D$ contains a Scott closed neighborhood of x.

Proof. We adapt the proof of Smyth (2006, Theorem 4.6 (i)), avoiding the use of the axiom of choice. Write $\textrm{StrongMax}(D)$ for the subspace of strongly maximal elements of D and let x be a strongly maximal element. It suffices to prove the claim for basic Scott open neighborhoods of x. So suppose that for some $u \in D$. By interpolation, there exists ${v \in D}$ such that . We will construct a Scott closed subset C such that and

Define the Scott open subset V by

and the Scott closed subset $C := \lnot V = D \setminus V$.

Note that if $y \in V$, then $y \in U$ for some Scott open U with , so that . Hence, , so . Thus, , so C is a Scott closed neighborhood of x, as desired.

It remains to show that . So let $y \in C$ be strongly maximal. Then $u \ll y$ holds or v and y are Hausdorff separated. If $u \ll y$, then and we are done. So suppose that v and y are Hausdorff separated. We prove that this is impossible. Assume for a contradiction that we have disjoint Scott opens $U_v$ and $U_y$ containing v and y, respectively. Since $U_v$ is an upper set, we have . As $U_v$ and $U_y$ are disjoint, we thus get . Hence, $y \in U_y \,\subseteq\, V$, contradicting $y \in C$.

7. Examples

In this final section before the conclusion, we illustrate the foregoing notions of intrinsic apartness, sharpness, and strong maximality, by studying several natural examples. The first three examples are generalized domain environments in the sense of Heckmann (1998): we consider dcpos D and topological spaces X such that X embeds into the subspace of maximal elements of D. In fact, we will see that X is homeomorphic to the subspace of strongly maximal elements of D. Specifically, we will consider Cantor space, Baire space, and the real line. The penultimate example shows that sharpness characterizes exactly those lower reals that are located. The final example showcases another natural embedding of Cantor space into a dcpo constructed using exponentials and the lifting monad.

7.1 The Cantor and Baire domains

Fix an inhabited set A with decidable equality. Typically, we will be interested in $A = \mathbf{2} := \{{0,1}\}$ and $A = \mathbb{N}$. Recall that a finite sequence on A is a function $\{{0,1,\dots,{n-1}}\} \to A$ for a natural number $n \in \mathbb{N}$ (for $n = 0$ we get the empty sequence). An infinite sequence on A is simply a function $\mathbb{N} \to A$.

Definition 87 ($\mathbf{A}$ and $\mathcal{A}$).

1. (1) We write $({A^\ast , \preceq})$ for the poset of finite sequences on A ordered by prefix and $\mathcal{A}$ for the ideal completion of $({A^\ast , \preceq})$, which is an algebraic dcpo by Lemma 21.

2. (2) For an infinite sequence $\alpha$, we write $\bar{\alpha}_{n}$ for the first n elements of $\alpha$. Given a finite sequence $\sigma$, we write $\sigma \prec \alpha$ if $\sigma$ is an initial segment of $\alpha$.

3. (3) We write $\mathbf{A}$ for the space $A^\mathbb{N}$ of infinite sequences on A with the product topology, taking the discrete topologies on $\mathbb{N}$ and A. The sets $\{{\alpha \in \mathbf{A} \mid \sigma \prec \alpha}\}$ with $\sigma$ a finite sequence form a basis of opens for $\mathbf{A}$. Furthermore, the space $\mathbf{A}$ has a natural notion of apartness: $\alpha \mathrel{\#}_{\mathbf{A}} \beta \iff \exists_{n \in \mathbb{N}}\,\bar{\alpha}_{n} \neq \bar{\beta}_{n}$.

Definition 88 (Cantor and Baire space/domain). If $A = \mathbf{2}$, then $\mathbf{A}$ is Cantor space and we call $\mathcal{A}$ the Cantor domain, and if we take $A = \mathbb{N}$, then $\mathbf{A}$ is Baire space and we call $\mathcal{A}$ the Baire domain.

Definition 89 ($\iota$). We define an injection $\iota \colon \mathbf{A} \hookrightarrow \mathcal{A}$ by $\iota(\alpha) := \bigcup_{\sigma\prec\alpha} \,\downarrow\,\sigma = \{{\tau \in A^\ast \mid \tau \prec \alpha}\}$.

Theorem 90. The image of $\iota$ is exactly the subset of strongly maximal elements of $\mathcal{A}$.

Proof. We first prove that $\iota(\alpha)$ is strongly maximal for every infinite sequence $\alpha$, using Lemmas 74 and 21. So let $\sigma$ be a finite sequence. Since A has decidable equality and $\sigma$ is finite, either $\sigma \prec \alpha$ or not. If $\sigma \prec \alpha$, then $\,\downarrow\,\sigma = \{{\tau \in A^\ast \mid \tau \preceq \sigma}\} \ll \iota(\alpha)$ and we are done. So suppose that $\sigma \nprec \alpha$. Writing n for the length of $\sigma$, we see that $\sigma \neq \bar{\alpha}_{n}$. Therefore, the Scott opens and must be disjoint, while the former contains $\sigma$ and the latter contains $\alpha$, completing the proof that $\iota(\alpha)$ is strongly maximal.

Conversely, suppose that $x \in \mathcal{A}$ is strongly maximal. Using induction, we will construct for every natural number n, a finite sequence $\sigma_n$ of length n such that $\sigma_n \preceq \sigma_{n+1} \in x$. Given such finite sequences, we define the infinite sequence $\alpha$ by $\bar{\alpha}_{n} := \sigma_n$ and we claim that $x = \iota(\alpha)$. The inclusion $\iota(\alpha) \,\subseteq\, x$ is clear. For the other inclusion, suppose that $\tau \in x$. Then by directedness of x, we must have $\sigma_k = \tau$ where $k = \textrm{length}(\tau)$. Hence, $\tau \in \iota(\alpha)$, as desired. We now describe how to inductively construct each $\sigma_n$, starting with the empty sequence $\sigma_0$. Assume that we are given $\sigma_0 \preceq \sigma_1 \preceq \cdots \preceq \sigma_m \in x$ of length $0,1,\dots,m$ for some natural number m. We construct $\sigma_{m+1} \in x$ of length $m+1$ extending $\sigma_m$. Since A is assumed to be inhabited, we can extend $\sigma_m$ by some element $a \in A$ to get a finite sequence $\tau$ of length $m+1$. By Lemma 74, either $\tau \in x$ or $\,\downarrow\, \tau$ and x are Hausdorff separated. If $\tau \in x$, then we set $\sigma_{m+1} := \tau$. If $\,\downarrow\, \tau$ and x are Hausdorff separated, then by Lemma 76, there exists a finite sequence $\rho \in x$ such that $\rho$ and $\tau$ agree on the first m indices (since $\sigma_m \in x$), but disagree on index $m+1$. We now define $\sigma_{m+1}$ to be the extension of $\sigma_m$ by $\rho({m+1})$. Notice that $\sigma_{m+1} \in x$, as desired.

Proposition 91. Suppose that A has at least two elements. If every maximal element of $\mathcal{A}$ is strongly maximal, then weak excluded middle holds.

Proof. Let $a_0$ and $a_1$ be two nonequal elements of A. We use Lemma 81 with the following elements ${x := \iota(\langle{a_0,a_0,\dots}\rangle)}$ and $y := \iota(\langle{a_1,a_1,\dots}\rangle)$ of $\mathcal{A}$. By Theorem 90, the elements x and y are both strongly maximal. Moreover, x and y have a greatest lower bound, namely the singleton containing the empty sequence $\langle\rangle$. Finally, x and y are apart, as witnessed by the disjoint Scott opens and .

Example 92. Theorem 90 tells us that functions $\mathbb{N} \to A$ give strongly maximal elements of $\mathcal{A}$. An example of a maximal element that constructively fails to be strongly maximal is given by a $\lnot\lnot$-total function. More precisely, suppose that $R \,\subseteq\, \mathbb{N} \times A$ is a single-valued binary relation such that (1) membership of R is decidable, and (2) the relation R is $\lnot\lnot$-total, that is, we have $\lnot\lnot({\forall_{n \in \mathbb{N}}\exists_{a \in A}\,(n,a) \in R})$. We define

\[ \overline{R} := \{{\sigma \in A^\ast \mid (0,\sigma_0) , \ldots , (n-1,\sigma_{n-1}) \in R { with \textit{n} the \textrm{length} of $\sigma$}}\}. \]

Then $\overline R$ is a lower set and semidirected by single-valuedness of R, so that $\overline R \in \mathcal{A}$. Note that, by Theorem 90, $\overline R$ is not necessarily strongly maximal as R is only $\lnot\lnot$-total. But we claim that $\overline R$ is maximal. For suppose that $x \in \mathcal{A}$ is such that $\overline R \,\subseteq\, x$; we show that $x \,\subseteq\, \overline R$. So let $\sigma \in x$. By our assumption that membership of R is decidable it suffices to check that for every natural number i less than the length of $\sigma$ we have $\lnot((i,\sigma_i) \not\in R)$. So suppose for a contradiction that there exists an i with $(i,\sigma_i) \not\in R$. Since membership of R is decidable, we may assume that i is the least such number. We claim that there is no element $a \in A$ for which $(i,a) \in R$ holds, which contradicts $\lnot\lnot$-totality of R. For if $a \in A$ were such an element, then we define the sequence $\tau$ by extending $\overline{\sigma_{i-1}}$ with a. By the choice of i, we have $\tau \in \overline R$ and hence $\tau \in x$ since $\overline R \,\subseteq\, x$. But then $a = \sigma_i$ by semidirectedness of x, but we had $(i,\sigma_i) \not\in R$.

Definition 93 (Markov’s Principle). Markov’s Principle is the assertion that for every infinite binary sequence $\phi$ we have that $\lnot ({\forall_{n \in \mathbb{N}}\,\phi(n) = 0})$ implies $\exists_{k \in \mathbb{N}}\,\phi(k) =1$.

Markov’s Principle (Bridges and Richman 1987) follows from excluded middle but is independent in constructive mathematics, that is, Markov’s Principle is not provable and neither is its negation.

Theorem 94. For the Cantor domain, the strongly maximal elements are exactly those elements that are both sharp and maximal. For the Baire domain, the strongly maximal elements are exactly the elements that are both sharp and maximal if and only if Markov’s Principle holds.

Proof. By Propositions 71 and 80, every strongly maximal element of a continuous dcpo is both sharp and maximal, so it is the assertion that strong maximality follows from the conjunction of sharpness and maximality that matters.

Let x be a sharp and maximal element of the Cantor domain. We prove that x is strongly maximal using Lemma 74. So let $\sigma$ be a finite binary sequence. We must show that $\,\downarrow\, \sigma \mathrel{\sqsubseteq} x$ or $\,\downarrow\, \sigma$ and x are Hausdorff separated. By sharpness of x and Proposition 62, membership of x is decidable. If $\sigma \in x$, then $\,\downarrow\, \sigma \mathrel{\sqsubseteq} x$ holds and we are done. So suppose that $\sigma \not\in x$. Then using decidability of membership of x and finiteness of $\sigma$, we can find the shortest prefix $\tau$ of $\sigma$ for which $\tau \not\in x$. Assume without loss of generality that $\tau$ ends with 0 and write $\rho$ for the sequence obtained by replacing the final 0 in $\tau$ by 1. By definition of $\tau$ and the fact that x is a maximal ideal, it must be the case that $\rho \in x$. But now and are disjoint Scott opens witnessing Hausdorff separation of $\,\downarrow\, \sigma$ and x. So x is strongly maximal, as desired.

Now suppose that every sharp and maximal element of the Baire domain is strongly maximal. We show that Markov’s Principle follows. Let $\phi$ be an infinite binary sequence for which $\lnot(\forall_{n\in\mathbb{N}}\,\phi(n)=0)$ holds. We need to find $k \in \mathbb{N}$ such that $\phi(k) = 1$. Define the following element of the Baire domain

\[ x_\phi := \{{\sigma \in \mathbb{N}^\ast \mid \sigma \text{ is empty or } \sigma \prec \langle{k,k,\dots}\rangle { and \textit{k} is the least $m \in \mathbb{N}$ with $\phi(m) = 1$}}\}. \]

By Proposition 62 and the fact that $x_\phi$ has decidable membership, we see that $x_\phi$ is sharp. We proceed to show that $x_\phi$ is maximal. So suppose that we have y in the Baire domain with $x_\phi \,\subseteq\, y$. We must show that $y \,\subseteq\, x_\phi$, so let $\sigma \in y$ be a finite sequence of natural numbers. We are going to show that $\sigma \not\in x_\phi$ is impossible, which suffices, because membership of $x_\phi$ is decidable. So assume for a contradiction that $\sigma \not\in x_\phi$. Then $\sigma$ must be nonempty and $\sigma(0)$ is not the least $m \in \mathbb{N}$ for which $\phi(m) = 1$. We are going to show that $\phi$ must be zero everywhere, contradicting our assumption. Let $n \in \mathbb{N}$ be arbitrary. Then either $\phi(n) = 0$ in which case we are done, or $\phi(n) = 1$. We show that the second case is impossible. For if $\phi(n) = 1$, then we can find $k \in \mathbb{N}$ such that k is the least natural number $m \in \mathbb{N}$ for which $\phi(m) = 1$. But then $\langle{k}\rangle \in x_\phi$, so $\langle{k}\rangle \in y$, but also $\sigma\in y$ while $\sigma(0) \neq k$, contradicting directedness of y. Thus, we have proved that $x_\phi$ is both sharp and maximal. Hence, by assumption, the element $x_\phi$ is strongly maximal. By Theorem 90, this means that $x_\phi = \iota(\alpha)$ for some infinite sequence $\alpha$ of natural numbers. But then $\phi(\alpha(0)) = 1$, so $\alpha(0)$ is the sought value.

Conversely, suppose that Markov’s Principle holds and let x be a sharp and maximal element of the Baire domain. We prove that x is strongly maximal using Lemma 74. So let $\sigma$ be a finite sequence of natural numbers. We must show that $\,\downarrow\, \sigma \mathrel{\sqsubseteq} x$ or $\,\downarrow\, \sigma$ and x are Hausdorff separated. By sharpness of x and Proposition 62, membership of x is decidable. If $\sigma \in x$, then $\,\downarrow\, \sigma \mathrel{\sqsubseteq} x$ holds and we are done. So suppose that $\sigma \not\in x$. Then using decidability of membership of x and finiteness of $\sigma$, we can find the longest prefix $\tau$ of $\sigma$ for which $\tau$ is still in x. Now, using decidability of membership of x again, consider the infinite binary sequence $\chi$ given by

Notice that $\chi$ cannot be zero everywhere, as this would contradict the assumed maximality of x. Hence, by Markov’s Principle, there exists $k \in \mathbb{N}$ such that $\tau$ extended by k is in x. We define $\rho$ to be this extension of $\tau$, so that $\rho \in x$. Then and are disjoint Scott opens witnessing Hausdorff separation of $\,\downarrow\, \sigma$ and x. Hence, x is strongly maximal, as we wished to prove.

Lemma 95. The space $\mathbf{A}$ is $T_0$-separated with respect to $\mathrel{\#}_{\mathbf{A}}$, that is, for $\alpha,\beta \in \mathbf{A}$ we have $\alpha \mathrel{\#}_{\mathbf{A}} \beta$ if and only if there exists an open containing x but not y or vice versa.

Proof. If $\alpha \mathrel{\#}_{\mathbf{A}} \beta$, then there exists a natural number n such that $\bar{\alpha}_{n} \neq \bar{\beta}_{n}$ and $\{{\gamma \in \mathbf{A} \mid \bar{\alpha}_{n} \prec \gamma}\}$ is an open containing $\alpha$ but not $\beta$. Conversely, suppose that U is an open containing $\alpha$ but not $\beta$. By the description of basic opens of $\mathbf{A}$, there exists a finite sequence $\sigma$ such that $\sigma \prec \alpha$, while $\sigma \nprec \beta$. Hence, if we take n to be the length of $\sigma$, then $\bar{\alpha}_{n} \neq \bar{\beta}_{n}$, finishing the proof.

Theorem 96. The map $\iota$ is a homeomorphism from the space $\mathbf{A}$ of infinite sequences to the space of strongly maximal elements of the algebraic dcpo $\mathcal{A}$ with the relative Scott topology. Moreover, $\iota$ preserves and reflects apartness: $\alpha \mathrel{\#}_{\mathbf{A}} \beta$ if and only if $\iota(\alpha) \mathrel{\#}_{\mathcal{A}} \iota(\beta)$ for every two infinite sequences $\alpha,\beta \in \mathbf{A}$.

Proof. Let $\textrm{StrongMax}(\mathcal{A})$ be the space of strongly maximal elements of $\mathcal{A}$ with the relative Scott topology. By Theorem 90, the map $\iota \colon \mathbf{A} \to \textrm{StrongMax}(\mathcal{A})$ is a bijection. Now let $\sigma$ be a finite sequence and consider the basic open of $\mathcal{A}$. By Theorem 90, we have , which is $\iota$ applied to a basic open of $\mathbf{A}$. It follows that $\iota$ is both open and continuous. Finally, note that

as desired.

Thus, the intrinsic apartness generalizes the well-known apartness on infinite sequences and in particular those on Cantor and Baire space.

7.2 Partial Dedekind reals

The previous section illustrated the theory of the intrinsic apartness and sharp and strongly maximal elements in the algebraic case. For the continuous case, the partial Dedekind reals are a very natural example. We begin by recalling the definition of a (two-sided) Dedekind real number.

Definition 97 (Dedekind real). Given a pair $x = (L_x,U_x)$ of subsets of $\mathbb{Q}$, we suggestively write $p < x$ for $p \in L_x$ and $x < q$ for $q \in U_x$. A Dedekind real x is a pair $(L_x,U_x)$ of subsets of $\mathbb{Q}$ satisfying the following properties:

1. (1) boundedness: there exist $p,q \in \mathbb{Q}$ such that $p < x$ and $x < q$;

2. (2) roundedness: for every $p \in \mathbb{Q}$, we have $p < x \iff \exists_{r \in \mathbb{Q}} ({p < r}) \land ({r < x})$ and similarly, for every $q \in \mathbb{Q}$, we have $x < q \iff \exists_{s \in \mathbb{Q}}({s < q}) \land ({x < s})$;

3. (3) transitivity: for every $p,q \in \mathbb{Q}$, if $p < x$ and $x < q$, then $p < q$;

4. (4) locatedness: for every $p,q\in\mathbb{Q}$ with $p < q$ we have $p < x$ or $x < q$.

Definition 98 (Real line $\mathbb{R}$). The real line $\mathbb{R}$ is the topological space of all Dedekind real numbers whose basic opens are given by $\{{x \in \mathbb{R} \mid p < x \text{ and } x < q}\}$ for $p,q \in \mathbb{Q}$. The space $\mathbb{R}$ has a natural notion of apartness, namely: $x \mathrel{\#}_{\mathbb{R}} y \iff {\exists_{p \in \mathbb{Q}}\,({x < p < y}) \vee ({y < p < x})}$.

Definition 99 (Partial Dedekind reals $\mathcal{R}$). Consider the set $\mathbb{Q} \times_{<} \mathbb{Q} := \{{(p,q) \in \mathbb{Q}\times\mathbb{Q} \mid p < q}\}$ ordered by defining the strict order $(p,q) \prec (r,s) \iff p < r < s < q$. The pair $({\mathbb{Q} \times_{<} \mathbb{Q} , \prec})$ is an abstract basis, so $\mathcal{R} := \textrm{Idl}(\mathbb{Q}\times_{<}\mathbb{Q},\prec)$ is a continuous dcpo and we refer to its elements as partial Dedekind reals.

Lemma 100. For every two rationals $p < q$ and $I \in \mathcal{R}$, we have $\,\downarrow\,(p,q) \ll I$ if and only if $(p,q) \in I$. In particular, $\,\downarrow\,(p,q) \ll \,\downarrow\,(r,s)$ if and only if $p < r < s < q$.

Proof. Suppose that $\,\downarrow\,(p,q) \ll I$. By a well-known fact (Abramsky and Jung 1995, Item 2 of Proposition 2.2.22) of rounded ideals, there exists $(p',q') \in I$ such that $\,\downarrow\,(p,q) \,\subseteq\, \,\downarrow\,(p',q')$. Using roundedness, there exists $(r,s) \in I$ such that $p' < r < s < q'$. We claim that $p < r$ and $s < q$, from which $(p,q) \in I$ follows as I is a lower set. We use trichotomy on the rationals, so assume for a contradiction that $r \leq p$. Then $p' < p$, contradicting $\,\downarrow\,(p,q) \,\subseteq\, \,\downarrow\,(p',q')$. Thus, $p < r$ and similarly, $s < q$, as desired. The converse follows directly from Abramsky and Jung (1995, Item 2 of Proposition 2.2.22).

Definition 101 ($\iota$). We define an injection $\iota \colon \mathbb{R} \hookrightarrow \mathcal{R}$ by $\iota({L_x,U_x}) := \{{(p,q) \mid p \in L_x, q \in U_x}\}$. The map $\iota$ is well-defined precisely because a Dedekind real is required to be bounded, rounded, and transitive.

Theorem 102. The image of $\iota$ is exactly the subset of strongly maximal elements of $\mathcal{R}$.

Proof. Suppose that x is a Dedekind real. We show that $\iota(x)$ is strongly maximal in $\mathcal{R}$. We use Lemma 73, so assume that we have rationals $p,q,r,s \in \mathbb{Q}$ such that $\,\downarrow\,(p,q) \ll \,\downarrow\,(r,s)$. Then we have $p < r < s < q$ by Lemma 100. By locatedness of x, we have $p < x$ or $x < r$. If $x < r$, then there exist rationals $u < x < v$ such that $u < v < r$, so that the intervals (u,v) and (r,s) do not overlap. Hence, $\,\downarrow\, (r,s)$ and x are seen to be Hausdorff separated using Lemma 76. Now suppose that $p < x$. We use locatedness of x once more to decide whether $s < x$ or $x < q$. If $s < x$, then, similarly to the above, we show that $\,\downarrow\, (r,s)$ and x are Hausdorff separated. And if $x < q$, then $(p,q) \in \iota(x)$, so $\,\downarrow\, (p,q) \ll \iota(x)$ by Lemma 100. Thus, $\iota(x)$ is strongly maximal in $\mathcal{R}$.

Conversely, suppose that $I \in \mathcal{R}$ is strongly maximal. Define $L := \{{p \in \mathbb{Q} \mid \exists_{q \in \mathbb{Q}}\,(p,q) \in I}\}$ and $U := \{{q \in \mathbb{Q} \mid \exists_{p \in \mathbb{Q}}\,(p,q) \in I}\}$ and set $x = ({L,U})$. It is straightforward to show that x is bounded, rounded, and transitive. We show that x is also located. So suppose that we have rationals $p < q$. Then there exist rationals r and s such that $\,\downarrow\,(p,q) \ll \,\downarrow\,(r,s)$, that is, $p < r < s < q$. By strong maximality of I, we have $\,\downarrow\, (p,q) \ll I$ or $\,\downarrow\, (r,s)$ and I can be Hausdorff separated. If $\,\downarrow\,(p,q) \ll I$, then $p \in L$ (and $q \in U$) by Lemma 100, so we are done. Now if $\,\downarrow\,(r,s)$ and I are Hausdorff separated, then by Lemma 76, there exist $u \in L$ and $v \in U$ such that the intervals (r,s) and (u,v) do not overlap. So either $s < u$ or $v < r$. If $s < u$, then $p < x$, and if $v < r$, then $x < q$. Thus, $x = ({L,U})$ is located and indeed a Dedekind real. Finally, one can verify that $\iota(x) = I$, as desired.

With excluded middle, the image of $\iota$ is just the set of maximal elements of $\mathcal{R}$. The following result highlights the constructive strength of locatedness of Dedekind reals.

Proposition 103. If every maximal element of $\mathcal{R}$ is strongly maximal, then weak excluded middle holds.

Proof. We use Lemma 81 with the following elements $x := \iota(0)$ and $y := \iota(1)$ of $\mathcal{R}$. By Theorem 102, the elements x and y are both strongly maximal. Moreover, x and y have a greatest lower bound, namely $\,\downarrow\,(0,1)$. Finally, x and y are apart, as witnessed by the disjoint Scott opens and .

We conjecture that $\mathcal{R}$ is similar to the Baire domain in that the strongly maximal elements of $\mathcal{R}$ only coincide with the elements that are both sharp and maximal if a constructive taboo holds.

Lemma 104. The Dedekind real numbers are $T_0$-separated with respect to $\mathrel{\#}_{\mathbb{R}}$, that is, for $x,y \in \mathbb{R}$ we have $x \mathrel{\#}_{\mathbb{R}} y$ if and only if there exists an open U containing x but not y or vice versa.

Proof. If $x \mathrel{\#}_\mathbb{R} y$, then we may assume without loss of generality that there exists $p \in \mathbb{Q}$ with $x < p < y$. Then there also exists $q \in \mathbb{Q}$ such that $p < y < q$ and $\{{z \in \mathbb{R} \mid p < z < q}\}$ is an open separating x and y. Conversely, suppose that U is an open containing x but not y. By description of the basic opens of $\mathbb{R}$, there exists a rationals p and q with $p < x < q$, while $\lnot({({p < y}) \land ({y < q}) })$. Now find $r,s \in \mathbb{Q}$ such that $p < r < x < s < q$. Using locatedness of y, we have $p < y$ or $y < r$. In the second case, we see that $x \mathrel{\#}_\mathbb{R} y$, as desired. And if $p < y$, then as y is located and $y < q$ is now impossible, we must have $s < y$, so that $x \mathrel{\#}_\mathbb{R} y$ again.

Theorem 105. The map $\iota$ is a homeomorphism from $\mathbb{R}$ to the space of strongly maximal elements of the continuous dcpo $\mathcal{R}$ with the relative Scott topology. Moreover, $\iota$ preserves and reflects apartness.

Proof. Let $\textrm{StrongMax}(\mathcal{R})$ be the space of strongly maximal elements of $\mathcal{R}$ with the relative Scott topology. By Theorem 102, the map $\iota \colon \mathbb{R} \to \textrm{StrongMax}(\mathcal{R})$ is a bijection. Now let $p < q$ be rationals and consider the basic open of $\mathcal{R}$. By Lemma 100, this basic open is equal to $\{{I \in \mathcal{R} \mid (p,q) \in I}\}$. So Theorem 102 tells us , which is $\iota$ applied to a basic open of $\mathbb{R}$. It follows that $\iota$ is both open and continuous. Finally, note that

as desired.

7.3 Lower reals

We now consider lower reals, which feature a nice illustration of sharpness.

Definition 106 (Lower reals $\mathcal{L}$). The pair $({\mathbb{Q} , <})$ is an abstract basis, so $\mathcal{L} := \textrm{Idl}(\mathbb{Q},<)$ is a continuous dcpo and we refer to its elements as lower reals.

Lemma 107. For every $p \in \mathbb{Q}$ and $L \in \mathcal{L}$, we have $\,\downarrow\, p \ll L$ if and only if $p \in L$.

Proof. Similar to Lemma 100.

Lemma 108. If $L \in \mathcal{L}$ is a lower real, then the pair (L,U) with $U := \{{q \in \mathbb{Q} \mid \exists_{s \in \mathbb{Q} \setminus L}\,s < q}\}$ is rounded and transitive in the sense of Definition 97. Moreover, if $\mathbb{Q} \setminus L$ is inhabited, then (L,U) is bounded too.

Proof. Let $L \in \mathcal{L}$ be a lower real and let U be as in the lemma. We claim that $U \,\subseteq\, \mathbb{Q} \setminus L$. For if $q \in U$, then there exists $s \in \mathbb{Q} \setminus L$ with $s < q $. But L is a lower set, so $q \in L$ would imply $s \in L$, contradicting that $s \not\in L$. We first prove transitivity. Suppose that $p \in L$ and $q \in U$. By trichotomy on the rationals, it suffices to prove that $q \leq p$ is impossible. So assume for a contradiction that $q \leq p$. Then $q \in L$, because L is a lower set. But $q \in U \,\subseteq\, \mathbb{Q} \setminus L$, so $q \not\in L$, contradicting $q \in L$. For roundedness, observe that $p \in L \iff \exists_{r \in \mathbb{Q}}({p < r}) \land ({r \in L})$, because L is a rounded ideal. Now suppose that $q \in U$. Then there exists $s \in \mathbb{Q} \setminus L$ with $s < q$. Now find $r \in \mathbb{Q}$ such that $s < r < q$ and we see that $r \in U$. Conversely, if we have $s \in \mathbb{Q}$ with $s < q$ and $s \in U$, then $q \in U$, because $s \in U \,\subseteq\, \mathbb{Q}\setminus L$. Hence, $q \in U \iff \exists_{s \in \mathbb{Q}}({s < q} \land ({s \in U}$, so (L,U) is rounded. Finally, if $\mathbb{Q} \setminus L$ is inhabited, then (L,U) is bounded, because L is inhabited too, as it is directed.

Classically, every lower real whose complement is inhabited determines a Dedekind real by the construction above. It is well known that constructively a lower real may fail to be located. The following result offers a domain-theoretic explanation of that phenomenon.

Theorem 109. A lower real $L \in \mathcal{L}$ is sharp if and only if the pair (L,U) with U as in Lemma 108 is located.

Proof. Suppose that $L \in \mathcal{L}$ is sharp and let $p < q$ be rationals. Find $r \in \mathbb{Q}$ such that $p < r < q$. By Lemma 107, we have $\,\downarrow\, p \ll \,\downarrow\, r \ll \,\downarrow\, q$. By sharpness, we have $\,\downarrow\, p \ll L$ or $\,\downarrow\, r \not\,\subseteq\, L$. In the first case, $p \in L$ and we are done; if $\,\downarrow\, r \not\,\subseteq\, L$, then $r \not\in L$, so $q \in U$. Hence, (L,U) is located. For the converse, assume that (L,U) is located. We use Lemma 61 to prove that L is sharp. So let $p,q \in \mathbb{Q}$ with $\,\downarrow\, p \ll \,\downarrow\, q$. By Lemma 107, this yields $p < q$. By locatedness, $p \in L$ or $q \in U$. If $p \in L$, then $\,\downarrow\, p \ll L$ and we are done; if $q \in U$, then we have $s \in \mathbb{Q} \setminus L$ with $s < q$ so that $\,\downarrow\, q \not\,\subseteq\, L$. Hence, L is sharp, as desired.

7.4 An alternative domain for Cantor space

An alternative domain for Cantor space is given by embedding Cantor space $\mathbf{2}^\mathbb{N}$ into the exponential of free pointed dcpos $\mathcal L(\mathbf{2})^{\mathcal L(\mathbb{N})}$; we study sharpness for this domain.

Classically, the free pointed dcpo on a set X is given by the flat dcpo $X \cup \{{\bot}\}$. Constructively, we use the lifting (Escardó and Knapp 2017) of X and we denote it by $\mathcal L(X)$. We can explicitly describe the elements of $\mathcal L(X)$ as partial maps from a singleton to X, but for our present purposes it will be easier to work with the lifting abstractly and only use the following properties, which were proved in de Jong and Escardó (2021a) and de Jong (2022):

• • The unit $\eta \colon X \to \mathcal L(X)$ is injective for every set X.

• • The elements in the image of $\eta$ are all incomparable in the order of $\mathcal L(X)$.

• • For every map of sets $f \colon X \to Y$, the functor $\mathcal L$ yields a Scott continuous function $\mathcal L(f)$ that is strict, that is, $\mathcal L(f)$ preserves the least element. Also, if $\mathcal L(f) = \mathcal L(g)$, then $f = g$ by injectivity and naturality of $\eta$.

• • The lifting $\mathcal L(X)$ is algebraic and bounded complete for every set X. Its compact elements are given by $\{{\bot}\} \cup \{{\eta(x) \mid x \in X}\}$.

Definition 110 ($\varepsilon$). The lifting functor $\mathcal L$ defines an injection $\varepsilon \colon \mathbf{2}^\mathbb{N} \hookrightarrow \mathcal L(\mathbf{2})^{\mathcal L(\mathbb{N})}$ from Cantor space into the exponential dcpo.

The exponential $\mathcal L(\mathbf{2})^{\mathcal L(\mathbb{N})}$ is important in higher-type computability (Escardo 2008) for instance. What is noteworthy about $\mathcal L(\mathbf{2})^{\mathcal L(\mathbb{N})}$ is that, unlike in Section 7.1, it is not the (strongly) maximal elements of $\mathcal L(\mathbf{2})^{\mathcal L(\mathbb{N})}$ that matter, but the sharp elements still play an important role.

Theorem 111. Every element in the image of $\varepsilon$ is sharp, but not all of them are maximal. Also, not every sharp element is in the image of $\varepsilon$.

Proof. Let $\alpha \in \mathbf{2}^\mathbb{N}$ be arbitrary. We wish to show that $\varepsilon(\alpha)$ is sharp. By Propositions 32 and 62, it suffices to show that is decidable for elements $a \in \{{\bot}\}\cup\{{\eta(n) \mid n \in \mathbb{N}}\}$ and elements $b \in \{{\bot}\}\cup\{{\eta(i) \mid i \in \mathbf{2}}\}$. By Lemma 29, this reduces to proving decidability of $b \mathrel{\sqsubseteq} \varepsilon(\alpha)(a)$ for such elements a and b. If $b = \bot$, then the inequality certainly holds. So suppose that $b = \eta(i)$ for some $i \in \mathbf{2}$. If $a = \bot$, then $\varepsilon(\alpha)(\bot) = \bot$ by strictness of $\varepsilon(\alpha)$, so $b = \eta(i) \mathrel{\sqsubseteq} \varepsilon(\alpha)(a)$ is false. And finally, if $a = \eta(n)$ for some $n \in \mathbb{N}$, then $\varepsilon(\alpha)(a) = \varepsilon(\alpha)(\eta(n)) \equiv \mathcal L(\alpha)(\eta(n)) = \eta(\alpha(n))$, by naturality of $\eta$. So we need to decide $\eta(i) \mathrel{\sqsubseteq} \eta(\alpha(n))$, which is equivalent to $\eta(i) = \eta(\alpha(n))$, because elements in the image of $\eta$ are all incomparable. And $\eta(i) = \eta(\alpha(n))$ holds if and only if $i = \alpha(n)$ does, because $\eta$ is injective. But $i = \alpha(n)$ is decidable, because $\mathbf{2}$ has decidable equality.

For the second claim, fix an element $i \in \mathbf{2}$ and consider the constant map $n \mapsto i$ as an element of $\mathbf{2}^\mathbb{N}$. Notice that the inequality $\varepsilon(n \mapsto i) \mathrel{\sqsubseteq} ({x \mapsto \eta(i)})$ holds in $\mathcal L(\mathbf{2})^{\mathcal L(\mathbb{N})}$. But $\varepsilon(n \mapsto i)$ is strict, while $x \mapsto \eta(i)$ is not, so $\varepsilon(n \mapsto i)$ and $x \mapsto \eta(i)$ are not equal and hence, $\varepsilon(n \mapsto i)$ is not maximal.

Finally, one can check that, for any $i \in \mathbf{2}$, the element $x \mapsto \eta(i)$ in $\mathcal L(\mathbf{2})^{\mathcal L(\mathbb{N})}$ is sharp (in fact, it is strongly maximal). But it is not strict, so it cannot be in the image of $\varepsilon$.

Theorem 112. The map $\varepsilon$ is a homeomorphism from Cantor space to the image of $\varepsilon$. Moreover, $\varepsilon$ preserves and reflects apartness.

Proof. The basic opens of $\mathcal L(\mathbf{2})^{\mathcal L(\mathbb{N})}$ are of the form with s the join of some Kuratowski finite subset $\{{a_i \Rightarrow b_i \mid 0 \leq i \leq n-1}\}$ of single-step functions, where $a_k \in \{{\bot}\}\cup\{{\eta(n) \mid n \in \mathbb{N}}\}$ and $b_k \in \{{\bot}\}\cup\{{\eta(i) \mid i \in \mathbf{2}}\}$. By Lemma 29, we have $s \mathrel{\sqsubseteq} f$ for a function $f \in \mathcal L(\mathbf{2})^{\mathcal L(\mathbb{N})}$ if and only if $b_k \mathrel{\sqsubseteq} f(a_k)$ for every $0 \leq k \leq {n-1}$ if and only if $i_k = \alpha(n_k)$ for every such k, where $\beta_k = \eta(i_k)$. Now define the set of indices $K := \{ {0 \leq k \leq n-1 \mid a_k,b_k \neq \bot}\}$. Because $\varepsilon(\alpha)$ is strict for every $\alpha \in \mathbf{2}^\mathbb{N}$, we see that $s \mathrel{\sqsubseteq} \varepsilon(\alpha)$ if and only if $b_k \mathrel{\sqsubseteq} \varepsilon(\alpha)(a_k)$ for every $k \in K$. If $i \in \mathbf{2}$ and $n \in \mathbb{N}$, then $\eta(i) \mathrel{\sqsubseteq} \varepsilon(\alpha)(\eta(n))$ holds if and only if $i = \alpha(n)$, by naturality of $\varepsilon$, injectivity of $\eta$, and the fact that elements in the image of $\eta$ are incomparable. Hence, the set is seen to be $\varepsilon$ applied to a basic open of Cantor space. It follows that $\varepsilon$ is open and continuous. The proof that $\varepsilon$ preserves and reflects apartness is similar to the proof of the second part of Theorem 96.

8. Conclusion

Working constructively, we studied continuous dcpos and the Scott topology and introduced notions of intrinsic apartness and sharp elements. We showed that our apartness relation is particularly well-suited for continuous dcpos that have a basis satisfying certain decidability conditions, which hold in examples of interest. For instance, for such continuous dcpos, the Bridges–Vîţă apartness topology and the Scott topology coincide. We proved that no apartness on a nontrivial dcpo can be cotransitive or tight unless (weak) excluded middle holds. But the intrinsic apartness is tight and cotransitive when restricted to sharp elements. If a continuous dcpos has a basis satisfying the previously mentioned decidability conditions, then every basis element is sharp. Another class of examples of sharp elements is given by the strongly maximal elements. In fact, strong maximality is closely connected to sharpness and the Lawson topology. For example, an element x is strongly maximal if and only if x is sharp and every Lawson neighborhood of x contains a Scott neighborhood of x. Finally, we presented several natural examples of continuous dcpos that illustrated the intrinsic apartness, strong maximality, and sharpness.

In future work, it would be interesting to explore whether a constructive and predicative treatment is possible, in particular, in univalent foundations without Voevodsky’s resizing axioms as in de Jong and Escardó (2021a). Steve Vickers also pointed out two directions for future research. The first is to consider formal ball domains (Gierz et al. 2003, Example V-6.8), which may subsume the partial Dedekind reals example. The second is to explore the ramifications of Vickers’ observation that refinability (Definition 75) is decidable, even when the order is not, if the dcpo is algebraic and 2/3 SFP (Vickers 1989, p. 157). Related to the examples, there is still the question of whether we can derive a constructive taboo from the assumption that strong maximality of a partial Dedekind real follows from having both sharpness and maximality, as discussed right after Proposition 103. Finally, the Lawson topology deserves further investigation within a constructive framework.