Skip to main content
Humanities LibreTexts

3.15.3: Soundness for Predicate Logic Derivations

  • Page ID
    1900
  • \( \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}}\)

    To extend the proof for sentence logic, we need to prove rule soundness for the four new predicate logic rules. Two are easy applications of definitions and lemmas given in section 15-1:

    L33 (Soundness for 31): If Zk~(s), then Zk(3u)~(u,s),where (3u)P(u,s) is an existential generalization of P(s), that is, P(u,s) results from P(s) by replacing any number of occurrences of s with u.

    L34 (Soundness for VE): If z~(vu)P(u), then ZkP(s), where P(s) is a substitution instance of (Vu)P(u), that is, s is substituted for all free occurrences (

    EXERCISES 15-20. Apply lemma L30 to prove lemma L33. 15-2 1. Apply lemma L3 1 to prove lemma L34.

    Let's look at VI in a bit more detail. We want to prove

    L35 (Soundness for VI): Assume that the name s does not occur in Z or in (Vu)P(u). On this assumption, if ~kP(s), then Zk(Vu)P(u), where (Vu)P(u) is the universal generalization of P(s), that is, P(u) results by replacing all occurrences of s in P(s) with u.

    Let's consider an arbitrary interpretation, I, in which all the sentences in Z are true. What will it take for (Vu)P(u) to be true also in I? Lemma L28 tells us that given any name, s, not appearing in (Vu)P(u), we need only show that P(s) is true in all s-variants of I. What we need to do is squeeze the conclusion that P(s) is true in all the s-variants of I out of the assumption that Z~P(S) and the hypothesis that Mod(1.Z).

    But this is easy. The assumption that s does not occur in Z allows us to apply lemma L25 as follows: I is a model for Z. Since s does not occur in Z, L25 tells us that any s-variant of I is also a model of Z. Then the assumption that ~kP(s) tells us that any s-variant of I makes P(s) true.

    You should carefully note the two restrictions which play crucial roles in this demonstration. In order to apply lemma L25, s must not appear in Z. Also, in order to apply lemma L28, s must not appear in (Vu)P(u). The latter restriction is encoded in the VI rule by requiring that (Vu)P(u) be the universal generalization of P(s).

    In a similar way, the restrictions built in the 3E rule play a pivotal role in proving

    L36 (Soundness for 3E): Assume that s does not appear in Z, in (3u)P(u), or in X. Then if ZU{(~U)P(U),P(~))~X, then ZU{(~U)P(U)}~X.

    You will immediately want to know why the restrictions stated in L36 are not the same as the restriction I required of the 3E rule, that s be an isolated name. If you look back at section 5-6, you will remember my commenting that requiring s to be an isolated name involves three more specific requirements, and that other texts state the 3E rule with these three alternative requirements. These three requirements are the ones which appear in the assumption of L36. Requiring that s be an isolated name is a (superficially) stronger requirement from which the other three follow. Since we are proving soundness, if we carry out the proof for a weaker requirement on a rule, we will have proved it for any stronger requirement. You can see this immediately by noting that if we succeed in proving L36, we will have proved any reformulation of L36 in which the assumption (which states the requirement) is stronger.

    Of course, by making the requirement for applying a rule stronger (by making the rule harder to apply), we might spoil completeness-we might make it too hard to carry out proofs so that some valid arguments would have no corresponding proofs. But when we get to completeness, we will check that we do not get into that problem.

    Let's turn to proving L36. The strategy is like the one we used in proving L35, but a bit more involved. Assume that I is a model for Z and (3u)P(u). Since s does not appear in (3u)P(u), there is an s-variant, I, of I, such that P(s) is true in I,. Since s does not appear in (3u)P(u) or in Z, and since I and I, differ only as to s, lemma L25 tells us that (3u)P(u) and 236 Zntcrpretationr, Soundness, and Completeness for Predicate Logic 154. Completeness for Predicate Logic Derivations 237 Z are also true in I,. The hypothesis, that ZU{(~U)P(U),P(S)}~X, then tells us that X is true in I,. Finally, since s is assumed not to appear in X and I and I, differ only as to s, lemma L25 again applies to tell us that X is true in I.

    The soundness of the quantifier rules immediately gives us

    T14 (Soundness for predicate logic derivations): For any set of sentences, Z, and sentence, X, if ZkX, then Z~X.

    The proof is a trivial extension of the proof for sentence logic, but to fix the ideas you should carry out this extension.

    EXERCISE 15-22. Prove T14. You only need to extend the inductive step in the proof of T5 to cover the cases of the four quantifier rules.

    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.15.3: Soundness for Predicate Logic Derivations is shared under a not declared license and was authored, remixed, and/or curated by LibreTexts.

    • Was this article helpful?