8/17/26
Reading
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
∼ & ∨ ⊃ ≡ ∀ ∃ ∴ □ ◊
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)
- You have to use the right (unicode/html) logical symbols. Check Writing 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)).
- The iPad, and similar, keyboards have a little trick that might catch you out. If you type a single letter, say 'a', they will automatically put it in upper case to 'A' because they assume you are starting a sentence. But, actually, if you are instantiating a quantifier you have to use lower case.
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).