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 w is a string of digits x_0x_1...x_n. And we will define w^* to be the result of decreasing w‘s last digit x_n by 1 if you can, or deleting that digit if it is already 0.

And now consider a sequence of worms w_0, w_1, w_2, \ldots constructed according to the following two rules:

(1) if x_n = 0, then put w_{m+1} = w^*_m (chop off the head of the worm!);

(2) if x_n > 0,  let k = be the maximum i < n such that x_i < x_n. Then  put w_{m+1} to be w^*_m followed by m copies of the part of w^*_m starting after position k.

For example, suppose we start with the worm

w_o = 2031

Then the sequence continues …

w_1 =203030
w_2 = 20303
w_3 = 20302222
w_4 = 203022212221222122212221
w_5 = 203022212221222122212220 following by five copies of 22212221222122212220

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 w_0, there is an m such that w_m 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.]

4 thoughts on “Beklemishev’s worm”

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

    1. Formatting … 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!

      1. Oh 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.

    2. I’ve now installed a shiny new \LaTeX 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!

Leave a Comment

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

Scroll to Top