Chapter 4 of Mileti’s MML is on “First-order logic: languages and structures” — so some 40 pages on basic semantics. Chapter 5 is on “Relationships between structures” — another longish chapter, 35 pages on substructures, homomorphisms between structures, embeddings, and the like. Chapter 6 , “Implications and compactness”, is an even longer chapter — some 48 pages introducing a proof system for FOL and proving soundness and completeness, then drawing out some consequences of compactness, before going on to talk about theories framed in a first-order language, with a substantial final section on random graphs. I can’t say that I have carefully read every word, but that hasn’t stopped me forming pretty firm opinions.
In headline terms: I found the basic treatment of the semantics, and again of the formal proof-system and completeness, pretty unattractive. Not to put too fine a point on it, I would have thought that a typical student would find some of the episodes here rather rebarbative. On the other hand, the more model-theoretic Chapter 5, and the second half of Chapter 6 strike me as notably more readable.
In just a bit more detail, we get a highly conventional story about the syntax of FOL languages. In particular, the same symbols are recruited for double duty, as part of the construction of a quantifier operator, and for use as parameters/temporary names — in other words “
” has to serve, in different contexts, as both a bound and a free variable. Of course, this means we have to fuss about rules for distinguishing free from bound occurrences of variables, and fuss at length about avoiding unwanted variable capture when substituting terms for variables (MML‘s §4.4 on substitution is no less than eleven rather dense pages long). Why do things this old-fashioned way? It’s only ninety years since Gentzen taught us how to do better, in ways that have become more and more familiar as modern proof-theorists spread the word!
In the middle of Chapter 4, though, there is a nice short first section on definability. Issues of definability and related topics about what classes of structures can be captured by which languages, and so on, are then taken up in the next chapter — which ends with a nice section §5.5 which introduces the Tarski-Vaught test and shows how to get from there to a version of the downward L-S theorem for a countable language. §4.3 and Chapter 5 could I think be tackled standalone by someone who knows some basic FOL from other sources; and these sections do work pretty well.
After a section defining semantic entailment for FOL, Chapter 6 introduces a deductive system for quantificational logic, far too briskly (it seems to me) to be of much use to anyone who is encountering one for the first time. And the soundness and completeness results are done no more attractively than for the earlier propositional logic case. I can’t recommend these sections at all. But then §6.4 on applications of compactness and §6.5 on theories are nice (and the concluding section on random graphs is an interesting bonus).
A pretty mixed verdict on these three chapters, then.