# What Sorts of People Should There Be?

From my colleague up north, Rob Wilson:

The What Sorts of People blog is now up and running: check it out. This is the blog for the What Sorts of People Should There Be? network, a collaborative blog with regular contributions from around 10 team members. Short, recent posts are available on double-amputee Oscar Pistorius’s bid to compete Olympically, and on a so-recent-it’s-still-forthcoming piece by Steve Pinker in The New Republic on the concept of dignity and its use in a recent President’s Council on Bioethics report. Biella Coleman, who was a Killam Postdoc at Alberta last year and now teaches at NYU, has just posted a tempered rant on the blog on medical genetics and eugenics.

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

*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.”