Separatedness in Constructive Topology

Douglas Bridges and Luminiţa Vîţă

Received: October 10, 2002

Communicated by Anil Nerode

Abstract. We discuss three natural, classically equivalent, Hausdorff separation properties for topological spaces in constructive mathematics. Using Brouwerian examples, we show that our results are the best possible in our constructive framework.

1 Introduction

A typical feature of constructive mathematics—that is, mathematics with intuitionistic logic [1, 2, 3, 4, 10]—is that a classical property may have several constructively inequivalent counterparts. In this paper we describe such counterparts of the notion of a Hausdorff space, examine their interconnections, and, by means of Brouwerian examples, show that our results cannot be improved without some additional, nonconstructive principles. The original impetus for our work came from the constructive theory of apartness (point–set [5, 11] and set–set [9]). However, in order to make the work below accessible to anyone familiar with only the most basic notions of topology, we have chosen to work with the usual notion of topological space. Note, however, that we require a topological space to be equipped from the outset with an inequality relation ≠ satisfying the following properties for all x and y:

x ≠ y ⇒ ¬ (x = y) ,
x ≠ y ⇒ y ≠ x.

We then denote the complement of a subset S of X by

∼S = {x ∈ X : ∀y ∈ S (x ≠ y)} .

On the other hand, the apartness complement of S defined to be

−S = ( ∼S)^{∘} .

If

∀x, y (¬ (x ≠ y) ⇒ x = y) ,

then we say that the inequality is tight. We note here, for future reference, that a topological space X is

• topologically cotransitive if

(x ∈ U ∧ U ∈ τ) ⇒ ∀y ∈ X (x ≠ y ∨ y ∈ U) ;

• locally decomposable if

(x ∈ U ∧ U ∈ τ) ⇒ ∃V ∈ τ (x ∈ V ∧ X = U∪ ∼V) .

Note that local decomposability implies topological cotransitivity. In the constructive theory of point–set apartness spaces, topological cotransitivity is postulated, and local decomposability is an extremely valuable property to have [6, 7]. For example, local decomposability ensures that if an apartness relation is induced by a topology, then the natural topology produced by the apartness relation coincides with the original topology. So important is local decomposability that it is actually postulated as a property of an apartness relation between sets [6]. We will need some basic facts about nets in constructive topology. By a directed set we mean a nonempty set D with a preorder^{1} ≽ such that for all m, n ∈ D there exists p ∈ D with p ≽ m and p ≽ n. If (X, τ) is a topological space, then to each x in X there corresponds a special net defined as follows. Let

D_{x} = {(ξ, U) ∈ X × τ : x ∈ U ∧ ξ ∈ U} ,

with equality defined by

(ξ, U) = (ξ′, U′) ⇔ (ξ = ξ′ ∧ U = U′) ,

and for each n = (ξ, U) in D_{x} define x_{n} = ξ. It is easy to see that D is a directed set under the inclusion preorder defined by

(ξ, U) ≽ (ξ′, U′) ⇔ U ⊂ U′,

so that N_{x} = (x_{n})_{n∈D_{x}} is a net—the basic neighbourhood net of x. We say that a net (x_{n})_{n∈D} in X converges to a limit x in X if

∀U ∈ τ (x ∈ U ⇒ ∃ n_{0} ∈ D ∀n ≽ n_{0} (x_{n} ∈ U)) .

1The classical theory of nets requires a partial order. If we used a partial order in our constructive theory, we would run into difficulties which the classical theory avoids by applications of the axiom of choice.

Documenta Mathematica 8 (2003) 567–576

2 Hausdorff and unique limit properties

Let (X, τ) be a topological space. More or less as in classical topology, we say that X is Hausdorff, or separated, if it satisfies the following condition:

H If x, y ∈ X and x ≠ y, then there exist U, V ∈ τ such that x ∈ U, y ∈ V, and U ⊂∼V

In that case, V ⊂∼ U. Classically, being Hausdorff is equivalent to having the unique limits property:

ULP If (x_{n})_{n∈D} is a net converging to limits x and y in X, then x = y.

We say that a point y in X is eventually bounded away from a net (x_{n})_{n∈D} in X if there exists n_{0} ∈ D such that

y ∈ − {x_{n} : n ≽ n_{0}} .

From a constructive viewpoint, the unique limits property appears rather weak; of more likely interest is the (classically equivalent) strong unique limits property:

SULP If (x_{n})_{n∈D} is a net in X that converges to a limit x, and if x ≠ y ∈ X, then (x_{n})_{n∈D} is eventually bounded away from y.

In this section we investigate constructively the connection between these two uniqueness properties and condition H. Specifically, we prove that the following diagram of implications occurs:

SULP Hausdorff  ULP

We first have an elementary, but useful, lemma.

Lemma 1 Let X be a topological space, x a point of X, and ν = (ξ, U) ∈ D_{x}. Then

U = {x_{n} : n ∈ D_{x}, n ≽ ν} .  (1)

Proof. Consider n ∈ D_{x}. If n = (x_{n}, W) ≽ ν, then x_{n} ∈ W ⊂ U. Hence {x_{n} : n ≽ ν} ⊂ U. On the other hand, for each y ∈ U we have (y, U) ≽ ν, so y ∈ {x_{n} : n ≽ ν} .

Proposition 2 A topological space is Hausdorff if and only if it has the strong unique limits property.

Proof. Let (X, τ) be a topological space. Assume first that X is Hausdorff, let (x_{n})_{n∈D} be a net converging to a limit x in X, and let x ≠ y in X. Choose U, V ∈ τ such that x ∈ U, y ∈ V, and U ⊂∼V. There exists n_{0} such that x_{n} ∈ U for all n ≽ n_{0}. Then

y ∈ V ⊂∼ U ⊂∼ {x_{n} : n ≽ n_{0}} ,

so

y ∈ (∼ {x_{n} : n ≽ n_{0}})^{∘} = − {x_{n} : n ≽ n_{0}} .

Now suppose that X has the strong unique limits property, and let x, y be points of X with x ≠ y. Since the net N_{x} converges to x, there exist n_{0} = (ξ, U) ∈ D_{x} and V ∈ τ such that

y ∈ V ⊂∼ {x_{n} : n ∈ D_{x}, n ≽ n_{0}} .

By Lemma 1,

U = {x_{n} : n ∈ D_{x}, n ≽ n_{0}} .

Thus x ∈ U, y ∈ V, and V ⊂∼U; so X is Hausdorff.

Corollary 3 A Hausdorff space with tight inequality has the unique limits property.

Proof. Let (x_{n})_{n∈D} be a net converging to limits x, y in a Hausdorff space X with tight inequality. If x ≠ y, then we obtain a contradiction from Proposition 2. Hence ¬ (x ≠ y) , and so, by tightness, x = y.

By a T_{1}–space we mean a topological space (X, τ) with the property

x ≠ y ⇒ ∃U ∈ τ (x ∈ U ⊂ ∼{y}) .

The following lemma enables us to prove a partial converse to Corollary 3.

Lemma 4 Let X be a topological space. If X is a T_{1}–space with tight inequality, then

∀x, y ∈ X (y ∈ \overline{\{x\}} ⇒ x = y) .  (2)

Conversely, if (2) holds and X is topologically cotransitive, then the inequality on X is tight.

Proof. Suppose that X is a T_{1}–space with tight inequality, let y ∈ \overline{\{x\}}, and assume that x ≠ y. Then there exists U ∈ τ such that x ∈ U ⊂ ∼{y}; whence y ∉ \overline{\{x\}}, which is absurd. Thus ¬ (x ≠ y) and therefore, by tightness, x = y. Conversely, suppose that (2) holds and that X is topologically cotransitive. Let ¬ (x ≠ y) . For each U ∈ τ with x ∈ U, the topological cotransitivity of X implies that either x ≠ y or else y ∈ U; the former alternative is ruled out, so we must have y ∈ U. Hence y ∈ \overline{\{x\}} and so, by (2), x = y.

Proposition 5 In a topological space with the unique limits property the inequality is tight.

Proof. Let X be a topological space with the unique limits property, and suppose that y ∈ \overline{\{x\}}. Then every open set containing x contains y. Let

L = {(z, U, V) : U, V ∈ τ, x ∈ U, y ∈ V, z ∈ U ∩ V },

where

(z, U, V) = (z′, U′, V′) ⇔ z = z′ ∧ U = U′ ∧ V = V′.

Define a binary relation ≽ on L by

(z_{1}, U_{1}, V_{1}) ≽ (z_{2}, U_{2}, V_{2}) ⟺ U_{1} ⊂ U_{2}.

It is easy to show that L is directed with respect to this binary relation. For each n = (z, U, V) in L define x_{n} = z. Then the net (x_{n})_{n∈L} converges to both x and y in X; whence x = y. It follows from Lemma 4 that the inequality on X is tight.

3 Limiting examples

In this section we show that the connections (summarised in the diagram presented earlier) we have established between the Hausdorff condition, the unique limits property, and the strong unique limits property are the best possible within our constructive framework. We begin by showing that Hausdorff is not enough to establish tightness.

Proposition 6 If every topologically cotransitive topological space with the unique limits property has tight inequality, then the law of excluded middle holds in the weak form (¬¬P ⇒ P) .

Proof. Let P be any syntactically correct statement such that ¬¬P holds, and take X = {0, 1, 2} with equality satisfying

0 = 1 ⇔ P

and inequality given by

0 ≠ 2, 1 ≠ 2, and (0 ≠ 1 ⇔ ¬P) .

Define a topology τ on X by taking the basic open sets to be the complements of subsets of X. To see that X has the topological cotransitivity property, consider all possible cases that arise when x ∈ U and U ∈ τ. We may assume that U = ∼S for some S ⊂ X. If x = 0, then 0 ∈ ∼S. It follows that S ⊂ {2} : for if s ∈ S, then either s = 1 or s = 2; in the former case, 0 ≠ 1 and therefore ¬P, which contradicts our hypotheses. Since 1 ≠ 2, we have 1 ∈ ∼S; since also 0 ≠ 2, we conclude that

∀y ∈ X (0 ≠ y ∨ y ∈ ∼S = U) .

The case x = 1 is similar, and the case x = 2 is even easier to handle. We claim that X is a Hausdorff apartness space. If x ≠ y, then without loss of generality, either x = 0 and y = 2 or else x = 1 and y = 2. Taking, for illustration, the former case, we have 0 ∈ {0, 1} = ∼ {2} , 2 ∈ {2} = ∼ {0} , and ∼ {2} = ∼∼ {0} .Thus there exist U, V ∈ τ such that x ∈ U, y ∈ V, and U ⊂ ∼V. Finally, if the inequality on X is tight, then as ¬ (0 ≠ 1) , we have 0 = 1 and therefore P.

Our final proposition shows that, even when the inequality is tight and certain additional hypotheses hold, the strong unique limits property does not entail being Hausdorff. For the proof we introduce a strange lemma and a general construction. The lemma may seem obvious, but in fact we have to be careful to avoid the axiom of choice, which implies the law of excluded middle [8].

Lemma 7 Let C be a class of subsets of a set X, and let (S_{i})_{i∈I} be a family of subsets of X such that for each i, if S_{i} ≠ ∅, then S_{i} is a union of sets in C. If S = _{⋃i∈I}S_{i} ≠ ∅, then S is also a union of sets in C.

Proof. For each x ∈ X define

I_{x} = {i ∈ I : x ∈ S_{i}} .

Then

S = _{⋃x∈X}_{⋃i∈I}S_{i}.

If x ∈ S and i ∈ I_{x}, then S_{i} ≠ ∅ and so is a union of sets in C. Hence S itself is such a union.

Let X be a set with a nontrivial inequality ≠. We say that a subset S of X is

• finitely enumerable (respectively, finite) if there exist a natural number n and a mapping (respectively, one–one mapping) f of {1, …, n} onto S;

• cofinite if it is the complement of a finitely enumerable subset.

Note that the empty set is finitely enumerable, so X is cofinite. Also, if S is finitely enumerable, then either S = ∅ or else S ≠ ∅ (that is, there exists an element of S). We define the cofinite topology on X to be

τ = {S ⊂ X : S ≠ ∅ ⇒ S is a union of cofinite sets} .

To see that this is a topology, note that (as above) X ∈ τ and, by ex falso quodlibet, ∅ ∈ τ. The unions axiom for a topology is an immediate consequence of Lemma 7 with C = τ. To verify the intersections axiom, let (S_{i})_{i∈I} and (T_{j})_{j∈J} be families of sets in τ. For all i, j choose finitely enumerable subsets A_{i}, B_{j} of X such that S_{i} =∼A_{i} and T_{j} =∼B_{j}. Then

(_{⋃i∈I}S_{i}) ∩ (_{⋃j∈J}T_{j}) = (_{⋃i∈I} ∼A_{i}) ∩ (_{⋃j∈J} ∼B_{j})
= _{⋃i∈I}_{⋃j∈J} (∼A_{i}∩ ∼B_{j})
= _{⋃i∈I}_{⋃j∈J} ∼(A_{i} ∪ B_{j}) ,

where each A_{i} ∪ B_{j} is cofinite. We now recall Markov’s Principle,

For every binary sequence (a_{n})_{n=1}^{∞} such that ¬∀n (a_{n} = 1) , there exists n such that a_{n} = 0,

a form of unbounded search that is well–known to be independent of Heyting arithmetic (Peano arithmetic with intuitionistic logic) and is therefore generally regarded as essentially nonconstructive.

Proposition 8 If every locally decomposable T_{1}–space with the unique limits property and tight inequality is Hausdorff, then Markov’s Principle holds.

Proof. We take a specific case of the foregoing construction. Let (a_{n})_{n=1}^{∞} be a decreasing binary sequence such that a_{1} = 1 and ¬∀n (a_{n} = 1) . Take

X = \{0\} ∪ \{\frac{a_{n}}{n} : n = 1, 2, 3, …\}

with the discrete inequality, and let τ be the cofinite topology on X. To show that X is a T_{1}–space, let x ≠ y in X. Either one of x, y is 0 or else both are nonzero. If, for example, x = 0, then y = 1/n for some n with a_{n} = 1. Writing

U = \{0\} ∪ \{\frac{a_{k}}{k} : k > n\} = ∼\{\frac{a_{k}}{k} : k ≤ n\} ,

we see that

U ∈ τ and x ∈ U ⊂ ∼{y} .  (3)

So we are left with the case where x = 1/m and y = 1/n, with a_{m} = a_{n} = 1. In this case, without loss of generality taking m > n, we obtain (3) by defining

U = \{0\} ∪ \{\frac{a_{k}}{k} : k ≥ m\} .

To show that X is locally decomposable, again consider x ∈ X and U ∈ τ with x ∈ U. We may assume that U = ∼A for some finitely enumerable set A ⊂ X; without loss of generality, A ≠ ∅. Consider first the case x = 0. Let

K = max \{k : \frac{1}{k} ∈ A\}

and

V = \{0\} ∪ \{\frac{a_{k}}{k} : k > K\} = ∼\{\frac{a_{k}}{k} : k ≤ K\} .

Then V is a neighbourhood of 0. For each y ∈ X, either y = 0 ∈ U or else y = 1/k for some k with a_{k} = 1. In the latter case, if k > K, then y ∈ ∼A = U; whereas if k ≤ K, then y ∈ ∼ V. This deals with the case x = 0. Now consider the case where x = 1/m for some m with a_{m} = 1. Again let U = ∼ A be an open neighbourhood of x, where A is finitely enumerable. If a_{m+1} = 0, then X is finite and hence locally decomposable; so we may assume that a_{m+1} = 1. Without loss of generality we may further assume that 1/ (m + 1) ∈ A. Thus

L = max \{n : \frac{1}{n} ∈ A\} > m.

Set

V = \{\frac{a_{k}}{k} : (k > L ∧ a_{k} = 1) ∨ k = m\} = ∼(\{0\} ∪ \{\frac{a_{k}}{k} : k ≤ L, k ≠ m\}) .

Then V is a neighbourhood of x. For each y ∈ X, either y = 0 and hence y ∈ ∼V, or else y = a_{k}/k for some k with a_{k} = 1. If k > L, then y ∈ ∼A = U; if k = m, then y ∈ U; if k ≤ L and k ≠ m, then y ∈ ∼V. Next, we prove that X has the unique limits property. To this end, suppose that (x_{n})_{n∈D} is a net in X that converges to both x and y. Suppose also that x ≠ y. For each n, if a_{n} = 0, then X is finitely enumerable and so has the unique limits property; whence x = y, a contradiction. Thus a_{n} = 1 for all n, which is also a contradiction. We conclude that ¬ (x ≠ y) ; since we are dealing with a discrete inequality, it follows that x = y. Finally, noting that 0 ≠ 1, suppose there exist U, V in τ such that 0 ∈ U, 1 ∈ V, and U ∩ V = ∅. There exist finitely enumerable sets A, B ⊂ X such that 0 ∈ ∼A ⊂ U and 1 ∈ ∼B ⊂ V. Let

N = max \{n : \frac{1}{n} ∈ A ∪ B\} .

Then

\{\frac{a_{k}}{k} : k > N\} ⊂ ∼A∩ ∼B ⊂ U ∩ V.

If a_{N+1} = 1, then U ∩ V ≠ ∅, a contradiction. Hence a_{N+1} = 0.

Acknowledgements: The authors thank the Marsden Fund of the Royal Society of New Zealand for supporting Luminiţa Vîţă as a Postdoctoral Research Fellow for 2001–2002.

References

[1] Errett Bishop, Foundations of Constructive Analysis, McGraw–Hill, New York, 1967.

[2] Errett Bishop and Douglas Bridges, Constructive Analysis, Grundlehren der Math. Wissenschaften 279, Springer–Verlag, Heidelberg–Berlin–New York, 1985.

[3] Douglas Bridges, ‘Constructive mathematics: a foundation for computable analysis’, Theoretical Computer Science 219 (1–2), 95-109, 1999.

[4] Douglas Bridges and Fred Richman, Varieties of Constructive Mathematics, London Math. Soc. Lecture Notes 97, Cambridge Univ. Press, 1987.

[5] Douglas Bridges and Luminiţa Vîţă, ‘Apartness spaces as a foundation for constructive topology’, to appear in Ann. Pure Appl. Logic.

[6] Douglas Bridges and Luminiţa Vîţă, Foundations of Constructive Topology, preprint, University of Canterbury, Christchurch, New Zealand, 2002.

[7] Douglas Bridges, Peter Schuster, and Luminiţa Vîţă, ‘Apartness, topology, and uniformity: a constructive view’, to appear in Computability and Complexity in Analysis (Proc. Dagstuhl Seminar 01461, 11–16 November 2001), special issue of Math. Logic Quarterly, 2002.

[8] N. D. Goodman and J. Myhill, “Choice Implies Excluded Middle”, Zeit. Logik und Grundlagen der Math. 24, 461.

[9] Peter Schuster, Luminiţa Vîţă, and Douglas Bridges, ‘Apartness as a relation between subsets’, in: Combinatorics, Computability and Logic (Proceedings of DMTCS’01, Constanţa, Romania, 2–6 July 2001; C.S. Calude, M.J. Dinneen, S. Sburlan, eds.), 203–214, DMTCS Series 17, Springer– Verlag, London, 2001.

[10] A.S. Troelstra and D. van Dalen, Constructivism in Mathematics: An Introduction (two volumes), North Holland, Amsterdam, 1988.

[11] Luminiţa Vîţă and Douglas Bridges, ‘A constructive theory of point–set nearness’, to appear in Topology in Computer Science: Constructivity; Asymmetry and Partiality; Digitization (Proc. Dagstuhl Seminar 00231, 4-9 June 2000); R. Kopperman, M. Smyth, D. Spreen, eds.), special issue of Theoretical Computer Science.

Douglas Bridges Department of Mathematics & Statistics University of Canterbury Private bag 4800 Christchurch New Zealand d.bridges@math.canterbury.ac.nz Luminiţa Vîţă Department of Mathematics & Statistics University of Canterbury Private bag 4800 Christchurch New Zealand l.vita@math.canterbury.ac.nz