1
$\begingroup$

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?

$\endgroup$
2
  • 2
    $\begingroup$ 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. $\endgroup$
    – Arthur
    Commented Dec 18, 2015 at 11:43
  • $\begingroup$ thank you for your reply! Would you say that number 6 necessary if I'm using an assumption? $\endgroup$
    – qwerty
    Commented Dec 18, 2015 at 11:52

3 Answers 3

Reset to default
3
$\begingroup$

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$.

$\endgroup$
1
  • $\begingroup$ Ah, that's great, thank you do much! That's really helpful :) $\endgroup$
    – qwerty
    Commented Dec 18, 2015 at 12:05
1
$\begingroup$

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)

$\endgroup$
1
$\begingroup$

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:

enter image description here

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

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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .