# Proving $(A \implies B) \land (\lnot A \implies C)~,~~ (A \implies \lnot B) \land (\lnot A \implies C) \vdash C$?

Just to let you know - This is an assignment, so I wouldn't like a full answer, just some hints. :)

I am required to prove the following:

$$(A \implies B) \land (\lnot A \implies C)~,~~ (A \implies \lnot B) \land (\lnot A \implies C) \ \vdash \ C$$

I am allowed to use any semantic or syntactic methods, except truth tables (i.e. equivalences and the rules of inference, primitive and derived).

I produced the following, however, I am not too sure if it is a correct/most efficient way of proving the above.

1. (A→ B) ∧ (¬A → C)         (given)
2. (A→ ¬B) ∧ (¬A → C)        (given)
3. A→ B                      (1, ∧ E)
4. A→ ¬B                     (2, ∧ E)
5. ¬A → C                    (1, ∧ E)
6. ¬A → B                    (4, dilemma)
7. A                     (3, assume)
8. B                     (3, → E)
9. ¬B                    (4, → E)
10. ¬A                   (RRA)
11. C


Can anyone help me out a little?

• I think noting that premise 1 and 2 give $A \to (B\land \lnot B)$, and conclude that we have $\lnot A$ from there (which is what you have done) is the best solution. Commented Dec 18, 2015 at 11:43
• thank you for your reply! Would you say that number 6 necessary if I'm using an assumption? Commented Dec 18, 2015 at 11:52

Assuming your allowed rules from what you've produced. You would want to use $\neg A\rightarrow C$ (too) and use the "dilemma" rule to get $\neg C\rightarrow A$.

So you've already found $\neg A$ and by assuming $\neg C$ you can prove $A$ too and by "RAA" you conclude $C$.

• Ah, that's great, thank you do much! That's really helpful :) Commented Dec 18, 2015 at 12:05

Well, it might be a matter of taste but I don't like the "assume" part given it is unnecessary. From 'A implies B' and 'A implies not B' you get by contraposition 'not B implies not A' and 'B implies not A'. The last two premises allow for 'not A'. (No matter what 'not A') Together with 'not A implies C' you get 'C'.(MP)

As already noticed by Arthur in its comment, there is a "simpler" way to prove this without using the dilemma rule. I formalized its argument in natural deduction:

It is worth noting that this derivation does not need the rule RAA and hence it is also intuitionistically valid, not only classically.

• Could you say which software was used to accomplish that nice looking proof ? Commented Sep 15, 2020 at 20:36
• @F.Zer - I use LaTeX with the package ebproof. Another popular LaTeX package for proof-trees is bussprooofs. Commented Sep 15, 2020 at 22:12