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 *f* *g* iff *f* = *g*|_{dom f}.

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

**Proposition.** *f* *g* 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.** *f* *g* <=> *f** *g** <=> *f** *g**.

**Proof.** Obvious. **End of proof.**

**Theorem.** *f* *g* 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.** *f* *g* implies *f* *g*.

**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 *f* *g* and *g* *h*. Then *f* = *g*|_{dom f} = (*h*|_{dom g})|_{dom f} = *h*|_{dom f} because dom *f* dom *g*. So *f* *h*.

*Antisymmetry.* Let *f* *g* and *g* *f*. Then *f* *g* and *g* *f*. 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 *f* *g*.

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

**Proof.** This follows from *f* *g* <=> *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 (*f* *g*)* = *f** *g**. **End of proof.**.

Related theorems

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

**Related links**

- A theorem about vertical order of binary relations.
- My category theory research, particularly the theory of dependencies.