2 Soundness and Completeness for Analytic Tableaux

Recall that we have called a branch of a tableau “complete” if every formula on it “has been used”. With our convention on using the letters α and β for signed formulas, we may express this more precisely:

A branch θ of a tableau T is complete if for every α ∈ θ, both α_{1}, α_{2} ∈ θ, and for every β ∈ θ, either β_{1} ∈ θ or β_{2} ∈ θ.

As before, we say that a tableau T is completed if every branch θ of T is either closed or complete.

2.1 Tableaux and valuations

Let [[−]] be a valuation. We extend [[−]] to signed formulas in the obvious way by letting [[T X]] = [[X]] and [[F X]] = 1 − [[X]]. Thus, F X is true under a given valuation iff X is false under that valuation.

Definition. Let [[−]] be a valuation. We say that a branch θ of a tableau T is true under [[−]] if for all φ ∈ θ, [[φ]] = 1. We say that T is true under [[−]] if there is at least one branch θ of T such that θ is true under [[−]].

2.2 Soundness

Soundness states that if a formula X is provable by the tableaux method, then X is a tautology.

Theorem 2.1 (Soundness). Suppose X is a proposition, and T is a closed tableau with origin F X. Then X is a tautology.

The proof depends on the following lemma:

Lemma 2.2. Suppose T_{1} and T_{2} are tableaux such that T_{2} is an immediate extension of T_{1}. Then T_{2} is true under every interpretation under which T_{1} is true.

Proof. Suppose T_{1} is true under the given valuation [[−]]. Then T_{1} has at least one true branch θ. Now T_{2} was obtained by adding one or two successors to the endpoint of some branch θ_{1} of T_{1}. If θ_{1} ≠ θ, then θ is still a branch of T_{2}, hence T_{2} is true and we are done. Assume therefore that θ_{1} = θ. Then θ was extended by one of the following operations:

(A) For some α ∈ θ, we have added α_{1} or α_{2}, so θ ∪ {α_{1}} or θ ∪ {α_{2}} is a branch of T_{2}. But [[α]] = 1, therefore [[α_{1}]] = 1 and [[α_{2}]] = 1, therefore T_{2} contains a true branch.

(B) For some β ∈ θ, we have added both β_{1} and β_{2}, so both θ ∪ {β_{1}} and θ ∪ {β_{2}} are branches of T_{2}. But [[β]] = 1, therefore [[β_{1}]] = 1 or [[β_{2}]] = 1, therefore T_{2} contains at least one true branch. □

Lemma 2.3. Let [[−]] be a fixed valuation. For any tableau T , if the origin of T is true under [[−]], then T is true under [[−]].

Proof. This is an immediate consequence of the previous lemma, by induction: T is obtained from the origin by repeatedly extending the tableau in the sense of Lemma 2.2, at each step preserving truth. □

Proof of the Soundness Theorem: Let T be a closed tableau with origin F X, and let [[−]] be any valuation. Since T is closed, each branch contains some formula and its negation, and therefore T cannot be true under [[−]]. From Lemma 2.3, it follows that the origin of T is false under [[−]], thus [[F X]] = 0, thus [[X]] = 1. Since [[−]] was arbitrary, it follows that X is a tautology. □

2.3 Completeness

Completeness is the converse of soundness: it states that if X is a tautology, then X is provable by the tableaux method. In fact we will prove something slightly stronger, namely, if X is a tautology, then every strategy for completing a tableaux for X will lead to a closed tableaux.

Theorem 2.4 (Completeness). (a) Suppose X is a tautology. Then every completed tableau with origin F X must be closed.

(b) Suppose X is a tautology. Then X is provable by the tableaux method.

The main ingredient in the proof is the notion of a Hintikka set.

Definition. Let S be a (finite or infinite) set of signed formulas. Then S is called a Hintikka set (or downward saturated) if it satisfies the following three conditions:

(H_{0}) There is no propositional variable p such that both T p ∈ S and F p ∈ S.

(H_{1}) If α ∈ S, then α_{1} ∈ S and α_{2} ∈ S.

(H_{2}) If β ∈ S, then β_{1} ∈ S or β_{2} ∈ S.

Note that, by definition, a complete non-closed branch θ is a Hintikka set.

If S is a set of signed formulas, we say that S is satisfiable if there exists a valuation [[−]] such that for all φ ∈ S, [[φ]] = 1.

Lemma 2.5 (Hintikka Lemma). Every Hintikka set is satisfiable.

Proof. Let S be a Hintikka set, and define a valuation as follows: for any propositional variable p, let

[[p]] = 1 if T p ∈ S,
[[p]] = 0 if F p ∈ S,
[[p]] = 1 if T p ∉ S and F p ∉ S.

Note that, since S is a Hintikka set, we cannot have T p ∈ S and F p ∈ S at the same time. Thus, this is well-defined. We recursively extend [[−]] to composite formulas in the unique way.

We now claim that for all φ ∈ S, [[φ]] = 1. This is proved by induction on φ. For atomic φ, this is true by definition. If φ is composite, then there are two cases:

(A) φ is some α. Then by (H_{1}), α_{1} ∈ S and α_{2} ∈ S. By induction hypothesis, [[α_{1}]] = 1 and [[α_{2}]] = 1, therefore [[α]] = 1.

(B) φ is some β. Then by (H_{2}), β_{1} ∈ S or β_{2} ∈ S. By induction hypothesis, [[β_{1}]] = 1 or [[β_{2}]] = 1, therefore [[β]] = 1.

Thus, [[φ]] = 1 for all φ ∈ S, and hence S is satisfiable as desired. □

Proof of the Completeness Theorem:

(a) Suppose X is a tautology, and T is some completed tableau with origin F X. Suppose θ is some branch of T which is not closed. Then θ is a Hintikka set by definition, hence satisfiable by the Hintikka Lemma. Thus, there exists some valuation [[−]] which makes θ true. Since F X ∈ θ, we have [[F X]] = 1, hence [[X]] = 0, hence X is not a tautology, a contradiction. It follows that every branch of T is closed.

(b) It is easy to see that for any signed formula φ, there exists a completed tableau with origin φ. For example, such a tableau is obtained by following Strategy 1 or Strategy 2 from Section 1. In particular, if X is a tautology, then there exists a completed tableau with origin F X, which is closed by (a), and hence X is provable by the tableaux method. □

2.4 Discussion of the proofs

We note the following features of the soundness and completeness proofs:

Soundness proof. The proof of soundness essentially proceeds by induction on tableaux, as is evident in the proof of Lemma 2.3. One fixes a valuation, then proves by induction that all derivations respect the given valuation.

This proof method is typical of soundness proofs in general. Compare this proof e.g. to the soundness proof for natural deduction in Lemma 1.5.1 of van Dalen’s book. Most of the time, soundness proofs are relatively easy.

Completeness proof. The central part of any completeness proof is a satisfiability result: for a certain set of formulas, one must show that there exists a valuation making all the formulas true. To see why this is central, notice that the completeness property can be equivalently expressed as follows:

If X is not provable, then X is not a tautology.

Thus, it is natural to start by assuming that X is not provable (e.g., its analytic tableau does not close). Now one must prove that X is not a tautology, which amounts to finding a specific valuation which makes X false. In the case of analytic tableaux, this valuation is obtained using Hintikka’s lemma.

Compare this to the completeness proof for natural deduction in Section 1.5 of van Dalen’s book. It uses a completely different method, yet the central lemma is the one which allows one to construct a valuation, namely Lemma 1.5.11 (every consistent set is satisfiable). The method used for constructing a suitable valuation varies from proof system to proof system, and usually gets more difficult as features are added to the logic.