Soundness and Completeness for SL Trees

In Chapter 5 we introduced a proof system for SL. Trees provide a method for answering the question of whether a given set of SL sentences is jointly satisfiable. Our focus last chapter was on using trees to answer those questions; this chapter we turn to the study of the proof system itself. This chapter engages in a project of metalogic. In particular, we aim to first precisify, then answer, this question: is the tree method a good method?

It might not be obvious at first that there is even a genuine question here. The tree method is a formal method, with precisely defined rules. You might be tempted to think that, by definition, following the rules makes it a good method. There is one sense in which that is right --- the rules laid out last chapter tell you to follow the rules laid out last chapter, so following the rules is doing what the system tells you to do. But there is also a deeper question to be asked. The rules were not selected at random. They were designed to do something in particular: namely, to tell whether a set of sentences is satisfiable. This isn't a question about trees. (Note that we were considering this question back in Chapter 4, before we had even introduced the idea of trees.) So there is a question to be asked about whether the tree method actually does what it's supposed to do.

Recall the distinction between our two turnstiles: we use '𝒳 ⊨ ⊥' to mean that no interpretation satisfies 𝒳; '𝒳 ⊢ ⊥' means that a tree with root closes. We interpret the latter as our proof system saying that nothing satisfies the root. Our question now is, can our proof system be trusted? Is it reliable? The main project of this chapter is to prove in a rigorous way that it can, and is.

6.1 Informal proof

In Chapter 5 we learned a formal proof system. This chapter, we will prove important results about that system. It is important to emphasize, however, that the formal proof system isn't the only way to 'prove' things. In particular, the tree method is not an appropriate methodology for the task of this chapter. When we say we wish to prove that the tree method is good, we don't mean that we will put the negation of that claim --- i.e., that the tree method is not good --- in the root of a tree. That would get us nowhere.

Instead, we will be engaging in an informal proof about the formal system. An informal proof needn't be any less conclusive or compelling than a formal proof is, but evaluating it makes use of our general ability to recognize what follows from what, rather than working through a list of syntactically-defined rules.

6.2 Soundness

If a tree with root 𝒳 closes, we interpret that as the system telling us that 𝒳 is unsatisfiable. If our system is a good one, then a tree will never mislead us in this respect. Tree closure should guarantee unsatisfiability. We call this property soundness. The soundness of our SL tree system is the first important metalogical theorem we will prove in this chapter. (A 'metalogical' theorem is a theorem about logic.)

soundness: If a tree closes, that guarantees that its root is unsatisfiable. In other words: 𝒳 ⊢ ⊥ ⇒ 𝒳 ⊨ ⊥

Here is a way to illustrate that soundness is a substantive result, and to clarify what it is we're trying to prove. Recall the resolution rule for disjunction:

Let's suppose for the purpose of argument that we had a different disjunction rule instead of this one. Suppose, for example, that our rule for disjunction had been this:

If this had been our disjunction rule, and all the other rules remained the same, our tree system would have been unsound. It would have been possible for satisfiable roots to result in closed trees. That is to say, there would have been possible sets of sentences 𝒳 such that 𝒳 ⊢ ⊥, even though it is NOT the case that 𝒳 ⊨ ⊥. Consider for example these sentences:

P
¬P ∨ Q

These sentences are obviously jointly satisfiable, by an interpretation that assigns 1 to P and 1 to Q. But if we used the tree system with the alternate disjunction rule above, the tree would close:

This would be a counterexample to the soundness of the SL tree system. This explains what's wrong with the alternate disjunction rule --- it would allow trees to 'prove' that a root is unsatisfiable, even if it really is satisfiable. In considering the soundness of our system, we are investigating whether our actual proof system is defective in the same way this hypothetical modification of the system would have been. We will prove that it is not.

6.3 Recursive proofs

Our proof of soundness will be a recursive proof. A recursive proof is a proof that proceeds stepwise: one first demonstrates that the claim to be proven holds for some simple case, and then shows that, if it holds for some case, then it also holds for some other, slightly more complicated case. More ways of complicating cases may also be discussed, each along with the assurance that if the claim holds for a simpler case, then it will also hold for each more complex one. Finally, if one can demonstrate that the ways of complicating cases considered are exhaustive --- that is, if these represent the only possible cases --- then this has been shown for every possible case. You may be familiar with recursive proofs already in the context of mathematical induction. (This is a topic that comes up in many high school algebra classes.)

Here is an example illustrating proof by induction. Suppose that Sir Roderic Murgatroyd has been cursed. The curse is subject to the following rules:

1. The only way for someone to escape the curse is to transfer it to someone else.

2. There are only three ways to transfer the curse to someone else:

   1. One may transfer it to one's parent.

   2. One may transfer it to one's child.

   3. One may transfer it to one's sibling.

Given these rules, it's not difficult to see that the Murgatroyd curse will never leave the family. We know that Sir Roderic has the curse. He could transfer it to a parent, a child, or a sibling, but none of those actions would remove the curse from the family, since one's parents, one's children, and one's siblings are all family members. And any of those people, if they had the curse, can only transfer it to someone else within the family. No curse transfer can get the curse outside the family. So someone in the family will remain cursed forever.

Slightly more precisely: we're attempting to prove that the curse will always be in the family. Roderic is in the family. And, for any person, if they are in the family, then they cannot get rid of the curse without transferring it to another member of the family. The proof is perfectly general; it applies to Roderic's great-great-great-grandchildren just as well as it applies to Sir Roderic himself. This is a simple example of a recursive proof. The proof of the soundness of the SL tree method is more complex, but it has the same basic structure.

6.4 Proving soundness

Soundness is the claim that any time a tree closes, the root must be unsatisfiable. This is equivalent to the claim that any time the root is satisfiable, the tree won't close. (Compare: if every new citizen swears loyalty to the Queen, then everyone who doesn't swear loyalty to the Queen must not be a new citizen.) So to prove soundness, we can assume that the root is satisfiable, and show that it follows that the tree doesn't close.

Suppose, then, we have some satisfiable set of sentences 𝒳 in the root of a tree. If the root is satisfiable, then there is some interpretation that satisfies it. (Recall that an interpretation in SL is an assignment of truth values to atomic sentences.) Call this interpretation ℐ. We will begin by proving that, if our tree follows the rules given in Chapter 5, then ℐ doesn't just satisfy the root --- it satisfies every sentence in some branch of the completed tree. Once we establish that claim, it's only a short step to demonstrate that this branch doesn't close. Branches only close when they contain some formula and its negation. But no interpretation can satisfy a formula and its negation; so if ℐ satisfies every formula in the branch, that means that branch must not contain any formula along with its negation. So the tree will remain open.

This is the broad structure of our proof. The key step is in proving that ℐ has the property mentioned above --- that it satisfies every sentence in an open branch. We will prove this recursively.

6.4.1 Root

Start with the root, 𝒳. This is trivial. We are assuming that our tree begins with a satisfiable root, because we are trying to prove what follows from that assumption. (Namely, that the tree won't close.) ℐ is just our name for one of the interpretations we are assuming must exist. So ℐ satisfies everything in the root. This is a reasonable thing to assume, when proving soundness, because soundness only tells us what happens when the root is satisfiable: namely, that the tree won't close. Soundness doesn't say anything about what happens if the root is unsatisfiable.

We want our proof to be perfectly general, so we don't want to make any particular assumptions about what the tree does beyond the root. But, given the resolution rules outlined in §5.4, there are only nine possible ways the tree might develop at each step. (Compare the three possible ways the curse might move in the Murgatroyd example.) We will prove, for each of these nine resolution rules, the following: if ℐ satisfies all the sentences in the branch above, then ℐ also satisfies at least one branch of what comes below. In other words, we'll prove, for each inference rule, that that rule cannot take you from a satisfiable branch to a tree with no satisfiable branches.

6.4.2 Conjunction

Suppose that a tree develops via the conjunction rule:

We assume that ℐ satisfies the branch above the development. So in particular, ℐ must satisfy Φ&Ψ. We may write this as

ℐ(Φ&Ψ) = 1

We know from the definition of truth in SL that any interpretation that assigns 1 to a conjunction must assign 1 to each conjunct. So:

ℐ(Φ) = 1 ℐ(Ψ) = 1

What we've just shown is that, if ℐ satisfies the branch above this development, then it also satisfies everything in the new development. The conjunction rule will never take us from a satisfiable branch to an unsatisfiable one. We need to prove that every possible way of developing the tree is like that.

6.4.3 Negated conjunction

Negated conjunctions develop in our system with a branching rule:

Once again, we are assuming for the purpose of argument that our interpretation ℐ satisfies everything up until this development. So ℐ(¬(Φ&Ψ)) = 1. Since ℐ satisfies that negation, ℐ(Φ&Ψ) = 0. Given our definition of truth in SL, any interpretation that assigns 0 to this conjunction must assign 0 to at least one of its conjuncts. So either ℐ(Φ) = 0 or ℐ(Ψ) = 0. (It might assign 0 to both, but what we know for sure is that it assigns 0 to at least one.) If ℐ(Φ) = 0, then ℐ(¬Φ) = 1, and so the new left branch is satisfied. If ℐ(Ψ) = 0, then ℐ(¬Ψ) = 1, and so the new right branch is satisfied. Since (at least) one of these must be the case, we know that ℐ satisfies at least one branch of our extended tree, assuming it satisfied that which came before the extension. So the negated conjunction rule will never take us from a satisfiable branch to an unsatisfiable one.

6.4.4 Disjunction

Disjunctions branch according to this rule:

Assume ℐ(Φ∨Ψ) = 1. Then either ℐ(Φ) = 1 or ℐ(Ψ) = 1. If ℐ(Φ) = 1, then ℐ satisfies the left branch. If ℐ(Ψ) = 1, then ℐ satisfies the right branch. So, assuming that ℐ satisfies the sentences above this resolution rule, it must satisfy at least one branch below it. So the disjunction rule will never take us from a satisfiable branch to an unsatisfiable one.

Hopefully the pattern is becoming clear by now. We've proven, for three of our nine rules, that they cannot take us from a satisfiable branch to an unsatisfiable one. Six resolution rules remain to be considered.

Consider again the variant disjunction rule hypothesized above:

If we attempted to go through the same reasoning we've been going through, we'd fail. Assume ℐ(Φ∨Ψ) = 1. By the definition of truth in SL, we know that ℐ assigns 1 to at least one of Φ and Ψ, but there is no guarantee that it will satisfy both. So we have no assurance that, if one follows this rule, ℐ will satisfy the development of the tree, even if we assume it satisfies the sentences above. We cannot prove that the use of this rule will never lead to an inappropriate tree closure.

6.4.5 Negated Disjunction

Here is the rule for negated disjunctions:

Suppose that ℐ(¬(Φ∨Ψ)) = 1. Given the definition of negation, this means that ℐ(Φ∨Ψ) = 0. This in turn means, given the definition of disjunction, that ℐ must assign 0 to both Φ and Ψ. And so of course, given the definition of negation again, we know that ℐ assigns 1 to ¬Φ, and also assigns 1 to ¬Ψ. Therefore, if we began with a satisfiable tree branch, invoking this rule, like the other good rules we've considered, will preserve satisfiability; the negated disjunction rule will never take one from a satisfiable branch to an unsatisfiable one.

6.4.6 Conditional

The conditional rule is:

As before, assume that the material above the branch is satisfiable; so some interpretation ℐ satisfies it. Any interpretation that satisfies a conditional must assign 0 to the antecedent, or 1 to the consequent (or both). If ℐ assigns 0 to the antecedent, then it satisfies the left development of the tree. If ℐ assigns 1 to the consequent, then it satisfies the right development of the tree. So, given that it satisfies the conditional, ℐ is guaranteed to satisfy at least one branch of the tree as developed by the conditional rule.

6.4.7 Negated Conditional

The rule given in Chapter 5 for negated conditionals was this:

I hope the procedure is feeling a bit tedious by now. As before, we assume that the negated conditional is satisfiable, and prove that the tree as developed by this rule will remain satisfiable. Since we're assuming that ¬(Φ⊃Ψ) is satisfiable, it follows that some interpretation ℐ satisfies it. But ℐ(¬(Φ⊃Ψ)) only if ℐ(Φ) = 1 and ℐ(Ψ) = 0. So ℐ will satisfy Φ and Ψ. That is to say, it will satisfy the continuation of the branch given this rule. The negated conditional rule can never take one from a satisfiable root to an unsatisfiable tree.

We have three more rules to consider.

6.4.8 Biconditional

Here is the biconditional rule:

Assuming that ℐ satisfies Φ ≡ Ψ, it must either assign 1 to both Φ and Ψ, or it must assign 0 to both Φ and Ψ. If the former, ℐ will satisfy the left branch of the new development from this rule. If the latter, it will satisfy the right branch, since any interpretation that assigns 0 to a sentence must assign 1 to its negation. So this rule too can never take one from a satisfiable root to an unsatisfiable tree.

6.4.9 Negated biconditional

The reasoning is much as before. If our interpretation satisfies the negated biconditional, then it must assign opposite values to each side; i.e., either ℐ(Φ) = 1 and ℐ(Ψ) = 0, or ℐ(Φ) = 0 and ℐ(Ψ) = 1. If the former, ℐ satisfies the left branch; if the latter, ℐ satisfies the right branch. So if the negated biconditional is satisfiable, this rule will never result in an unsatisfiable tree.

6.4.10 Double negation

Here is our final tree resolution rule:

One last time, we assume that we begin with something satisfiable; so we allow that some interpretation ℐ assigns 1 to ¬¬Φ. If it assigns 1 to this negation, then it must assign 0 to its negand, ¬Φ. That is to say, ℐ(¬Φ) = 0. And since it assigns 0 to this negation, it must assign 1 to its negand: ℐ(Φ) = 1. But this just is the new branch development. So if we began with something satisfiable, this rule will result in something satisfiable.

6.4.11 Taking stock

We've shown, for the nine resolution rules in our tree system, that they each have the following important feature: if you begin with a satisfiable set of sentences, applying the rule will always result in at least one continuation of the tree that is also satisfiable. And since these nine rules are the only ways one can develop a tree, we've proven that there is no possible way, consistent with the tree rules, for a tree with a satisfiable root to develop into a tree with no satisfiable branches.

Branches can only be closed if they contain a sentence and its negation, which a satisfiable branch will never have. So, assuming we started with a satisfiable root, the rules will never result in a tree with all branches closed. Satisfiable roots will always result in open trees. The tree method will never erroneously "prove" that a root is unsatisfiable. Equivalently, tree closure guarantees unsatisfiability of the root. The tree method is sound.

If a tree closes, that guarantees that its root is unsatisfiable. In other words: 𝒳 ⊢ ⊥ ⇒ 𝒳 ⊨ ⊥

6.5 Completeness

Soundness is the first of two important metalogical theorems considered in this chapter. The second is completeness. One can think of soundness as a guarantee against a system proving too much; in proving soundness, we were assuring ourselves that a tree would close only if the root was unsatisfiable. Completeness, as the name suggests, concerns whether our system proves enough. We want our system to be sure to close, if the root is unsatisfiable. Remember, we take open branches in completed trees as an indication that the root is satisfiable. Completeness is about ensuring that this is a warranted conclusion.

If a root is unsatisfiable, that guarantees that the tree will close. In other words: 𝒳 ⊨ ⊥ → 𝒳 ⊢ ⊥

Consider the unsatisfiable set of sentences, {¬Q, P&Q}. Given our conjunction rule, a tree with this root will close:

In proving completeness, we wish to demonstrate that this will always be the case: whenever we begin with an unsatisfiable root, the entire tree will eventually close. Notice that if we had a different conjunction rule that called for a branching development instead of a linear one, completeness would fail. Suppose we had this rule:

Using this rule, the tree with root {¬Q, P&Q} would remain open:

The right branch closes, but this tree has a left branch that remains open, even though the root is unsatisfiable. So if we modified our proof system by using this rule instead of the linear rule for conjunction, we would have a system that fails completeness. We wish to prove that, given the actual rules, our system is complete.

6.6 Proving completeness

Completeness is the claim that any time a set of sentences is unsatisfiable, a completed tree with that set as its root will close. This is equivalent to the claim that if a completed tree has a branch that remains open, then the root is satisfiable. To prove completeness, we will assume that a completed tree has a branch that remains open, and prove that, on this assumption, the root is satisfiable. In fact, we will prove something stronger than that: we will prove that every formula in a completed open branch is satisfiable, by demonstrating a recipe for constructing an interpretation that satisfies it. Since the root is part of every branch of the tree, this will suffice for proving completeness.

As in the case of our soundness proof, we will be giving an informal proof about our formal system.

Here is the broad shape of the proof. Suppose that a completed tree has at least one open branch. Then we can construct an interpretation, ℐ, based on that branch, as follows: if any atomic sentence Φ is in the branch, then ℐ(Φ) = 1. If any negated atomic sentence ¬Ψ is in the branch, then ℐ(Ψ) = 0. Let these assignments exhaust ℐ. We can guarantee that there will be a coherent interpretation like this. This recipe for constructing interpretations will fail only if some atomic sentence and its negation are both in the branch. But if a sentence and a negation are both in the branch, then that branch will close; by hypothesis, we're considering a completed branch that remains open. So we know it contains no explicit contradictions of this kind.

Now we want to prove that ℐ satisfies every formula in the branch (including the root). We know it satisfies every atomic formula and every negated atomic formula in the branch, given the way it was constructed. We'll now show that it must satisfy every other formula too. We'll exploit the recursive rules for SL grammaticality: there are only a certain number of ways that sentences can be created from simpler sentences. We'll show, for every sentence form, that if ℐ satisfies a branch downstream of a sentence of that form in a completed branch, then it satisfies that sentence too.

We begin with conjunction.

6.6.1 Conjunction

Suppose our completed, open branch contains a conjunction of the form Φ&Ψ. Since it is a completed branch, this means that the conjunction resolution rule must have been applied to this conjunction. (Remember, a branch isn't completed until every complex formula has a check mark next to it.) So, given the conjunction rule,

we know that the branch must also contain Φ and Ψ. If we assume that ℐ satisfies both these sentences, then we know from the definition of the truth of a conjunction in SL that ℐ satisfies (Φ&Ψ) too. In other words, there's no way to satisfy the simpler sentences that come after this resolution rule, without also satisfying the conjunction.

6.6.2 Negated conjunction

Suppose a negated conjunction appears in the open branch. Since the branch is complete, you know that the negated conjunction rule has been applied:

We are assuming that the negated conjunction is in an open branch. This is consistent with either one of the branches below closing, but they cannot both close. If they did, the negated conjunction would not be in an open branch. So we know that at least one branch is open. So either ℐ(Φ) = 0 (if the left branch is our open branch) or ℐ(Ψ) = 0 (if the right branch is the open branch). Since at least one of these sentences is assigned 0, their conjunction must also be assigned 0, which means the negated conjunction we're considering is assigned 1. So once again, if the material in at least one branch below the resolution rule is satisfied, then the negated conjunction is satisfied too.

6.6.3 Disjunction

Disjunctions are very similar to negated conjunctions. Since the tree is complete, any disjunction Φ ∨ Ψ has a branch below it containing Φ, and one containing Ψ. Whichever of these disjuncts is in the open branch, ℐ satisfies that disjunct, and so satisfies the disjunction too.

6.6.4 Negated disjunction

Negated disjunctions are similar to conjunctions. If a negated disjunction is in an open branch, then the negation of each disjunct is also in that branch. So, suppose that ℐ assigns 0 to each disjunct. Then it also assigns 0 to their disjunction. So once again, if the material below the negated disjunction is satisfied, then so is the negated disjunction itself.

6.6.5 Conditional

If a conditional is in a completed open branch, then it has been resolved by this branching rule:

If the left development is the open branch, then we suppose that ℐ(Φ) = 0, which means that ℐ(Φ⊃Ψ) = 1. If this right development is the open branch, then we suppose that ℐ(Ψ) = 1, which also means that ℐ(Φ⊃Ψ) = 1. So if the material below in at least one branch is satisfied, then the conditional is satisfied too.

6.6.6 Negated conditional

If a negated conditional ¬(Φ⊃Ψ) is in the open branch, then so too are Φ and ¬Ψ. So ℐ(Φ) = 1 and ℐ(Ψ) = 0. So ℐ falsifies the conditional, satisfying the negated conditional.

There are three more kinds of sentences that exist in SL.

6.6.7 Biconditional

Suppose a biconditional is in an open branch. If the branch is completed, then this rule has been performed:

One of these developments is the open branch. If it's the left branch, then, supposing that ℐ assigns 1 to both Φ and Ψ, ℐ must also assign 1 to the biconditional Φ ≡ Ψ. If it's the right branch, then, supposing that ℐ assigns 0 to both Φ and Ψ, this also means that ℐ must also assign 1 to the biconditional Φ ≡ Ψ. So whichever branch is satisfied by ℐ, the biconditional is also satisfied.

6.6.8 Negated biconditional

Exactly the same reasoning as above applies to negated biconditionals, except this time, the branches each assign opposite truth values to Φ and Ψ. So for our interpretation to satisfy either branch, it must falsify the biconditional, thus satisfying the negated biconditional.

6.6.9 Double negation

Finally, suppose there is a double-negated sentence in our completed open branch. Then this rule has been performed:

If ℐ(Φ) = 1, then, given the definition of truth in SL, ℐ(¬Φ) = 0, and ℐ(¬¬Φ) = 1. So once again, if our interpretation satisfies what comes below, then it satisfies the double-negation above.

6.6.10 Summarizing the completeness proof

What we've just shown is that, for any sentence of SL, if it has one of the nine structures just canvassed --- if it's a conjunction, a negated conjunction, a disjunction, etc. --- then, if it is in a completed open branch where the sentences below it are satisfied by ℐ, then it too is satisfied by ℐ. Given the way that ℐ was selected, we know that ℐ must satisfy every atomic sentence, and every negated atomic sentence, in the open branch. And since the nine structures considered are the only ways to develop more complex sentences, this implies that every SL sentence in the open branch is satisfied by ℐ. This includes the root. Since interpretation ℐ satisfies the root, this of course means that the root is satisfiable. That is to say, if a completed branch remains open, this guarantees that the root is satisfiable. Equivalently, if the root is unsatisfiable, a completed tree is guaranteed to close. Completeness is proven.

6.7 Testing alternate rules

We can use the reasoning involved in the soundness and completeness proofs above to consider various alternative tree rules. We saw one example of this here [insert link], when we observed that an alternate, linear rule for disjunctions would result in an unsound tree system. Here again was the rule we considered:

Note, however, that if we think through the completeness reasoning, we'll find that the completeness proof would still hold. If we assume that some interpretation ℐ satisfies both Φ and Ψ, we can be assured that it also satisfies the disjunction Φ ∨ Ψ. So changing the disjunction rule to this linear one would not interfere with the completeness of our tree system. Our trees would still close any time they began with unsatisfiable roots. But as we saw on [insert link], the soundness proof would fail, which is why a system with this rule could start in a satisfiable root, and result in a closed tree.

When either the soundness or the completeness proof fails, you know you are working with an inappropriate rule. To conclusively demonstrate this, you can provide a counterexample to the failed metalogical theorem. A counterexample to soundness would be a tree with a satisfiable root that closes. A counterexample to completeness would be a completed tree, with an unsatisfiable root, that remains open. The rule above violates soundness, so using that rule we can construct a tree with a satisfiable root, that closes. Constructing the right counterexample takes a bit of thought. The rule puts both disjuncts into a single branch below, and we want it to close, despite having a satisfiable root. So adding the negation of just one of the disjuncts to the root will close the tree, without making the root unsatisfiable:

This tree is a counterexample to soundness, using the hypothetical rule mentioned above. Note that a counterexample is a tree that uses SL sentences, not the Greek letters Φ and Ψ that we use in the statements of the rules.

Let's work through one more example. Suppose we changed the conjunction rule to this one:

Would our system still be sound? To answer this, we assume that the conjunction Φ&Ψ is satisfiable, and ask whether this guarantees that at least one branch below is also satisfiable. It does. (In fact, both branches are guaranteed to be satisfiable.) So the system will still be sound.

Would the system still be complete? To answer this, we ask whether each branch is such that, if we assume that an interpretation satisfies the developments below, it is guaranteed to satisfy the conjunction above. Begin with the left branch. If some interpretation satisfies both Φ and Ψ, then it will certainly satisfy the conjunction Φ&Ψ. So that branch looks fine. (Indeed, that branch is exactly the same as the linear development of our actual conjunction rule, so this reasoning is the same as that on above.)

But what of the right branch? Assume that some interpretation satisfies Ψ; does that guarantee that it satisfies Φ&Ψ? Certainly not. So if the right branch is our open branch, a completed tree using this rule may remain open, even if its root is unsatisfiable. Completeness will be violated. Let's construct a counterexample of that form. We want a tree that includes a conjunction, whose root is unsatisfiable, but whose right branch remains open. Notice that the right branch 'ignores' the first conjunct; this is a clue that a good way to construct a counterexample will be to locate the unsatisfiability within that first conjunct. Suppose, for example, that we let Φ itself stand for a contradiction. If so, any conjunction with Φ as a conjunct will be unsatisfiable. But if Ψ is not a contradiction, then a tree with root Φ&Ψ will remain open. Let's develop a tree with this root: (P≡¬P)&Q. Note that this sentence has a contradictory first conjunct, and a contingent, atomic second conjunct.

The left branch closes after we perform the unchanged biconditional rule on the contradictory first conjunct, but the right branch remains open. Since this is a completed tree with an open branch and an unsatisfiable root, it is a counterexample to completeness.

Remember that we are considering a modification to the tree system that uses a different conjunction rule. In this example I used P ≡ ¬P as my Φ, which let me use the unchanged biconditional rule. But if I had used a contradiction that used a conjunction, like P&¬P, I would have had to have used the revised rule within the left branch too.

It is also possible to construct counterexamples using simpler sentences if you add to the root. Instead of introducing a contradictory conjunct, we could have simply added to the root, in a way that makes the root unsatisfiable, but leaves the right branch open. Suppose for instance we put both P&Q and ¬P in the root. Then we'd have an unsatisfiable root, but the right branch would remain open:

This too is a counterexample to completeness, given the rule in question. So we see here two different kinds of strategies for generating counterexamples to completeness.

Practice Exercises

Part A Following are possible modifications to our SL tree system. For each, imagine a system that is like the system laid out in this chapter, except for the indicated change. Would the modified tree system be sound? If so, explain how the proof given in this chapter would extend to a system with this rule; if not, give a tree that is a counterexample to the soundness of the modified system.

1. Change the rule for conjunctions to this rule:

1. Change the rule for conjunctions to this rule:

1. Change the rule for conjunctions to this rule:

1. Change the rule for disjunctions to this rule:

1. Change the rule for disjunctions to this rule:

1. Change the rule for conditionals to this rule:

1. Change the rule for conditionals to this rule:

1. Change the rule for biconditionals to this rule:

1. Change the rule for disjunctions to this rule:

(This would mean that one can put whatever SL sentence one likes in the rightmost branch.)

Part B For each of the rule modifications given in Part A, would the modified tree system be complete? If so, explain how the proof given in this chapter would extend to a system with this rule; if not, give a tree that is a counterexample to the completeness of the modified system.