# Formal Proof of WFF using Rules of Inference

I am currently hung up on a practice problem that requires a formal proof of a WFF using ONLY rules of inference. I've been attempting this for hours, but it seems like there is something i'm missing. In this case, I know I need to get a C or ¬C to use Modus Ponens then Addition, but its not working for me.

WFF: (C→A) ∧ (¬C→B) → A∨B

[EDIT] Latest attempt:

1. (C→A) | Premise for Conditional Proof

2. (¬C→B) | Premise for Conditional Proof

3. ¬C | Premise for Indirect Proof

4. B | 2, 3 Modus Ponens

6. ¬C∧B | 3, 4 Conjunction

• There are many different deductive systems, so it's best to outline the system you're using or given a reference. I've done a good bit of logic and I'm not sure what "P for IP" means. (But for what it's worth, $C\lor \lnot C$ is a tautology, so you can certainly prove it. And the prove won't involve any $A$'s or $B$'s or nothing.) – spaceisdarkgreen Sep 11 '18 at 3:16

You are on the right trail. You may either:

(1) Accept the Law of Excluded Middle as an axiom, and eliminate that disjunction.

• $(C\to A)~\land ~(\neg C\to B)$ by premise.
• $C\vee\neg C$ by LEM
• $C$ by assumption
• $A\vee B$ by reasons
• $C\to(A\vee B)$ by conditional introduction
• $\neg C$ by assumption
• $\neg C\to B$ by conjunction elimination (simplification)
• $B$ by conditional elimination (modus ponens)
• $A\vee B$ by disjunction introduction
• $\neg C\to(A\vee B)$ by conditional introduction (deduction)
• $A\vee B$ by disjunction introduction

(2) Accept Double Negation Elimination as a rule of inference and Reduce to Absurdity.

• $(C\to A)~\land ~(\neg C\to B)$ by premise.
• $\neg(A\vee B)$ by assumption
• $C$ by assumption
• $\bot$ by reasons
• $\neg C$ by negation introduction
• $\neg C\to B$ by conjunction elimination (simplification)
• $B$ by conditional elimination (modus ponens)
• $A\vee B$ by disjunction introduction
• $\bot$ by negation elimination (sometimes called "contradiction introduction")
• $\neg\neg (A\vee B)$ by negation introduction
• $A\vee B$ by double negation elimination