The Tableau Rules

(Note that it is not necessary to put in the vertical line when drawing a tableau.)

The Propositional Rules

The Predicate Rules

where there is a designator D which has already occurred in the branch to which y is added, and y is the result of replacing each free occurrence of "x" in j by an occurrence of D. (i.e. the rule is that we can add "y" to any open branch in which ""xj" occurs where this condition is satisfied.)

where there is a proper name D which has not occurred anywhere in the branch to which y is added, and y is the result of replacing each free occurrence of "x" in j by an occurrence of D.

Identity rules

where the designator D occurs in j, and y is the result of replacing one or more occurrence of D in j by E.

Rules for closing a branch

Any branch containing both j and ¬j closes.

Any branch containing ¬D=D, where D is a designator, closes.

Which rules can I use?

With the exception of the identity rules, there is at most one rule for extending a branch which can be applied to any formula.

If the formula begins with "¬¬" the only rule that can be used is the ¬¬j rule.

If the formula begins with "[", the only rule that can be used is the rule for the truth functor to which this "[" belongs.

If the formula begins with "¬[", the only rule that can be used is the rule for the negated truth functor to which this "[" belongs.

If the formula begins with """, the only rule that can be used is the "xj rule.

If the formula begins with "¬"", the only rule that can be used is the ¬"xj rule.

If the formula begins with "$", the only rule that can be used is the $xj rule.

If the formula begins with "¬$", the only rule that can be used is the ¬$xj rule

Which rules are worth applying more than once?

The only rules which are worth applying more than once to the same formula in the same branch are the "xj rule and the identity rules. Sometimes these have to be applied more than once (to the same formula in the same branch). Though, of course, even these rules are worth re-applying only if they result in the addition of something new to the branch.

Notice, in particular, that there is never any point in applying the $xj rule twice to the same formula in the same branch - even though applying it a second time is, of course, bound to add something new to the branch.

Ticking

Ticking is optional if you are doing a predicate tableau, but you may find that, used with caution, it helps you to keep track. You should, however, tick a formula only if you have applied a rule which is not worth applying a second time to the same formula in the same branch, and have applied it in every open branch in which the formula occurs. So:

· do not tick a formula to which you have applied the "xj rule;

· do not tick a formula to which you have applied an identity rule;

· remember that you may want to use a ticked formula again in conjunction with one of the identity rules. (Though this is never actually necessary.)