1.2.5: Orders

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

Many of our comparisons involve describing some objects as being “less than”, “equal to”, or “greater than” other objects, in a certain respect. These involve order relations. But there are different kinds of order relations. For instance, some require that any two objects be comparable, others don’t. Some include identity (like \(\le\)) and some exclude it (like \(<\)). It will help us to have a taxonomy here.

Definition \(\PageIndex{1}\): Preorder

A relation which is both reflexive and transitive is called a preorder.

Definition \(\PageIndex{2}\): Partial order

A preorder which is also anti-symmetric is called a partial order.

Definition \(\PageIndex{3}\): Linear order

A partial order which is also connected is called a total order or linear order.

Every linear order is also a partial order, and every partial order is also a preorder, but the converses don’t hold.

Example \(\PageIndex{1}\)

Every linear order is also a partial order, and every partial order is also a preorder, but the converses don’t hold. The universal relation on \(A\) is a preorder, since it is reflexive and transitive. But, if \(A\) has more than one element, the universal relation is not anti-symmetric, and so not a partial order.

Example \(\PageIndex{2}\)

Consider the no longer than relation \(\preccurlyeq\) on \(\Bin^*\): \(x \preccurlyeq y\) iff \(\len{x} \le \len{y}\). This is a preorder (reflexive and transitive), and even connected, but not a partial order, since it is not anti-symmetric. For instance, \(01 \preccurlyeq 10\) and \(10 \preccurlyeq 01\), but \(01 \neq 10\).

Example \(\PageIndex{3}\)

An important partial order is the relation \(\subseteq\) on a set of sets. This is not in general a linear order, since if \(a \neq b\) and we consider \(\Pow{\{a, b\}} = \{\emptyset, \{a\}, \{b\}, \{a,b\}\}\), we see that \(\{a\} \nsubseteq \{b\}\) and \(\{a\} \neq \{b\}\) and \(\{b\} \nsubseteq \{a\}\).

Example \(\PageIndex{4}\)

The relation of divisibility without remainder gives us a partial order which isn’t a linear order. For integers \(n\), \(m\), we write \(n\mid m\) to mean \(n\) (evenly) divides \(m\), i.e., iff there is some integer \(k\) so that \(m=kn\). On \(\Nat\), this is a partial order, but not a linear order: for instance, \(2\nmid3\) and also \(3\nmid2\). Considered as a relation on \(\Int\), divisibility is only a preorder since it is not anti-symmetric: \(1\mid-1\) and \(-1\mid1\) but \(1\neq-1\).

Definition \(\PageIndex{4}\): Strict order

A strict order is a relation which is irreflexive, asymmetric, and transitive.

Definition \(\PageIndex{5}\): Strict linear order

A strict order which is also connected is called a strict linear order.

Example \(\PageIndex{5}\)

\(\le\) is the linear order corresponding to the strict linear order \(<\). \(\subseteq\) is the partial order corresponding to the strict order \(\subsetneq\).

Definition \(\PageIndex{6}\): Total order

A strict order which is also connected is called a total order. This is also sometimes called a strict linear order.

Any strict order \(R\) on \(A\) can be turned into a partial order by adding the diagonal \(\Id{A}\), i.e., adding all the pairs \(\tuple{x, x}\). (This is called the reflexive closure of \(R\).) Conversely, starting from a partial order, one can get a strict order by removing \(\Id{A}\). These next two results make this precise.

Proposition \(\PageIndex{1}\)

If \(R\) is a strict order on \(A\), then \(R^+ = R \cup \Id{A}\) is a partial order. Moreover, if \(R\) is total, then \(R^+\) is a linear order.

Proof. Suppose \(R\) is a strict order, i.e., \(R \subseteq A^2\) and \(R\) is irreflexive, asymmetric, and transitive. Let \(R^+ = R \cup \Id{A}\). We have to show that \(R^+\) is reflexive, antisymmetric, and transitive.

\(R^+\) is clearly reflexive, since \(\tuple{x, x} \in \Id{A} \subseteq R^+\) for all \(x \in A\).

To show \(R^+\) is antisymmetric, suppose for reductio that \(R^+xy\) and \(R^+yx\) but \(x \neq y\). Since \(\tuple{x,y} \in R \cup \Id{X}\), but \(\tuple{x, y} \notin \Id{X}\), we must have \(\tuple{x, y} \in R\), i.e., \(Rxy\). Similarly, \(Ryx\). But this contradicts the assumption that \(R\) is asymmetric.

To establish transitivity, suppose that \(R^+xy\) and \(R^+yz\). If both \(\tuple{x, y} \in R\) and \(\tuple{y,z} \in R\), then \(\tuple{x, z} \in R\) since \(R\) is transitive. Otherwise, either \(\tuple{x, y} \in \Id{X}\), i.e., \(x = y\), or \(\tuple{y, z} \in \Id{X}\), i.e., \(y = z\). In the first case, we have that \(R^+yz\) by assumption, \(x = y\), hence \(R^+xz\). Similarly in the second case. In either case, \(R^+xz\), thus, \(R^+\) is also transitive.

Concerning the “moreover” clause, suppose \(R\) is a total order, i.e., that \(R\) is connected. So for all \(x \neq y\), either \(Rxy\) or \(Ryx\), i.e., either \(\tuple{x, y} \in R\) or \(\tuple{y, x} \in R\). Since \(R \subseteq R^+\), this remains true of \(R^+\), so \(R^+\) is connected as well. ◻

Proposition \(\PageIndex{2}\)

If \(R\) is a partial order on \(X\), then \(R^- = R \setminus \Id{X}\) is a strict order. Moreover, if \(R\) is linear, then \(R^-\) is total.

Proof. This is left as an exercise. ◻

Problem \(\PageIndex{1}\)

Give a proof of Proposition \(\PageIndex{2}\).

Example \(\PageIndex{6}\)

\(\le\) is the linear order corresponding to the total order \(<\). \(\subseteq\) is the partial order corresponding to the strict order \(\subsetneq\).

The following simple result which establishes that total orders satisfy an extensionality-like property:

Proposition \(\PageIndex{3}\)

If \(<\) totally orders \(A\), then: \[(\forall a, b \in A)((\forall x \in A)(x < a \leftrightarrow x < b) \rightarrow a = b)\nonumber\]

Proof. Suppose \((\forall x \in A)(x < a \leftrightarrow x < b)\). If \(a < b\), then \(a < a\), contradicting the fact that \(<\) is irreflexive; so \(a \nless b\). Exactly similarly, \(b \nless a\). So \(a = b\), as \(<\) is connected. ◻