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.

Advertisements

Leave a Reply

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

WordPress.com Logo

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

Twitter picture

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

Facebook photo

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

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: