Show that Total Orders does not have the finite model property I am not sure whether my answer to this problem is correct. I would be grateful if anyone could correct my mistakes or help me to find the correct solutions.
The problem:  

Show that Total Orders does not have the finite model property by finding a sentence A which
  is refuted only in models with an infinite domain.

Just for reference purpose only:
A theory T has the finite model property if and only if whenever $T\nvdash A$ there is a model $\mathcal{M}$ with a finite domain, such that $\mathcal{M}$ satisfies the theory $T$ but $A$ does not hold in $\mathcal{M}$.
The theory of Total Orders (in the language with quantifiers, propositional
connectives, identity and one new binary relation symbol '<') defined as the set of consequences of the following three formulas:
1. $(\forall x)\neg(x<x)$
2. $(\forall x)((x<y\wedge y<z)\supset x<z)$
3. $(\forall x)(x<y\vee x=y\vee y<x)$
My answer is quite simple, but it is too simple that I doubt whether it is correct. I am trying to say that the statement "there is a least element" is refuted only in models with an infinite domain, for example the integers. My sentence A is $\neg((\exists y)(\forall x)(y<x))$.
I am not sure whether I am correct. Please correct me if I am wrong and please say so if there is any better answer.
Many thanks in advance!
 A: That's entirely correct. That's almost correct, see Arthur Fischer's answer.
You can craft more sentences from the knowledge that a finite total ordering is a well-ordering (see e.g. ProofWiki), although the one you gave (along with its "dual" $\neg((\exists y)(\forall x)(x = y \lor x < y))$) is likely among the simplest possible.
There are also sentences that do not need a negation, for example:
$$(\forall x)((\forall y)(y \le x) \lor (\exists y)(x < y \land (\forall z)(x < z \supset y \le z)))$$
which intuitively says "every element has a least successor". E.g. $\Bbb Q$ violates this statement.
For an example of a slightly different flavour you can consider the negation of the "denseness" statement: $$\neg((\forall x)(\forall y)(x < y \supset ((\exists z)(x < z \land z < y))))$$
The negation of this sentence can be expressed in natural language as: "between any two elements there is a third element". Examples of infinite orderings satisfying this are $\Bbb Q$ and $\Bbb R$.
A: Your sentence is almost correct, but it fails to be correct for one (dare I say dumb?) reason: it is actually provable from your theory $T$ of total orders, which is actually the theory of strict (irreflexive) total orders.  Note that your sentence is logically equivalent to $$( \forall y ) ( \exists x ) ( y \not< x ).$$
Now if $( X , < )$ is a strict total order, then taking any $y \in X$ we have, by irreflexivity, that $y \not< y$; i.e., there is an $x \in X$ (namely $y$) such that $y \not< x$.  As the sentence holds in all models, by the Completeness Theorem it is provable from $T$.  But we are specifically looking for a sentence which is not provable from $T$.
If you slightly alter your sentence to exclude the triviality mentioned above, it should work.
A: On taking a closer look, I see that your sentence $\neg((\exists y)(\forall x)(y<x))$ doesn’t quite work. The problem is that it’s a consequence of your first axiom: no matter what $y$, is it’s not the case that $\forall x(y<x)$, since it’s not the case that $y<y$. Another way to see this is by using some basic logical equivalences to move the negation inward: it’s equivalent to
$$\forall y\exists x\big(\neg(y<x)\big)\;,$$
which is true because $\forall y\big(\neg(y<y)\big)$. You can repair it by making it
$$\neg\exists y\forall x(y<x\lor y=x)\;,$$
which does say that there is no least element. Or you can express the same idea positively as
$$\forall x\exists y(y<x)\;,$$
‘for each element there is a smaller element’.
A: Looks like a good candidate to me. As you say, this clearly holds in every finite model of our theory, but infinite counterexamples exist, like $\mathbb{Z}$.
