Soundness and Completeness for QL Trees

In Chapter 6 we proved that our SL tree method works the way it is supposed to: any tree that closed was guaranteed to have a root that was unsatisfiable in SL, and any completed tree that remained open was guaranteed to describe an SL model that satisfies the root. These two theorems together are called soundness and completeness.

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

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

These definitions were first given in sections 6.2 and 6.5. They are equally applicable to our extended tree system for QL. The system introduced in Chapter 10 is also sound and complete. The rules are designed in a way so as to guarantee that if the tree closes, there is no model for the root (sound), and to guarantee that an open branch describes a model for the root (complete). The proofs for these two theorems are structurally very similar to the proofs given in Chapter 6.

11.1 Soundness

If our tree method is sound, then there is no possible set of QL sentences that are satisfiable, where a tree with root closes. Not every possible tree method is sound. For example, suppose we dropped the requirement, for a negated universal, that one take an instance with a new name.

In other words, suppose we replaced this rule (introduced in Chapter 10)

with this alternate one:

If we had this rule, there would be counterexamples to soundness---trees with satisfiable roots, which nevertheless closed. Here is an example:

This tree is a counterexample to the soundness of the alternate tree system just described. To prove that our system is sound is to prove that our actual rules do not allow for this kind of tree. To prove this, we'll begin by assuming that is satisfiable, and demonstrate from that assumption that at least one branch of any tree that develops according to our rules will remain open. As in the case of the parallel discussion in Chapter 6, our proof will be a recursive one. We will demonstrate that, if the tree starts with a set of satisfiable sentences, then, for each legal way the tree may develop, at least one branch will continue to have a set of satisfiable sentences. This is effectively to show that such a branch will never close, since branches only close when they contain some sentences and , which are of course never jointly satisfiable.

Suppose, then, we have some satisfiable set of sentences in the root of a tree. If the root is satisfiable, then there is some model that satisfies it. Call this interpretation ℐ. We prove that, if our tree follows the rules given in Chapter 10, then ℐ doesn't just satisfy the root --- it satisfies every sentence in any completed branch. We will prove this recursively.

Root

We assume that the tree begins with a satisfiable root. Given this assumption, ℐ is just our name for one of the interpretations we are assuming must exist. So ℐ trivially satisfies everything in the root.

Now we must prove, for each possible way of developing the tree, that if the sentences in the branch we begin with are satisfiable, then the sentences we have after applying the rule are satisfiable too. There are thirteen possible ways a tree can develop, corresponding to the thirteen kinds of non-atomic sentences in QL, each of which has a particular processing rule. The thirteen kinds of sentences are:

• double negation

• conjunction

• negated conjunction

• disjunction

• negated disjunction

• conditional

• negated conditional

• biconditional

• negated biconditional

• existential

• negated existential

• universal

• negated universal

Fortunately, we've already proven what we need to prove for the first nine items on the list. Our QL tree method uses all the same rules as the SL method did for the sentential connectives; we proved in §6.4, for each of those rules, that it has the key property: if some interpretation ℐ satisfies what comes above the rule, then the development below it is also satisfiable. (Indeed, we proved there that the very same interpretation, ℐ, satisfied it.)

So to extend our soundness proof to our QL system, we need only prove the same thing for the four rules for quantifiers. This is the project of the next four subsections.

Existentials

Suppose some satisfiable set of QL sentences 𝒳 𝒳 is developed according to the existential rule:

We assume that ℐ models 𝒳, which includes some existential ∃𝓍Φ. We want to prove that there is a model for the expanded branch which comprises both 𝒳 and Φ[𝓍⇒a], i.e., 𝒳 ∪ Φ[𝓍⇒a] (the set containing and the new development sentence too). Unlike in the parallel proof for the sentential rules, we cannot assume that ℐ itself satisfies our new development, because our new development introduces a new name; we cannot assume that ℐ included any assignment for the new name a. Nor, if it did, are we sure that the object a denotes satisfies Φ. But we can be assured that ℐ can be expanded into a new, similar interpretation, ℐ^*, which does include a. Moreover, since we know that ℐ satisfied the existential ∃𝒳Φ, we know that there was some object in ℐ's domain that satisfied Φ. So it will be possible to construct our new interpretation ℐ^* so that it includes the new name, and assigns it to that object. This will ensure that ℐ^*(Φ[𝓍⇒a]) = 1. And since ℐ^* is just like ℐ with respect to everything other than a--- and since we are assured that a was not in 𝒳 (the rule requires that it be new) --- ℐ^* will satisfy 𝒳 in just the same way that ℐ did.

This will be clearer with an example. Suppose ∃xFx is part of a satisfiable set of sentences. So assume that ℐ interprets it. The tree resolution for rule for existentials requires that one take an instance corresponding to a new name. Suppose this is done thus:

We cannot simply say that since some model ℐ satisfies the existential ∃xFx, it thereby must also satisfy Fa; plenty of interpretations satisfy the former while falsifying the latter. But what we can say, since a is a new name, with no previous commitments specific to it earlier in the tree, is that we can construct a model ℐ^* that satisfies every sentence above in the tree (in this case, just the one existential), and that also satisfies the new development (in this case, Fa). We do so by assigning the name a to refer to some object that is F in ℐ. We’re sure there is such an object there because it is stipulated that ℐ satisfies the existential.

In general, assuming that ℐ satisfies every sentence in a branch before the existential rule is performed, there is guaranteed to be a new interpretation, ℐ^*, which is an extension of ℐ that includes a new name attached to an object in the UD satisfying the existential, which satisfies everything in the branch up to the point after the existential rule is performed. That is to say, like the nine sentential rules considered in Chapter 6 , the existential rule can never take you from a satisfiable branch to an unsatisfiable one.

Universals

Suppose a branch of a tree uses the rule for universals:

Assume that the set of QL sentences 𝒳 above this development is satisfiable. Then some model ℐ makes it true. The universal rule allows an instance to be developed using any name, so, as before, we cannot guarantee that ℐ makes the development true, because ℐ may or may not interpret the name a; but as before, we can be assured if it doesn’t, we can extend the interpretation to include it. So consider a new model ℐ^*, which includes the name a. If a wasn’t interpreted by ℐ, then it can be assigned to any element of the UD. Since the rest of ℐ is unchanged, and since ℐ(∀𝓍Φ) = 1, we know that our new extended interpretation will satisfy Φ[𝓍⇒a] too.

That is to say, once again, if we assume that ℐ satisfies every sentence in a branch before the universal rule is performed, there is guaranteed to be a model --- either the very same one, ℐ, or a modification of it, ℐ^*, which assigns a new name to any object in the UD, which satisfies everything in the branch up to the point after the universal rule is performed. In other words, the universal rule can never take you from a satisfiable branch to an unsatisfiable one.

Note that the fact that we can perform this rule multiple times does not interfere with the soundness proof. We have proven that each time you perform it, you are guaranteed not to switch from a satisfiable branch to an unsatisfiable one. So no matter how many times you take an instance of a universal, you won't be able to go from a satisfiable set of sentences to an unsatisfiable one.

Negated Existential

The reasoning behind soundness for the negated existential rule is exactly parallel to that for the universal rule. We begin by assuming that some negated universal ¬∃𝓍Φ, is satisfied by ℐ. Here is the rule for negated existentials:

We want to prove that the result of this rule is also satisfied, either by ℐ itself (if a was interpreted in ℐ), or by an extension of it ℐ^*, that preserves the satisfaction of everything above (if a was a new name). Since ℐ satisfies ¬∃𝓍Φ, it makes every substitution instance for 𝓍 of Φ false. If a was interpreted by ℐ already, then ℐ(Φ[𝓍⇒a]) = 0. If it wasn’t, the new model ℐ^* will assign the new name to some object in the UD of the original model; since no object in that model satisfied Φ, ℐ^*(Φ[𝓍⇒a]) = 0. Either way, our interpretation falsifies Φ[𝓍⇒a], and so satisfies that sentence’s negation, which is the continuation of the branch.

So this rule too can never take us from a satisfiable set of QL sentences to an unsatisfiable one.

Negated Universal

Negated universals are similar to existentials. Assume that a negated universal is part of a set of sentences satisfied by ℐ, and that this rule is then applied:

Construct a new interpretation ℐ^*, which differs from ℐ only in that it includes an interpretation of the new name a, and assigns that name to some object that falsifies Φ. We know there is at least one such object because we are assuming that ℐ satisfies the negated universal. Then our new interpretation ℐ^* satisfies the new development of the branch. It also satisfies everything above the branch, just like ℐ did, because nothing above the branch included the name a.

That last bit of reasoning relied centrally on the requirement that we're taking a new name. We saw in the introduction to this chapter that if we do not include that requirement, soundness would be violated.

Summarizing the soundness proof

We have now shown, for our four quantifier rules, that each of them has the following property: you can never start with a branch that is satisfiable, and use that rule to extend that branch into one that is unsatisfiable. Since we've also shown that the nine sentential rules also have this property, we've effectively shown that there is no possible way to start with a satisfiable set of sentences and develop the branch into one that is not satisfiable. This in turn means that if the branch starts with a satisfiable set of sentences, the branch will never close. But that's just what soundness says: if the root is satisfiable, the tree is guaranteed to remain open. Soundness is proven.

11.2 Completeness

Completeness says that if a branch of a completed tree remains open, then the root is satisfiable. We prove this by assuming that we have an open completed branch, and use it to construct an interpretation that satisfies every sentence in that branch, which includes the root. The proof for completeness of our QL tree system is structurally just like the one given in Chapter 6.

Given a completed open branch, we construct a model ℐ, based on that branch, as follows: for any predicate ℱ, if some QL atom ℱa₁, …, a_n is in the branch --- i.e., if P or Fa or Rab is in the branch --- then ℐ makes that atom true, ℱ by putting <a₁, …, a_n> in the extension of ℱ.And if ¬ℱa₁, …, a_n is in the branch, ℐ excludes <a₁, …, a_n> from the extension of ℱ, thus making the negation of the atom true. This is of course just the way that we construct interpretations from open branches of completed trees.

Now we will prove, for every sentence in QL, that if it is in the open branch, it is made true by ℐ. The QL atoms trivially meet this criterion --- ℐ was designed precisely to satisfy them. We will prove by induction that every possible QL sentence also meets this criterion. In §6.6 we showed, for each propositional connective, if you construct a more complex SL sentence out of simpler SL sentences that have this criterion, the more complex one will too. That proof carries on unchanged here. So it remains only to show that the same is true of our four quantifier rules.

Existential

Consider an existential --- a QL sentence of the form ∃𝓍Φ. We need to prove that if it is in the open, completed branch, ℐ satisfies it. Since the branch is complete, we know that the existential rule has been performed to resolve this sentence. So the branch includes a substitution instance of Φ that used a new name. For our present purposes, it doesn't actually matter whether the name was new --- the fact that there is some instance of Φ in the branch already is enough to prove what we need to prove. Since there is an instance of Φ in the branch, if it is satisfied by ℐ, the existential ∃𝓍Φ must be satisfied by ℐ too.

So, just as we showed for the nine sentential rules, the existential rule has this important property: in a completed tree, any interpretation that satisfies the simpler sentences below the existential development, must also satisfy the existential above it.

Universal

Suppose a universal sentence ∀𝓍Φ appears in a completed open branch. Since the branch is complete, that means that, for every name a in the branch, Φ[𝓍⇒a] is also in the branch. We therefore assume that ℐ satisfies each Φ[𝓍⇒a]; so ℐ must also satisfy ∀𝓍Φ. Because the UD for ℐ includes only those names that occur in the branch, every instance of Φ is included, so the universal is true.

Once again, any interpretation that satisfies everything below the universal development, must also satisfy the universal above it.

Negated Existential

Negated existentials work just like universals. If ¬∃𝓍Φ is in a completed open branch, then for every name a in ℐ, ¬Φ[𝓍⇒a] is below it in the branch. And if ℐ satisfies each of these negations, it will also satisfy the negated existential.

Negated Universal

Negated universals work just like existentials. If ¬∀𝓍Φ is in the branch, then some instance of the negation is in the branch below. If ℐ satisfies some instance of ¬Φ, then, given the definition of truth for negation and universals in QL, it will also satisfy ¬∀𝓍Φ.

Summarizing the completeness proof

The sentence shapes just considered, combined with the nine shapes considered in §6.6, correspond to all the possible QL sentences. So we have proven that, for any possible QL sentence , if an interpretation satisfies the simpler sentences below it in the branch, that interpretation also satisfies itself. Since we also have a recipe for constructing an interpretation ℐ that is guaranteed to satisfy the atoms, we can prove by induction that it can satisfy everything in the branch, including the root. A completed open branch guarantees a satisfiable root. Completeness is proven.

Part A

Following are possible modifications to our QL 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 existentials to this rule:

1. Change the rule for existentials to this rule:

1. Change the rule for existentials to this rule:

1. Change the rule for universals to this rule:

1. Change the rule for existentials to this rule:

1. Change the rule for universals to this rule:

1. Change the rule for conjunction to this rule:

1. Change this requirement (given in section 10.10)...

A branch is complete if and only if either (i) it is closed, or (ii) every resolvable sentence in every branch has been resolved, and for every general sentence and every name a in the branch, the a instance of that general sentence has been taken.

... to this one:

A branch is complete if and only if either (i) it is closed, or (ii) every resolvable sentence in every branch has been resolved, and for every general sentence, at least one instance of that general sentence has been taken.

1. Change the branch completion requirement to:

...and for every general sentence and every name a that is above that general sentence in the branch, the a instance of that general sentence has been taken.

1. Change the branch completion requirement to:

...and for every general sentence and every name a in the branch, the a instance of that general sentence has been taken, and at least one additional new instance of that general sentence has also been taken.

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.

1. Change the rule for existentials to this rule:

1. Change the rule for existentials to this rule:

1. Change the rule for existentials to this rule:

1. Change the rule for universals to this rule:

1. Change the rule for existentials to this rule:

1. Change the rule for universals to this rule:

1. Change the rule for conjunction to this rule:

1. Change this requirement (given in section 10.10)...

A branch is complete if and only if either (i) it is closed, or (ii) every resolvable sentence in every branch has been resolved, and for every general sentence and every name a in the branch, the a instance of that general sentence has been taken.

... to this one:

A branch is complete if and only if either (i) it is closed, or (ii) every resolvable sentence in every branch has been resolved, and for every general sentence, at least one instance of that general sentence has been taken.

1. Change the branch completion requirement to:

...and for every general sentence and every name a that is above that general sentence in the branch, the a instance of that general sentence has been taken.

1. Change the branch completion requirement to:

...and for every general sentence and every name a in the branch, the a instance of that general sentence has been taken, and at least one additional new instance of that general sentence has also been taken.