Non-Classical Logic [under construction]

Logical System

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)

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