completeness theorem for propositional logic


The completeness theorem of propositional logicPlanetmathPlanetmath is the statement that a wff is tautologyMathworldPlanetmath iff it is a theoremMathworldPlanetmath. In symbol, we have

AiffA

for any wff A. The “if” part of the statement is the soundness theorem, and is proved here (http://planetmath.org/TruthValueSemanticsForPropositionalLogicIsSound). We will prove the “only if” part, which is also known as the completeness portion of the theorem. We will give a constructive proofMathworldPlanetmath of this. Before proving this, we state and prove some preliminary facts:

  1. 1.

    A,BAB

  2. 2.

    A,¬B¬(AB)

  3. 3.

    ¬A,BAB

  4. 4.

    ¬A,¬BAB

  5. 5.

    Let v be a valuationMathworldPlanetmathPlanetmath. For any wff A, let v[A] be defined as follows:

    v[A] is {Aif v(A)=1,¬Aif v(A)=0.

    Suppose p1,,pn are the propositional variables in A. Then

    v[p1],,v[pn]v[A].
  6. 6.

    if Δ,AB and Δ,¬AB, then B.

Proof.

Facts 1 and 3 come from the axiom schemaMathworldPlanetmath B(AB). From B(AB), we have CB(AB), so C,BAB. If C is A, we have fact 1, and if C is ¬A, we have fact 3.

Fact 2: this is proved here (http://planetmath.org/SubstitutionTheoremForPropositionalLogic).

Fact 4: By ex falso quodlibet, B, so AB, and therefore A(B) by the deduction theoremMathworldPlanetmath. Now, (A(B))((A)(AB)) is an axiom instance, so (A)(AB), or ¬A(AB), or ¬AAB, and

¬A,¬BAB

all the more so.

Fact 5: by inductionMathworldPlanetmath on the number n of occurrences of in A. If n=0, then A is either or a propositional variable p. In the first case, v[A] is ¬, and from , we get , or ¬. In the second case, v[p]v[p]. Now, suppose there are n+1 occurrences of in A. Let p1,,pm be the propositional variables in A. By unique readability, A is BC for some unique wff’s B and C. Since each B and C has no more than n occurrences of , by induction, we have

v[pi(1)],,v[pi(s)]v[B]  and  v[pj(1)],,v[pj(t)]v[C],

where the propositional variables in B are pi(1),,pi(s), and in C are pj(1),,pj(t). So

v[p1],,v[pm]v[B]  and  v[p1],,v[pm]v[C].

Next, we want to show that v[B],v[C]v[BC]. We break this into four cases:

  • if v[B] is B and v[C] is C: then v[BC] is BC, and use Fact 1

  • if v[B] is B and v[C] is ¬C: then v[BC] is ¬(BC), and use Fact 2

  • if v[B] is ¬B and v[C] is C: then v[BC] is BC, and use Fact 3

  • if v[B] is ¬B and v[C] is ¬C: then v[BC] is BC, and use Fact 4.

In all cases, we have by applying modus ponensMathworldPlanetmath,

v[p1],,v[pm]v[BC].

Fact 6 is proved here (http://planetmath.org/SubstitutionTheoremForPropositionalLogic). ∎

Theorem 1.

Propositional logic is completePlanetmathPlanetmathPlanetmath with respect to truth-value semantics.

Proof.

Suppose A is a tautology. Let p1,,pn be the propositional variables in A. Then

v[p1],,v[pn]v[A]

for any valuation v. Since v[A] is A. We have

v[p1],,v[pn]A.

If n=0, then we are done. So suppose n>0. Pick a valuation v such that v(pn)=1, and a valuation v such that v(pi)=v(pi) and v(pn)=0 Then

v[p1],,v[pn-1],pnA  and  v[p1],,v[pn-1],¬pnA,

where the first deducibility relation comes from v and the second comes from v. By Fact 6 above,

v[p1],,v[pn-1]A.

So we have eliminated v[pn] from the left of v[p1],,v[pn]A. Now, repeat this process until all of the v[pi] have been eliminated, and we have A. ∎

The completeness theorem can be used to show that certain complicated wff’s are theorems. For example, one of the distributive laws

(AB)C(AC)(BC)

To see that this is indeed a theorem, by the completeness theorem, all we need to show is that it is true using the truth tableMathworldPlanetmath:

(A B) C (A C) (B C)
T T T T T T T T T T T T T
T T T T F T T T F T T T F
T F F T T T T T T T F T T
T F F F F T T T F F F F F
F F T T T T F T T T T T T
F F T F F T F F F F T T F
F F F T T T F T T T F T T
F F F F F T F F F F F F F

Similarly,onecanshow⊢(A∨B)∧C ↔(A∧C)∨(B∧C).Titlecompleteness theorem for propositional logicCanonical nameCompletenessTheoremForPropositionalLogic1Date of creation2013-03-22 19:32:47Last modified on2013-03-22 19:32:47OwnerCWoo (3771)Last modified byCWoo (3771)Numerical id21AuthorCWoo (3771)Entry typeTheoremClassificationmsc 03B05