5: Predicate Calculus: TableauxPredicate TableauxThere are four new rules to deal with the quantifiers: one each for "xj (and, of course, for "yj, etc), and for ¬"xj; and one each for $xj and ¬$xj. In addition to these we retain the rules for propositional tableaux, except that we dispense with ticking. (See the paragraph on ticking below.)
The "xj ruleThe rule is:
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.)
Note particularly:
The rationale of this rule is that, if something is true of everything, it is true in particular of whatever D stands for – assuming that it stands for something (see below: example (vi)).
Example: a proof that {Fa, "x[Fx®Gx], "x¬Gx} is inconsistent:
The tableau closes; so the original set is inconsistent.
The following are correct applications of the rule:
(The rule applies to "y, "z , etc as well as "x)
("a" occurs in the branch to which "[$x[Gx®Raa]ÙFa]" is added; it doesn't need to occur higher than the line to which the rule is applied.)
The following are incorrect attempts to apply the rule; the incorrect applications are starred.
Wrong, because the rule applies only to formulae beginning with """. If this application were correct, we would be able to "prove" the following inconsistent: {Buttercup is brown, not everything is brown}.
Again the mistake consists in applying the rule to a formula which does not begin with """. The following would have been correct:
Again the mistake consists in applying the rule to a formula which does not begin with """. The following would have been correct:
But now the left branch does not close.
The mistake is that the "a" which is introduced in "Fa" has not occurred already in the branch. The tableau is a faulty attempt to prove that {"xFx, "x¬Fx} is inconsistent. But it is not: in the empty domain both ""xFx" and ""x¬Fx" will be true. The point of the requirement that the designator should already have occurred in the branch is to block such a faulty proof. One can look at it like this: the use of "a" is permitted only if "a" names something; but since "a" does not already occur in the branch, "a" may not name anything at all.
Note: disallowing the empty domain Hodges's
tableau system is designed to allow for the possibility that we may be
dealing with an empty domain. Most systems, on the other hand, allow us
to assume that we are not dealing with an empty domain. But if
we are not {"xFx, "x¬Fx}
will after all be inconsistent, and there is no need to require that the
designator which is introduced by the "xj rule already occurs in the branch. After
all, if we are allowed to assume that the domain is not empty, we may
safely assume that there is something for the designator to name. Rule VIIwhere no designators have occurred in the branch to which y is added, D is a proper name and y is the result of replacing each free occurrence of "x" in j by an occurrence of D. You should note, however, that Hodges himself does NOT adopt this rule


