I thought it would be a doddle to update the chapter on modal logic for the Study Guide. But — needless to say! — it hasn’t quite worked out that way.

Now, propositional modal logics have long been of considerable interest to philosophers reflecting on notions of necessity, or when thinking about the logic of tensed discourse and the like. And first-order and higher-order quantified modal logics are of current interest to philosophers dabbling in modal metaphysics (no don’t! — that way madness lies …). Propositional modal logics are also of interest to mathematicians and computer scientists theorizing about relational structures. But none of *these* topics need be of much concern to those beginning mathematical logic. Apart from the link between modal S4 and Intuitionistic logic, the one bit of modal logic that is of real core interest to mainstream mathematical logic is (surely) provability logic, with its closest of connections to issues about Gödelian incompleteness etc.

So that’s the thought which is now going to structure the coverage of modal logic in the *Beginning Mathematica Logic *guide. I’ll introduce a modicum a modal logic at an introductory level: then let’s move on to the fun stuff about provability logics.

But what to recommend by way of accessible introductory reading on provability logic? I’ve found myself revisiting the classics by Smoryński and Boolos, and then reading a variety of Handbook articles, as well as some other pieces. Which has been fun — and instructive, as I’d forgotten an embarrassing amount. Rather to my surprise, however, I found Boolos’s *The Logic of Provability *rather less easy going than I’d remembered it; so I’m left a bit uncertain what to recommend as the most approachable path into the subject. Perhaps half of Smoryński’s book …

(An aside: Smoryński’s 1985 book seemingly reproduces pages produced by an electric typewriter. Boolos’s 1993 book is more conventionally typeset, but it’s done in such a cluttered way as to be often very unfriendly to the eye. We are so used now to seeing decently LaTeXed maths books that ploughing through less well-produced texts like these can be enough of a chore to get in the way of processing the content.)

Anyway, here for fun is a result proved by Beklemishev that I’ve been reminded of, that he got by a proof using an extension of provability logic.

Call finite strings in the alphabet of e.g. ordinary decimal arithmetic *worms*. So the worm is a string of digits . And we will define to be the result of decreasing ‘s last digit by 1 if you can, or deleting that digit if it is already 0.

And now consider a *sequence* of worms constructed according to the following two rules:

(1) if , then put (chop off the head of the worm!);

(2) if , let be the maximum such that . Then put to be followed by copies of the part of starting after position .

For example, suppose we start with the worm

Then the sequence continues …

following by five copies of

And so it goes.

Well, you know your Goodstein sequences and your hydra battles, so you can predict what follows. But it is nice to know all the same!

THEOREM

(1) For any initial worm , there is an such that is empty.

(2) That result, suitably coded, is unprovable in first-order Peano arithmetic. In fact, its statement is equivalent to the 1-consistency of PA.

[For references see Sergei Artemov’s article in the *Handbook of Modal Logic*.]

Rowsety Moid1. Has something gone wrong with the formatting? At first I thought backslash-paren might just be peculiar notation, but there’s a backslash-ldots as well, and notations that look like they’re supposed to make sub- or superscripts.

2. I’m not sure it’s a good idea to go straight to provability logic, rather than introduce modal logic more generally first. In any case, the Stanford Encyclopedia article on Provability Logic might be a better entry point than the books you mentioned.

Peter SmithFormatting … that’s odd, works fine in Safari but goes as you describe in Firefox. I’ll investigate why. (Is this the first time I’ve embedded LaTeX since transferring to new WordPress set-up?– could be!) Thanks for alerting me!!

I perhaps misexpressed myself. When I said “I’ll introduce the very idea of a modal logic at an introductory level”I meant I was indeed going to introduce modal logic more generally first. And part of the SEP article was going to be my starting point: but then where? then which book (or part of book) was what I was/am wondering about!

David AuerbachOh good. I was going to say something like Rowsety’s 2. Because you want to tell them about Kripke semantics, which metaphysical cases coheres with an intuitive semantics. But with provability logics that’s a harder row to hoe.

Peter SmithI’ve now installed a shiny new plugin for WordPress which is also easier to use — and formatting seems to be working fine in various browsers on desktop, and also on iPhone. So I think that issue is sorted. Thanks again for the heads up, as they say!