# Partial order on the set of binary relations

On the set of binary relations there exists well known set theoretic partial order ⊆. (Recall that a binary relations is a set of pairs.)

Here I will introduce an another partial order (vertical order) on the set of binary relations. (Analogously can be also introduces horizontal order, and also their intersection/conjunction rectangular order.)

Definition

Let f and g are binary relations. By definition fg iff f = g|dom f.

I will call the relation ⊑ vertical order. Below I will prove that ⊑ is a partial order.

Proposition. fg iff exists a set K such that f = g|K.

Proof. Direct implication is obvious. Reverse implication. Let f = g|K. Then dom f = K ∩ dom g. From this follows f = g|dom f. End of proof.

Reducing vertical order of relations to functions

For any relation p I will denote p* the corresponding function mapping an X to a set of Y. p* is defined by the following two equations:

dom p* = dom p and p*(x) = {y : (x, y) in p} for any x in dom p.

Note that dom f* = dom f.

Proposition. f = g <=> f* = g* for any binary relations f and g.

Proof. Obvious. End of proof.

Proposition. fg <=> f* ⊑ g* <=> f* ⊆ g*.

Proof. Obvious. End of proof.

Theorem. fg iff ∀x∈dom f : f*(x) = g*(x).

Proof. It follows from the last proposition. End of proof.

Vertical order as a partial order

Proposition. fg implies fg.

Proof. Obvious. End of proof.

Theorem. ⊑ is a partial order.

Proof. We need to prove reflexivity, transitivity, and antisymmetry of ⊑.

Reflexivity is obvious.

Transitivity. Let fg and gh. Then f = g|dom f = (h|dom g)|dom f = h|dom f because dom f ⊆ dom g. So fh.

Antisymmetry. Let fg and gf. Then fg and gf. So f = g. End of proof.

I will denote infimum of two elements set {f, g} (where f and g are binary relations), corresponding to the vertical order of, as fg.

Theorem. Vertical order is a meet-semilattice (that is has infimum ⊓ of any two binary relations).

Proof. This follows from fg <=> f* ⊆ g* and that any two elements of the set of functions, whose images are sets of sets, have the infimum (namely set theoretic intersection). The operation * is a partial order isomorphism and so maps a semilattice to semilattice. Vertical infimum of two binary relations f and g can be so restored by the formula (fg)* = f* ∩ g*. End of proof..

Related theorems

About vertical order of binary relations there is an interesting theorem.