Avigad, MLC — 3: are domains sets?

The next two chapters of MLC are on the syntax and proof systems for FOL — in three flavours again, minimal, intuitionstic, and classical — and then on semantics and a smidgin of model theory. Again, things proceed at pace, and ideas come thick and fast.

One tiny stylistic improvement which could have helped the reader (ok, this reader) would have been to chunk up the sections into subsections — for example, by simply marking the start of a new subsection/new subtheme by leaving a blank line and beginning the next paragraph  “(a)”, “(b)”, etc. A number of times, I found myself re-reading the start of a new para to check whether it was supposed to flow on from the previous thought. Yes, yes, this is of course a minor thing! But readers of dense texts like this need all help we can get!

So in a bit more detail, how do Chapters 4 and 5 proceed? Broadly following the pattern of the two chapters on PL, in §4.1 we find a brisk presentation of FOL syntax (in the standard form, with no syntactic distinction made between variables-as-bound-by-quantifiers and variables-standing-freely). Officially, recall, wffs that result from relabelling bound variables are identified. But this seems to make little difference: I’m not sure what the gain is, at least here in these chapters, in a first encounter with FOL.

§4.2 presents axiomatic and ND proof systems for the quantifiers, adding to the systems for PL in the standard ways. §4.3 deals with identity/equality and says something about the “equational fragment” of FOL. §4.4 says more than usual about equational and quantifier-free subsystems of FOL, noting some (un)decidability results. §4.5 briefly touches on prenex normal form. §4.6 picks up the topic (dealt with in much more detail than usual) of translations between minimal, intuitionist, and classical logic. §4.7 is titled “Definite Descriptions” but isn’t as you might expect about how to add a description operator, a Russellian iota, but rather about how — when we can prove \forall x\exists! yA(x, y) — we can add a function symbol f such that f(x) = y holds when A(x, y), and all goes as we’d hope. Finally, §4.8 treats two topics: first, how to mock up sorted quantifiers in single-sorted FOL; and second, how to augment our logic to deal with partially defined terms. That last subsection is very brisk: if you are going to treat any varieties of free logic (and I’m all for that in a book at this level, with this breadth) there’s more worth saying.

Then, turning to semantics, §5.1 is the predictable story about full classical logic with identity,  with soundness and completeness theorems, all crisply done. §5.2 tells us more about equational and quantifier-free logics.  §5.3 extends Kripke semantics to deal with quantified intuitionistic logic. We then get algebraic semantics for classical and intuitionistic logic in §5.4 (so, as before, A is casting his net more widely than usual — though the treatment of the intuitionistic case is indeed pretty compressed). The chapter finishes with a fast-moving 10 pages giving us two sections on model theory. §5.5 deals with some (un)definability results, and talks briefly about non-standard models of true arithmetic. §5.6 gives us the L-S theorems and some results about axiomatizability. So that’s a great deal packed into this chapter. And at a sophisticated level too — it is perhaps rather telling that A’s note at the end of the chapter gives Peter Johnstone’s book on Stone Spaces as a “good reference” for one of the constructions!


What more is there to say? I’m enjoying polishing off some patches of rust! — but as is probably already clear, these initial chapters are pitched at what many student readers will surely find a pretty demanding level, unless they bring quite a bit to the party. That’s not a criticism (except perhaps of Avigad’s initial advertising pitch, saying that this book will be accessible to advanced undergraduates without actually requiring a logical background): I‘m just locating the book on the spectrum of texts. I’d have slowed down the exposition a bit at a number of points, but that (as I said in the last post) is a judgement call, and it would be unexciting to go into details here.

One general comment, though. I note that A does define a model for a FOL language as having a set for quantifiers to range over,  but with a function (of the right arity) over that set as interpretation for each function symbol, and a relation (of the right arity) over that set as interpretation for each relation symbol. My attention might have flickered, but A seems happy to treat functions and relations as they come, not explicitly trading them in for set-theoretic surrogates (sets of ordered tuples). But then it is interesting to ask — if we treat functions and relations as they come, without going in for a set-theoretic story, then why not treat the quantifiers as they come, as running over some objects plural? That way we can interpret e.g. the first-order language of set theory (whose quantifiers run over more than set-many objects) without wriggling.

A does nicely downplay the unnecessary invocation of sets — though not consistently. E.g. he later falls into saying “the set of primitive recursive functions is the set of functions [defined thus and so]” when he could equally well have said, simply,  “the primitive recursive functions are the functions [defined thus and so]”. I’d go for consistently avoiding unnecessary set talk from the off — thus making it much easier for the beginner at serious logic to see when set theory starts doing some real work for us. Three cheers for sets: but in their proper place!

Leave a Comment

Your email address will not be published. Required fields are marked *

Scroll to Top