connected relation

Connected relations


A (binary) relation \sim on a set AA is connected (or sometimes linear) if any two elements that are related in neither order are equal:

(x,y:A),xyyxx=y. \forall (x, y: A),\; x \nsim y \;\wedge\; y \nsim x \;\Rightarrow\; x = y .

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:

(x,y:A),xyx=y. \forall (x, y: A),\; x \nsim y \;\Rightarrow\; x = y .

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.)

Constructive aspects

Using excluded middle, it is equivalent to say that every two elements are related in some order or equal:

(x,y:A),xyyxx=y. \forall (x, y: A),\; x \sim y \;\vee\; y \sim x \;\vee\; x = y .

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 AA 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:

(x,y:A),x#yxyyx. \forall (x, y: A),\; x \# y \;\Rightarrow\; x \sim y \;\vee\; y \sim x .

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).

Revised on April 21, 2017 02:07:27 by Toby Bartels (