Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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. – Brian M. Scott Apr 7 '12 at 12:16
@ 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. – Rotwang Apr 9 '12 at 19:50
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! – Brian M. Scott Apr 9 '12 at 19:55
Will do. (padding for minimum comment length) – Rotwang Apr 9 '12 at 20:18
up vote 3 down vote accepted

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)$

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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