Starting a tree
The Deriver host for a tree might have a Journal panel and a button Start from selection or it might alternatively have a few buttons labeled Tree1, Tree2, etc. .
If the Journal is in use, you need to select:
- a single formula, e.g. A&B or
- a list of formulas, e.g. A&B, CvD, ~A or
- a single formula, or list of formulas, followed by a 'therefore' symbol, followed by another formula e.g. A&B, CvD, ~A ∴ ~D or
- a 'therefore' symbol followed by a formula e.g. ∴ (E v ~E)
then pressing Start from selection will launch a Tree.
If, instead, buttons labeled Tree1, Tree2, etc. are in use, pressing one will launch its tree.
A Simple Tree to illustrate Extend, Close, and Closed
[This is a Video, click the Play button to view it.]
Extend requires the selection of a single, non-atomic formula, and it will extend all the branches that the formula belongs to. Extend operates under rules, which will be described later. At most, only one rule will apply to a formula and that rule will be determined by the main connective of the formula.
Closing a branch requires the selection of two formulas in branch, one of which needs to be the negation of the other.
To gain some familiarity:
Try building some trees (click on the formula to select, choose 'extend' from the menu). Close branches if you can (click on a formula to select, command-click on the negation of that formula (in the same branch), choose 'close' from menu).
Try building different trees from the same starting point (the order you apply the rules matters in terms of the tree generated) ie click on Tree 1, build it, click on Tree 1 again and build it again.
Notice
a) you cannot extend the same formula twice (once it is 'ticked' it is dead and unusable). [There is a qualification to this. In more advanced work, in predicate logic, universally quantified formulas can be extended again and again (to different individuals). Of course, such formulas are never ticked, nor do they ever become dead.]
b) no rule applies to either an atomic formula or the negation of an atomic formula
c) you get a smaller tree if you delay using splitting rules (ie use 'straight ahead' rules first).
d) you get a smaller tree if you close branches as soon as you can.