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)?
Best Answer
Noah and Brian have given one of the canonical examples of a finitely axiomatizable theory with no finite model (their examples are essentially the same). I'll give the other - it shows that this behavior is possible even in a relational language without definable functions, so thinking about constant symbols and terms is a red herring (unless you think about Skolemization, as Noah says).
Let $L$ be the language consisting of a single binary relation symbol $\leq$, and let $T$ be the theory asserting that $\leq$ is a non-empty linear order with no greatest element. That is, $T$ contains the three linear order axioms, together with the sentences $\forall x\, \exists y\, (x\leq y\land \lnot (x = y))$ and $\exists x\, x = x$ (to rule out the empty structure, if your semantics for first-order logic allows it).
So it's not true that every finitely axiomatizable theory has a finite model. In fact, the problem of determining whether a given theory has a finite model is undecidable in general. This is known as Trakhtenbrot's theorem.
Time for a tangent: If your guess were correct, and every finitely axiomatizable first-order theory had a finite model, then in fact the decision problem for first-order logic would be decidable. That is, one could write a computer program that takes as input a first-order sentence $\varphi$ and outputs "yes" or "no" according to whether $\varphi$ has a model. This program would start enumerating the finite $L$-structures and checking whether they are models of $\varphi$, while simultaneously searching for proofs of $\lnot \varphi$. If $\varphi$ has no model, a proof of $\lnot\varphi$ will eventually be found (by the completeness theorem), while if $\varphi$ has a model, a finite model will eventually be found.
Of course, the decision problem for first-order logic is well-known to be undecidable. But there are classes of first-order sentences (e.g. in a relational language the universal sentences $\forall \overline{x}\, \varphi(\overline{x})$ with $\varphi$ quantifier-free) which do have the finite model property (if they have a model, then they have a finite model) and hence these classes are decidable by the argument above.