University of Calgary
UofC Navigation

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

LogBlog Has Moved!

You are looking at the old blog archive. LogBlog has moved to
If you'd like to receive updates on new posts, please subscribe there!

Submitted by Richard Zach on Wed, 05/14/2008 - 8:09am

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.

*According to Google Scholar, Kleene's monograph is cited a lot, but as far as I can tell overwhelmingly for the other paper, which is another classic logic paper: "Permutation of inferences in Gentzen’s calculi LK and LJ."