# [FOM] Finite axiomatisation

Thomas Forster T.Forster at dpmms.cam.ac.uk
Mon Aug 18 18:51:27 EDT 2008

```
Thanks to all who replied.  I shall go and chase up the references so
kindly supplied.   I am wondering if there isn't perhaps a different,
less semantic proof.  After all, why would one expect a theory with an
r.e. axiomatisation to be somehow equivalent to a finitely axiomatisable
one?  If T has an r.e. axiomatisation, there is a finite engine that emits
axioms of T.  Is there a mathematically robust way of recovering a finite
set of axioms from the finite engine?  The kind of thing i have in mind is
a proof due i think to Bill Craig (I have no idea where i learned it) that
if T has a r.e. axiomatisation then it has a recursive axiomatisation.
The proof is purely syntactic.  I was wondering whether, if one works
the same technique a little harder, one can prove the stronger result.

On Mon, 18 Aug 2008, Alasdair Urquhart wrote:

>
>
> > 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.
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>

--
URL:  www.dpmms.cam.ac.uk/~tf;
DPMMS ph: +44-1223-337981;
mobile in UK +44-7887-701-562;
mobile in US: +1-412-818-1316;
mobile in NZ +64-210580093.

```