Finite structures are not first-order axiomatizable (source code)

= Finite structures are not first-order axiomatizable

If a first-order theory had exactly the finite structures in a class containing arbitrarily large members, adjoin constants $c_1,c_2,\ldots$ and require them to be pairwise distinct. Every finite fragment has a sufficiently large finite model, while <compactness theorem>[compactness] produces an infinite model, a contradiction. In particular, finite groups are not first-order axiomatizable.