S5 Modal Trees

Logical System


Rod Girle [2000] Modal Logics and Philosophy Chapter 2

You can make a reasonable start here by thinking about how truth tables might work once there are the modal operators, necessary □ and possible ◊.

To remind ourselves, ordinary truth tables are filled out as follows. [What we are doing here is taking a random ordinary propositional formula, say ~A⊃B then valuing the atomic propositions in it to get, perhaps,  ~True⊃False which is abbreviated ~T⊃F and then you are being asked to fill out the values for the connectives, in this case you will get FTTF.]

Truth Table Widget [Single Line]



Modal 'Truth Table Widget' [Single Line]



S5 Modal Trees

[Click to select or unselect. Select one item to extend the Tree, select two to close a branch. [Select two for extending with identity, necessityR etc,]]

You can adjust the layout, to a degree, using the vertical lines at the top.

Here are the Basic Tree Rules for Propositional Logic and the S5 Extension Rules. [If you haven't tried any Trees in this setting, you could look at the video Help with Trees. ]

a) ∴□H⊃H

b) ∴◊H⊃□◊H

c) ∴◊◊H⊃◊H

d) ∴(□(H⊃G)&□(~H ⊃G))≡□G

Roll your own

Girle's Chapter 2 has a number of exercises. You can do them here (be sure to use the following logical symbols)

∼ & ∨ ⊃ ≡ ∀ ∃ ∴ □ ◊

If you are really giving this a good workout.... There is a puzzling little trap here that sometimes occurs (but rarely). When you copy and paste, or drag and drop, html text across browsers, desktops, etc., crossing from one application to another, your computer sometimes adds an extra invisible character which marks the end of the text. You cannot see that character, but the logic software parsing formulas certainly can. So sometimes the logic software may tell you that an apparently good formula is not well formed. If trailing invisible characters seem to be an issue, one workaround is to put the insertion point after the formula and hit backspace or delete (that will delete the invisible character).