[FOM] finite axiomatisation

[Richard Zach]

It was Kleene. From a post I wrote a while ago at
http://www.ucalgary.ca/~rzach/logblog/2008/05/finite-axiomatizability-of-theories-in.html

Wednesday, May 14, 2008
Finite Axiomatizability of Theories in the Predicate Calculus Using
Additional Predicate Symbols (Classic Logic Papers, Pt. 4) 

You probably all know the result that Peano Arithmetic is not finitely
axiomatizable (a result due to Ryll-Nardzewski), and a similar result
for ZFC (due to Richard Montague, I believe). The standard axiom system
for PA is not finite since the axiom scheme of induction stands for
infinitely many sentences. Ryll-Nardzewski showed that there is no
finite set S of sentences in the language of PA so that S ⊢ φ iff PA ⊢
φ. I don't know how widely known this is,* but by contrast it is
possible to finitely axiomatize (almost) any theory T, if you allow new
predicate symbols in the axiomatization. This is a result due to Kleene:
        Stephen Cole Kleene, Finite axiomatizability of theories in the
        predicate calculus using additional predicate symbols, in: Two
        Papers on the Predicate Calculus. Memoirs of the American
        Mathematical Society, no. 10, Providence, 1952, 27-68.
The "almost" above, as you might have guessed, applies to the theory
itself: it has to be recursively enumerable and, if the language
includes identity, must have only infinite models (Kleene's original
paper does not deal with identity). The basic idea is that you use the
new predicate symbols to finitely axiomatize a weak arithmetic in which
you can formalize semantics and do primitive recursion. The first part
gives you a truth predicate for the language of T, the second part gives
you a predicate that's satisfied of exactly the Gödel numbers of
sentences of T. Then you say that all the axioms of the (r.e.) theory T
are true. Kleene's result was later strengthened by Craig and Vaught in:
        William Craig and Robert L. Vaught, Finite axiomatizability
        using additional predicates. The Journal of Symbolic Logic 23
        (1958) 289-308.
A sketch of Craig and Vaught's proof is given in Michael Makkai's
review.


On Mon, 2008-08-18 at 03:29 +0100, Thomas Forster 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.
> 
>     Thomas Forster
> 
> 
> 
> 
> 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.
> 
> 
> 
> 
> 
> 
>