nLab total relation

Redirected from "linear relation".
Total relations

Total relations

Idea

A total relation or linear relation is a binary relation on a set with the property that distinguishes the total orders/linear orders among the partial orders.

Terminology

An entire relation is sometimes called ‘total’, but these are unrelated concepts. The ‘total’ there is in the sense of a total (as opposed to partial) function, while the ‘total’ here is in the sense of a total (as opposed to partial) order.

A total relation is necessarily reflexive. For an irreflexive version, see connected relation. In classical mathematics, total relations and connected relations are equivalent concepts, since either may be constructed from the other by changing every truth value of the form xxx \sim x, and so the distinction is not always maintained.

Definitions

A binary relation RR on a set AA is total if any two elements are related in one order or the other:

(x,y:A),x Ryy Rx. \forall (x, y: A),\; x \sim_R y \;\vee\; y \sim_R x .

In other words, RR is total if its union with its reverse is the universal relation?:

A×ARR op. A \times A \subseteq R \cup R^{op} .

(Of course, this containment is in fact an equality.) In this way, the concept can be generalized from Rel to any 22-poset-with-duals?; part of the definition then becomes the requirement that the union RR opR \cup R^{op} exists.

In constructive mathematics, we can distinguish between a strongly total relation, defined as above, and a weakly total or linear relation:

(x,y:A),¬(x Ry)y Rx. \forall (x, y: A),\; \neg(x \sim_R y) \;\Rightarrow\; y \sim_R x .

(In theory, this should be conjoined with ¬(y Rx)x Ry\neg(y \sim_R x) \Rightarrow x \sim_R y, but this follows because the original definition is symmetric in xx and yy.) This can also be expressed in RelRel using the weak union \parr instead of \cup and generalized to other 22-posets with the structure to support this operation. We can define an even weaker notion:

(x,y:A),¬(x Ry)¬¬(y Rx), \forall (x, y: A),\; \neg(x \sim_R y) \;\Rightarrow\; \neg\neg(y \sim_R x) ,

which is based on using the double negation of union in RelRel, but I'm not sure that anyone uses this in practice.

We can also let RR be a disjoint pair? of relations, denoted R +R^+ and R R^- or (more suggestively) R\sim_R and R\nsim_R, related according to the antithesis interpretation of linear logic within constructive mathematics, which requires that

(x,y:A),x Ry¬(x Ry) \forall (x, y: A),\; x \nsim_R y \;\Rightarrow\; \neg(x \sim_R y)

(but not the converse). Then RR is weakly total or linear if additionally

(x,y:A),(x Ryy Rx). \forall (x, y: A),\; (x \nsim_R y \;\Rightarrow\; y \sim_R x) .

It's strongly total if, in addition to all of the above,

(x,y:A),x Ryy Rx. \forall (x, y: A),\; x \sim_R y \;\vee\; y \sim_R x .

This can all be expressed in a 22-poset of disjoint pairs of relations equipped with strong (\uplus) and weak (\parr) notions of union.

Properties

A total order is precisely a partial order that is total in the sense of this article.

In classical logic, RR is total if and only if R=R˙Δ AR = \dot{R} \cup \Delta_A for some connected relation R˙\dot{R}, and then R˙\dot{R} must be RΔ AR \setminus \Delta_A. (Here, Δ A\Delta_A is the equality relation on the set AA.)

Totality is antithetical to asymmetry. In classical logic, this means that RR is total if and only if its negation is asymmetric. More generally, in terms of the antithesis interpretation, the disjoint pair R=(R +,R )R = (R^+,R^-) is strongly/weakly total if and only if its formal negation R =(R ,R +)R^\bot = (R^-,R^+) is strongly/weakly asymmetric.

In particular, R R^- is asymmetric in its own right whenever a disjoint pair (R +,R )(R^+,R^-) is weakly total. Conversely, a disjoint pair (R +,R )(R^+,R^-) is strongly total if (and only if) R +R^+ is strongly total in its own right and R R^- is asymmetric in its own right.

References

For linearity of relations as weak totality, see section 11.2.1 of:

Last revised on December 26, 2023 at 04:50:05. See the history of this page for a list of all contributions to it.