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?


2 Answers 2


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.


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$.
  • 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$
    – user856
    May 31, 2014 at 2:52
  • $\begingroup$ Ah, sorry I misunderstood. I have updated my answer. $\endgroup$
    – StumpyLeg
    May 31, 2014 at 7:12
  • $\begingroup$ That's what I wanted! Thanks. $\endgroup$
    – user856
    May 31, 2014 at 8:08

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  

You must log in to answer this question.