# Axiomatizable orderings

### From Learning Logic for Computer Science

In the following, classes of strict orderings are axiomatized in the signature $\{{<}/2\}$.

A partial order relation is an irreflexive and transitive relation. So the class of all partial orderings is axiomatized by \begin{align} \tag{irr} & \forall x_0 (\neg x_0 < x_0)\\ \tag{trs} & \forall x_0 \forall x_1 \forall x_2 (x_0 < x_1 \wedge x_1 < x_2 \rightarrow x_0 < x_2) \end{align}

A partial order is **discrete** if the ordering relation is empty. So the class of discrete orderings is axiomatized by (irr), (trs), and
\begin{align}
\tag{dscr}
\forall x_0 \forall x_1 \neg x_0 < x_1 \enspace.
\end{align}

A partial order is **dense** if between any two comparable elements there is another one. So the class of dense orderings is axiomatized by (irr), (trs), and
\begin{align}
\tag{dns}
\forall x_0 \forall x_1 (x_0 < x_1 \rightarrow \exists x_2 (x_0 < x_2 \wedge x_2 < x_1)) \enspace.
\end{align}

A partial order is **linear** if any two elements are comparable. So the class of linear orderings is axiomatized by (irr), (trs), and
\begin{align}
\tag{lin}
\forall x_0 \forall x_1 (x_0 < x_1 \vee x_1 < x_0 \vee x_0 \doteq x_1) \enspace.
\end{align}