OR implication
Sandip Ray
I thought I'd post a solution to the OR-implication exercise that I
suggested in class a week back. If you're working on the problem
please don't look at the solution --- it's important to get an
understanding of how this works yourself rather than see someone
else's solution. But I'm posting the solution just in case...
I put some amount of white space before the answer so that someone
does not inadvertently see it while working on the problem.
-- Sandip
(Scroll down for the solution)
[OR-Implication] Derive (A v B) => C from (A => C) and (B => C)
1. B => C (Given)
2. ~B v C (Abbreviation)
3. ~(A v B) v (A v B) (Propositional Axiom)
4. (~(A v B) v A) v B (Associativity)
5. B v (~(A v B) v A) (Commutativity)
6. (~(A v B) v A) v C (Cut, 5 & 2)
7. C v (~(A v B) v A) (Commutativity)
8. (C v ~(A v B)) v A (Associativity)
9. A v (C v ~(A v B)) (Commutativity)
10. A => C (Given)
11. ~A v C (Abbreviation)
12. ~A v (C v ~(A v B)) (OR insertion)
13. (C v ~(A v B)) v (C v ~(A v B)) (Cut, 9 & 12)
14. (C v ~(A v B)) (Contraction)
15. ~(A v B) v C (Commutativity)
16. (A v B) => C (Abbreviation)
As you can see, this kind of things can get pretty tedious, so it's
imperative that we can do this stuff mechanically as much as possible.
It should best be viewed as a game in which you are provided with
certain symbol manipulation rules and you're trying to get to a
formula using the rules of the game. We will not do any further proof
at this level in the class, and we'll take propositional calculus for
free.