The Tree Applet for Modal Trees

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]

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

 

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.]

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

 

 

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

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

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

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

 

Modal Predicate S5

a) ∴∀x□F(x) → □∀xF(x)

b) ∴∃x□F(x) → □∃xF(x)

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

 

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))

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

 

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).

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.