Actions

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}