Survey of finite axiomatizability for relational theories?

Question

An $L$-theory $T$ is finitely axiomatizable if there is a finite set $A$ of $L$-sentences with the same consequences as $T$, i.e. such that $M \models T$ iff $M \models A$ for every $L$-structure $M$. (Here $L$ is a first-order language, and I am mostly interested in languages with relational symbols and no function symbols.)

Is there a survey of ways to show that finite axiomatizability holds or does not hold?

The obvious way to establish that a theory is finitely axiomatizable is by (1) constructing a finite set of $L$-sentences $A$ and (2) proving that $A$ is a set of axioms for $T$. For finite axiomatizability, I am especially interested in any results that may help when it is difficult to establish part (2), even when given a likely candidate set of axioms $A$.

For theories that are not finitely axiomatizable, I am thinking of results such as a theorem of Cherlin, Harrington and Lachlan, which is summarized by Theorem 12.2.18(a) in Hodges' Model Theory as:

If $T$ is $\omega$-stable and $\omega$-categorical, then $T$ is not finitely axiomatizable.

or a basic result such as Theorem 5.9.2 in Jezek's Universal Algebra:

A class $K$ of $L$-structures is finitely axiomatizable iff both $K$ and the complement of $K$ in the class of all $L$-structures are axiomatizable.

Finite axiomatizability is a rather natural notion, so it seems unlikely to me that there is no good source of results that can be used as tools to establish or deny it. So I am probably either missing some classic result (perhaps relating finite axiomatizability to recursive axiomatizability a la results of Kleene or Craig and Vaught for finite axiomatizability using additional predicates), or am not aware of one of the multitude of classic texts which exist but are difficult to locate via online searches. Any pointers would therefore be welcome!

Edit: I am slightly aware of the work in universal algebra that relates a finite basis of equations to properties of the lattice of congruences of the variety. A nice survey along these lines is by Maróti and McKenzie. However, my main interest is relational languages (and arbitrary axioms). This is in contrast to (usually functional) languages with equational (or quasi-equational) bases, which are sets of universal Horn sentences.

• Cherlin, G., Harrington, L., and Lachlan, A. H. $\aleph_0$-categorical, $\aleph_0$-stable structures, Annals of Pure and Applied Logic 28(2), 1985, 103–135. doi:10.1016/0168-0072(85)90023-5
• Hodges, W. Model Theory. Cambridge University Press, 1993.
• Ježek, J. Universal Algebra (First edition, April 2008). (PDF version)
• Maróti, M. and McKenzie, R. Finite Basis Problems and Results for Quasivarieties, Studia Logica 78, 2004, 293–320. doi:10.1007/s11225-005-3320-5 (reprint from author)

Answer 1

Going in the opposite direction than stable theories, you can use Gödel’s theorems to prove finite nonaxiomatibility:

Theorem: If $T$ is a consistent complete theory interpreting Robinson’s arithmetic $\mathrm Q$, then $T$ is not finitely axiomatizable.

(In fact, not even recursively axiomatizable.)

Theorem: If $T$ is a consistent reflexive theory, then $T$ is not finitely axiomatizable.

Here, a theory is reflexive if there is a fixed interpretation $I$ of $\mathrm Q$ in $T$ such that $T$ proves $\mathrm{Con}_S^I$ for every finitely axiomatized subtheory $S$ of $T$.

A useful criterion, mentioned in https://mathoverflow.net/questions/87249, is

Theorem: Any sequential theory proving the induction schema for all formulas in its language is reflexive (hence not finitely axiomatizable unless inconsistent).

(A theory is sequential if it can define a coding of finite sequences of its objects, loosely speaking.) In particular, all consistent extensions (in the same language) of Peano arithmetic or of set theories like ZF are non-finitely axiomatizable.

Answer 2

The proof of non-finite axiomatizability of $\omega$-stable, $\omega$-categorical theories is one of the earliest results of geometric stability theory, and is based on the structure theory of definable sets in such theories (they turn out to posses a property called "1-basedness" that gives certain control over the definable sets). Also, by $\omega$-categoricity there are only finitely many formulas in $n$ variables for each $n$, up to equivalence. You can find an account of the proof in Pillay's book "Geometric stability theory", Chapter 2.

There is also an important result by Zilber that $\omega$-stable, $\omega$-categorical theories are finitely axiomatizable modulo an axiom scheme saying that there are infinitely many elements ("quasi-finite axiomatizability"). This is covered in Chapter 3 of Pillay's book.

Answer 3

Another method, which can be used with theories such as ZFC and PA, is that these theories are not finitely axiomatizable because they prove the consistency of their own restrictions to any fixed level of complexity. For example, the reflection theorem shows that ZFC proves of any finite part of it that it holds in some rank initial segment of the universe $V_\kappa$. It follows by the completeness theorem that ZFC, if consistent, cannot be proved finitely axiomatizable. A similar theorem applies to the case of PA, which proves the consistency of its restriction to the $\Sigma_n$ induction scheme, for any fixed $n$.