2
$\begingroup$

I have the following premise: \begin{gather} ¬B⟹D \\ ¬A⟹C \end{gather}

And I have to prove this formula: $$ ¬(A\vee B)⟹C \wedge D $$ I'm allowed to use only the following rules I$\wedge$, E$\wedge$, I$\vee$, E$⟹$, I$⟹$, I$¬$, E$¬$, E$\vee$, it.

I understand the rules. But in this problem I don't know how to start. I'm a beginner in natural deduction.

$\endgroup$
  • $\begingroup$ Are you sure about the first premise ? Maybe $\lnot B \to D$ ... $\endgroup$ – Mauro ALLEGRANZA Mar 18 '17 at 16:53
  • $\begingroup$ Yes! Sorry... edited $\endgroup$ – user425260 Mar 18 '17 at 16:54
  • $\begingroup$ How is $ I \neg$ defined? $\endgroup$ – Bram28 Mar 18 '17 at 18:12
1
$\begingroup$

With Natural Deduction rules:

1) $\lnot B \to D$ --- premise

2) $\lnot A \to C$ --- premise

3) $\lnot (A \lor B)$ --- assumed [a]

4) $A$ --- assumed [b]

5) $A \lor B$ --- from 4) by $\lor$I

6) $\bot$ --- from 3) and 5) by $\lnot$E

7) $\lnot A$ --- from 4) and 6) by $\lnot$I, discharging [b]

Note: without $\bot$, probably your $\lnot$I rule allows you to derive $\lnot \varphi$ after a derivation of a contradiction from the assumption $\varphi$. If so, you can skip 6) and justify 7) with: from 4), 3) and 5) by $\lnot$I, discharging [b].

8) $C$ --- from 2) and 7) by $\to$E

9) $B$ --- assumed [c]

In the same way as before, we derive a contradiction, frow which derive $\lnot B$ (discharging [c]) and with 1) we derive (by $\to$E) :

10) $D$

11) $C \land D$ --- from 8) and 10) by $\land$I

12) $\lnot (A \lor B) \to (C \land D)$ --- from 3) and 12) by $\to$I, discharging [a].

$\endgroup$
  • $\begingroup$ Sorry maybe I have to explain better my questions. But I don't understand the meaning of ⊥. We didn't study that. We can't use derivative rules in this exercise. Thanks for show me how to start! $\endgroup$ – user425260 Mar 18 '17 at 17:15
  • $\begingroup$ @JosepB - I've understood that you are "a beginner in natural deduction", but I've assumed that you have at least studied the rules of ND. $\endgroup$ – Mauro ALLEGRANZA Mar 18 '17 at 17:30
  • $\begingroup$ Yes, maybe in the next units we study the meaning of ⊥. Anyway I'll google it. Thanks @Mauro $\endgroup$ – user425260 Mar 18 '17 at 17:43
  • $\begingroup$ @JosepB - I've linked a good on-line presentation of ND and its rules exactly to support my proof; maybe you have to provide in your question the list of rules you are allowed to use... $\endgroup$ – Mauro ALLEGRANZA Mar 18 '17 at 17:50
  • $\begingroup$ You're right @Mauro. I edited the question with the rules that I'm allowed to use. $\endgroup$ – user425260 Mar 18 '17 at 18:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy