6/23/12
Reading
Rod Girle [2000] Modal Logics and Philosophy Chapter 3
S4 has the rules
{Non-modal propositional rules + Modal Negation + ◊R + □R+ □T+□□R}
These are described in Review of S4 Rules.
The extra rule (over T) is the Rule □□R and what it allows you to do it this. Without it (but with the other rules) you could reason from
□F (n)
Access(nw)
to
F (w)
But Rule □□R allows you to reason from
□F (n)
Access(nw)
to
□F (w)
The first piece of reasoning allows you to go from the fact that a formula is necessarily true and you have access to a different world, to the conclusion that the formula holds in the different world. The second piece of reasoning allows you to go from the fact that a formula is necessarily true and you have access to a different world, to the conclusion that the formula is also necessarily true in the different world.
There is another way of looking at S4 (what Girle calls the 'orthodox' way), and that is to stick with the rules of K but to add Reflexive and Transitive Access, that is any world can access itself ie Access(m,m) is available for all worlds m. And if Access(m,n) and Access(n,o) then Access(m,o) (for any worlds, m,n,o)
You can any proofs 'in S4' this way. Start the proof. switch the rule set to K (yes, K). But you can also use the reflexive rule off the Access menn (just select a formula, in the branch, with the world, say m, whose self-access you want and the rule will add Access(mm) and then you can use □R if you need to). And you can also use the transitive rule off the Access menu (just select two access formulas, in the branch, of the form Access(m,n) and Access(n,o) and the menu rule will add Access(m,o)).
Roll your own trees with S4
Girle's Chapter 3 has a number of exercises. You can do them here (be sure to use the following logical symbols)
∼ & ∨ ⊃ ≡ ∀ ∃ ∴ □ ◊
[Switch the Rule Set to S4, and do not use any of the Access Rules. Or Switch the Rule Set to K, and use either of the Reflexive or Transitive Access Rules].