10/3/08 10 Software, under construction.
K Modal Trees
Close the following 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 1, and an access relation 1r2 and then you can go to F for the world 2. [To make this kind of extension you need to select two lines, click on one then command click on the other.]
a) ∴□F⊃□□F
b) ∴F⊃□◊F
c) ∴ (□A ∧□B)⊃□(A∧B)
d) ∴ (□A∨□B)⊃□(A∨B)
Roll your own
Type your own entries into the next applet. The applets can be configured to run a variety of symbol systems. This particular one is running those of Priest's book, so use these symbols for the logical connectives.
F ∴ F ∧ G ¬ ∧ ∨ ⊃ ≡ ∀ ∃ ∴ □ ◊
You need a list of zero or more premises, separated by commas, then a therefore, and then the conclusion. Use this as a template
P, Q, R ∴ S
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).