apartness relation

Given two arbitrary real numbers r,s, how does one (better yet, a computer) prove r=s? Given decimal representations of r and s:

r=r0.r1r2r3  s=s0.s1s2s3

one needs to show that r0=s0, r1=s1, r2=s2, etc… which involves demonstrating an infiniteMathworldPlanetmathPlanetmath number of equalities. On the other hand, showing that rs is a finitary process, in that one proceeds as above, and then stops when he/she finds a decimal place n where the two corresponding digits differ: rnsn. Therefore, in constructive mathematics, inequality is a more appropriate choice of study than equality. The formal notion of inequality in constructive mathematics is that of an apartness relation.

An apartness relation on a set X is a binary relationMathworldPlanetmath # on X satisfying the following conditions:

  1. 1.


  2. 2.

    xy(x#yy#x), and

  3. 3.


And if in addition, we have the following

  1. 4.


Then # is said to be tight.

In classical mathematics where the law of the excluded middle is accepted, the following are true:

  1. 1.

    the first condition is redundant if # is assumed to be tight.

  2. 2.

    the second condition above is redundant, for if x#y, then x#x or y#x by condition 3, but then by condition 1, x#x is false, therefore y#x.

  3. 3.

    the converseMathworldPlanetmath of an apartness relation is an equivalence relationMathworldPlanetmath: define xRy iff not x#y. Since x#x is false for all xX, xRx for all xX. Also, the contrapositive of the second condition above shows that R is symmetricPlanetmathPlanetmath. Now, suppose xRy and yRz. Then not x#y and not y#z, or not (x#yz#y). Applying the contrapositive of the third condition, we have not x#z, or xRz. So R is transitiveMathworldPlanetmathPlanetmathPlanetmath.

  4. 4.

    Conversely, the converse of an equivalence relation is an apartness relation: suppose R is an equivalence relation, and define x#y iff not xRy. Then irreflexivity and symmetry of # are clear from the reflexivityMathworldPlanetmath and symmetry of R. Now, suppose x#y. Pick any zX. If not x#z and not y#z, then xRz and yRz, or zRy, which means xRy since R is transitive. But this contradicts the assumptionPlanetmathPlanetmath x#y, or not xRy.

Based on the last two observations, we see that the notion of apartness is not a very useful in mathematics based on classical logic, as the study of equivalence relation suffices.

On the other hand, arguing constructively, the second and the last statements above no longer hold, because the law of the excluded middle (and proof by contradictionMathworldPlanetmathPlanetmath) is used to derive both results. In other words, the apartness relation is a distinct concept in constructive mathematics. Below are some examples (and non-examples) of tight apartness relations:

  • is a tight apartness relation on the set of rationals .

  • more generally, is a tight apartness relation on a set X if “=” on X is a deciable predicateMathworldPlanetmath, that is, for any pair x,yX, either x=y or xy.

  • However, is not a tight apartness relation on the set of reals , since if xy, it may not be possible to prove constructively that, for any given real number z, xz or yz (because such a proof may be infinite in length).

  • However, if we define x#y iff there is a rational number r such that


    then # is a tight apartness relation. To see this, first note that # is irreflexiveMathworldPlanetmath and symmetric. Also, it is not hard to see that the converse of # is =. Now, suppose x#y. Pick any real number z. If not x#z, then x=z, which means y#z. Similarly, if not y#z, then x#z.

Title apartness relation
Canonical name ApartnessRelation
Date of creation 2013-03-22 19:35:45
Last modified on 2013-03-22 19:35:45
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 13
Author CWoo (3771)
Entry type Definition
Classification msc 03F99
Classification msc 03F65
Classification msc 03F60
Defines tight