Arbitrary large finite models imply an infinite model - any interesting consequences? A simple application of the Compactness theorem shows that for any first order theory $T$, if it has aribtrarily large finite models, then it also has an infinite model.
This is an interesting result, even surprising, one might say. However, I couldn't come up with any interesting examples for $T$ for which this result is not trivial. For the theory of groups, or of fields, or graphs - it's very easy to construct an infinite model. So, Are there any interesting consequences from this result?
 A: I mostly see this result used in the contrapositive: if you have a class of objects for which there are arbitrarily large finite objects but no infinite object, then your class of objects is not the class of models of a first-order theory. For example, there is no first-order theory whose models are exactly the finite groups, etc.
In turn, I mostly see this result used as follows: suppose you have some theory $T_1$ whose models are some objects you're interested in (groups, etc.) and you want to know whether some property of these objects is finitely axiomatizable by a finite set of axioms $T_2$. You can rule this out by considering the single sentence consisting of the conjunction of the negation of every sentence in $T_2$, which together with $T_1$ gives the objects not satisfying your your property. If there are arbitrarily large finite objects but no infinite object not satisfying your property, then $T_2$ can't exist.
Unfortunately the examples I can think of of this situation usually involve using more of the strength of the compactness theorem. For example, you can show that for fields, having characteristic $0$ is not finitely axiomatizable, because the negation of this condition (having positive characteristic) does not satisfy the compactness theorem: if you add sentences equivalent to "the characteristic is not $2$, not $3$, not $5$," etc. then every finite subset of those has a model (a field of larger positive characteristic) but the entire set of sentences can't have a model (within fields of positive characteristic).
A: Is there a group on which the maps
$x \mapsto x^2, x \mapsto x^3, x \mapsto x^4, \dots$
are injective precisely if they are surjective? For example, $\mathbb{Z}$ is not such a group, since the map $x \mapsto x + x$ is injective, but not surjective.
You can use your knowledge of group theory to construct such a group explicitly (easy to think of Abelian examples, so let's make it non-Abelian), or you can appeal to compactness. Consider the first-order theory over the language of group theory that has the axioms of group theory (again, you can make it non-Abelian), along with axioms asserting that each of the functions above is injective precisely if it is surjective.
On a finite set, every function is injective precisely if it is surjective, so every finite group (every finite non-Abelian group) is a model of this theory. Therefore, there must be an infinite group that is a model of this theory as well.
One can, of course, immediately start asking less trivial questions along the same lines (until directly constructing the groups gets difficult enough): this eventually leads to the theory of pseudofinite structures, structures that satisfy all sentences that every finite structure of the same kind satisfies (if you thought of $(\mathbb{Q},+)$ in the Abelian case: that is actually a pesudofinite group, but proving that is much harder).
