apartness relation

Apartness relations


An apartness relation is a binary relation that, instead of saying when two things are the same (as an equivalence relation), states when two things are different – an inequality relation.

Apartness relations are most used in constructive mathematics; in classical mathematics, equivalence relations can take their place (mediated by negation).

The apartness relations that we discuss here are sometimes called point–point apartness, to distinguish this from the related concepts of set–set or point–set apartness relations; see proximity space and apartness space (respectively) for these.



A set SS equipped with an apartness relation is a groupoid (with SS as the set of objects) enriched over the cartesian monoidal category TV opTV^\op, that is the opposite of the poset of truth values, made into a monoidal category using disjunction. By the law of excluded middle (which says that TVTV is self-dual under negation), this is equivalent to equipping SS with an equivalence relation (which makes SS a groupoid enriched over the cartesian category TVTV itself). But in constructive mathematics (or interpreted internally), it is a richer concept with a topological flavour.


Of course, nobody but a category-theorist would use the above as a definition of an apartness relation. Normally, one defines an apartness relation on SS as a binary relation #\# satisfying these three properties:

  • irreflexivity: for all x:Sx: S, x#xx \# x is false;
  • symmetry: for all x,y:Sx, y: S, if y#xy # x, then x#yx # y;
  • comparison: for all x,y,z:Sx, y, z: S, if x#zx # z, then x#yx # y or y#zy # z.

(Notice that these are dual to the axioms for an equivalence relation; like those axioms, these correspond to identity morphisms, inverses, and composition in a groupoid.)

The negation of an apartness relation is an equivalence relation. (The converse of this is equivalent to excluded middle.) An apartness relation is tight (see connected relation) if this equivalence relation is equality; any apartness relation defines a tight apartness relation on the quotient set. A tight apartness relation, also called an inequality, is often written \ne instead of #\#, but keep in mind that \ne is not the negation of ==; rather, == is the negation of \ne. (So inequality, when it exists, is more basic than equality.)

If SS and TT are both sets equipped with apartness relations, then a function f:STf\colon S \to T is strongly extensional if x#yx \# y whenever f(x)#f(y)f(x) \# f(y); that is, ff reflects apartness. The strongly extensional functions are precisely the enriched functors between TV opTV^\op-enriched groupoids, so they are the correct morphisms. (Note that there is no nontrivial notion of enriched natural isomorphism, at least not when the apartness in TT is tight.)

The category of inequality spaces

By an inequality space, I mean a set equipped with a tight apartness relation. By a map, I mean a strongly extensional function between inequality spaces.

The category of inequality spaces has all (small) limits, created by the forgetful functor to Set. (For example, (a,b)(x,y)(a,b) \ne (x,y) iff axa \ne x or byb \ne y.) Similarly, it has all finite coproducts, and it has quotients of equivalence relations. In fact, this category is a complete pretopos. It is not, however, a Grothendieck topos (or even a topos at all), because it doesn't have all infinite coproducts. (To be precise, the statement that it has all small coproducts, or even that it has a subobject classifier, seems to be equivalent to excluded middle.)

We can say, however, that it has coproducts indexed by inequality spaces, although to make this precise is a triviality. More interestingly, it has products indexed by inequality spaces; that is, it is (even locally) a cartesian closed category. In particular, given inequality spaces XX and YY, the set StrExt(X,Y)\StrExt(X,Y) of maps from XX to YY becomes an inequality space under the rule that fgf \ne g iff f(x)g(x)f(x) \ne g(x) for some x:Xx\colon X.

If you generalise from inequality spaces to allow non-tight apartness relations, then you get (at first) a different category. However, now you also have 22-morphisms which serve to identify unequal but equivalent (that is, not apart) elements of a space, so the resulting bicategory is equivalent to the category of inequality spaces.

Topological aspects

Let SS be a set equipped with a tight apartness relation \ne. Using \ne, many topological notions may be defined on SS. (It's not really necessary that the apartness be tight; this corresponds to the T 0T_0 separation axiom in topology.)

If UU is a subset of SS and xx is an element, then UU is a \ne-neighbourhood (or \ne-neighborhood) of xx if, given any y:Sy\colon S, xyx \ne y or yUy \in U; note that xUx \in U by irreflexivity. The neighbourhoods of xx form a filter: a superset of a neighbourhood is a neighbourhood, and the intersection of 00 or 22 (hence of any finite number) of neighbourhoods is a neighbourhood.

A subset GG is \ne-open if it's a neighbourhood of all of its members. The open subsets form a topology (in the sense of Bourbaki): any union of open subsets is open, and the intersection of 00 or 22 (hence of any finite number) of open subsets is open.

The \ne-complement of xx is the subset {y:S|xy}\{y\colon S \;|\; x \ne y\}; this is open by comparison. More generally, the \ne-complement of any subset AA is the set A˜\tilde{A}, defined as:

A˜{y|xA,xy}. \tilde{A} \coloneqq \{y \;|\; \forall{x} \in A,\; x \ne y\} .

This is not in general open, but you would use it where you would classically use the set-theoretic complement. However, if AA is open to begin with, then A˜\tilde{A} equals the set-theoretic complement.

If xyx \ne y, then xy˜x \in \tilde{y} and yx˜y \in \tilde{x}, which shows that (S,)(S, \ne) satisfies the T 1T_1 separation axiom. Symmetry is important here; if we removed symmetry from the axioms of apartness, then we would still get a T 0T_0 topology, but it would not be T 1T_1. This is a version of the fact that failure of T 1T_1 is given by a partial order (or a preorder if T 0T_0 might also fail).

The \ne-closure A¯\bar{A} of a subset AA is the complement of its complement. This closure is a closure operator: AA¯A \subset \bar{A}, A¯¯=A¯\overline{\bar{A}} = \bar{A} (in fact, A˜¯=A˜\overline{\tilde{A}} = \tilde{A}), A¯B¯\bar{A} \subset \bar{B} whenever ABA \subset B, S¯=S\overline{S} = S (in fact, ¯=\bar{\empty} = \empty too), and AB¯=A¯B¯\overline{A \cap B} = \bar{A} \cap \bar{B} (but not AB¯=A¯B¯\overline{A \cup B} = \bar{A} \cup \bar{B}).

The antigraph of a function f:STf\colon S \to T is

{(x,y)|x:S,y:T|f(x)y}. \{(x,y) \;|\; x\colon S, y\colon T \;|\; f(x) \ne y\} .

Recall that in ordinary topology, a function between Hausdorff spaces is continuous iff its graph is closed. Similarly, a function f:STf\colon S \to T is strongly extensional iff its antigraph is open. (Then the graph of ff is the complement of the antigraph.)

One important topological concept that doesn't appear classically is locatedness; in an inequality space, a subset AA is located if, given any point xx and any neighbourhood UU of xx, either UAU \cap A is inhabited (that is, it has a point) or some neighbourhood of xx (not necessarily UU) is contained in A˜\tilde A. Note that every point is located. (For an example of a set that need not be located, consider {x:S|p}\{x\colon S \;|\; p\}, where pp is an arbitrary truth value. In an inhabited space, this set is located iff pp is true or false.)

Relation to metric spaces

Recall that, as Bill Lawvere taught us, a metric space is a groupoid (or dag\dag-category) enriched over the category ([0,[ op,+)([0,\infty[^\op,+) of nonnegative real numbers, ordered in reverse, and made monoidal under addition. (Actually, you get a metric only if you impose a tightness condition, although again you can recover this up to equivalence from the 22-morphisms. Furthermore, Lawvere advocated using [0,][0,\infty] instead of [0,[[0,\infty[, and also dropping the symmetry requirement to get enriched categories instead of groupoids. Thus, he dealt with extended quasipseudometric spaces. These details are not really important here.)

There is a monoidal functor from ([0,[ op,+)([0,\infty[^\op,+) to TV opTV^\op that maps a nonnegative real number xx to the truth value of the statement that x>0x \gt 0. Accordingly, any (symmetric) metric space becomes an inequality space, and any function satisfying d(f(x),f(y))d(x,y)d(f(x),f(y)) \leq d(x,y)) is strongly extensional.

The topological properties of metric spaces fit well with those of inequality spaces if you always work in this direction. For example, a set which is dd-open will also be \ne-open, but not necessarily the other way around. Similarly, a (merely) continuous function between metric spaces is (still) strongly extensional.

Relation to gauge spaces and uniform spaces

In analysis, many spaces are given as gauge spaces, that is by families of pseudometrics; these also become inequality spaces by declaring that xyx \ne y iff d(x,y)>0d(x,y) \gt 0 for some pseudometric dd in the family. (This will actually be a tight apartness iff the family of pseudometrics is separating.)

Classically, any uniform space may be given by a family of pseudometrics, but this doesn't hold constructively. In particular, a topological group may not be an inequality group (as in the next section). However, we can generalize a bit beyond gauge spaces: any uniformly regular uniform space becomes an inequality space by declaring that xyx \ne y iff there is an entourage UU with (x,y)U(x,y)\notin U. (If the uniform space is not uniformly regular, the result is merely an inequality relation, not an apartness.)

Relation to proximity spaces

The constructive theory of proximity spaces is based on a generalisation of apartness relations (which here go between points) to an apartness relation between sets. These are called apartness spaces; just as apartness relations (between points) are classically equivalent to equivalence relations, so apartness spaces are classically equivalent to proximity spaces, with two sets being proximate if and only if they are not apart.

Of course, any apartness space has an apartness relation between points: xx and yy are apart iff {x}\{x\} and {y}\{y\} are apart.

In algebra

Since inequality spaces have finite limits, the usual constructions of universal algebra apply; it's straightforward to define inequality groups, inequality rings, and so on.

The various subsets that appear in algebra (such as ideals and cosets) become less fundamental than certain subsets that are, classically, simply their complements. For example, a left ideal in a ring RR is a subset II such that 0I0 \in I, x+yIx + y \in I whenever x,yIx, y \in I, and xyIx y \in I whenever xIx \in I. But a left antiideal in RR is a subset AA such that 0A0 \in A is false, xAx \in A or yAy \in A whenever x+yAx + y \in A, and xAx \in A whenever xyAx y \in A. Notice that an antiideal is necessarily \ne-open (using that the ring operations are strongly extensional), and its complement is an ideal. But the converse of this is not constructively valid, so antiideals are more fundamental than ideals, in an inequality ring.

Prime ideals are even more interesting. A two-sided antiideal AA (so also satisfying that yAy \in A whenever xyAx y \in A) is antiprime if 1A1 \in A and xyAx y \in A whenever x,yAx, y \in A. Now the complement of an antiprime antiideal may not be a prime ideal (as normally defined). But in fact, it is antiprime antiideals that are more important in constructive algebra. In particular, an integral domain in constructive algebra is an inequality ring in which the antiideal of nonzero elements is antiprime.


The notion of apartness as fundamental in metric spaces may be found in Errett Bishop’s Foundations of Constructive Analysis (1967) (or the 1985 edition with Douglas Bridges, Constructive Analysis). But as I recall, this doesn't introduce the concept in general; that came in Anne Troelstra's and Dirk van Dalen's Constructivism in Mathematics (1988). For apartness in algebra, see A Course in Constructive Algebra (also 1988), by Ray Mines, Fred Richman, and Wim Ruitenburg. A great reference for point-set topology in constructive mathematics is the Ph.D. thesis of Frank Waaldijk, Modern Intuitionist Topology (1996). Please note that I (Toby Bartels) have not read the algebra book.


Urs says: What you say at the entry vector space about the relation between apartness relations and topology and the continuum sounds very interesting. It would be nice if you could move these comments here and maybe flesh them out a little. Because, while it sounds interesting, I don’t yet understand what you are saying!

  • Toby replies: I will try to write a bit about the topological ideas that come up. But keep in mind that classically it is all trivial, unless you rephrase it internal to some more general notion of category than a boolean topos, and these things are not normally so phrased.

    Urs replies to the reply: Okay, I’ll keep it in mind. But I am still interested! :-)

I already have problems with the above definition. When you say “coproduct” do you mean to equip {true,false}\{true, false\} with the monoidal structure given by logical OR? This is the only meaning I can give this word here, but a category enriched over ({true,false},=OR)(\{true, false\},\otimes = OR) seems necessarily to be an indiscrete groupoid over its set of objects. (Because hom(a,a)=truehom(a,a) = true for all objects aa and then hom(a,b)=hom(a,a)ORhom(a,b)=truehom(a,b) = hom(a,a) OR hom(a,b) = true, too, for all bb.)

  • Toby replies: To begin with, I defined it incorrectly; the trouble with these slick category-theoretic definitions is that a small error makes things completely messed up! I rephrased it quite a bit, but the key point is the new word ‘opposite’. That said, your analysis of even my original definition is unsound; keep in mind that the unit of disjunction is false.

    Toby adds: Also, it's an enriched groupoid, not an enriched category.

I am also not sure in which sense you refer to the law of the excluded middle. Should we maybe more generally say that the 0-category of (-1)-categories internal to a given topos TT is the subobject classifier, (1)Cat:=Ω(-1)Cat := \Omega?

  • Toby replies: Yes, that is correct; (1)Cat=Ω(-1)\Cat = \Omega. Even when T:=SetT := \Set, you have (1)Cat={,}(-1)\Cat = \{\top, \bot\} only if you believe excluded middle, which constructivists do not. Thus, constructivists will talk about apartness relations in Set\Set, while a classical mathematician will have to put the discussion internal to TT to get nontrivial results.

    Urs replies to the reply: I like this statement “(1)Cat=Ω(-1)\Cat = \Omega”. Would we also want to say (2)Cat={1Ω}(-2)Cat = \{1 \stackrel{\top}{\to} \Omega\}?

Revised on January 11, 2017 15:01:41 by Mike Shulman (