Following on from the very interesting Chapter 6 on cut-elimination, there’s one further chapter on FOL, Chapter 7 on “Properties of First-Order Logic”. There are sections on Herbrand’s Theorem, on the Disjunction Property for intuitionistic logic, on the Interpolation Lemma, on Indefinite Descriptions and on Skolemization. This nicely follows on from the previous chapter, as the proofs here mostly rely on the availability of cut-elimination. I’m not going to dwell on this chapter, though, which I think most readers will find quite hard going. Hard going in part because, apart from perhaps the interpolation lemma, it won’t this time be obvious from the off what the point of various theorems are.
Take for example the section on Skolemization. This goes at pace. And the only comment we get about why this might all matter is at the end of the section, where we read:
The reduction of classical first-order logic to quantifier-free logic with Skolem functions is also mathematically and philosophically interesting. Hilbert viewed such functions (more precisely, epsilon terms, which are closely related) as representing the ideal elements that are added to finitistic reasoning to allow reasoning over infinite domains.
So that’s just one sentence expounding on the wider interest — which is hardly likely to be transparent to most readers! It would have been good to hear more.
Avigad’s sections in this chapter are of course technically just fine and crisply done, and can certainly be used as a good source to consolidate and develop your grip on their cluster of topics if you already have met the key ideas. But to be honest I wouldn’t recommend starting here.
OK: The chapters to this point take us some 190 pages into MLC — they form, if you like, a book within the book, on core FOL topics but with an unusually and distinctively proof-theoretic flavour. So this is well worth having. But to repeat what I’ve said more than once before, I suspect that a reader who is going to happily navigate and appreciate the treatments of topics here will typically need rather more background in logic than Avigad implies.
So when I get round to revising the Beginning Mathematical Logic Study Guide, these opening chapters will find their place in the suggested more advanced supplementary readings.