I'm currently reading The Logic of Provability by George Boolos and there's a step in a proof that I don't understand.

The author has defined a system of modal logic called GL; its language has a countable collection of sentence letters $p$, $q$, $\ldots$ as well as the symbols $\to$, $\bot$ and $\Box$; sentences are defined inductively in the obvious way (i.e. $\bot$ and each sentence letter $p$ is a sentence, $(A \to B)$ and $\Box A$ are sentences whenever $A$ and $B$ are), $\neg A$ is defined to be $(A \to \bot)$ and $\Diamond A$ is defined to be $\neg \Box \neg A$.

The axioms of GL are all tautologies (although the author hasn't said as much, I assume that the truth of $\Box A$ should be taken as independent of that of any subsentences of $A$ in determining whether something is a tautology) as well as all sentences of the following forms:

$\Box (A \to B) \to (\Box A \to \Box B)$

$\Box (\Box A \to A) \to \Box A $

and its rules of inference are modus ponens and necessitation (i.e. from $A$ infer $\Box A$). It has been proved that all sentences of the form

$\Box A \to \Box \Box A$

are theorems, and that theorems of GL are closed under substitution of arbitrary sentences for sentence letters. The author has also proved Theorem 21 for all $p$:

$\mathrm{GL} \vdash \Box \bot \leftrightarrow \Box \Diamond p$.

A couple of pages later, the author says "by Theorem 21 (with $\bot$ for $p$)

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box \Box (p \leftrightarrow \neg \Box p)$"

I've been scratching my head for a while and I've no idea how he gets this. Can anyone help?

  • 2
    $\begingroup$ Just so you know that the question hasn’t sunk without a trace: even after checking the context via Google Books and staring at it for quite a while, I have no idea what he’s thinking there. $\endgroup$ – Brian M. Scott Apr 7 '12 at 12:16
  • $\begingroup$ @ Brian: thanks. I already asked on sci.logic (where I know that some regulars have read the book) and got no replies. I'll probably try asking MathOverflow at some point. $\endgroup$ – Rotwang Apr 9 '12 at 19:50
  • $\begingroup$ If you get an answer at some point, you might post it here, not only to get this off the Unanswered list, but ’cause I’m curious now! $\endgroup$ – Brian M. Scott Apr 9 '12 at 19:55
  • $\begingroup$ Will do. (padding for minimum comment length) $\endgroup$ – Rotwang Apr 9 '12 at 20:18

I still don't know what the author had in mind, but over in sci.logic Daryl McCullough has presented an alternative proof of the statement in question:

From the rule $\Box A \to \Box \Box A$ and distribution we can derive

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box (\Box p \leftrightarrow \Box \neg \Box \bot)$

From Theorem 21 (with $\neg \bot$ for $p$) we have

$\mathrm{GL} \vdash \Box \neg \Box \bot \leftrightarrow \Box \bot$

From both of the above we have

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box (\Box p \leftrightarrow \Box \bot)$

Also by tautology and distribution

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box (\neg p \leftrightarrow \Box \bot)$

From the last two equations,

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box (\Box p \leftrightarrow \neg p)$

The above, together with tautology and distribution, gives

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box (p \leftrightarrow \neg \Box p)$

And again from $\Box A \to \Box \Box A$,

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box \Box (p \leftrightarrow \neg \Box p)$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.