Skip to main content
Humanities LibreTexts

3.13.2: Soundness for Derivations- Formal Details

  • Page ID
    1885
  • \( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)\(\newcommand{\AA}{\unicode[.8,0]{x212B}}\)

    The straightforward but messy procedure in our present case is to do a double induction. One defines the complexity of a derivation as the number of levels of subderivations which occur. The inductive property is that all derivations of complexity n are sound. One then assumes the inductive hypothesis, that all derivations with complexity less than n are sound, and proves that all derivations of complexity n are sound. In this last step one does another induction on the number of lines of the derivation. This carries out the informal thinking developed in the last section. It works, but it's a mess. A different approach takes a little work to set up but then proceeds very easily. Moreover, this second approach is particularly easy to extend to predicate logic.

    This approach turns on a somewhat different way of characterizing the truth preserving character of the rules, which I call Rule Soundness, and which I asked you to explore in exercises 10-4, 10-5, and 10-6. One might argue about the extent to which this characterization corresponds intuitively to the idea of the rules being truth preserving. I will discuss this a little, but ultimately it doesn't matter. It is easy to show that the rules are truth preserving in the sense in question. And using the truth preserving character thus expressed, proof of soundness is almost trivial.

    194 Sowrdness and Compkteness for Sentence Logic Derivations 13-2. Soundness for Derivations: Fd Details 195 Here is the relevant sense of rule soundness, illustrated for the case of &I. Suppose we are working within a derivation with premises Z. Suppose we have already derived X and Y. Then we have ZtX and ZtY. &I then licenses us to conclude X&Y. In other words, we can state the &I rule by saying

    &I Rule: If ZtX and ZtY, then ZtX&Y.

    There is a fine point here, about whether this really expresses the &I rule. The worry is that 'ZtX' means there exists a derivation from Z to X, and 'ZtY' means that there exists a derivation from Z to Y. But the two derivations may well not be the same, and they could both differ extensively from some of the derivations in virtue of which 'ZtX&Y' is true.

    For sentence rules, this worry can be resolved. But it's really not important because, as with rule soundness, this way of stating the rules will provide us with all we need for the soundness proof. We proceed by introducing the sense in which the &I rule is sound. We do this by taking the statement of the rule and substituting 'k' for 't':

    L7 (Soundness of &I): If Z~X and Z~Y, then Z~X&Y.

    Why should we call this soundness of the &I rule? First, it has the same form as the rule &I. It is the semantic statement which exactly parallels the syntactic statement of the &I rule. And it tells us that if we start with any interpretation I which makes the premises Z true, and if we get as far as showing that X and Y are also true in I, then the conjunction X&Y is likewise true in I.

    In particular, you can show that L7 directly implies that &I is truth preserving in the original sense by looking at the special case in which Z = {X,Y}. {x,Y}~x and {X,Y}~Y are trivially true. So L7 says that {x,Y}~x&Y, which just says that any interpretation which makes X true and also makes Y true makes the conjunction X&Y true.

    We treat the other sentence rules in exactly the same way. This gives

    L8 (Soundness of &E: If z~x&Y, then Z~X; and if Z~X&Y, then Z~Y.

    L9 (Soundness of vI): If ZkX, then Z~XVY; and if Z~Y, then Z~XVY.

    L10 (Soundness of vE): If Z~XVY and Zk-X, then Z~Y; and if Z~XVY and Zk - Y, then ZkX.

    L11 (Soundness of -E): 1f Zk--x, then Z~X.

    L12 (Soundness of 3E: If Z~X~Y and Z~X, then Z~Y.

    L13 (Soundness of =I): If Z~X~Y and Z~Y~X, thenZ~XEY.

    L14 (Soundness of =E): If Z~XEY, then Z~X~Y; and if Z~X~Y, then zky3x.

    EXERCISES 13-3. Prove lemmas L7 to L14. Note that in proving these you do not need to deal with t at all. For example, to prove L7, you need to show, using the antecedent, that Z~X&Y. So you assume you are given an I for which all sentences in Z are true. You then use the antecedent of L7 to show that, for this I, X&Y is also true. 13-4. In this problem you will prove that for sentence rules, such as the rules described in L7 to L14, what I have called rule soundness and the statement that a rule is truth preserving really do come to the same thing. You do this by giving a general expression to the correspondence between a syntactic and a semantic statement of a rule:

    Suppose that X, Y, and W have forms such that

    (i) (VI){[Mad(I,X) & Mod(I,Y)] 3 Mod(I,W)}.

    That is, for all I, if I makes X true and makes Y true, then I makes W true. Of course, this won't be the case for just any X, Y, and W. But in special cases, X, Y, and W have special forms which make (i) true. For example, this is so if X = U, Y = UIV, and W = V. In such cases, thinking of X and Y as input sentences of a rule and W as the output sentence, (i) just says that the rule that allows you to derive W from X and Y is truth preserving in our original sense.

    Now consider

    (ii) If Z~X and ZkY, then Z~W.

    This is what I have been calling soundness of the rule stated by saying that if ZtX and ZtY, then ZtW. (ii) gives turnstyle expression to the statement that the rule which licenses concluding W from X and Y is truth preserving.

    Here is your task. Show that, for all X, Y, and W, (i) holds iff and (ii) holds. This shows that for sentence rules (rules which have only sentences as inputs) the two ways of saying that a rule is truth preserving are equivalent. Although for generality, I have expressed (i) and (ii) with two input sentences, your proof will work for rules with one input sentence. You can show this trivially by letting Y = Av-A for rules with one input sentence.

    I have not yet discussed the two subderivation rules, 31 and -I. Soundness of these rules comes to

    L15 (Soundness of >I): 1f ZU{X}~Y, then ZkX>Y.

    L16 (Soundness of -I): 1f ZU{X)~Y and ZU{X}~-Y, then Zk-X.

    In the case of >I and -I there is a more substantial question of whether, and in what sense, L15 and L16 also express the intuitive idea that these rules are truth preserving. The problem is that the turnstyle notion makes no direct connection with the idea of subderivations. Thus, if the syntactic counterpart of L15 is assumed (if ZU{X}kY, then ZkX>Y), it is not clear whether, or in what sense, one can take this to be a statement of the >I rule. (The converse is clear, as you will show in exercise 13-6.) However, this issue need not sidetrack us, since L15 and L16 will apply directly in the inductive proof, however one resolves this issue. EXERCISES 13-5. Prove L15 and L16. 13-6. Prove that if the system of derivations includes the rule >I, then if ZU{X}kY, then ZkX>Y. Also prove that if the system of derivations includes the rule -I, then if both ZU{X}kY and ZU{X}k-Y, then Zk-X.

    We are now ready to prove T5, soundness for derivations. Here is an outline of the proof: W; will start with an arbitrary derivation and look at an arbitrary line, n. We will suppose that any interpretation which makes governing premises and assumptions true makes all prior lines true. Rule soundness will then apply to show that the sentence on line n must be true too. Strong induction will finally tell us that all lines are true when their governing premises and assumptions are true. The special case of the derivation's last line will constitute the conclusion we need for soundness.

    To help make this sketch precise, we will use the following notation:

    X,, is the sentence on line n of a derivation. Z, is the set of premises and assumptions which govern line n of a derivation.

    Now for the details. Suppose that for some Z and X, ZkX. We must show that Z~X. The assumption ZkX means that there is some derivation with premises a subset of Z, final conclusion X, and some final line number which we will call n*. The initial premises are the sentences, Z,., governing the last line, n*; and the final conclusion, X, is the sentence on the last line, which we are calling X,.. We will show that z,.~x,.. This will establish ZkX because X,,. = X and Z,. is a subset of Z. (Remember exercise 10-10.)

    We will establish Z,.kX,. by showing that z,kX, for all n, 1 5 n 5 n*. And in turn we will establish this by applying strong induction. We will use the

    Inductive property: &k&.

    and the

    Inductive hypothesis: ZikX, holds for ail i < n.

    So let's consider an arbitrary line, n, and assume the inductive hypothesis. What we have to do is to consider each of the ways in which line n might be justified and, applying the inductive hypothesis, show that the inductive property holds for line n. First, X,,

    might be a premise or an assumption. Notice, by the way, that this covers the special case of the first line (n = l), since the first line of a derivation is either a premise or, in the case of a derivation with no premises, the assumption of a subderivation. But if X,, is a premise or assumption, X,, is a member of Z,. Therefore, z,~x,.

    Next we consider all the sentence rules. I'll do one for you and let you do the rest. Suppose that X,, arises by application of &I to two previous lines, Xi and Xj, so that X,, = X,&X,. By the inductive hypothesis

    4k~i and Zjk% (Inductive hypothesis)

    Since we are dealing with a sentence rule, Xi, Xj, and X,, all occur in the same derivation. Consequently, Zi = Zj = Z,. So

    Z,kxi and Z,kxj.

    This is just the antecedent of lemma 7, which thus applies to the last line to give z,kX,,.

    EXERCISE 13-7. Apply lemmas L8 to L14 to carry out the inductive step for the remaining sentence rules. Your arguments will follow exactly the same pattern just illustrated for &I.

    Turning to the other rules, suppose that X, arises by reiteration from line i. That is just to say that X,, = Xi. We have as inductive hypothesis that zikxi. If lines i and n are in the same derivation, Z, = Zi, so that z,kX,,, as we require. If we have reiterated Xi into a subderivation, Z, 198 Soundness and Completeness for Sentence Logic Derivations 13-3. Completeness fm Dm'votionr: Znfd Zntruduetion 199 differs from Zi by adding the assumption of the subderivation (or the assumptions of several subderivations if we have reiterated several levels down). That is, Zi is a subset of Z,. But as you have shown in exercise 10- 10, if ~~1% and Zi is a subset of Z,, then z,kX,.

    Now suppose that X,, arises by >I. Then on previous lines there is a subderivation, beginning with assumption Xi and concluding with Xj, so that X,, = Xi>Xj. By inductive hypothesis,

    zjkxj (Inductive hypothesis for line j)

    The trick here is to notice that the subderivation has one more assumption than Z,. Though not perfectly general, the following diagram will give you the idea:

    Set of Premises and Assumptions

    When we start the subderivation with the assumption of Xi, we add the assumption Xi to Z, to get Zi = Z,U{XJ as the total set of premises and assumptions on line i. When we get to line n and discharge the assumption of Xi, moving back out to the outer derivation, we revert to Z, as the set of governing premises and assumptions.

    Since Zj = Z,u{Xi), we can rewrite what the inductive hypothesis tells us about line j as

    But this is just the antecedent of lemma L15! Thus lemma L15 immediately applies to give z,kXi>Xj, or z,~x,, since X, = Xi>Xj.

    13-8. Carry out the inductive step for the case in which X, arises by application of -I. Your argument will appeal to lemma L16 and proceed analogously to the case for >I.

    We have covered all the ways in which X,, can arise on a derivation. Strong inducton tells us that z,kX,, for all n, including n*, the last line of the derivation. Since Z,* is a subset of Z and X,. = X, this establishes ZkX, as was to be shown.

    Contributors and Attributions

    • Paul Teller (UC Davis). The Primer was published in 1989 by Prentice Hall, since acquired by Pearson Education. Pearson Education has allowed the Primer to go out of print and returned the copyright to Professor Teller who is happy to make it available without charge for instructional and educational use.


    3.13.2: Soundness for Derivations- Formal Details is shared under a not declared license and was authored, remixed, and/or curated by LibreTexts.

    • Was this article helpful?