show that a formula belongs to theory of strict linear order

Question

I'm studying for my exam and I've been stuck on this problem for hours, I'd appreciate any help.

We have the following signature F = ∅ and P = {$<^{(2)},=^{(2)}$} and we define the axiomatization $ A_{slo} $ that contains the following formulas :

$ ∀x. ¬(x < x) $

$∀x∀y∀z. (x < y∧y < z) ⇒ x < z $

$∀x∀y∀z. (x = y∧x < z) ⇒y < z$

$∀x∀y∀z. (x = y∧z < x) ⇒z < y$

$∀x∀y.x < y∨x = y∨y < x$

The interpretation I of domain $D_I ={a,b,c} $ where:

$<^I$ ={$(a,b),(a,c),(b,c)$}
$ =^I$ = {$(a,a),(b,b),(c,c)$}

is a model of $A_{slo}$

Show that the formula below belongs to this theory ($\varphi \in Th(A_{slo}) $)

$\varphi = \forall x \exists y.(\neg(y<x) \Rightarrow \forall z.(x<z\ \lor \ x = z))$

I read that if $T\vDash \varphi$ then $\varphi \in T $, but I don't know how to prove it in this exercise.

Answer 1

Formula $\varphi$ is equivalent to: $∀x \ (∀y¬(y<x) \to ∀z(x<z \lor x=z))$, i.e to:

$∀x \ (∃y(y<x) \lor ∀z(x<z \lor x=z))$.

Your model is: $a < b < c$.

The formula says: for every element $x$, either $x$ is bigger than something, and this is true of $b$ and $c$, or it is less-or-equal than every element, and this is true of $a$.

Thus: $I \vDash \varphi$.

---

Having said that, we may consider that the above equivalent formulation of $\varphi$ is also eqyuivalent to :

$∀x ∀z ∃y \ (y<x \lor x<z \lor x=z)$

which is "trichotomy in disguise".

Answer 2

As noticed by Mauro Allegranza, $\varphi$ is equivalent to $\psi := \forall x \ (\exists y (y < x) \vee \forall z( x < z \vee x=z))$

Let's show that $A_{slo} \models \psi$. Let $M \models A_{slo}$ and $x \in D_M$.
If there is $y \in D_M$ such that $y < x$ then clearly $M \models \psi$.
If there is no such $y$ then by the 5th axiom of $A_{slo}$, this means that any $y \in D_M$ satisfies $x < y \vee x = y$. Of course the name $y$ is of no importance and we might as well rename $y$ to $z$ : we have $x < z \vee x = z$ for all $z$. qed