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)
Best Answer
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.