Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A (binary) relation $\sim$ on a set $A$ is connected (or sometimes linear) if any two elements that are related in neither order are equal:
This is a basic property of linear orders.
An apartness relation (or indeed any inequality) is usually called tight if it is connected, in which case equality is its negation. Since these are symmetric, one can use a simpler definition:
Thus, one could in principle distinguish connected from tight relations in the nonsymmetric case (with tightness stronger than connectedness), but it's not clear that anybody does this. (That is, it may be that the term ‘tight’ is only ever applied to symmetric relations.)
Using excluded middle, it is equivalent to say that every two elements are related in some order or equal:
However, this version is too strong for the intended applications to constructive mathematics. (In particular, $\lt$ on the located Dedekind real numbers satisfies the first definition but not this one.)
On the other hand, there is a stronger notion that may be used in constructive mathematics, if $A$ is already equipped with a tight apartness $\#$. In that case, we say that $\sim$ is strongly connected if any two distinct elements are related in one order or the other:
Since $\#$ is connected itself, every strongly connected relation is connected; the converse holds with excluded middle (through which every set has a unique tight apartness).
We can do a similar thing if $A$ is equipped with any inequality $\#$, except that in the general case, this is not necessarily stronger than being connected, and so we should call it $\#$-connected.
Last revised on November 27, 2021 at 14:54:06. See the history of this page for a list of all contributions to it.