irreflexive symmetric relation in nLab

Contents

 Definition

An irreflexive symmetric relation or sometimes inequality relation is a binary relation that is irreflexive and symmetric.

Examples

• Every apartness relation is an irreflexive symmetric relation which is also a comparison.

• The negation of a reflexive symmetric relation is an irreflexive symmetric relation.

• Every denial inequality is a weakly tight irreflexive symmetric relation.

In constructive mathematics

In constructive mathematics, not ever tight irreflexive symmetric relation is a denial inequality, and not every denial inequality is tight. Instead, every denial inequality is only weakly tight. Indeed, since excluded middle cannot be proven, we could distinguish between the following irreflexive symmetric relations in constructive mathematics:

• denial inequality, an irreflexive symmetric relation ≠\neq which additionally satisfies ¬(a=b)\neg(a = b) implies (a≠b)(a \neq b)

• tight irreflexive symmetric relation, an irreflexive symmetric relation ≠\neq which additionally satisfies ¬(a≠b)\neg(a \neq b) implies (a=b)(a = b)

• weakly tight irreflexive symmetric relation, an irreflexive symmetric relation ≠\neq which additionally satisfies ¬(a≠b)\neg(a \neq b) implies ¬¬(a=b)\neg \neg (a = b)

• stable irreflexive symmetric relation, an irreflexive symmetric relation ≠\neq which additionally satisfies ¬¬(a≠b)\neg \neg (a \neq b) implies (a≠b)(a \neq b)

• decidable irreflexive symmetric relation, an irreflexive symmetric relation ≠\neq which additionally satisfies (a≠b)(a \neq b) or ¬(a≠b)\neg (a \neq b)

• apartness relation, an irreflexive symmetric relation ≠\neq which additionally satisfies a≠ba \neq b implies that a≠ca \neq c or c≠bc \neq b

or any combination of the above, such as tight apartness relation.

The notion of “inequality relation” in constructive mathematics usually refers to either the denial inequality or a tight apartness relation. On the other hand, some authors have used “inequality relation” to refer to general irreflexive symmetric relations.

Irreflexive symmetric relations and equality of sets

In classical mathematics, every set SS comes with an irreflexive symmetric relation ≠\neq such that for all xx and yy in SS, x=yx = y or x≠yx \neq y.

However, in constructive mathematics, the usual classical notion of disjunction bifurcates into multiple notions which are not equivalent to each other. Here is a Hasse diagram of some of them, applied to the equality and irreflexive symmetric relation, with the strongest statement at the bottom and the weakest at the top (so that each statement entails those above it):

¬(¬(x=y)∧¬(x≠y)) ⇗ ⇖ ¬(x=y)→x≠y x=y←¬(x≠y) ⇖ ⇗ (¬(x=y)→x≠y)∧(x=y←¬(x≠y)) ⇑ x=y∨x≠y \array { & & \neg(\neg(x = y) \wedge \neg(x \neq y)) \\ & ⇗ & & ⇖ \\ \neg(x = y) \rightarrow x \neq y & & & & x = y \leftarrow \neg(x \neq y) \\ & ⇖ & & ⇗ \\ & & (\neg(x = y) \rightarrow x \neq y) \wedge (x = y \leftarrow \neg(x \neq y)) \\ & & \Uparrow \\ & & x = y \vee x \neq y }

• apartness relation
• inequality relation
• reflexive symmetric relation
• antithesis partial order
• antithesis interpretation
• inequality ring
• affine set

References

• Michael Shulman, Affine logic for constructive mathematics. Bulletin of Symbolic Logic, Volume 28, Issue 3, September 2022. pp. 327 - 386 (doi:10.1017/bsl.2022.28, arXiv:1805.07518)