Beklemishev’s worm

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.]