[FOM] Finite axiomatisation

[Thomas Forster]

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:

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