Even though we can’t apply the method of truth tables to first order logic we can still apply the method of analytic tableaux. As with zeroeth order logic these are essentially just bookkeeping devices to keep from getting confused in formal arguments like the ones above.
The tableaux rules for the logical operators remain the same but we need new rules for quantifiers. \[ \begin{array}{r|l} [ ∀ V . ( P V ) ] & \cr \hline ( P A ) & \end{array} \quad \begin{array}{r|l} [ ∃ V . ( P V ) ] & \cr \hline ( P B ) & \end{array} \] \[ \begin{array}{r|l} & [ ∀ V . ( P V ) ] \cr \hline & ( P B ) \end{array} \quad \begin{array}{r|l} & [ ∃ V . ( P V ) ] \cr \hline & ( P A ) \end{array} \] The notational conventions are as discussed previously but in this case \({ A }\) stands for any parameter but \({ B }\) stands for any new parameter, i.e. one which has not been used previously in the tableau. \({ P V }\) stands for any expression and \({ P A }\) or \({ P B }\) stand for the same expression but with all free occurrences of the variable denoted by \({ V }\) replaced by the parameter denoted by \({ A }\) or the parameter denoted by \({ B }\), respectively.
So if we have the expression \({ [ ∀ x . ( F x ) ] }\) on the left hand side of the vertical bar we’d be allowed to write \({ ( F a ) }\) to the left of the bar. We’d also be allowed to write \({ ( F b ) }\) or \({ F }\) followed by any other parameter. But this rule isn’t restricted to unary predicates. It applies to any expression. If, for example, we had the expression to the left of the bar \({ \{ ∀ x . [ ( g w x ) ⊃ ( h x y ) ] \} }\) then we could write \({ [ ( g w a ) ⊃ ( h a y ) ] }\) to the left. This is the tableau counterpart of saying “We know that \({ [ ( g w x ) ⊃ ( h x y ) ] }\) for all \({ x }\) so in particular \({ [ ( g w a ) ⊃ ( h a y ) ] }\).”
The rule for a \({ ∃ }\) on the left is similar, but the counterpart in an informal proof is now “We know there is at least one \({ x }\) such that \({ [ ( g w x ) ⊃ ( h x y ) ] }\). Let \({ a }\) be such an \({ x }\). Then \({ [ ( g w a ) ⊃ ( h a y ) ] }\).” This explains reason for the restriction to new parameters, which we already met in the second of our two informal proofs above. As another example of this phenomenon, if we have the statements “there is at least one even number” and “there is at least one one odd number” then we can legitimately say “Let \({ a }\) be an even number and let \({ b }\) be an odd number”. We couldn’t legitimately say “Let \({ a }\) be an even number and let \({ a }\) be an odd number” and then conclude that some number is simultaneously even and odd.
The rules to the right of the bar are similar. The only way a universal statement can be false is if there is at least one counterexample. The corresponding tableau rule allows us to name that counterexample with a parameter. It has to be a new parameter because we have no right to assume it is equal to any previously named value. For a universal statement there is no such restriction. If a universal statement is false then every instance of it is false, so it will be false for any previously named value as well.
The restriction to names which have never appeared in the tableau for the two rules where we made such a restriction is in fact unnecessarily drastic. It would have been enough to require that the parameter does not appear anywhere in that branch rather than in the tableau as a whole.