10/7/09 10Software
Reading
Rod Girle [2000] Modal Logics and Philosophy Chapter 3
T has the rules
{Non-modal propositional rules + Modal Negation + ◊R + □R+ □T}
These are described in Review of T Rules.
Basically what you have here are the restricted rules and some Access. Use of the possibility elimination rule will provide you with access to the generated world, and, with certain arguments, there may be explicit access given by the premises. Additionally, thanks to the rule □T if you have the ability to reason from, say, □P to P.
This means that inferences like
∴ □P ⊃P
will be valid (they are invalid in K).
Try to derive it [switch the Rule Set to T, and do not use any of the Access Rules]. You should be able to close the tree.
There is another way of looking at T (what Girle calls the 'orthodox' way), and that is to stick with the rules of K but to add Reflexive Access, that is any world can access itself ie Access(m,m) is available for all worlds m.
You can do the above proof of ∴ □P ⊃P 'in T' 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).
Roll your own trees with T
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 T, and do not use any of the Access Rules. Or Switch the Rule Set to K, and use any of the Reflexive Access Rule].