S4 Propositional Rules

Topic
Logical System

10/7/09

There are the ordinary (non-modal) tree propositional rules plus

The Modal Negation (MN) rules

 




 plus

◊ R world, k, must be new [here the computer will choose for you]. The rule gives you two lines. It gives you access to the world it generates and it gives you the body of the modal possible formula asserted for the generated world



□ R , before, you need to select two lines (one a modal necessary formula and the other a suitable Access relation)


then □ R , after, will give you


 

 plus

□ T you select a necessary formula and the rule gives you the body of the modal necessary formula asserted for the same world as that of the necessary formula



 plus

□ □ R before, you need to select two lines (one a modal necessary formula and the other a suitable Access relation)


then □ □ R , after, will give you