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 equality and for quantifiers. The rules for equality are relatively straightforward.
First, we can always write a statement of the form \({ ( A = A ) }\) to the left of the vertical, where \({ A }\) is any parameter. Second, if we have a statement of the form \({ ( A = B ) }\) to the left of the line, where \({ A }\) and \({ B }\) are parameters, then in any statement we can replace some or all \({ A }\)’s by \({ B }\)’s or vice versa.
The rules for quantifiers require a bit of notation to describe. In what follows, \({ P }\) is an expression, \({ V }\) is a variable, \({ A }\) is a parameter, \({ B }\) is a parameter which has not appeared previously in the tableau, \({ Q }\) is the expression obtained by substituting the parameter \({ A }\) for all free occurrences of \({ V }\) in \({ P }\) and \({ R }\) is the expression obtained by substituting the parameter \({ B }\) for all free occurrences of \({ V }\) in \({ P }\). In terms of these we can express the following four rules for the two quantifiers, either of which can appear either to the left or the right of the line.
If we have an expression of the form \({ ( ∀ V . P ) }\) to the left of the line we branch, with one of the branches having a \({ [ ∃ V . ( V = A ) ] }\) to the right of the line and the other having a \({ Q }\) to the left.
If we have a \({ ( ∃ V . P ) }\) to the left of the line we don’t branch and we put a \({ [ ∃ V . ( V = B ) ] }\) to the left of the line and an \({ R }\) to the left.
If we have a \({ ( ∀ V . P ) }\) to the right of the line we don’t branch and we put a \({ [ ∃ V . ( V = B ) ] }\) to the left of the line and a an \({ R }\) to the right.
If we have a \({ ( ∃ V . P ) }\) to the right of the line then we branch and, with one of the branches having a \({ [ ∃ V . ( V = A ) ] }\) to the right of the line and the other having a \({ Q }\) to the right.
These may seem obscure but they are relatively easily explained. As with the Boolean operators we just need to examine the ways in which each statement could occur.
For example if \({ ( ∀ V . P ) }\) is true then the statement \({ P }\) holds for any value of the variable \({ V }\). If \({ A }\) is a parameter then either \({ A }\) is a possible or it isn’t. If it isn’t then there is no value of \({ V }\) equal to \({ A }\). If there is then the statement \({ P }\) with each free occurrence of \({ V }\) replaced by an \({ A }\) must be true.
If \({ ( ∃ V . P ) }\) is true then there is a value of \({ V }\) which makes the statement \({ P }\) true. We can give this value a name, but we can’t assume that it is equal to any previously named value so we give it the new name \({ B }\). Since this name corresponds to an actually existing value we have \({ [ ∃ V . V = B ] }\). Since this value is one that when substituted for \({ V }\) in \({ P }\) gives a true statement we have \({ R }\).
The other two cases, the ones with statements to the right of the line can be analysed similarly.
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.