left and right euclidean;
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 equipped with an apartness relation is a groupoid (with as the set of objects) enriched over the cartesian monoidal category , 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 is self-dual under negation), this is equivalent to equipping with an equivalence relation (which makes a groupoid enriched over the cartesian category 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 as a binary relation satisfying these three properties:
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 instead of , but keep in mind that is not the negation of ; rather, is the negation of . (So inequality, when it exists, is more basic than equality.)
If and are both sets equipped with apartness relations, then a function is strongly extensional if whenever ; that is, reflects apartness. The strongly extensional functions are precisely the enriched functors between -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 is tight.)
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, iff or .) 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 and , the set of maps from to becomes an inequality space under the rule that iff for some .
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 -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.
Let be a set equipped with a tight apartness relation . Using , many topological notions may be defined on . (It's not really necessary that the apartness be tight; this corresponds to the separation axiom in topology.)
If is a subset of and is an element, then is a -neighbourhood (or -neighborhood) of if, given any , or ; note that by irreflexivity. The neighbourhoods of form a filter: a superset of a neighbourhood is a neighbourhood, and the intersection of or (hence of any finite number) of neighbourhoods is a neighbourhood.
A subset is -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 or (hence of any finite number) of open subsets is open.
The -complement of is the subset ; this is open by comparison. More generally, the -complement of any subset is the set , defined as:
This is not in general open, but you would use it where you would classically use the set-theoretic complement. However, if is open to begin with, then equals the set-theoretic complement.
If , then and , which shows that satisfies the separation axiom. Symmetry is important here; if we removed symmetry from the axioms of apartness, then we would still get a topology, but it would not be . This is a version of the fact that failure of is given by a partial order (or a preorder if might also fail).
The antigraph of a function is
Recall that in ordinary topology, a function between Hausdorff spaces is continuous iff its graph is closed. Similarly, a function is strongly extensional iff its antigraph is open. (Then the graph of is the complement of the antigraph.)
One important topological concept that doesn't appear classically is locatedness; in an inequality space, a subset is located if, given any point and any neighbourhood of , either is inhabited (that is, it has a point) or some neighbourhood of (not necessarily ) is contained in . Note that every point is located. (For an example of a set that need not be located, consider , where is an arbitrary truth value. In an inhabited space, this set is located iff is true or false.)
Recall that, as Bill Lawvere taught us, a metric space is a groupoid (or -category) enriched over the category 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 -morphisms. Furthermore, Lawvere advocated using instead of , 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 to that maps a nonnegative real number to the truth value of the statement that . Accordingly, any (symmetric) metric space becomes an inequality space, and any function satisfying ) 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 -open will also be -open, but not necessarily the other way around. Similarly, a (merely) continuous function between metric spaces is (still) strongly extensional.
In analysis, many spaces are given as gauge spaces, that is by families of pseudometrics; these also become inequality spaces by declaring that iff for some pseudometric 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 iff there is an entourage with . (If the uniform space is not uniformly regular, the result is merely an inequality relation, not an apartness.)
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: and are apart iff and are apart.
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 is a subset such that , whenever , and whenever . But a left antiideal in is a subset such that is false, or whenever , and whenever . Notice that an antiideal is necessarily -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 (so also satisfying that whenever ) is antiprime if and whenever . 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 with the monoidal structure given by logical OR? This is the only meaning I can give this word here, but a category enriched over seems necessarily to be an indiscrete groupoid over its set of objects. (Because for all objects and then , too, for all .)
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 is the subobject classifier, ?
Toby replies: Yes, that is correct; . Even when , you have only if you believe excluded middle, which constructivists do not. Thus, constructivists will talk about apartness relations in , while a classical mathematician will have to put the discussion internal to to get nontrivial results.
Urs replies to the reply: I like this statement “”. Would we also want to say ?