[FOM] Finite axiomatisation

[Alasdair Urquhart]

Thomas Forster asked:

> Can anyone on this list state - and cite! - a theorem to the effect that
> to any recursively axiomatisable theory $T$ in a language $L$ there is a
> finitely axiomatisable theory $T'$ in a suitable language $L'$ with $T'$
> equivalent to $T'$ in some very strong sense.   Somebody must have proved
> a rigorous version of this, and I am hoping that listmembers will know
> who and how.

The basic references here are S.C. Kleene, Finite Axiomatizability of
theories in the predicate calculus using additional predicate symbols,
Memoirs of the AMS, No. 10, and Craig and Vaught, Finite axiomatizability
using additional predicates, JSL, Volume 23, pp. 289-308.

There is a very clear review of both papers by Makkai in the JSL,
Volume 36 (1971), pp. 334-335 that also provides a sketch of the proof.
Kleene's main result is:

 	If T is a recursively axiomatizable theory that has only infinite
 	models, then it has a finitely axiomatized conservative extension.

The fundamental idea of the proof is to formalize the inductive
clauses of the truth definition for T.