As in zeroeth order logic the method of analytic tableaux in first order logic can be thought of in terms of nondeterministic computation. There the order in which the rules are applied turned out to be relevant only in the sense that some orders gave an answer faster than others. Here the situation is unfortunately more complicated. There’s no guarantee, for example that the method ever terminates. In zeroeth order logic this was guaranteed by two facts: that all tableaux rules result in statements of lower degree than what we start with and that only finitely many–in fact at most two–statements can be derived from any statement. The first of these is still true for tableaux in first order logic but the second is not. Our rules for quantifiers can be used to derive infinitely many statements from a single one, just by using a different parameter each time.
Even when the tableau can be made to terminate after finitely many steps a poor set of choices can result in it not terminating. In our first example we derived \({ ( f a ) }\) from \({ [ ∃ x . ( f x ) ] }\), for example. Instead of proceeding as I did above I could then have derived \({ ( f b ) }\) and then \({ ( f x ) }\), etc., never arriving at a contradiction.
The tableaux method for first order logic is more like the parsing problem where we first met nondeterministic computation than it is like the tableaux method for zeroeth order logic. As happened in that problem we can replace the nondeterministic computation by a deterministic one by calculating all paths the nondeterministic calculation could take. As happened there, this deterministic calculation will terminate successfully in finite time if the nondeterministic one could terminate successfully in finite time. Also as happened there, there is no guarantee that it will terminate unsuccessfully in finite time if it can’t terminate successfully. It could just run forever.
There is one complication here that we didn’t meet in the parsing problem. There there were only finitely many options at each step. Here there will be infinitely many if we are able to apply our quantifier rules, since there are always infinitely many parameters to choose from. This problem is more apparent than real though. If we choose a new parameter then it doesn’t really matter which one we choose. If we choose a different one then the rest of the computation will proceed exactly the same, just with some parameters replaced by others. Whether it terminates, and if so whether it terminates successfully, will remain unchanged. So instead of following all possible substitutions by a parameter we can follow just a single new parameter and, in the two cases where it’s allowed, substitution of a parameter already used in the tableau, of which there are only finitely many at each stage.
In this way we obtain an algorithm which is guaranteed to prove any valid statement in finite time. It can prove some invalid statements invalid in finite time as well, but is not guaranteed to do so.