12/31/09 10 Software under construction.
You are invited to review
Most of these pages load java applets and that means that they may take 20 seconds or so to load. [Your browser will then 'cache' the applets and subsequent work will proceed much more quickly.]
Extensive use is going to be made of Trees or Tableaux. A good way in, even before you get started on the material here, is to look at the Notes on Colin Howson's book on Trees, say the first three tutorials. [The Howson book uses → for the conditional, we're going to use ⊃ here.]
The text that is essential here is
Graham Priest [2008] An Introduction to Non-Classical Logic
All we are going to do is to provide software support, so that you can explore the systems he explains (and do more of his exercises (quickly and correctly)).
S5 Modal Trees
a) ∴□F⊃F
b) ∴◊F⊃□◊F
c) ∴◊◊F⊃◊F
d) ∴(□(F⊃G)∧□(¬F ⊃G))≡□G
Modal Predicate S5
a) ∴∀x□Fx ⊃ □∀xFx
b) ∴∃x□Fx ⊃ □∃xFx
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 ⊃ (□Fa⊃□Fb)
c) ∴ □a=b ⊃ (Fa⊃Fb)
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 Gentzen, so use these symbols for the logical connectives.
F ∴ F ∧ G ¬ ∧ ∨ ⊃ ≡ ∀ ∃ ∴ □ ◊
a) ∴ ◊∃xFx⊃∃x◊Fx Barcan
b) ∴ ∃x◊Fx⊃◊∃xFx Barcan converse
c) ∴ ∀x□Fx⊃□∀xFx Barcan
d) ∴ □∀xFx⊃∀x□Fx 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).