Kleene: Introduction to Metamathematics
First published seventy years ago, Stephen Cole Kleene’s Introduction to Metamathematics (North-Holland, 1952; reprinted Ishi Press 2009: pp. 550) for a while held the field as a survey treatment of first-order logic (without going much past the completeness theorem) and as a more in-depth treatment of the theory of computable functions and Gödel’s incompleteness theorems. In a 1991 note about writing the book, Kleene notes that up to 1985, about 17,500 copies of the English version of his text were sold, as were thousands of various translations (including a sold-out first print run of 8000 of the Russian translation). So this is a book with a quite pivotal influence on the education of later logicians, and on their understanding of the fundamentals of recursive function theory and the incompleteness theorems in particular.
But it isn’t just nostalgia that makes old hands continue to recommend it. Kleene’s book remains particularly lucid and accessible: it is often discursive, pausing to explain the motivation behind formal ideas. It is indeed still a pleasure to read (or at least, it ought to be a pleasure for anyone interested enough in logic to be reading these pages). And if you have read some modern texts, then modulo relatively superficial presentational matters, you’ll probably be struck by a sense of familiarity when reading through, as aspects of his discussions evidently shape many later textbooks (not least, IGT). The Introduction to Metamathematics remains a really impressive achievement: and not one to be admired only from afar, either.
Some details Chs. 1–3 are introductory. There’s a little about enumerability and countability (Cantor’s Theorem); then a chapter on natural numbers, induction, and the axiomatic method; then a little tour of the paradoxes and some possible responses to them.
Chs. 4–7 are a gentle introduction to the propositional and predicate calculus and a formal system which is in fact first-order Peano Arithmetic (you need to be aware that the identity rules are treated as part of the arithmetic, not the logic). Although Kleene’s official proof-system is Hilbert-style, he shows that ‘natural deduction’ introduction and elimination rules can be thought of as derived rules in his system, so it all quickly becomes reasonably user-friendly. (He doesn’t at this point prove the completeness theorem for his predicate logic: as I said, things go quite gently at the outset!)
Ch. 8 starts work on ‘Formal number theory’, showing that his formal arithmetic has nice properties, and then defines what it is for a formal predicate to capture (‘numeralwise represent’) a numerical relation. Kleene then proves Gödel’s incompleteness theorem, assuming a Lemma – eventually to be proved in his Chapter 10 – about the capturability of the relation ‘m numbers a proof [in Kleene’s system] of the sentence with number n’.
Ch. 9 gives an extended treatment of primitive recursive functions, and then Ch. 10 deals with the arithmetization of syntax, yielding the previously stated Lemma needed for the incompleteness theorem.
Chs. 11-13 then give a nice treatment of general (total) recursive functions, partial recursive functions, and Turing computability. This is all very attractively done.
The last two chapters, forming the last quarter of the book, go under the heading ‘Additional Topics’. In Ch. 14, after proving the completeness theorem for the predicate calculus without and then with identity, Kleene discusses the decision problem. And the final Ch. 15 discusses Gentzen systems, the normal form theorem, intuitionistic systems and Gentzen’s consistency proof for arithmetic.
Summary verdict This book can still be warmly recommended as an enjoyable and illuminating presentation of fundamental material, written by someone who was himself so closely engaged in the early developments back in the glory days. It should be entirely accessible if you have managed e.g. Chiswell and Hodges and then my Gödel book, and will enrich and broaden your understanding.