Mathematical Foundation of Computer Science

DHARM

PROPOSITIONAL LOGIC 123

Example 5.18.

1. J ∨ (~ K ∨ J)


2. K ∨ (~ J ∧ K) / ∴ (J ∧ K) ∨ (~ J ∧ ~ K)
   (Apply rules of inference and rules of replacement
   whenever necessary and obtain new premises
   until we reach to conclusion)


3. (J ∨ ~ K) ∨ J 1, Assoc


4. J ∨ (~ K ∨ J) 3, Assoc


5. J ∨ (J ∨ ~ K) 4, Comm


6. (J ∨ J) ∨ ~ K 5, Assoc


7. J ∨ ~ K 6, Taut


8. (K ∨ ~ J) ∧ (K ∨ K) 2, Dist


9. (K ∨ ~ J) ∧ K 8, Taut


10. (K ∨ ~ J) 9, Simp


11. ~ J ∨ K 10, Assoc


12. J → K 11, Imp


13. ~ K ∨ J 7, Comm


14. K → J 13, Imp


15. (J → K) ∧ (K → J) 12, & 14, Conj


16. (J ∧ K) ∨ (~ J ∧ ~ K) 15, Equiv
    Thus given premises derived the valid conclusion. Hence argument is valid.
    III. Rule of Conditional Proof (CP)
    We shall now introduce another rule of inference known as conditional proof, which is only
    applicable if the conclusion is an implicative statement.
    Assume the argument,


17. X 1


18. X 2
    ................
    ................
    ................
    k. Xk
    ∴ A → B
    So, we obtain the formula ( ......(X 1 ∧ X 2 ) ∧ .......∧ Xk) → (A → B)
    Assume ( ......(X 1 ∧ X 2 ) ∧ .......∧ Xk):P
    Thus, we have P → (A → B)
    ⇔ (P ∧ A) → B by rule Exp ...(A)
    We observe that, if antecedent part of conclusion goes to the set of premises then we will
    have the consequent part as conclusion.