Towards the end of last year, within a week or two of publishing Jeremy Avigad’s Mathematical Logic and Computation (a bumpy ride, but very well worth having), CUP also released another textbook, Joseph Mileti’s Modern Mathematical Logic. I’d earlier seen a substantial set of notes that Mileti had posted online, and (to be frank) wasn’t over-impressed; so I haven’t been rushing to read this. But I thought I would now take a look at the book version, with a view to seeing whether there are any chapters which I’d want to mention or even recommend in the next iteration of the Beginning Mathematical Logic Study Guide.
Level and coverage? MML is announced as aimed at advanced undergraduates or beginning graduates (by US standards, anyway), though the book is distinctly less ambitious than Avigad’s. Mileti says he assumes familiarity with some basic abstract algebra; however, this seems perhaps more needed to best appreciate some illustrative examples rather than as necessary background for grasping core content. The coverage is broadly conventional, starting with basic first-order logic (though with the opposite emphasis to Avigad: there’s no real proof theory). Then there’s a little model theory, entry-level axiomatic set theory, some computability theory, and a treatment of incompleteness. At this point, then, at least just glancing at the table of contents and diving into the first chapters, I’m not at all sure quite what makes this a book on especially modern mathematical logic in either topics or general approach.
I rather liked the tone of the short Introduction; and going through the next couple of chapters, there is friendly signposting and some nice turns of phrase. But …
But Chapter 2, the first substantial chapter, is thirty pages on ‘Induction and Recursion’. We get a pretty dense treatment of what Mileti calls “generating systems”, three different ways of defining the set of generated whatnots, proofs that these definitions come to the same, then a criterion for free generating systems, a proof we can do recursive definitions over the free systems, and so on. This is all done in what strikes me as a rather heavy-handed way which could be pretty off-putting as a way of starting out. Many students, I would have thought, will just feel they have been made to labour unnecessarily hard at this point for small returns. And when the very general apparatus is applied e.g. in the next chapter to prove, e.g., unique parsing results, I don’t think that what we get is more illuminating than a more local argument. (I suppose my pedagogic inclination in such cases is to motivate a general proof idea by proving an interesting local case first and then, at an appropriate point later, saying “Hey, we can generalize …”.) I note, by the way, that by the end of §2.2 the reader is already supposed to know about countable sets and accept without demur that a countable union of countable sets is countable.
Chapter 3, the next fifty pages, is on propositional logic. A minor complaint is that the arrow connective is initially introduce in the preface as meaning “implies” (oh dear), and then we get not a word of discussion of the truth-functional treatment of the connective unless my attention flickered. But my main beef here is on the chosen formal proof system. This is advertised as natural deduction, but it is a sequent system, where on the left of sequents we get sequences rather than sets (why?). And although the rules are set out in a way that would naturally invite tree-shaped proofs, they are actually applied to produce linear proofs (why?). Moreover, the chosen rule-set is not happily motivated. We have disjunctive syllogism rather than a proper vE rule; double negation elimination is called ¬E; removing double negation elimination doesn’t give intuitionistic logic. OK Mileti isn’t going to be interested in proof theory; but he should at least have chosen a modern(!) proof system with proof-theoretic virtues!
As for completeness, we get the sort of proof that (a) involves building up a maximal consistent set starting from some given wffs by going along looking at every possible wff in turn to see if it can next be chucked into our growing collection while maintaining consistency, rather than the sort of proof that (b) chucks in simpler truth-makers only as needed, Hintikka style. We are not told what might make the Henkin strategy better than the more economical Hintikka one.
To finish on a positive note, perhaps the best/most interesting thing in this chapter is the final section (and the accompanying exercises) on compactness for propositional logic, which gives a nice range of applications.
To be continued