Mathematical Foundation of Computer Science

(Chris Devlin) #1
DHARM

124 MATHEMATICAL FOUNDATION OF COMPUTER SCIENCE


That is,


  1. X 1

  2. X 2
    ..............
    .............
    ............
    k. Xk
    k+1. A
    ∴ B
    So we construct the formula, (( ......(X 1 ∧ X 2 ) .......∧ Xk) ∧ A) → B
    Assume ( ......(X 1 ∧ X 2 ) .......∧ Xk) : P
    Thus we have, (P ∧ A) → B ...(B)
    We will see that expression (A) and expression (B) are similar.
    Hence we conclude that rule CP is applied when conclusion is of the form A → B. In such
    a case, A is taken as an additional premise and B is derived from set of premises including A.


Example 5.19. Show that A → B derives the conclusion A → (Α → B).
Sol. Here, we observe that the conclusion is of implication form. Hence, we can apply rule of
conditional proof, so the antecedent part of conclusion will be added to the list of premise,
therefore we have,



  1. A → B/∴ A → (A ∧ B)

  2. A/∴ A ∧ B CP
    (Apply rules of inference and rules of replacement
    whenever necessary and obtain new premises
    until we reach to conclusion)

  3. B 1 & 2, Imp

  4. A ∧ B 2 & 3, Conj
    Since, we obtain the conclusion, therefore argument 2, is valid hence previous argu-
    ment is valid.


Example 5.20. Show that (A ∨ B) → ((C ∨ D) → E) /∴ A → ((C ∧ D) → E).
Sol. Since conclusion is of implication form, hence we proceed with conditional proof. That is,
instead of deriving A → ((C ∧ D) → E), we shall include A as an additional premise and derive
the conclusion (C ∧ D) → E. That is also an implication conclusion, so apply again Conditional
proof s.t. (C ∧ D) as an additional premise and E will be the final conclusion.
s.t.



  1. (A ∨ B) → ((C ∨ D) → E) /∴ A → ((C ∧ D) → E)

  2. A/∴ (C ∧ D) → E CP

  3. C ∧ D/∴ E CP

  4. A ∨ B 2, Add

  5. (C ∨ D) → E 1 & 4, MP

  6. C 3, Simp

  7. C ∨ D 6, Add

  8. E 5 & 7, MP

Free download pdf