Survey of finite axiomatizability for relational theories?

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.
• 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)
-
If instead of finite axiomatizability (presumably with respect to a theory in first order logic, although it would help to say so explicitly) you had mentioned finitely-based (which for me means in equational logic, or a finite set of identities, i.e. a conjunction of universallly quantified equations), I would point you to a wealth of examples, many of which can be found in general algebra texts, possibly even in Jezek's text to which you refer. Gerhard "Ask Me About Finitely Based" Paseman, 2012.10.25 – Gerhard Paseman Oct 25 '12 at 14:18
@Gerhard: An equational theory is axiomatizable by finitely many first-order sentences if and only if it is axiomatizable by finitely many identities, so there is no difference. – Emil Jeřábek Oct 25 '12 at 14:22
Also, while one result (Murskii, 1975) shows that in a certain sense most finite algebraic structures of finite type have finitely based equational theories, another (Murskii, 1967) gives a structure which is not finitely based, but which is finitely axiomatizable. Not quite your expressed cup of tea, but I can offer more. Gerhard "And Then There's Tarski's Problem" Paseman, 2012.10.25 – Gerhard Paseman Oct 25 '12 at 14:30
Emil, I beg to differ, giving Murskii's three element groupoid as my example. Gerhard "Water Pistols At Dawn, Sir" Paseman, 2012.10.25 – Gerhard Paseman Oct 25 '12 at 14:31
OK, let me summarize this. An equational theory is finitely based iff it is finitely axiomatizable. However, the equational theory and the first-order theory of a particular algebra (or a class of algebras) may be different, and in particular, one may be finitely axiomatizable while the other is not. – Emil Jeřábek Oct 25 '12 at 16:14

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 http://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.

-
I should probably stress that many theories are reflexive despite not having full induction, e.g., the primitive recursive arithmetic PRA. – Emil Jeřábek Oct 25 '12 at 15:05

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.

-

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$.

-