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!


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.

  • $\begingroup$ Oops. Nice catch Arthur. $\endgroup$ – Lord_Farin Jun 5 '13 at 7:08

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$.

  • $\begingroup$ That $\supset$ is awfully old-fashioned; it would be more readable with $\to$ (or $\implies$, though I really prefer $\to$). $\endgroup$ – Brian M. Scott Jun 5 '13 at 6:49
  • $\begingroup$ @Brian I know, but I was following OPs notation. I always use $\to$ when I can influence the choice of a symbol. $\endgroup$ – Lord_Farin Jun 5 '13 at 6:49
  • $\begingroup$ Ah. I think that this is a case in which I’d do a little silent arm-twisting. :-) $\endgroup$ – Brian M. Scott Jun 5 '13 at 6:51

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’.


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}$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.