Strict Weak Ordering Induces Partition

Theorem

Let $\struct {S, \prec}$ be a relational structure such that $\prec$ is a strict weak ordering on $S$.

That is, each of the partitions $A$ of $S$ is a relational structure $\struct {\mathbb S, <}$ such that:

$\mathbb S$ is the set of these partitions of $S$;

$<$ is the strict total ordering on $\mathbb S$ induced by $\prec$.

From the definition of strict weak ordering, we define the symbol $\Bumpeq$ as:

$a \Bumpeq b := \neg a \prec b \land \neg b \prec a$

that is, $a \Bumpeq b$ means "$a$ and $b$ are non-comparable".

Checking in turn each of the criteria for equivalence:

As $\prec$ is antireflexive, by definition $\forall a \in S: \neg a \prec a$.

Hence by the Rule of Idempotence $\neg a \prec a \land \neg a \prec a$ and so $\forall a \in S: a \Bumpeq a$.

We have that $a \Bumpeq b$ is defined as being $\neg a \prec b \land \neg b \prec a$.

It follows from the Rule of Commutation that $\neg b \prec a \land \neg a \prec b$, and so $b \Bumpeq a$.

The relation $a \Bumpeq b$ is defined as being transitive in a strict weak ordering.

$\blacksquare$