apartness space

Apartness spaces


An apartness space is a set equipped with an “apartness relation” that distinguishes between pairs of points or sets. They are particularly interesting in constructive mathematics; in classical mathematics they tend to be equivalent to better-known definitions expressed in terms of “closeness” rather than “apartness”.


There are actually several different notions of “apartness space” depending on whether the objects being compared on each side are points or sets.

  • A point–point apartness space is a set XX equipped with an apartness relation, usually written x#yx # y on elements x,yXx,y\in X. Sometimes it is required to be tight, or to be only an inequality relation.

  • A point–set apartness space is a set XX equipped with a relation xAx \bowtie A between points xXx\in X and subsets AXA\subseteq X, satisfying appropriate axioms. In classical mathematics, these axioms are obtained by contraposition from the definition of a topological space in terms of a right exact Moore closure operator, so that point–set apartness spaces are equivalent to topological spaces. In constructive mathematics … well, keep reading.

  • A set–set apartness space is a set XX equipped with a relation ABA\bowtie B between subsets A,BXA,B\subseteq X, satisfying appropriate axioms. A set–set apartness space is one of the ways to describe the classical notion of a proximity space. In constructive mathematics, the definition of a proximity space in terms of \bowtie can be taken as a definition of a set–set apartness space.

  • A uniform apartness space is a set XX equipped with a collection of “co-entourages”, each giving a different notion of when two points are apart, satisfying appropriate axioms. In classical mathematics, the co-entourages are exactly the complements of the entourages of a uniform space, and the same is true constructively if the space is uniformly regular.

Since point–point apartness spaces are described at apartness relation, set–set apartness spaces at proximity space, and uniform apartness spaces at uniformly regular space, the rest of this page will be about point–set apartness spaces.

Point–set apartness spaces


An apartness space is a set XX equipped with a relation \bowtie between points xXx\in X and subsets AXA\subseteq X such that

  1. xx\bowtie \emptyset for any xx.
  2. if xAx\bowtie A, then xyx\neq y for all yAy\in A.
  3. x(AB)x\bowtie (A\cup B) iff xAx\bowtie A and xBx\bowtie B.
  4. If xAx\bowtie A, then x{yz,(zAzy)}x \bowtie \{ y \mid \forall z, (z\bowtie A \to z\neq y) \}.

The relation xAx\bowtie A should be regarded as a “positive” way of saying that xx does not belong to the closure of AA, i.e. xA¯x\notin \overline{A}. Under this interpretation, the above axioms contrapose to become

  1. ¯=\overline{\emptyset} = \emptyset.
  2. If xAx\in A, then xA¯x\in \overline{A}, i.e. AA¯A\subseteq \overline{A}.
  3. A¯B¯=AB¯\overline{A} \cup \overline{B} = \overline{A\cup B} (and in particular (AB)(A¯B¯)(A\subseteq B) \to (\overline{A}\subseteq \overline{B})).
  4. If BA¯B\subseteq \overline{A} and xB¯x\in \overline{B}, then xA¯x\in\overline{A}, i.e. A¯¯=A¯\overline{\overline{A}} = \overline{A}.

which are precisely the axioms of a topology expressed in terms of a closure operator. In constructive mathematics, of course, the law of contraposition does not hold.

The axiom xx\bowtie \emptyset is almost unnecessary, since the last axiom ensures that if xAx\bowtie A for any set AA then xx\bowtie\emptyset. In particular, this is the case if XX is T 1T_1 (see below) and for any xXx\in X there is a yXy\in X with xyx\neq y.

The above definition is almost exactly that of a “pre-apartness” from BV11. The differences are (1) they require XX to be inhabited (which category-theoretically is wrong-headed, since it excludes the initial object), and (2) they assume that XX is given with an ambient inequality relation that is referred to by the symbol \neq in axioms 2 and 4. (If \neq is the denial inequality, then these axioms can be written more simply as “if xAx\bowtie A then xAx\notin A” and “if xAx\bowtie A then x{y¬(yA)}x\bowtie \{ y \mid \neg(y\bowtie A) \}”.) Note that if the space is T 1T_1 (see below) then this ambient inequality is definable in terms of \bowtie as x{y}x\bowtie \{y\}. For an “apartness”, BV11 also require comparability (see below).

Axiom 4 is phrased in BV11 as “if x,(xA(yB,xy))\forall x, (x\bowtie A \Rightarrow (\forall y\in B, x\neq y)), then x,(xAxB)\forall x, (x\bowtie A \Rightarrow x\bowtie B). This is equivalent to our version, since B={yz,(zAzy)}B = \{ y \mid \forall z, (z\bowtie A \to z\neq y) \} is the largest set BB satisfying x,(xA(yB,xy))\forall x, (x\bowtie A \Rightarrow (\forall y\in B, x\neq y)).

The earlier paper BSV02 omits the axiom xx\bowtie \emptyset, and phrases axiom 2 with the denial inequality but axiom 4 with an ambient inequality — although these are probably oversights — and requires T 1T_1 as part of the definition too (see below). An earlier, more predicative presentation of “apartness spaces” can be found in Waaldijk.

Separation properties

Any apartness space comes with an irreflexive relation \nleq defined by xyx \nleq y iff x{y}x \bowtie \{y\}. This is a positive version of the negation of the specialization order. A topological space is called T 1T_1 (see separation axioms) if its specialization order is discrete, i.e. (xy)(x=y)(x\le y) \to (x=y); thus an apartness space is called T 1T_1 if ¬(xy)(x=y)\neg(x\nleq y) \to (x=y).

We could contrapose this to obtain ¬(x=y)(xy)\neg(x=y) \to (x\nleq y), but it is usually too strong constructively to have a denial statement imply a positive one. However, if we replace ¬(x=y)\neg(x=y) with a given apartness relation or inequality relation other than the denial inequality, then we obtain an axiom (xy)(xy)(x\neq y) \to (x\nleq y) that is a purely positive version of T 1T_1. Note that if \neq is tight, then this statement implies the negative version of T 1T_1, while conversely if \nleq is symmetric (see below) then the negative version of T 1T_1 says precisely that \nleq is tight.

Note that axiom 2 implies the converse (x{y})(xy)(x\bowtie \{y\}) \to (x\neq y), so that if the axioms and the T 1T_1 property are stated with reference to some ambient inequality \neq, then \neq can be defined in terms of \bowtie. If we define \neq in this way, then axiom 2 should be stated in terms of the denial inequality (thereby asserting that this relation x{y}x\bowtie \{y\} is irreflexive).

If one wants the relation x{y}x\bowtie \{y\} to be symmetric and thus an “inequality relation” one needs to assert this separately. An apartness space with this property is naturally called R 0R_0, or perhaps strongly R 0R_0, since it implies (and classically is equivalent to) the topological property called R 0R_0 that the specialization order is symmetric (see separation axioms).

However, stating axiom 4 in terms of the \bowtie-derived inequality is weaker, even in classical mathematics, than stating it in terms of the denial inequality. For instance, if X={x,y,z}X = \{x,y,z\} with the only nonempty apartness relations x{z}x\bowtie \{z\} and z{x}z\bowtie \{x\}, then axiom 4 for the denial inequality fails for A={z}A=\{z\}, since {y¬(yA)}={y,z}\{ y \mid \neg(y\bowtie A)\} = \{y,z\} which is not apart from xx; but stated in terms of the \bowtie-derived inequality it holds, since {vu,(uAu{v})}={z}\{ v \mid \forall u, (u\bowtie A \Rightarrow u \bowtie \{v\})\} = \{z\}. This is a pretopological space that is not a topological space; thus only axiom 4 with the denial inequality (or at least a tight inequality, which classically becomes equivalent to denial) gives a notion of point-set apartness space that reduces classically to ordinary toplogical spaces. In BV11, axiom 4 for the denial inequality is called the reverse Kolmogorov property.

An apartness space may be called comparable (nonce definition on this page) if xAx\bowtie A implies (xy)(yA)(x\neq y) \vee (y\bowtie A) for any yy, where \neq might also be a given apartness on XX. This condition is classically trivial, and generalizes the comparison axiom on a point–point apartness relation. In particular, if \neq denotes the relation \nleq defined above, then this property implies that \nleq is a comparison, and hence (if the space is also R 0R_0, so it is symmetric) an apartness relation. It is also related topologically to Penon’s definition of intrinsic open subset in synthetic topology and to the natural topology on a point-point apartness space, and can be viewed as a very weak version of regularity.

An apartness space is locally decomposable if whenever xAx\bowtie A, there exists a set BB such that xBx\bowtie B and every yy satisfies either yAy\bowtie A or yBy\in B. This condition is also classically trivial: take B={y¬(yA)}B = \{ y \mid \neg(y\bowtie A) \}. It implies comparability (for \neq the denial inequality).

Relation to topological spaces

If XX is a topological space, we define xAx\bowtie A if there is a neighborhood of xx disjoint from AA, or equivalently if the complement of AA is a neighborhood of xx. This makes XX an apartness space. Only the last axiom is somewhat nontrivial: if xUx\in U with UU open and UA=U\cap A = \emptyset, and y,(yAyB)\forall y, (y\bowtie A \to y\notin B), then since (yU)(yA)(y\in U) \Rightarrow (y\bowtie A) we have UB=U\cap B = \emptyset too, so xBx\bowtie B.

Conversely, if XX is an apartness space, define UXU\subseteq X to be a neighborhood of xUx\in U if there is a set AA such that xAx\bowtie A and y,(yAyU)\forall y, (y\bowtie A \Rightarrow y\in U). This makes XX a topological space. Again the nontrivial part is the “transitivity” of neighborhoods, i.e. that if UU is a neighborhood of xx then so is {yU\{ y \mid U is a neighborhood of y}y \}. To see this, if xAx\bowtie A and y,(yAyU)\forall y, (y\bowtie A \Rightarrow y\in U), then UU is a neighborhood of any point yy with yAy\bowtie A, so it suffices to show that {yyA}\{ y \mid y\bowtie A\} is a neighborhood of xx; but this is obvious.

If we order the topologies on XX by τ 1τ 2\tau_1 \le \tau_2 if τ 2τ 1\tau_2 \subseteq \tau_1 (i.e. τ 1\tau_1 is finer than τ 2\tau_2), and the apartnesses by 1 2\bowtie_1 \le \bowtie_2 if (x 2A)(x 1A)(x\bowtie_2 A) \Rightarrow (x\bowtie_1 A), then these constructions define monotone functions τ τ\tau \mapsto \bowtie_\tau and τ \bowtie \mapsto \tau_\bowtie respectively. Moreover, we have:


The above functions exhibit the poset of apartnesses on XX as a reflective sub-poset of the poset of topologies on XX: we have ττ τ\tau \le \tau_{\bowtie_\tau} and τ =\bowtie_{\tau_\bowtie} = \bowtie.


For the former inequality, if UU is open in τ τ\tau_{\bowtie_\tau}, then for every xUx\in U there is a set AA such that x τAx\bowtie_\tau A and y,(y τAyU)\forall y, (y\bowtie_\tau A \Rightarrow y\in U). Since x τAx\bowtie_\tau A, there is an open set VV with xVx\in V and VA=V\cap A = \emptyset. But then every yVy\in V satisfies y τAy\bowtie_\tau A, hence yUy\in U; so VUV\subseteq U. Thus UU is open.

For the latter equation, if xAx\bowtie A, then to show x τ Ax \bowtie_{\tau_\bowtie} A we must construct an open set Uτ U\in \tau_\bowtie with xUx\in U and UA=U\cap A = \emptyset; but it suffices to take U={yyA}U = \{ y \mid y\bowtie A \}. Conversely, if x τ Ax \bowtie_{\tau_\bowtie} A, then there is an open set Uτ U\in \tau_\bowtie with xUx\in U and UA=U\cap A = \emptyset. By definition, Uτ U\in \tau_\bowtie and xUx\in U mean there is a set BB with xBx\bowtie B and y,(yByU)\forall y, (y\bowtie B \Rightarrow y\in U). And by the last axiom of an apartness space, to show xAx\bowtie A it suffices to show y,(yByA)\forall y, (y\bowtie B \to y\notin A); but this follows since yByUy\bowtie B \Rightarrow y\in U and UA=U\cap A = \emptyset.

In other words, an apartness space can be regarded as a well-behaved kind of topological space: one in which for every open neighborhood UU of a point xx there is a set AA and an open neighborhood VV of xx such that VA=V\cap A = \emptyset and UU contains the interior of the complement of AA. Note that VV is then in the interior of the complement of AA, and if xx is in the interior of the complement of AA then the latter is such a VV. Thus, the condition can equivalently be phrased as: for every open neighborhood UU of xx, there is a set AA such that xint(¬A)Ux \in int(\neg A) \subseteq U. In other words, the interiors of complements form a base for the topology. In Bridges et. al. this condition is called being topologically consistent.

A sufficient condition for topological consistency is local decomposability. This was defined above for apartness spaces; more generally, a topological space is said to be locally decomposable if for every open neighborhood UU of xx there is an open neighborhood VV of xx such that U¬V=XU \cup \neg V = X, i.e. every yXy\in X satisfies (yU)(yV)(y\in U)\vee (y\notin V). This implies that xint(¬¬V)¬¬VUx\in int(\neg\neg V) \subseteq \neg\neg V \subseteq U, giving topological consistency. (Of course, in classical mathematics every space is locally decomposable.)

In contrast to the above theorem, it is not quite justified to say that the category of apartness spaces is a subcategory of the category of topological ones. It is most natural to say that a function f:XYf:X\to Y between apartness spaces is continuous if for all xXx\in X and AXA\subseteq X, if f(x)f(A)f(x) \bowtie f(A) then xAx\bowtie A. It is true that if XX and YY are topological spaces and ff is topologically continuous, then it is apartness-continuous in this sense for the induced apartnesses. For if f(x)f(A)f(x)\bowtie f(A), then f(x)Uf(x) \in U for some open set UU disjoint from f(A)f(A); topological continuity of ff then gives that f 1(U)f^{-1}(U) is an open set containing xx and disjoint from AA, so that xAx\bowtie A. Thus we do have a functor TopApartTop \to Apart.

However, a continuous map between apartness spaces in the above sense apparently need not be continuous for the induced topologies; but this is true if YY is locally decomposable. For if UYU\subseteq Y is open and xf 1(U)x\in f^{-1}(U), we have a set AYA\subseteq Y such that f(x)Af(x)\bowtie A and yAy\bowtie A implies yUy\in U, and by local decomposability gives a BYB\subseteq Y such that f(x)Bf(x)\bowtie B and every yy satisfies either yAy\bowtie A or yBy\in B. Let C=f 1(B)C = f^{-1}(B); if xCx'\bowtie C, we have xCx'\notin C and hence f(x)Bf(x')\notin B, so f(x)Af(x')\bowtie A and thus f(x)Uf(x')\in U and xf 1(U)x'\in f^{-1}(U). Moreover, since f(x)Bf(x)\bowtie B we have xCx\bowtie C by apartness-continuity. Thus, f 1(U)f^{-1}(U) is open.

Thus, the category of locally decomposable apartness spaces is equivalent to the category of locally decomposable topological spaces.


Notions of “apartness space” based on a presentation in terms of basic opens, somewhat akin to formal topology, were developed in:

The above definition in terms of an apartness relation between points and subsets is slightly adapted from the version given in:

  • Douglas Bridges, Peter Schuster, and Luminita Vita, Apartness, Topology, and Uniformity: a Constructive View, 2002, doi
  • Douglas Bridges and Luminita Vita, Apartness and Uniformity: A Constructive Development. 2011, link

Revised on January 20, 2017 13:15:06 by Mike Shulman (