2 Orders and Abstract Reduction Relations

2.1 Foundedness Properties

Definition 5

✓

Let $r$ be a relation on $M$. Then $r$ is called

reflexive if $\Delta (M) \subseteq r$,
symmetric if $r \subseteq r^{-1}$,
transitive if $r \circ r \subseteq r$,
antisymmetric if $r \cap r^{-1} \subseteq \Delta (M)$,
connex if $r \cup r^{-1} = M \times M$,
irreflexive if $\Delta (M) \cap r = \emptyset $,
strictly antisymmetric if $r \cap r^{-1} = \emptyset $,
an equivalence relation on $M$ if $r$ is reflexive, symmetric, and transitive,
a quasi-order (preorder) on $M$ if $r$ is reflexive and transitive,
a partial order on $M$ if $r$ is reflexive, transitive and antisymmetric,
a (linear) order on $M$ if $r$ is a connex partial order on $M$, and
a linear quasi-order on $M$ if $r$ is a connex quasi-order on $M$.

Definition 6

✓

Let $r$ be a relation on $M$ with strict part $r_s$, and let $N \subseteq M$.

Then an element $a$ of $N$ is called $r$-minimal ($r$-maximal) in $N$ if there is no $b \in N$ with $b \, r_s \, a$ (with $a \, r_s \, b$). For $N = M$ the reference to $N$ is omitted.
A strictly descending (strictly ascending) $r$-chain in $M$ is an infinite sequence $\{ a_n\} _{n \in \mathbb {N}}$ of elements of $M$ such that $a_{n+1} \, r_s \, a_n$ (such that $a_n \, r_s \, a_{n+1}$) for all $n \in \mathbb {N}$.
The relation $r$ is called well-founded (noetherian) if every non-empty subset $N$ of $M$ has an $r$-minimal (an $r$-maximal) element. $r$ is a well-order on $M$ if $r$ is a well-founded linear order on $M$.

Definition 7 The “Antisymmetrization” of $M$

✓

Let $(M,\le )$ be a preordered set. Define an equivalence relation

\[ \sim \; \colon \; M\times M\; \to \; \mathrm{Prop}, \qquad a\sim b \; \iff \; \bigl(a\le b \wedge b\le a\bigr). \]

We write $[a]$ for the equivalence class of $a$, and denote the quotient by

\[ \mathrm{Quot}(M,\sim )=\{ \, [a]\mid a\in M\} . \]

Definition 8

✓

Let $\preceq $ be a quasi-order on $M$ and let $N \subseteq M$. Then a subset $B$ of $N$ is called a Dickson basis, or simply basis of $N$ w.r.t. $\preceq $, if for every $a \in N$ there exists some $b \in B$ with $b \preceq a$.

We say that $\preceq $ has the Dickson property, or is a well-quasi-order(wqo), if every subset $N$ of $M$ has a finite basis w.r.t. $\preceq $.
A well partial order, or a wpo, is a wqo that is a proper ordering relation, i.e., it is antisymmetric.

Definition 9 Minimal elements and min–classes

✓

Let $N \subseteq M$. An element $a \in N$ is called minimal in $N$ if there is no $b \in N$ such that $b {\lt} a$ (where ${\lt}$ is the strict part of the quasi-order). We denote the set of all minimal elements of $N$ by:

\[ \operatorname {Minimal}(N) = \{ a \in N \mid \forall b \in N, \neg (b {\lt} a) \} \]

The min–classes of $N$ are the intersections of $N$ with the $\sim $-equivalence classes of its minimal elements:

\[ \operatorname {minClasses}(N) = \{ [a]_{\sim } \cap N \mid a \in \operatorname {Minimal}(N) \} \]

Lemma 10

✓

Let $N \subseteq M$ and let $a \in N$. Consider the restricted subset

\[ N_{\le a} \coloneqq \{ \, d \in N \mid d \le a \, \} . \]

Then every min–class of $N_{\le a}$ is also a min–class of $N$, i.e.

\[ \operatorname {minClasses}(N_{\le a}) \subseteq \operatorname {minClasses}(N). \]

Proof ▶

Let $[d] \in \operatorname {minClasses}(N_{\le a})$. By definition of $\operatorname {minClasses}$ there exists an element $d$ such that

\[ d \in N_{\le a} \qquad \text{and}\qquad \forall x \in N_{\le a},\; \neg (x {\lt} d). \]

Thus $d \in N$ and $d \le a$, and for every $x \in N$ with $x \le a$ we have $\neg (x {\lt} d)$.

We claim that $[d] \in \operatorname {minClasses}(N)$. For this it suffices to show that $d \in N$ (which we already know) and that there is no $x \in N$ with $x {\lt} d$.

So let $x \in N$ and assume, for a contradiction, that $x {\lt} d$. Then in particular $x \le d$, and since $d \le a$, by transitivity we obtain $x \le a$. Hence $x \in N_{\le a}$, and the minimality condition of $d$ in $N_{\le a}$ tells us that $\neg (x {\lt} d)$, contradicting $x {\lt} d$.

Therefore no such $x$ exists, so $d$ is also minimal in $N$. Consequently $[d] \in \operatorname {minClasses}(N)$, and hence

\[ \operatorname {minClasses}(N_{\le a}) \subseteq \operatorname {minClasses}(N). \]

Proposition 11

✓

Let $\preceq $ be a quasi-order on $M$ with associated equivalence relation $\sim $. Then the following are equivalent:

$\preceq $ is a well-quasi-order.
Whenever $\{ a_n\} _{n \in \mathbb {N}}$ is a sequence of elements of $M$, then there exist $i {\lt} j$ with $a_i \preceq a_j$.
For every nonempty subset $N$ of $M$, the number of min-classes in $N$ is finite and non-zero.

Proof ▶

(i)$\Longrightarrow $(ii): Set $N = \{ a_n \mid n \in \mathbb {N}\} $ and let $B$ be a finite basis of $N$. Pick $j \in \mathbb {N}$ such that $j {\gt} i$ for all $i \in \mathbb {N}$ with $a_i \in B$. Then $a_{i_0} \preceq a_j$ for some $a_{i_0} \in B$, and the choice of $j$ implies $i_0 {\lt} j$.

(ii)$\Longrightarrow $(iii): Suppose there exist infinitely many min-classes in some non-empty subset $N$ of $M$. Using the axiom of choice, we get an infinite sequence $\{ a_n\} _{n \in \mathbb {N}}$ of pairwise $\sim $-inequivalent minimal elements in $N$. By our assumption (ii), $a_i \preceq a_j$ for some $i {\lt} j$. From the minimality of $a_j$, we conclude that $a_j \preceq a_i$ and so $a_i \sim a_j$, a contradiction. If, on the other hand, $N$ has no minimal element, then we can produce a strictly descending $\preceq $-chain as in the proof of Proposition 4.31, contradicting (ii).

(iii)$\Longrightarrow $(i): Let $N$ be a non-empty subset of $M$. Choosing one element out of each of the finitely many min-classes, we can find a finite subset $B$ of $N$ such that each $b \in B$ is minimal, and such that every minimal $a \in N$ is $\sim $-equivalent to some $b \in B$. We claim that $B$ is a basis of $N$. Let $a \in N$. Then the set

\[ N' = \{ d \in N \mid d \preceq a \} \]

contains a minimal element $c$. It is easy to see that $c$ is minimal in $N$ too, and so $c \sim b$ for some $b \in B$. We now have $b \preceq c \preceq a$ and hence $b \preceq a$.

Theorem 12

✓

Let $(M,\le )$ be a preorder. Then

\[ \text{$\le $ has the Dickson property} \quad \Longleftrightarrow \quad \text{$\le $ is a well quasi-order}. \]

Proof ▶

This is exactly the equivalence $(i)\Longleftrightarrow (ii)$ in Proposition (Becker–Weispfenning, Proposition 4.42). In our Lean development we prove the two implications as follows:

$(i)\Rightarrow (ii)$ is shown by extracting a finite basis for the set $N=\{ a_n\mid n\in \mathbb N\} $ and choosing $i{\lt}j$ accordingly.
$(ii)\Rightarrow (i)$ is obtained by first proving $(ii)\Rightarrow (iii)$ (finiteness and nonemptiness of min–classes for every nonempty subset), and then applying $(iii)\Rightarrow (i)$.

Proposition 13

✓

Let $\preceq $ be a well- quasi-order on $M$, and let $\{ a_n\} _{n \in \mathbb {N}}$ be a sequence of elements of $M$. Then there exists a strictly ascending sequence $\{ n_i\} _{i \in \mathbb {N}}$ of natural numbers such that $a_{n_i} \preceq a_{n_j}$ for all $i {\lt} j$.

Proof ▶

We define the sequence $\{ n_i\} _{i \in \mathbb {N}}$ recursively, and by simultaneous induction on $i$ we verify the following properties:

$a_{n_i} \preceq a_{n_{i+1}}$ for all $i \in \mathbb {N}$, and
for all $i \in \mathbb {N}$, the set $\{ n \in \mathbb {N} \mid a_{n_i} \preceq a_n\} $ is infinite.

For $i=0$, let $\{ b_1, \dots , b_k\} $ be a finite basis of the set $\{ a_n \mid n \in \mathbb {N}\} $, and for each $j$ with $1 \le j \le k$, set

\[ B_j = \{ n \in \mathbb {N} \mid b_j \preceq a_n\} . \]

Then $\bigcup _{j=1}^k B_j = \mathbb {N}$ by the choice of $B$. Since the union of finitely many finite sets is finite, we can find a $B_j$ which is infinite. Moreover, $b_j = a_m$ for some $m \in \mathbb {N}$, and we set $n_0 = m$. For $i+1$, we consider the set

\[ U_i = \{ a_n \mid a_{n_i} \preceq a_n, n_i {\lt} n\} . \]

By condition (ii) for $i$, the set $\{ n \in \mathbb {N} \mid a_n \in U_i\} $ is infinite. Choosing some finite basis of $U_i$, we can, as before, find an element $a_m$ in this basis such that $a_m \preceq a_n$ for infinitely many different $n \in \mathbb {N}$, and we take $n_{i+1} = m$. Conditions (i) and (ii) obviously continue to hold. It now follows easily from condition (i) and the transitivity of $\preceq $ that $\{ n_i\} _{i \in \mathbb {N}}$ has the desired property.