Skip to main content
Humanities LibreTexts

3.13.3: Completeness for Derivations- Informal Introduction

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

    We still need to prove

    T6 (Completeness for sentence logic derivations): For any finite set of sentences, Z, and any sentence, X, if Z~X, then ZtX.

    where 'I-' is understood to mean kd, derivability in our natural deduction system. The proof in this section assumes that Z is finite. Chapter 14 will generalize to the case of infinite Z. -

    The proof of completeness for derivations is really an adaptation of the completeness proof for trees. If you have studied the tree completeness proof, you will find this and the next section relatively easy. The connection between trees and derivations on this matter is no accident. Historically, the tree method was invented in the course of developing the sort of completeness proof that I will present to you here.

    Begin by reading section 12-1, if you have not already done so, since we will need lemma L1 and the notation from that section. Also, do exercises 12-1 and 12-2. (If you have not studied trees, you will need to refresh your memory on the idea of a counterexample; see section 4-1, volume I.) For quick reference, I restate L1:

    L1: Z~X iff ZU{-X} is inconsistent.

    The basis of our proof will be to replace completeness with another connection between semantic and syntactic notions. Let us say that

    D19: Z is Syntactically Inconsirtent iff ZtA&-A.

    Semantic inconsistency is just what I have been calling 'inconsistency', defined in chapter 10, D7, as (V1)-Mod(1,Z). L1 says that an argument is valid iff the premises together with the negation of the conclusion form a semantically inconsistent set. Analogously

    L17: ZU{-X}tA&-A iff ZtX.

    says that -X together with the sentences in Z form a syntactically inconsistent set iff there is a proof using sentences in Z as premises to the conclusion X. Together, L1 and L17 show that T6 is equivalent to

    T7: For any finite set of sentences, Z, if Z is semantically inconsistent, then Z is syntactically inconsistent; that is, if (W)-Mod(I,Z), then ZkA&-A.

    EXERCISES 13-9. Prove L17. 13-10. Using L1 and L17, prove that T6 is equivalent to T7.

    We have boiled our problem down to proving T7. We do this by developing a specialized, mechanical kind of derivation called a Semantic Tableau Derivation. Such a derivation provides a systematic way of deriving a contradiction if the original premises form an inconsistent set.

    If you haven't done trees, it is going to take you a little time and patience to see how this method works. On a first reading you may find the next few paragraphs very hard to understand. Read them through even if you feel quite lost. The trick is to study the two examples. If you go back and forth several times between the examples and the text you will find that the ideas will gradually come into focus. The next section will add further details and precision.

    A semantic tableau derivation is a correct derivation, formed with a special recipe for applying derivation rules. Such a derivation is broken into segments, each called a Semantic Tableau, marked off with double horizontal lines. We will say that one tableau Generates the next tableau. Generating and generated tableaux bear a special relation. If all of a generated tableau's sentences are true, then all the sentences of previous generating tableaux are true also. In writing a derivation, each tableau we produce has shorter sentences than the earlier tableaux. Thus, as the derivation develops, it provides us with a sequence of tableaux, each a list of sentences such that the sentences in the later tableaux are shorter. The longer sentences in the earlier tableaux are guaranteed to be true if all of the shorter sentences in the later tableaux are true.

    A tableau derivation works to show that if a set, Z, of sentences is semantically inconsistent, then it is syntactically inconsistent. Such derivations accomplish this aim by starting with the sentences in Z as its premises. The derivation is then guaranteed to have 'A&-A' as its final conclusion if Z is (semantically) inconsistent.

    To see in outline how we get this guarantee, suppose that Z is an arbitrary finite set of sentences, which may or may not be inconsistent. (From now on, by 'consistent' and 'inconsistent' I will always mean semantic consistency and inconsistency, unless I specifically say 'syntactic consistency' or 'syntactic inconsistency'.) A tableau derivation, starting from Z as premises, will continue until it terminates in one of two ways. In the first way, some final tableau will have on it only atomic and/or negated atomic sentences, none of which is the negation of any other. You will see that such a list of sentences will describe an interpretation which will make true all the sentences in that and all previous tableaux. This will include the original premises, Z, showing this set of sentences to be consistent. Furthermore, we will prove that if the initial sentences form a consistent set, the procedure must end in this manner.

    Consequently, if the original set of sentence forms an inconsistent set, the tableau procedure cannot end in the first way. It then ends in the second way. In this alternative, all subderivations end with a contradiction, 'A&-A'. As you will see, argument by cases will then apply repeatedly to make 'A&-A' the final conclusion of the outermost derivation.

    Altogether we will have shown that if Z is (semantically) inconsistent, then Z!-A&-A, that is, Z is syntactically inconsistent.

    To see how all this works you need to study the next two examples. First, here is a tableau derivation which ends in the first way (in writing lines 3 and 4, I have omitted a step, '-B&-C', which gives 3 and 4 by &E):

    You can see that this is a correct derivation in all but two respects: I have abbreviated by omitting the step '-B&-C', which comes from 1 by DM and gives 3 and 4 by &E; and I have not discharged the assumptions of the subderivations to draw a final conclusion in the outer derivation.

    Each tableau is numbered at the end of the double lines that mark its -(BvC) P BvD P 1 -B 1, DM, &E -C 1, DM, &E BvD 2, R 6 7 8 9 A&-A 6, 7, CD X 3 11 12 -C 4, R 4 + PO2 Soundness and Completeness for Sentence Lo& Mvations 134. Completeness for Denenvathis: Ponnal Details PO3 end. A tableau may generate one new tableau (Sequential Generation): In this example tableau 1 generated tableau 2 by applying the rules DM, &E, and R. Or a tableau may generate two new tableaus (Branching Generatian): In the example tableau 2 generated tableaux 3 and 4 by starting two new subderivations, each using for its assumption one of the disjuncts, 'B' and 'D' of 'BvD' on line 5, and each reiterating the rest of tableau 2.

    Tableau 3 ends in a contradiction. It can't describe an interpretation. We mark it with an 'x' and say that it is Closed. Tableau 4, however is Open. It does not contain any sentence and the negation of the same sentence; and all its sentences are Minimal, that is, either atomic or negated atomic sentences. Tableau 4 describes an interpretation by assigning f to all sentence letters which appear negated on the tableau and t to all the unnegated sentence letters. In other words, the interpretation is the truth value assignment which makes true all the sentences on this terminal tableau.

    Note how the interpretation described by tableau 4 makes true all the sentences on its generator, tableau 2. The truth of '-B' and '4' carries upward simply because they are reiterated, and the truth of 'D' guarantees the truth of 'BvD' by being a disjunct of the disjunction. You should check for yourself that the truth of the sentences in tableau 2 guarantees the truth of the sentences in tableau 1.

    Examine this example of a tableau derivation which ends in the second way:

    1 2 3 4 5 6 7 8 9 10 11 12 13 14 -(BvC) BvC 1 - B -C BvC -C A&-A P P 1, DM, &E 1, DM, &E 2, R A 3, R 4, R 6, 7, CD

    In this example, all terminal tableaux (3 and 4) close, that is, they have both a sentence and the negation of the same sentence, to which we apply the rule CD. We can then apply AC to get the final desired conclusion, 'A&-A'.

    Again, here is the key point: I am going to fill in the details of the method to guarantee that a consistent initial set of sentences will produce a derivation like the first example and that an inconsistent set will give a result like the second example. More specifically, we will be able to prove that if there is an open terminal tableau, like tableau 4 in the first example, then that tableau describes an interpretation which makes true all its sentences and all the sentences on all prior tableaux. Thus, if there is an open terminal tableau, there is an interpretation which constitutes a model of all the initial sentences, showing them to form a consistent set. Conversely, if the original set is inconsistent, all terminal tableaux must close. We will than always be able to apply argument by cases, as in the second example, to yield 'A&-A' as a final conclusion. But the last two sentences just state T7, which is what we want to prove.

    To help you get the pattern of the argument, here is a grand summary which shows how all our lemmas and theorems connect with each other. We want to show T6, that if ZkX, then ZkX. We will assume ZkX, and to take advantage of lemmas L1 and L17, we then consider a semantic tableau derivation with the sentences in ZU{-X} as the initial tableau. Then we argue

    (1) Z~X. (Assumption)

    (2) If Z~X, then ZU{-X} is inconsistent. (By L1)

    (3) If some terminal tableau is open, then ZU{-X} is consistent. (By L18, to be proved in the next section)

    (4) If ZU{-X} is inconsistent, then all terminal tableaux close. (Contrapositive of (3))

    (5) If all terminal tableaux close, then ZU{-X}l-A&-A. (L20, to be proved in the next section)

    (6) If ZU{-X}l-A&-A, then Zl-X. (By L17)

    Now all we have to do is to discharge the assumption, (I), applying it to (2), (4), (5), and (6), giving T6: If Z~X, then Zl-X.

    In the next section we carry out this strategy more compactly by proving T7 (corresponding to (4) and (5) above), which you have already proved to be equivalent to T6.

    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.3: Completeness for Derivations- Informal Introduction is shared under a not declared license and was authored, remixed, and/or curated by LibreTexts.

    • Was this article helpful?