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=r_0.r_1{r}_2{r}_3\mathrm{\dots }\mathit{\hspace{1em}\hspace{1em}}s=s_0.s_1{s}_2{s}_3\mathrm{\dots }$$

one needs to show that $r_0=s_0$, $r_1=s_1$, $r_2=s_2$, etc… which involves demonstrating an infinite number of equalities. On the other hand, showing that $r\ne s$ 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: $r_n\ne s_n$. 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 relation $\mathrm{\#}$ on $X$ satisfying the following conditions:

1. $\forall x(\mathrm{\neg }x\mathrm{\#}x)$,

2. $\forall x\forall y(x\mathrm{\#}y\to y\mathrm{\#}x)$, and

3. $\forall x\forall y\forall z(x\mathrm{\#}y\to (x\mathrm{\#}z\vee y\mathrm{\#}z))$.

And if in addition, we have the following

1. $\forall x\forall y(\mathrm{\neg }x\mathrm{\#}y\leftrightarrow x=y)$

Then $\mathrm{\#}$ is said to be tight.

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

1. the first condition is redundant if $\mathrm{\#}$ is assumed to be tight.

2. the second condition above is redundant, for if $x\mathrm{\#}y$, then $x\mathrm{\#}x$ or $y\mathrm{\#}x$ by condition 3, but then by condition 1, $x\mathrm{\#}x$ is false, therefore $y\mathrm{\#}x$.

3. the converse of an apartness relation is an equivalence relation: define $xRy$ iff not $x\mathrm{\#}y$. Since $x\mathrm{\#}x$ is false for all $x\in X$, $xRx$ for all $x\in X$. Also, the contrapositive of the second condition above shows that $R$ is symmetric. Now, suppose $xRy$ and $yRz$. Then not $x\mathrm{\#}y$ and not $y\mathrm{\#}z$, or not $(x\mathrm{\#}y\vee z\mathrm{\#}y)$. Applying the contrapositive of the third condition, we have not $x\mathrm{\#}z$, or $xRz$. So $R$ is transitive.

4. Conversely, the converse of an equivalence relation is an apartness relation: suppose $R$ is an equivalence relation, and define $x\mathrm{\#}y$ iff not $xRy$. Then irreflexivity and symmetry of $\mathrm{\#}$ are clear from the reflexivity and symmetry of $R$. Now, suppose $x\mathrm{\#}y$. Pick any $z\in X$. If not $x\mathrm{\#}z$ and not $y\mathrm{\#}z$, then $xRz$ and $yRz$, or $zRy$, which means $xRy$ since $R$ is transitive. But this contradicts the assumption $x\mathrm{\#}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 contradiction) 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:

• $\ne$ is a tight apartness relation on the set of rationals $\mathbb{Q}$.

• more generally, $\ne$ is a tight apartness relation on a set $X$ if “$=$” on $X$ is a deciable predicate, that is, for any pair $x,y\in X$, either $x=y$ or $x\ne y$.

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

• However, if we define $x\mathrm{\#}y$ iff there is a rational number $r$ such that

  then $\mathrm{\#}$ is a tight apartness relation. To see this, first note that $\mathrm{\#}$ is irreflexive and symmetric. Also, it is not hard to see that the converse of $\mathrm{\#}$ is $=$. Now, suppose $x\mathrm{\#}y$. Pick any real number $z$. If not $x\mathrm{\#}z$, then $x=z$, which means $y\mathrm{\#}z$. Similarly, if not $y\mathrm{\#}z$, then $x\mathrm{\#}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