The ¬"xj rule

The rule is:  

The rationale for this rule is that "$x¬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 ""x¬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:

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: