7/27/08 10 Software
Skills to be acquired in this tutorial:
None really: this is merely to give you a whiff of the topic of trees for modal logic.
Reading
Colin Howson, [1997] Logic with trees Chapter 12 Section 2
The Howson [1997] does not expand on modal logic (and modal trees) so a text like
Rod Girle [2000] Modal Logics and Philosophy
would definitely be a help here.
Tutorial
In modal logic, there are the additional symbols □ (necessary) and ◊ (possible) and, in the background, the notion of 'possible worlds'.
And, we keep in mind the indexing to possible worlds. So for example, ◊F ('it is possible that F') and ◊¬F ('it is possible that not-F') can both be true at the same time. That might happen when F is true in one possible world, say m, and ¬F is true in another possible world, say, n. Of course, such formulas {F,¬F} cannot both be true at the same time in the same world. This means that when you are closing branches, say for F and ¬F, the formulas have to be in the same world.
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 Applet [Single Line]
The big difference the modal operators make
You cannot in general tell whether a formula □<formula> is true merely by looking at the <formula> [of course, if <formula> is false you know □<formula> is false also]. And you cannot in general tell whether a formula ◊<formula> is false merely by looking at the <formula> [of course, if <formula> is true you know ◊<formula> is true also]. Usually what you have to do is to look what is happening to the truth value of the formula in other worlds (other 'accessible' worlds, to be more precise, but let us not worry about accessibility right now).
ModalTruth Table Applet [Single Line] [This is a new applet which is still under test.]
[You can leave the access butttons alone in this setting.]
There is much more to be said here, but you could probably make a fair fist of the following trees with that knowledge alone.
Formulas will have indexes to show which world they are supposed to apply to. So F (n) indexes the formula F to the possible world n ; and the assertion is that F holds in n. Omitting the possible world index completely just shows that the formulas in question hold of all worlds.
This indexing to worlds has an effect on closing branches. To close a branch, two formulas must contradict in the same world. So F (n) can be used to close with ¬F (n) but not with ¬F (w).
S5 Modal Trees
a) ∴□F→F
b) ∴◊F→□◊F
c) ∴◊◊F→◊F
d) ∴(□(F→G)∧□(¬F →G))↔□G
K Modal Trees
Close the following two trees using S5. Then go to the Rule Set Menu and change the rules to K, then try to close the trees a second time.
Remember that, with K, to remove or instantiate necessity across worlds, you also need access to the world you want to instantiate. So you will need two lines in the tree, one with the form □F for some world, say a, and an access relation Access(a,b) and then you can go to F for the world b.
a) ∴□F→□□F
b) ∴F→□◊F
Modal Predicate S5
a) ∴∀x□F(x) → □∀xF(x)
b) ∴∃x□F(x) → □∃xF(x)
Modal Predicate Logic with Contingent Identity (S5QT=)
When there is identity in a tree, branches can be closed in either of two ways: the familiar way of selecting two formulas that contradict each other in the same world, or selecting a single formula like ¬(a=a) which says that something is not identical to itself.
When substituting with identity in a tree you need to select two formulas: one is an identity, the other is any formula.
a) ∴ a=b → □a=b (hint, this is invalid in S5QT= ie you won't be able to close the tree)
b) ∴ a=b → (□F(a)→□F(b))
c) ∴ □a=b → (F(a)→F(b))
Roll your own
Type your own entries into the next applet.
F ∴ F ∧ G ∼ ∧ ∨ → ↔ ∀ ∃ ∴ □ ◊
a) ∴ ◊∃xF(x)→∃x◊F(x) Barcan
b) ∴ ∃x◊F(x)→◊∃xF(x) Barcan converse
c) ∴ ∀x□F(x)→□∀xF(x) Barcan
d) ∴ □∀xF(x)→∀x□F(x) Barcan converse
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).