nLab apartness relation

Apartness relations

Apartness relations

Idea

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.

Definitions

Abstract

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, as TV opTV^\op is a co-Heyting algebra.

Concrete

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. (On the other hand, the statement that every equivalence relation is the negation of some apartness relation is equivalent to excluded middle, and the statement that the negation of an equivalence relation is always an apartness relation is equivalent to the nonconstructive de Morgan law.) An apartness relation is a tight apartness relation if this equivalence relation is equality; any apartness relation defines a tight apartness relation on the quotient set.

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.)

(2,1)-category of sets with apartness relations

Sets with apartness relations, strongly extensional functions, and equivalences of strongly extensional functions, which serve to identify unequal but equivalent (that is, not apart) elements of a set, form a locally thin (2,1)-category; i.e. a bicategory enriched in thin groupoids. This bicategory is locally small and a univalent bicategory.

Topological aspects

The apartness topology

Let SS be a set equipped with an apartness relation \ne. Using \ne, many topological notions may be defined on SS. (Often one assumes that the apartness is 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}. Thus, if \ne is tight, then (S,)(S, \ne) satisfies the T 1T_1 separation axiom. Symmetry is important here; if we removed symmetry from the axioms of apartness (obtaining a quasi-apartness?) but retained tightness, 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 \dagger-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.

Relation to locales

Let XX be a set, regarded as a discrete locale, whose frame of opens is O(X)=P(X)O(X) = P(X), the power set of XX. That is, the opens in the locale XX are precisely the subsets of the set XX. Since discrete locales are locally compact (every set is the union of its K-finite subsets), the locale product X×XX\times X agrees with the spatial product, so that X×XX\times X is also discrete and every subset of X×XX\times X is open. Thus, the opens in the locale X×XX\times X are precisely the subsets of X×XX\times X. In particular, an equivalence relation on the set XX can be identified with an open equivalence relation (in Loc) on the discrete locale XX.

Thus, the following theorem gives a different precise sense in which apartness relations are dual to equivalence relations.

Theorem

An apartness relation on a set XX is the same as a (strongly) closed equivalence relation on the discrete locale XX. Moreover, the apartness topology defined above is, as a locale, the quotient of this equivalence relation.

Proof

By definition, a (strongly) closed sublocale of a locale YY is one of the form CU\mathsf{C}U, for some open UO(Y)U\in O(Y). Thus, when XX is a discrete locale, a closed sublocale of X×XX\times X is of the form CU\mathsf{C}U for some subset UU of X×XX\times X. This subset is the extension of the apartness relation, i.e. U={(x,y)x#y}U = \{ (x,y) \mid x\#y \}.

For the first claim, therefore, it remains to show that the three axioms of an equivalence relation for CU\mathsf{C}U correspond to the apartness axioms for #\#. Note that pullback along locale maps respects closed complements, i.e. f *(CU)=C(f *U)f^*(\mathsf{C}U) = \mathsf{C}(f^*U). Thus, the pullback of CU\mathsf{C}U along the twist map X×XX×XX\times X \to X\times X is the closed sublocale corresponding to the twist of UU, i.e. the set {(x,y)y#x}\{ (x,y) \mid y\#x \}. Since C\mathsf{C} is a contravariant order-isomorphism between the posets of open and closed sublocales, symmetry for CU\mathsf{C}U is equivalent to symmetry for #\#. Similarly, pulling CU\mathsf{C}U back to X×X×XX\times X\times X along one of the three canonical projections gives the closed sublocale dual to the corresponding pullback of UU itself, and C\mathsf{C} transforms unions to intersections; thus transitivity for CU\mathsf{C}U is equivalent to comparison for #\#. Finally, the pullback of CU\mathsf{C}U along the diagonal is the closed sublocale dual to the similar pullback of UU, so to say that the former is all of XX is equivalent to saying that the latter is \emptyset; thus reflexivity for CU\mathsf{C}U is equivalent to irreflexivity for #\#.

Now, the quotient in LocLoc of such an an equivalence relation in particular comes equipped with a surjective locale map from XX. Thus, it is a spatial locale and can be regarded as a topology on the set XX. Moreover, quotients in LocLoc are constructed as equalizers in FrmFrm, so we have to compute the equalizer of the two maps O(X)=P(X)O(CU)O(X) = P(X) \to O(\mathsf{C}U), where O(CU)O(\mathsf{C}U) is the frame of opens of CU\mathsf{C}U regarded as a locale in its own right. Equivalently, this means the equalizer of the two maps P(X)π iP(X×X)j CUP(X×X)P(X) \xrightarrow{\pi_i} P(X\times X) \xrightarrow{j_{\mathsf{C}U}} P(X\times X), where j CUj_{\mathsf{C}U} is the nucleus corresponding to CU\mathsf{C}U.

Now by definition, j CU(V)=VUj_{\mathsf{C}U}(V) = V\cup U. Thus, the elements of this equalizer — which is to say, the opens in the locale quotient — are subsets VV of XX such that (V×X)U=(X×V)U(V\times X) \cup U = (X\times V) \cup U. Reexpressed in terms of #\#, that means that for any x,yXx,y\in X we have (xVx#y)(yVx#y)(x\in V \vee x\#y) \iff (y\in V \vee x\#y). But since #\# is symmetric, this is equivalent to the unidirectional implication (xVx#y)(yVx#y)(x\in V \vee x\#y) \to (y\in V \vee x\#y), and since x#yx\#y always implies itself, this is equivalent to xV(yVx#y)x\in V \to (y\in V \vee x\#y), which is precisely the condition defining the open sets in the apartness topology above.

Recall that the negation of an apartness relation on XX is an equivalence relation on the set XX. This is the spatial part of the above closed localic equivalence relation, which in general (constructively) need not be itself spatial. The apartness relation is tight just when this spatial part is the diagonal. (By contrast, to say that the closed localic equivalence relation is itself the diagonal is to say that the discrete locale XX is Hausdorff, which is only true if XX has decidable equality.)

Another characterization of the #\#-open sets is that UU is #\#-open if U×X(X×U)W #U\times X \subseteq (X\times U) \cup W_\#, where W #W_\# is #\# regarded as a subset of X×XX\times X. Rephrased in terms of complementary closed sublocales, this says that CU\mathsf{C}U is “closed under the equivalence relation” dual to #\#. Thus, the closed sublocales of XX with its #\#-topology (i.e. the formal complements of #\#-open sets) correspond precisely to the closed sublocales of XX (the formal complements of arbitrary subsets of XX) that respect this equivalence relation.

As a partial converse to the above theorem, if XX is a localically strongly Hausdorff topological space, meaning that its diagonal is a strongly closed sublocale, then the pullback of this diagonal to the discrete locale on the set of points of XX is a closed localic equivalence relation, hence an apartness, whose \ne-topology refines the given topology. See this theorem. If we are given an apartness relation \ne, it is unclear whether the \ne-topology is localically strongly Hausdorff; but if it is, then the apartness relation resulting from this topology is stronger than the given \ne.

\phantom{-}symbol\phantom{-}\phantom{-}in logic\phantom{-}
A\phantom{A}\inA\phantom{A}element relation
A\phantom{A}:\,:A\phantom{A}typing relation
A\phantom{A}==A\phantom{A}equality
A\phantom{A}\vdashA\phantom{A}A\phantom{A}entailment / sequentA\phantom{A}
A\phantom{A}\topA\phantom{A}A\phantom{A}true / topA\phantom{A}
A\phantom{A}\botA\phantom{A}A\phantom{A}false / bottomA\phantom{A}
A\phantom{A}\RightarrowA\phantom{A}implication
A\phantom{A}\LeftrightarrowA\phantom{A}logical equivalence
A\phantom{A}¬\notA\phantom{A}negation
A\phantom{A}\neqA\phantom{A}negation of equality / apartnessA\phantom{A}
A\phantom{A}\notinA\phantom{A}negation of element relation A\phantom{A}
A\phantom{A}¬¬\not \notA\phantom{A}negation of negationA\phantom{A}
A\phantom{A}\existsA\phantom{A}existential quantificationA\phantom{A}
A\phantom{A}\forallA\phantom{A}universal quantificationA\phantom{A}
A\phantom{A}\wedgeA\phantom{A}logical conjunction
A\phantom{A}\veeA\phantom{A}logical disjunction
symbolin type theory (propositions as types)
A\phantom{A}\toA\phantom{A}function type (implication)
A\phantom{A}×\timesA\phantom{A}product type (conjunction)
A\phantom{A}++A\phantom{A}sum type (disjunction)
A\phantom{A}00A\phantom{A}empty type (false)
A\phantom{A}11A\phantom{A}unit type (true)
A\phantom{A}==A\phantom{A}identity type (equality)
A\phantom{A}\simeqA\phantom{A}equivalence of types (logical equivalence)
A\phantom{A}\sumA\phantom{A}dependent sum type (existential quantifier)
A\phantom{A}\prodA\phantom{A}dependent product type (universal quantifier)
symbolin linear logic
A\phantom{A}\multimapA\phantom{A}A\phantom{A}linear implicationA\phantom{A}
A\phantom{A}\otimesA\phantom{A}A\phantom{A}multiplicative conjunctionA\phantom{A}
A\phantom{A}\oplusA\phantom{A}A\phantom{A}additive disjunctionA\phantom{A}
A\phantom{A}&\&A\phantom{A}A\phantom{A}additive conjunctionA\phantom{A}
A\phantom{A}\invampA\phantom{A}A\phantom{A}multiplicative disjunctionA\phantom{A}
A\phantom{A}!\;!A\phantom{A}A\phantom{A}exponential conjunctionA\phantom{A}

References

According to Troelstra and van Dalen:

Brouwer (1919) introduced the notion of apartness (örtlich verschieden, Entfernung)…. The axioms of the theory of apartness were formulated by Heyting (1925).

  • L.E.J. Brouwer, Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten II: Theorie der Punktmengen. 1919

  • Arend Heyting, Intuïtionistische Axiomatiek der Projectieve Meetkunde (Dutch), Ph.D. Thesis, 1925

  • Errett Bishop‘s Foundations of Constructive Analysis (1967) uses apartness for the real numbers and more general metric spaces.

  • The 1985 edition with Douglas Bridges, Constructive Analysis, includes the general definition of apartness relation, there called an “inequality relation” (though in many other sources, as here, an inequality relation need not satisfy comparison).

  • Anne Troelstra's and Dirk van Dalen's Constructivism in Mathematics (1988) uses apartness for the reals (volume 1), and general apartness relations in algebra (volume 2, chapter 8). They say “preapartness” and “apartness” instead of “apartness” and “tight apartness” respectively.

  • Apartness plays a minimal role in 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).

Last revised on December 8, 2022 at 13:49:50. See the history of this page for a list of all contributions to it.