[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:
>
> 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.
More information about the FOM
mailing list