Tutorial Contents Tutorial Five: Predicate Calculus: Tableaux - The \$xj rule - Bad Mistakes and Technical Mistakes - Ticking - Finished Tableaux - Sequents - Soundness and Completeness - Proof of a syntactic sequent: example More Tutorials One Two Three Four Six Seven

#### The ¬"xj rule

The rule is:

The rationale for this rule is that "\$j" is equivalent to "¬"xj".

Note that the rule applies only to formulae which begin with "¬"".

#### The ¬\$xj rule

The rule is:

The rationale for this rule is that ""j" is equivalent to "¬\$xj".

Note that the rule applies only to formulae which begin with "¬\$".

Example: a proof that the following argument is valid:

 Fa [\$xFx®"xGx] So, Gb

The counterexample set is {Fa, [\$xFx®"xGx], ¬Gb}

The tableau closes; so the counterexample set is inconsistent; so the argument is valid.

The following is an incorrect attempt to apply the rule:

The mistake consists in the application of the rule to a formula which does not begin with "¬\$x".

The following is correct: