6/1/12
Reading
A text like
Rod Girle [2000] Modal Logics and Philosophy
would definitely be a help here.
Tutorial
[Modal logic is a vast area, what is being presented here is the briefest of glimpses through the shop window (a book like the Girle would help you go further).]
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. A propositional formula, say ~A→B, is valued by given a truth value to the atomic components, A and B, to get, perhaps, ~True→False (which can be abbreviated ~T→F and then taking this out to get values for the connectives, in this case FTTF.]
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).
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).
There are different rule sets that are used for different purposes within model logic. Here are a few central ones.
S5 Modal Trees
In S5 here we are doing propositional logic, and there are three additional modal rules ('if something is not possible then it is necessary that not...', 'if something is not necessary then it is possible that not', and 'if something is possible there is a world in which it is true'). The rules are given in a subsection below. Then here are some sample proofs.
a) ∴□F→F
b) ∴◊F→□◊F
c) ∴◊◊F→◊F
d) ∴(□(F→G)∧□(¬F →G))↔□G
K Modal Trees
To go further, we need the notion of 'accessibility'. Consider how we might want to range over possible worlds. With a statement like ◊F (it is possible that F), we want to say that there is a world in which F is true. But, in certain circumstance we might want to reason differently. Our world has certain causal laws, for example the Law of Gravity, under which a cannonball released from the top of the Tower of Pisa falls to the ground. It is not possible for this cannoball to fall upwards. Well, it is not possible in worlds that have the same causal laws as ours. However, we might want to say that there are worlds in which there is no Law of Gravity or a different one, and in those worlds cannonballs might fall upwards. So, there is a different level of discrimination going on here over what is possible and what is not. The idea of accessibility, that world a is accessible from world b is to help capture this. Then there are different rule sets depending on the desired features for accessibility.
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.
With rule set 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
This is the plain S5 (i.e. no worries about accessibility), but for Predicate Logic.
a) ∴∀x□F(x) → □∀xF(x)
b) ∴∃x□F(x) → □∃xF(x)
Modal Predicate Logic with Contingent Identity (S5QT=)
Identity itself can be 'contingent' or 'necessary'. So, for example, if water is H20, we might think that water has to be H20 in all possible worlds (that would be necessary identity) or we might think that water is H20 in some possible worlds but that there are other possible worlds in which it is not (that would be contingent identity).
The rules in this section permit a to equal b i.e. a=b in some worlds but not in others.
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))
The Barcan formulas
The Barcan formulas mentioned below are famous formulas in modal predicate logic.
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 decide to use the web application for the exercises you can launch it from here Deriver [default] — username 'logic' password 'logic'. Then either copy and paste the above formulas into the Journal or use the Deriver File Menu to Open Web Page with this address https://softoption.us/test/treesStandAlone/CombinedTutorialsDefault.html . Then select the desired formula(s) and Start Tree off the Actions Menu.
Preferences
You will need to set some Preferences for this.
- set identity to true (and that will give you the identity rules)
- set modal to true (to get modal)
- and you can check that the parser is set to default.