502 – Propositional logic (4)

11. Completeness

We now want to show that whenever {S\models A,} then also {S\vdash A.} Combined with the soundness Theorem 22, this shows that the notions of provable and true coincide for propositional logic, just as they did for the tree system. The examples above should hint at how flexible and useful this result actually is. This will be even more evident for first order (predicate) logic.

Theorem 26 (Completeness) For any theory {S} and any formula {A,} if {S\models A,} then {S\vdash A.}

Proof: We prove this by verifying that if {S} is formally consistent, then it is satisfiable. To see that this gives the result, suppose that {S\models A.} Then {S\cup\{\lnot A\}} is unsatisfiable, and it would therefore follow that {S\cup\{\lnot A\}} is formally inconsistent. Thus {S\vdash\lnot\lnot A,} and therefore {S\vdash A.}

Suppose then that {S} is a given formally consistent theory. By Corollary 13, we may assume that {S} is also complete, i.e., that for any formula {A,} either {A\in S} or {\lnot A\in S.} Consider the valuation

\displaystyle v(p)=\chi_S(p),

where {\chi_S} is the characteristic function of {S,} i.e., {v(p)=1} iff {p\in S.} We claim that {v\models S.}

To prove this, we require one additional result about the provability relation {\vdash:}

Lemma 27 {\lnot(A\rightarrow B)\vdash A,\lnot B.}

Proof: To show that {\lnot(A\rightarrow B)\vdash A,} it suffices to see that {\lnot(A\rightarrow B)\vdash\lnot\lnot A.} By proof by contrapositive, it is enough to show that {\lnot A\vdash\lnot\lnot(A\rightarrow B),} and for this it suffices to see that {\lnot A\vdash A\rightarrow B.} By the deduction theorem, one only needs to check that {\{\lnot A,A\}\vdash B.} But this is clear, since this set is formally inconsistent.

Similarly, by proof of contrapositive, to see that {\lnot(A\rightarrow B)\vdash\lnot B,} it suffices to see that {B\vdash A\rightarrow B,} but this is clear. \Box

We now proceed to prove that {v\models S} for {v} as above. We check for all formulas {A,} by induction on the length of a parsing sequence for {A,} that {A\in S} iff {v(A)=1.}

Since {S} is complete and {v=\chi_S,} this holds for {A} a propositional variable.

Assuming the result for {A,} it follows immediately for {\lnot A} by completeness of {S.}

Finally, assume the result for both {A} and {B,} and we need to show that it also holds for {A\rightarrow B.} We need to prove that {A\rightarrow B\in S} iff {v(A\rightarrow B)=1,} or equivalently, that {A\rightarrow B\notin S} iff {v(A\rightarrow B)=0} or, what is the same, {v(A)=1} and {v(B)=0.} By the induction hypothesis, this is equivalent to saying that {A\in S} and {B\notin S.}

This is finally what we prove: {A\rightarrow B\notin S} iff {A\in S} and {B\notin S.}

Assume first that {A\in S} and {B\notin S.} Then {A,\lnot B\in S.} If {A\rightarrow B\in S,} then {S\vdash B,\lnot B,} and therefore {S} is formally inconsistent.

Conversely, suppose that {A\rightarrow B\notin S.} Then {\lnot(A\rightarrow B)\in S.} By Lemma 27, {S\vdash A,\lnot B,} so {A\in S} and {B\notin S,} and we are done. \Box

Corollary 28 There is an algorithm that on input {S,A} where {S} is a finite set of formulas, and {A} is a formula, decides whether {S\vdash A.} {\Box}

On the other hand, the question of how efficient such an algorithm is, turns out to be much more complicated (it is equivalent to the P vs NP problem.)

12. Additional connectives

All the results above hold even if we allow additional connectives in the language, modulo a suitable extension of the propositional axioms. (Some of the proofs need minor modifications, such as the argument for unique readability.) It is a useful exercise to see that if we allow the standard connectives {\land,\lor,\leftrightarrow} in addition to {\lnot,\rightarrow} then, by extending the propositional axioms as follows, we can recover the completeness theorem:

  1. {(A\rightarrow (B\rightarrow A)),}
  2. {((A\rightarrow (B\rightarrow C)) \longrightarrow ((A\rightarrow B) \rightarrow (A\rightarrow C))),}
  3. {((\lnot A\rightarrow\lnot B)\rightarrow (B\rightarrow A)),}
  4. {((A\land B)\rightarrow A),}
  5. {((A\land B)\rightarrow B),}
  6. {((A\rightarrow B) \longrightarrow ((A \rightarrow C) \rightarrow (A \rightarrow (B\land C)))),}
  7. {(A\rightarrow (A\lor B)),}
  8. {(B\rightarrow(A\lor B)),}
  9. {((A\rightarrow C) \longrightarrow ((B\rightarrow C) \rightarrow ((A \lor B) \rightarrow C))),}
  10. {((A\leftrightarrow B)\rightarrow(A\rightarrow B)),}
  11. {((A\leftrightarrow B)\rightarrow(B\rightarrow A)),}
  12. {((A\rightarrow (B\rightarrow C)) \longrightarrow ((A\rightarrow (C\rightarrow B)) \rightarrow (A\rightarrow (B\leftrightarrow C)))).}

Typeset using LaTeX2WP. Here is a printable version of this post.

Advertisement

This entry was posted on Monday, September 14th, 2009 at 4:10 pm and is filed under 502: Logic and set theory. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

Leave a Reply

Fill in your details below or click an icon to log in:

Gravatar
WordPress.com Logo

You are commenting using your WordPress.com account. ( Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. ( Log Out /  Change )

Cancel

Connecting to %s

%d bloggers like this: