Is this a correct natural deduction proof?

496 Views Asked by At

Prove $ A \rightarrow B \vdash \neg (A \wedge \neg B)$

  1. $A \rightarrow B \quad\quad\quad\quad$ Premise
  2. $(A \wedge \neg B) \rightarrow B \quad \rightarrow $I, subcomputation below

$\quad\quad$ 2.1 $ A \wedge \neg B \quad $ Assumption
$\quad\quad$ 2.2 $ A \quad\quad\quad$ (2.1), $\wedge$E
$\quad\quad$ 2.3 $ B \quad\quad\quad$ (2.2)(1), $\rightarrow$E

  1. $(A \wedge \neg B) \rightarrow \neg B \quad \rightarrow$I, subcomputation below

$\quad\quad$ 3.1 $A \wedge \neg B \quad$ Assumption
$\quad\quad$ 3.2 $\neg B \quad\quad\space\space$ (3.1), $\wedge$E

  1. $\neg (A \wedge \neg B) \quad\quad\space\space$ (2)(3), $\neg$I
2

There are 2 best solutions below

0
On BEST ANSWER

For the inference system used in the proof, the answer is correct.

Please see @F. Zer answer for a proof using the Fitch Natural Deduction system.

6
On

As Mauro points out in the comments, there is no need to start two subproofs. Instead, you can use the rule of Negation Introduction by assuming $A \land \lnot B$ and trying to reach a contradiction ($\bot$).

A possible proof using Fitch Natural Deduction system, could be: $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $

Hint:

$$ \fitch{1.\,A \to B}{ \fitch{2.\,A \land \lnot B}{ 3.\,A \ce{2} \vdots\\ 6.\,\bot }\\ 7.\,\lnot(A \land \lnot B) \ni{2-6} } $$

Solution:

$$\fitch{1.\,A \to B}{ \fitch{2.\,A \land \lnot B}{ 3.\,A \ce{2} 4.\,B \ie{1,3} 5.\,\lnot B \ce{2} 6.\,\bot \ne{4,5}}\\7.\,\lnot(A \land \lnot B) \ni{2-6}}$$