3
$\begingroup$

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?

$\endgroup$
4
  • 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
    Commented Apr 7, 2012 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
    Commented Apr 9, 2012 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
    Commented Apr 9, 2012 at 19:55
  • $\begingroup$ Will do. (padding for minimum comment length) $\endgroup$
    – Rotwang
    Commented Apr 9, 2012 at 20:18

1 Answer 1

Reset to default
3
$\begingroup$

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

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .