Review of K Propositional Rules

Topic
Logical System

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