Consider the theory $\text{Th}(\mathbb{N}, 0, S)$, with $S$ being the successor function. In his book A Course in Model Theory, Poizat claims (p. 109) that this theory is not finitely axiomatizable. Intuitively, this is because we need to employ an axiom schema such that, for each $n$, there is an axiom saying that there is no cycle of length $n$ (i.e., $S^n(x) \neq x$, where $S^n(x)$ denotes the application of $S$ to $x$ $n$ times). That is fine as far as it goes, but how would one prove that this theory is not finitely axiomatizable? I mean, it is clear that no finite subset of this axiomatization will do, but perhaps there could be some other finite axiom set which would work. How do we rule that out?
The only proofs of non-finite-axiomatizability I am acquainted with are for PA and ZF, and they employ reflection schemas. What is the alternative here?
Best Answer
This is a great example of the power of compactness!
Since first-order logic is compact, it's enough to show that no finite sub-axiomatization of the standard axiomatization given in your earlier question will do the job (see e.g. here). And this is something we can do concretely: letting $\mathcal{M}_n$ be the successor structure consisting of a copy of $\mathbb{N}$ as usual and then a separate $n$-cycle, you can quickly check that each $\mathcal{M}_n$ satisfies the first $n$-many axioms of the theory, but no $\mathcal{M}_n$ satisfies the whole theory.
Note meanwhile that nothing like this can be super useful for $\mathsf{PA}$ or $\mathsf{ZFC}$, each of which have finitely axiomatized subtheories with no "simply-describable" models. And of course the whole idea would break down if we were working in a non-compact logic - showing that a given second-order theory, for example, is not finitely axiomatizable is usually extremely hard since we can't simplify things by focusing on a single well-understood family of candidate finite axiomatizations.