T

8/17/26

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)

∼ & ∨ ⊃ ≡ ∀ ∃ ∴ □ ◊

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