Stanford Encyclopedia of Philosophy

Supplement to Constructive Mathematics

Two Approaches to Constructive Topology

One of the basic results of classical point set topology is the Heine-Borel theorem (HBT): if a set of open intervals covers the closed unit interval [0,1], then already finitely many of them cover the interval; in other words, [0,1] is open-cover compact. Within INT the theorem is still valid by an appeal to the full fan theorem (Dummett 2000). Moerdijk (1984) has shown that HBT is strictly weaker than the full fan theorem, but we do not know of any natural fan theorem to which the Heine-Borel theorem is equivalent relative to BISH. This is one example of how fan theorems facilitate the development of topology within INT; see also Troelstra 1978 and Waaldijk 1996. However the effectivity of HBT can be called into question, as within RUSS the existence of ε-singular covers (see Section 3.2 above) provides a strong recursive counterexample to the theorem.

Bishop (1967) took a radical approach by limiting his attention to metric spaces, in which compactness can be defined as completeness plus total boundedness. Moreover, he took the continuity of a function from a compact metric space into a metric space to mean uniform continuity, by definition. This allowed him to regain most of the useful theorems about, for example, suprema and positive measures, without referring to HBT. It is possible to generalise his theory to uniform spaces, but for some applications this is clearly not sufficient: for instance, quotient spaces of uniform spaces need not be uniform spaces, a fact that bars direct applicability to fields such as algebraic topology.

The neighborhood structure on a topological space tells us only when points are close, but in general gives little information about the more global structure of the space. In order to go significantly beyond metric and uniform spaces, we need to consider topological spaces endowed with some not-necessarily-uniform structure over and above the neighbourhood one. We describe two alternative approaches below: apartness spaces, where the fundamental axioms capture the idea of subspaces being apart from one another, and point-free topology, where the notion of open sets and their mutual cover relations are taken as basics.

Apartness spaces

A classical theory of proximity spaces, based on the primitive notion of two sets being “near” each other, has been around for over 100 years, and has been developed substantially over the last 60 or so; see Riesz 1908, Naimpally and Warrack 1970, and Naimpally (forthcoming). It soon becomes clear, however, that the notion—a negative one, logically speaking—of “nearness” does not have much computational strength, and that, in some constructive form, its classical obverse—apartness—is what one needs for a constructively fruitful theory. In 2000, Bridges and Vîță began the development of a theory of apartness spaces, based on a few axioms specifying the fundamental properties of the notion of apartness (a) between a point and a set, and (b) between two sets. We now present a sketch of parts of that theory, whose definitive account can be found in Bridges and Vîță 2011.

Let X be an inhabited set equipped with an inequality relation ≠ : that is, a binary relation on X that satisfies these two properties for all x, y ∈ X :

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

Note that, in general, this inequality relation will be distinct from the special case of the denial inequality, in which the first implication in the preceding display is replaced by a bi-implication. This distinction gives rise to two notions "complement" for subsets S of X:

– the logical complement, ¬S ≡ {x ∈ X : ¬(x ∈ S)};
– the complement, ~S ≡ {x ∈ X : ∀s ∈ S (x ≠ s)}.

We also equip X with a binary relation ⋈ between points and subsets of X. This brings into play a third notion of complement:

– the apartness complement, –S ≡ {x ∈ X : x ⋈ S}.

It will follow from the axioms for ⋈ that –S ⊂ ~S ⊂ ¬S.

If ⋈ satisfies the following axioms (in which, for simplicity, we omit the quantifiers), then it is called a (point-set) pre-apartness on X, and X, taken with ⋈, becomes a (point-set) pre-apartness space:

A1    x ⋈ ∅

A2    –A ⊂ ~S

A3   x ⋈ (A ∪ B) ↔ (x ⋈ A ∧ x ⋈ B)

A4   –A ⊂ ~B ⇒ –A ⊂ –B

If, in addition to A1-A4, the pre-apartness satisfies

A5    x ⋈ A ⇒ ∀y ∈ X (x ≠ y ∨ y ⋈ A),

then we call it an apartness, and the space X a (point-set) apartness space. The value of the additional axiom A5 is that it provides us with alternatives that hold automatically in CLASS and that facilitate many constructive proofs. Nevertheless, it makes good sense to work without A5 where it is not needed.

The canonical example of an apartness space is an inhabited metric space (X,ρ), taken with the metric inequality defined by

x ≠ y ⇔ ρ(x, y) > 0

and with

x ⋈ S ⇔ ∃r > 0 ∀s ∈ S (ρ(x, s) ≥ r).

The real line R with its standard metric is such an apartness space. However, if we take the real line with the denial inequality, rather than metric one, then axiom A5 holds if and only if we adopt Markov's principle; so in the absence of the latter, the resulting space is only a pre-apartness one.

For the rest of this section only, we adopt the convention that a topological space X comes with an inequality relation ≠. The topology τ then induces a topological pre-apartness ⋈τ on X, defined by

x ⋈τ S ⇎ x ∈ (~S)o,

where, as usual, o denotes "interior". If X has the topological A5 property,

∀x ∈ X ∀U ∈ τ (x ∈ U ⇒ ∀y ∈ X (x ≠y ∨ y ε U)),

then the corresponding pre-apartness is an apartness. Note that on a metric apartness space the apartness corresponding to the metric topology coincides with the metric apartness. Every pre-apartness ⋈ on an inhabited set induces a natural apartness topology τ⋈, in which the nearly open sets are the unions of families of apartness complements. In turn, τ⋈ induces on X a pre-apartness, which turns out to be the original one. If the pre-apartness ⋈ is induced by a topology τ on X, then every nearly open subset of X is τ-open. When the converse holds, so that the apartness topology and the original one coincide, we say that the topological space X is topologically consistent. Topological consistency always holds classically, but need not hold constructively. One condition on X that ensures its topological consistency is that of topological local decomposability:

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

If we start with a pre-apartness ⋈ on a set X, then we can define a counterpart of this last condition—local decomposability:

∀x ∈ X ∀S ⊂ X (x ∈ –S ⇒ ∃T ⊂ X (x ∈ –T ∧ X = –S ∪ T)).

It turns out that a topological space (X, τ) is topologically locally decomposable if and only if it is topologically consistent and (X, ⋈τ) is locally decomposable (Bridges and Vîță 2011, Cor. 2.2.16).

One obvious way to introduce continuity of a mapping f : (X, ⋈X) → (Y, ⋈Y) between pre-apartness spaces is to work with the corresponding apartness topologies. Thus we say that f is topologically continuous if for each nearly open subset V of Y, f-1(V) is nearly open in X. But there is a notion of continuity that is more in the morphic spirit of category theory: we say that f is apartness continuous if for all x ∈ X and S ⊂ X,

f(x) ⋈Y f(S) ⇒ x ⋈X S.

If X and Y are metric spaces, then the apartness continuity of f is equivalent to continuity in the usual "ε-δ" sense. Connections between various types of continuity are explored in Chapter 2, Section 3, of Bridges and Vîță 2011.

The really hard work, with significant rewards, in the theory of apartness comes when we lift our attention to pre-apartness between subsets of an inhabited set X. For this, we require the (set-set) pre-apartness ⋈ to satisfy the following axioms:

B1    X ⋈ ∅

B2   –A ⊂ ~A

B3    (A1 ∪ A2) ⇔ (B1 ∪ B2) ⇎ ∀i, j ∈ {1, 2} (Ai ⋈ Bj)

B4   –A ⊂ ~B ⇒ –A ⊂ –B.

(The rather complicated form of axiom B3 enables us to work without assuming the symmetry of ⋈.)

As the reader will have realised, in axioms B2 and B4, –A is the apartness complement of A relative to the point-set relation defined by

x ⋈ A ⇔ {x} ⋈ A,

which is a point-set pre-apartness said to be associated with, or induced by, the set-set relation ⋈.

If axioms B1–B4 hold, then the pair (X, ⋈), or when no confusion is likely, the set X itself, a (set-set) pre-apartness space; and if A ⋈ B, we say that A is apart from B. By a (set-set) apartness on X we mean a relation ⋈ between subsets of X that satisfies axioms B1–B3 and

B5    x ∈ A ⇒ ∃S ⊂ X (x ∈ –S ∧ X = –A ∪ S).

The relation ⋈ then also satisfies B4 and so is a pre-apartness. Regarded as a point-set pre-apartness space, X is then locally decomposable (this is precisely what B5 says) and hence satisfies A5. In this case we call (X, ⋈), or simply X itself, a (set-set) apartness space.

The canonical example of a set-set apartness is again a metric space (X, ρ), in which we define the metric apartness by

A ⋈ B ⇎ ∃r > 0 ∀x ∈ A ∀y ∈ B (ρ(x, y) > 0).

A more general example, to which considerable space is devoted in Chapter 3 of Bridges and Vîță 2011, is a uniform space, whose definition we pass over here.

The natural morphisms in the category of set-set pre-apartness spaces are the functions f : (X, ⋈X) → (Y, ⋈Y) that are strongly continuous,in the sense that for all A, B ⊂ X,

f(A) ⋈Y f(B) ⇒ A ⋈X B.

Every uniformly continuous mapping between metric spaces is strongly continuous. Among other results connecting types of continuity for a mapping f : X → Y between metric spaces we have these:

– f is uniformly continuous if and only if the mapping f × f : (x, x′) rightsquigarrow (f(x), f(x′)) is strongly continuous on the product metric space X × X.

– If f is strongly continuous, then it is uniformly sequentially continuous (see Section 4.3 above).

– If f is strongly continuous and f(X) is totally bounded, then f is uniformly continuous.

– If X is totally bounded and f is strongly continuous, then f is uniformly continuous.

The proofs of the second and fourth of these results are particularly involved, and introduce a proof technique that has other applications, for example in the theory of convergence of sequences of functions between apartness spaces. Note that we cannot pass, in general, from uniform sequential continuity to uniform continuity without using BD-N (Bridges et al. 2005).

There is one matter in apartness-space theory whose resolution has proved elusive: the correct notion of compactness. Such a notion should reduce to completeness plus total boundedness when the apartness is induced by a metric (or, more generally, by a uniform structure). The open-cover compactness notion dealt with in Bridges and Vîță 2011 (Section 3.10) is due to Diener (2008, 2008a) and has many attractive properties. Other notions have been introduced by Steinke (2011). Bridges has even considered precompactness and a form of sequential compactness for apartness spaces (Bridges, 2012 and forthcoming). But none of these ideas carries the weight of conviction that it is the right one in the context of apartness spaces.

We refer the reader to Chapter 3 of Bridges and Vîță 2011 for more information, including an extensive bibliography, about set-set apartness relations.

Point-free topology

In point-set topology the ideal objects (points) X are taken as basic and we group them together in ever narrower sets, so-called open sets. The set O(X) of open sets defines the topology, and is required to be closed under arbitrary unions and finite intersections. The open sets are often described in terms of basic open sets, so that every open set may be written as a union of such sets. These basic open sets can be thought of as approximations to the points. To give a specific example, the topology of the real line R may be described in terms of the basic open sets

(p, q) = {x ∈ R : p < x < q }

where p and q are rational numbers. Each such basic open, an interval with rational endpoints, is specified by finite information and approximates all the real numbers x in the interval.

We may try to reverse the order of concepts, and take the basic opens, or approximations, as fundamental, and derive the ideal objects or points from the opens and their mutual relations. This is what is done in point-free topology, a field which has a long history going back to Wallman (1938), Menger (1940) and in its current form, Ehresmann and Isbell; see (Picardo and Pultr 2011). There is also a precursor in point-free geometry (Whitehead 1919). We shall here concentrate on formal topology (Sambin 1987), which is a version of locale theory (Johnstone 1982, Joyal and Tierney 1984, Picardo and Pultr 2011), where special consideration has been given to issues of constructivity and predicativity. Some seminal examples in formal topology were developed earlier in Martin-Löf 1970.

A formal topology is a triple (A, ≤, cov) consisting of a set A of basic opens, a transitive and reflexive relation ≤ on A, and a relation cov between elements of A and subsets of A. The relation a ≤ b is understood as (formal) inclusion, whereas a cov U is read a is covered by U. These are supposed to satisfy the following natural axioms.

A point in this topology is an inhabited subset α of basic opens which satisfies these conditions:

We think of a point as a set of approximations. The filtering property insures that any two approximations have a common refinement, whereas the splitting property allows an approximation to be refined in any way the cover relation allows.

For any set U ⊆ A, we let U* be the set of all points α where a ∈ U for some a ∈ α. It can be shown that the points together with the sets U* form a point-set topology in the usual sense, and that formal cover implies point-wise cover:

a cov U ⇒ {a}* ⊆ U*.

The converse implication usually fails.

For any S ⊆ A, we may define an associated closed subspace of A  ≡ (A, ≤, cov) by redefining the cover relation:

a covS U  ≡  a cov S ∪ U.

Note that if a cov S, then a covS ∅, so, in effect, the open set determined by S, gets identified with the empty set, as far as mutual covering goes. The topology

A - S  ≡ (A, ≤, covS)

represents the subspace corresponding to the points not in S.

The point-free Heine-Borel theorem

To illustrate the methods of formal topology, we shall give a proof of the point-free Heine-Borel theorem:
HBT  Every cover of the unit interval by open sets has a finitely enumerable subcover.

Note the use of “finitely enumerable” here. A set S is called finitely enumerable if there exist a positive integer N and a mapping f of {1, …, N} onto S. If the mapping f is one-one, then we say that S is finite. If the pairset {0, x} is finite, then we can decide whether x equals 0 or not. Thus (see Section 1 above), the statement “every finitely enumerable subset of R is finite” implies LPO.

To prove HBT, we need to construct the point-free reals. Accordingly, let R ≡ (I, ≤I, cov) be the formal topology given by the following data: I is the set of pairs (p, q) where

A pair in I is regarded as specifying an interval with rational end points. The cover relation cov is the smallest cover relation that satisfies the following axioms:

These axioms describe two principal ways of covering an interval by shorter intervals. The points of R are the real numbers. We define the order of the points by taking α < β if and only if there exist (p, q) ∈ α and (p′, q′) ∈ β with q < p′; we then take β ≤ α to mean that α < β is false. It is possible to show using transfinite induction on covers (cf. Coquand et al. 2003) that we have the following alternative characterisation of the above cover relation:

(p, q) cov U holds if and only if for any r < s with p < r < s < q, there exist t1 < t2 < … < tn, n ≥ 3, with r = t1, s = tn, such that each (ti, ti+2)  (1≤ i ≤ n − 2) is included in some interval of U (Cederquist and Negri 1996).

Let

S ≡ {(p, q) ∈ I : q < 0} ∪ {(p, q) ∈ I : 1 < p}.

It can be shown that the points of R - S are the real numbers in the interval [0, 1].

We now have the ingredients to prove HBT. To say that U covers the unit interval R − S means that (p, q) covS U for all (p, q). In particular (−2, 3) covS U; that is, (−2, 3) cov S ∪ U. Hence for r = −1 < s  =  2 there are t1 < t2 < … < t n with r = t1 and s  =  tn, such that each (ti, ti+2)  (1 ≤ i ≤ n-2) is included in some interval of S ∪ U. Thus for i  =  1, … ,n − 2, there exists (pi, qi) ∈ S ∪ U with (ti, ti+2) ≤  (pi, qi). It follows that there is a finitely enumerable F ⊂ U such that (−1, 2) covS F. But (p, q) covS (−1, 2) for all (p, q) ∈ I, so by transitivity, (p, q) covS F. Hence F is a finitely enumerable subcover of the unit interval. This establishes the theorem.

Another surprising result about compactness is that Tychonoff's theorem holds for formal topologies (Coquand 1992). In classical point-set topology this theorem is equivalent to the Axiom of Choice (Johnstone 1982). Moreover, the classically highly non-constructive Stone-Čech compactification has as well a constructive point-free version (Curi 2010).

The category of formal topologies

The category of (set-presented) formal topologies has good properties from a topological point of view: it has (finite) limits and (finite) colimits. In particular, it is possible to construct quotient spaces and to attach subspaces, so the category seems adequate for doing algebraic topology; see (Palmgren 2009). This category includes the metric spaces via so called localic completions (Palmgren 2007) and gives a solution (Palmgren 2008) to the problem of combining the reciprocal map with composition (Schuster 2005).

Other uses of point-free methods in constructive mathematics

Many results in functional analysis have natural point-free proofs (Johnstone 1982, Picardo and Pultr 2011); some of them—for instance, the Riesz representation theorem (Coquand and Spitters 2009)—can also be proved completely constructively. There are, in addition, methods for dealing with the Zariski topology and spectra of rings in a point-free way (Johnstone 1982); here, too, it is possible to make constructive developments (Schuster 2006, Coquand 2009).