Half of Martin Goldstern and Haim Judah’s The Incompleteness Phenomenon: A New Course in Mathematical Logic (A.K. Peters, 1995: pp. 247) is a treatment of first-order logic. The rest of the book is two long chapters (as it happens, of just the same length), one on model theory, one mostly on incompleteness and with a little on recursive functions. So the emphasis on incompleteness in the title is somewhat misleading: the book is at least equally an introduction to some model theory. I have had this book recommended to me more than once, but I seem to be immune to its supposed charms (I too often don’t particularly like the way that it handles the technicalities): your mileage may vary.
Some details Ch. 1 starts by talking about inductive proofs in general, then gives a semantic account of sentential and then first-order logic, then offers a Hilbert-style axiomatic proof system. Very early on, the authors introduce the notion of M-terms and M-formulae. An M-term (where M is model for a given first-order language L) is built up from L-constants, L-variables and/or elements of the domain of M, using L-function-expressions; an M-formula is built up from M-terms in the predictable way. Any half-awake student is initially going to balk at this. Re-reading the set-theoretic definitions of expressions as tuples, she will then realize that the apparently unholy mix of bits of language and bits of some mathematical domain in an M-term is not actually incoherent. But she will right wonder what on earth is going on and why: our authors don’t pause to explain why we might want to do things like this at the very outset. (A good student who knows other presentations of the basics of first-order semantics should be able to work out after the event what is going on in the apparent trickery of Goldstern and Judah’s sort of story: but I really can’t recommend starting like this, without a good and expansive explanation of the point of the procedure.)
Ch. 2 gives a Henkin completeness proof for the first-order deductive system given in Ch. 1. This has nothing special to recommend it, as far as I can see: there are many more helpful expositions available. The final section of the chapter is on non-standard models of arithmetic: Boolos and Jeffrey (Ch. 17 in their third edition) do this more approachably.
Ch.3 is on model theory. There are three main sections, ‘Elementary substructures and chains’, ‘ultra products and compactness’, and ‘Types and countable models’. So this chapter – less than sixty pages – aims quite high to be talking e.g. about ultraproducts and about omitting types. You could indeed usefully read it after working through e.g. Manzano’s book: but I certainly don’t think this chapter makes for an accessible and illuminating first introduction to serious model theory.
Ch. 4 is on incompleteness, and the approach here is significantly more gentle than the previous chapter. Goldstern and Judah make things rather easier for themselves by adopting a version of Peano Arithmetic which has exponentiation built in (so they don’t need to tangle with Gödel’s β function). And they only prove a semantic version of Gödel’s first incompleteness theorem, assuming the soundness of PA. The proof here goes as by showing directly that – via Gödel coding – various syntactic properties and relations concerning PA are expressible in the language of arithmetic with exponentiation (in other words, they don’t argue that those properties and relations are primitive recursive and then show that PA can express all such properties/relations).
How well, how accessibly, is this done? The authors hack through eleven pages (pp. 207–217) of the arithmetization of syntax, but the motivational commentary is brisk and yet the proofs aren’t completely done (the authors still leave to the reader the task of e.g. coming up with a predicate satisfied by Gödel numbers for induction axioms). So this strikes the present reader as really being neither one thing nor another – neither a treatment with all the details nailed down, nor a helpfully discursive treatment with a lot of explanatory arm-waving. And in the end, the diagonalization trick seems to be just pulled like a rabbit out of the hat.
After proving incompleteness, they prove Tarksi’s theorem and the unaxiomatizability of the set of arithmetic truths.To repeat, the authors assume PA’s soundness. They don’t say anything about why we might want to prove the syntactic version of the first theorem, and don’t even mention the second theorem which we prove by formalizing the syntactic version. So this could well leave students a bit mystified when they come across other treatments. The book ends by noting that the relevant predicates in the arithmetization of syntax are Σ1, and then defines a set as being recursively enenumerable if it is expressible by a Σ1 predicates (so now talk of recursiveness etc. does get into the picture). But really, if you want to go down this route, this is surely all much better handled in Leary’s book.
Summary verdict The first two chapters of this book can’t really be recommended either for making a serious start on first-order logic or for revision. The third chapter could be used for a brisk revision of some model theory if you have already done some reading in this area. The final chapter about incompleteness (which the title of the book might lead you to think will be a high point) isn’t the most helpful introduction in this style – go for Leary (2000) instead – and on the other hand doesn’t go far enough for revision/consolidatory purposes.