Does a finite first-order theory which has a model always have a finite model? I'm curious whether this is true or not:

Let T be a finite, first-order theory. If T has a model, then T has a finite model.

I would assume the answer is 'yes', but I wanted to make sure I haven't missed something obvious. The reason I believe this to be the case is that according to my understanding of the Lowenheim-Skolem theorem, the only way a countable first-order theory can 'force' a size onto its potential models is by including a countable number of constants which the model must have representations for. Therefore, if the theory is finite, then the number of constants it can 'force' to exist must also be finite, thereby ensuring the existence of a finite model (assuming any model can exist at all). Is anything wrong with my reasoning (apart from its relative informality)?

All the examples so far make use of the equality symbol $=$.  In some areas of logic (broadly construed) one often considers first-order languages without the equality symbol that's always interpreted as the true equality.  But one can construct a finite theory $T_0$ that doesn't mention equality such that $T_0$ does not have a finite model.
Take $T$ as in one of the other answers.  Then let $T_0$ be the theory obtained by:


*

*replacing each $=$ by $\equiv$, a new symbol

*adding the sentences that says $\equiv$ is an equivalent relation and

*for each other symbol occurring in $T$ (there are finitely many of them), adding the sentence that says the symbol is compatible with (the equivalence relation) $\equiv$.


Suppose $T_0$ had a finite model $M$.  Then the quotient $M/\equiv^M$ of $M$ by the interpretation of $\equiv$ is a model of the original theory $T$.  But $M/\equiv^M$ is also finite, a contradiction.
