Avigad, MLC — 2: And what is PL all about?

After the chapter of preliminaries, there are two chapters on propositional logic (substantial chapters too, some fifty-five large format pages between them, and they range much more widely than the usual sort of introductions to PL in math logic books).

The general approach of MLC foregrounds syntax and proof theory. So these two chapters start with §2.1 quickly reviewing the syntax of the language of PL (with \land, \lor, \to, \bot as basic — so negation has to be defined by treating \neg A as A \to \bot). §2.2 presents a Hilbert-style axiomatic deductive system for minimal logic, which is augmented to give systems for intuitionist and classical PL. §2.3 says more about the provability relations for the three logics (initially defined in terms of the existence of a derivation in the relevant Hilbert-style system). §2.4 then introduces natural deduction systems for the same three logics, and outlines proofs that we can redefine the same provability relations as before in terms of the availability of natural deductions. §2.5 notes some validities in the three logics and §2.6 is on normal forms in classical logic. §2.7 then considers translations between logics, e.g. the Gödel-Gentzen double-negation translation between intuitionist and classical logic. Finally §2.8  takes a very brisk look at other sorts of deductive system, and issues about decision procedures.

As you’d expect, this is all technically just fine. Now, A says in his Preface that “readers who have had a prior introduction to logic will be able to navigate the material here more quickly and comfortably”. But I suspect this rather misleads: in fact some prior knowledge will be pretty essential if you are really going get much out the discussions here. To be sure, the point of the exercise isn’t (for example) to get the reader to be a whizz at knocking off complex Gentzen-style natural deduction proofs; but are there quite enough worked examples for the real newbie to get a good feel for the claimed naturalness of such proofs? Is a single illustration of a Fitch-style alternative helpful? I’m doubtful. And so on.

To continue, Chapter 3 is on semantics. We get the standard two-valued semantics for classical PL, along with soundness and completeness proofs, in §3.1. Then we get interpretations in Boolean algebras in §3.2. Next, §3.3 introduces Kripke semantics for intuitionistic (and minimal) logic — as I said, A is indeed casting his net significantly more widely that usual in introducing PL. §3.4 gives algebraic and topological interpretations for intuitionistic logic. And the chapter ends with §3.5, ‘Variations’, introducing what A calls generalised Beth semantics.

Again I really do wonder about the compression and speed of some of the episodes in this chapter; certainly, those new to logic could find them very hard going. Filters and ultrafilters in Boolean algebras are dealt with at speed; some more examples of Kripke semantics at work might have helped to fix ideas; Heyting semantics is again dealt with at speed. And §3.5 will (surely?) be found challenging.

Still, I think that for someone coming to MLC who already does have enough logical background (perhaps half-baked, perhaps rather fragmentary) and who is mathematically adept enough, these chapters — perhaps initially minus their last sections — should bring a range of technical material into a nicely organised story in a very helpful way, giving a good basis for pressing on through the book.


For me, the interest here in the early chapters of MLC is in thinking through what I might do differently and why. As just implied, without going into more detail here, I’d have gone rather more slowly at quite a few points (OK, you might think too slowly — these things are of course a judgment call). But perhaps as importantly, I’d have wanted to add some more explanatory/motivational chat.

For example, what’s so great about minimal logic? Why talk about it at all? We are told that minimal logic “has a slightly better computational interpretation” than intuitionistic logic. But so what? On the face of it doesn’t treat negation well, its Kripke semantics doesn’t take the absurdity constant seriously, and lacking disjunctive syllogism minimal logic isn’t a sane candidate for regimenting mathematical reasoning (platonistic or constructive). And if your beef with intuitionist logic are relevantist worries about its explosive character, then minimal logic is hardly any better (since from a contradiction, we can derive any and every negated wff).  So — a reader coming with a bit of logical background might reasonably wonder — why seriously bother with it? It would be worth saying something.

Another, even more basic, example. We are introduced to the language of propositional logic (with a fixed infinite supply of propositional letters). Glancing ahead, in Chapter 4 we meet a multiplicity of first-order languages (with their various proprietary and typically finite supplies of constants and/or relation symbols and/or function symbols). Why the asymmetry? Connectedly but more basically, what actually are the propositional variables doing in a propositional language? Different elementary textbooks say different things, so A can’t assume that everyone is approaching the discussions here with the same background of understanding of what PL is all about. He cheerfully says that the propositional variables “stand for” propositions. Which isn’t very helpful given that neither “stand for” nor “proposition” is at all clear!

Now, of course, you can get on with the technicalities of PL (and FOL) while blissfully ignoring the question of what exactly the point of it all is, what exactly the relation is between the technical games being played and the real modes of mathematical argumentation you are, let’s hope, intending to throw light on when doing mathematical logic. But I still think that an author should fess up about  their understanding of these rather contentious issues, as such an understanding which must shape their overall approach. Avigad notes in his Preface that we can use formal systems to understand patterns of mathematical inference  (though he then oddly says that “the role of a proof system” for PL “is to derive tautologies”, when you would expect something like “is to establish tautological entailments”); and perhaps more will come out as the book progresses about how he conceives of this use. But for myself, I’d have liked to have seen rather more upfront.

Leave a Comment

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

Scroll to Top