Soundness and completeness

As with the proposition calculus, so with the predicate calculus, the tableau rules are both sound and complete. That is to say, if a syntactic sequent is correct, so is the corresponding semantic sequent – that is, the rules are sound; and if a semantic sequent is correct, so is the corresponding syntactic sequent - that is, the rules are complete.

Showing that a sequent is incorrect

The way to show that a semantic sequent is incorrect is to find a counterexample. Giving a counterexample involves specifying (a) a domain and (b) an interpretation which assigns meanings to all the sentence letters, predicate letters and individual constants (names) which appear in the sequent, which together make all the formulae (if any) before the turnstile true and the formula (if any) after the turnstile false. So a counterexample to a sequent is an interpretation which makes all the members of its counterexample set true in a specified domain.

With the propositional calculus there was a mechanical way of showing the incorrectness of a sequent – by drawing a truth-table; alas, with the predicate calculus the is no mechanical way of doing this. (Alonzo Church showed in 1936 that there could be no such method.) So a proof of incorrectness may require ingenuity.

One way to show that a syntactic sequent is incorrect, is by showing that it generates a tableau which does not close, but may be regarded as finished. However, as we have seen, a tableau may never finish; so this method is not always available. And, of course, the fact that a tableau has not closed after a certain number of steps is not a proof that it will not close after further steps. Generally the best way to show that a syntactic sequent is incorrect is to rely on the soundness of the tableau rules, and to find a counterexample. For instance one can show that the following sequent is incorrect:

            "x$yGyx |- $y"xGyx

by the following interpretation:

Domain: natural numbers

Gxy: x>y

This makes the formula before the turnstile true (In the case of every number, there is a number greater than it), and the one after it false (because no number is greater than itself).

One could instead have taken an interpretation with an empty domain.