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
