4
$\begingroup$

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
$\endgroup$
7
  • $\begingroup$ It looks ok to me. $\endgroup$ Aug 31, 2020 at 3:33
  • $\begingroup$ An alternative approach is to recognize that $A \rightarrow B$ is exactly equivalent to $\;$ (not $A$) or $B.$ $\endgroup$ Aug 31, 2020 at 7:14
  • 2
    $\begingroup$ Why two subproofs ? It is enough to assume $A \land \lnot B$ and derive both $B$ and $\lnot B$ from it. Thus, you have a contradiction and the conclusion follows. $\endgroup$ Aug 31, 2020 at 7:43
  • 1
    $\begingroup$ Some systems allow you to derive both conditionals from one subproof. Some require two. You to use the one you are allowed to use. $\endgroup$ Aug 31, 2020 at 22:41
  • 1
    $\begingroup$ Should I edit the question to add the rules I'm using? $\endgroup$
    – 0implies0
    Sep 1, 2020 at 2:40

2 Answers 2

5
$\begingroup$

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

$\endgroup$
6
  • $\begingroup$ Thanks, whilst this does make sense to me. The set of rules I'm using don't allow this. Assumptions can only be made with $\rightarrow$ Introduction. The assumption being the hypothesis of the implication and the conclusion of the sub-proof being the conclusion of the implication. $\endgroup$
    – 0implies0
    Aug 31, 2020 at 17:28
  • $\begingroup$ I am wondering if this system I'm working with has a name like the Fitch notation you just showed. $\endgroup$
    – 0implies0
    Aug 31, 2020 at 17:51
  • $\begingroup$ Are you using a book ? Class notes ? $\endgroup$
    – F. Zer
    Aug 31, 2020 at 17:53
  • 1
    $\begingroup$ Class notes. No name given other than 'Natural Deduction'. At the moment it's just a basic set with 1 elimination and 1 introduction rule for each of {$\neg, \wedge, \vee, \rightarrow$} $\endgroup$
    – 0implies0
    Aug 31, 2020 at 17:58
  • 3
    $\begingroup$ On a tangent, those systems that require you to prove $\Gamma, P \vdash Q$ and $\Gamma, P \vdash \lnot Q$ to conclude $\Gamma \vdash \lnot P$, instead of just allowing you to show $\Gamma, P \vdash \bot$, remind me of the chess rules defining the win condition to be checkmate, instead of defining the win condition as "capture the opponent's king". i.e. it stops one step short of what I view as the real goal. (Modulo the situations in the chess case where the official definition would result in a draw whereas the simplified definition would result in a win.) $\endgroup$ Sep 1, 2020 at 19:19
0
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

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