S4

8/17/26

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)

∼ & ∨ ⊃ ≡ ∀ ∃ ∴ □ ◊

• The symbols in use here are ∼ & ∨ ⊃ ≡ ∀ ∃ ∴ □ ◊ ₁ ₂ ₃ ₄ ₅ ₆ ₇ ₈ ₉ (so copy and paste or drag and drop these). In the syntax, the quantifiers have brackets around them so a quantified formula might look like (∀x)(Ax→Bxy). Notice that the 'arguments' to a predicate do not have brackets around them. You can use proper subscripts (shown above) on variables (or constants or predicates). For example, (∀x₁)(Ax₁→Bx₁y₁).
• When entering from a selection, the software will take a single formula (say, A) or a comma separated list of formulas (say, A,B,C) or a possibly empty comma separated list of formulas followed by ∴ and another formula (say, A,B,C ∴ D). In the last case it will load the negation of the conclusion.
• Lightweight Input. Just type, cut and paste, or drag and drop, whatever you wish, into the lower text box (the 'Journal'). Then make a selection and hit the Start button.
• Lightweight Output. You can write a tree out to the Journal (then copy it and paste it into WORD (for example)).

[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].