4
$\begingroup$

I'm reading about modal logic on the Stanford Encyclopedia of Philosophy. They define the modal logic S5 as propositional logic augmented with the modal operators $\square$ and $\Diamond=\lnot\square\lnot$ and the axioms

$$\begin{align} \square(A\to B)&\to(\square A\to\square B), \tag{K} \\ \square A&\to A, \tag{M} \\ \Diamond A&\to\square\Diamond A. \tag{5} \end{align}$$

They then state without proof that in S5 any string of modal operators is equivalent to the last operator in the string. That is, $00\cdots0\square=\square$ and $00\cdots0\Diamond=\Diamond$ where each $0$ is either $\square$ or $\Diamond$.

This claim is not at all obvious to me, so I would like to have a proof. I suppose we only need to show that $\Diamond\square=\square=\square\square$ and $\square\Diamond=\Diamond=\Diamond\Diamond$. Applying $(\mathrm M)$ to $\Diamond A$ yields the converse of $(5)$, showing that $\square\Diamond=\Diamond$; contrapositively, $\Diamond\square=\square$. Similarly, applying $(\mathrm M)$ to $\square A$ shows that $\square\square A\to\square A$ and $\Diamond A\to\Diamond\Diamond A$.

However, I can't see how to establish the converse $\square A\to\square\square A$ and $\Diamond\Diamond A\to\Diamond A$. It's been a while since I did logic. Help?

$\endgroup$
5
$\begingroup$

Preliminary comment: the interdefinability of $\square$ and $\Diamond$ using negation isn't specific to S5.

Now to the question. I don't know offhand how the derivations within the system go, but if you want the claim to be "obvious" I think you want an explanation that makes it intuitive. Such an explanation can be given in terms of Kripke semantics and constitutes a semantically-based proof.

Informally...

Basically S5 assumes a set of possible worlds where any possible world is accessible from any other possible world. (This is not technically quite right, but close enough.) Then $\square A$ means "In any possible world, $A$ is true," and $\Diamond A$ means "There is a possible world where $A$ is true." So then, if we iterate and write $\square \Diamond A$, we are saying that from the point of view of any possible world, there is a possible world where $A$ is true.

But since every possible world is accessible from every other possible world, there's no difference between saying that and just saying that from the point of view of this world, there is a possible world where $A$ is true. Which is just $\Diamond A.$ So the additional $\square$ operator doesn't change the statement.

A similar story goes for adding the $\Diamond$ where a $\Diamond$ or $\square$ is already present.

In other words, if we shift our world of evaluation from the actual one (this world) to another one, the set of modal truths we "see" doesn't change, even though the set of non-modal truths of course does. We see exactly the same modal truths, because the universal character of the accessibility relation ensures that we're always looking at the same set of possible worlds.

Does that help?

EDIT: In response to the OP's below comment, here's the desired answer (pulled together after paging through Hughes and Cresswell).

  1. Since it's agreed that $\Diamond \square = \square$, we have $\square A \rightarrow \Diamond \square A$.
  2. Substitute $\square A$ for $A$ in (5) to obtain $\Diamond \square A \rightarrow \square \Diamond \square A$. So then $\square A \rightarrow \square \Diamond \square A$
  3. Replace $\Diamond \square A$ with $\square A$ in the consequent to obtain $\square A \rightarrow \square \square A$.
  4. And then replacing $A$ with $\neg A$ and performing contraposition, from $\square A \rightarrow \square \square A$ we get $\Diamond\Diamond A \rightarrow \Diamond A$.
$\endgroup$
  • 1
    $\begingroup$ Thanks, but I'm already aware of the intended semantics of $\square$ and $\Diamond$ as necessity and possibility. And I can believe that if $00\cdots0\square=\square$ and $00\cdots0\Diamond=\Diamond$ then these interpretations make sense. But there's still the question of how all this follows from the axioms $(\mathrm{K,M,5})$ themselves, which is what I was asking. // P.S. It seems I misled you by my use of the word "obvious". All I meant was that I could not immediately see a proof of the claim. $\endgroup$ – Rahul May 31 '14 at 2:52
  • $\begingroup$ Ah, sorry I misunderstood. I have updated my answer. $\endgroup$ – StumpyLeg May 31 '14 at 7:12
  • $\begingroup$ That's what I wanted! Thanks. $\endgroup$ – Rahul May 31 '14 at 8:08
0
$\begingroup$

I like formal proofs:

ps i use slightly different names for the axioms, and us ethe rules

Modus ponens |-A , |- A -> B => |- B

and Necessitation |-A => |- []A

K |-|- [](A -> B) -> ([]A -> []B) 
T |-|- []A -> A 
E |-|- <>A -> []<> A  

1 |- ~[]<>~A -> ~<>~A    contra positive of Axiom E, [A/~A]
2 |- <>[]A -> []A        1 modal exchange
3 |- ~~[]A -> ~[]~[]A    contra positive of Axiom T, [A/~[]A] 
4 |- []A -> <>[]A.       3 modal exchange
5 |- <>[]A ->[]<>[]A     Axiom E [A/[]A] 
6 |- []A -> []<>[]A      4,5 modus ponens       
7 |- [](<>[]A -> []A)    2 necessitation
8 |- []<>[]A -> [][]A    7 rule K
9 |- []A -> [][]A        7,8 modus ponens  
$\endgroup$

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.