1
$\begingroup$

I'm having a hard time coming up with a formal proof by cases method for this set of premises and conclusion. Note that $\neg$ refers to negation and $\wedge$ denotes AND. | Denotes subproof

  1. $\neg(A\wedge B)$

  2. $\neg(A\wedge\neg B)$

Thus,

  1. $\neg A$

Use # for contradiction; justify subproof assumptions with Assume; always drop outer parentheses; no spaces in PROP.

  1. ~(A&B) Premise
  2. ~(A&~B) Premise
  3. | B Assume
  4. || ~B Assume
  5. || B Reit;3
  6. || # #Intro;4,5
  7. | A #Elim;6
  8. | A&~B &Intro;4,7
  9. | # #Intro;2,8
  10. ~A #Elim;9

This is what I have currently, but am not sure if the steps I took are okay.

$\endgroup$
4
  • $\begingroup$ Welcome to Math Stack Exchange. Do you know that $\sim$(A&B)=$\sim$A or $\sim$B? $\endgroup$ Feb 24 '19 at 3:28
  • 1
    $\begingroup$ Also, did you mean 3. $\sim$A? $\endgroup$ Feb 24 '19 at 3:32
  • $\begingroup$ As J.W.Tanner said, do you know De Morgan's laws? en.wikipedia.org/wiki/De_Morgan%27s_laws $\endgroup$ Feb 24 '19 at 3:43
  • $\begingroup$ *Sorry for all the miscommunication; this is my first post on Stack Exchange. $\endgroup$
    – brando
    Feb 24 '19 at 4:01
1
$\begingroup$

By De Morgan's law and double negation we have $\neg(A\wedge B) \Leftrightarrow \neg A \vee \neg B$ and $\neg(A\wedge \neg B) \Leftrightarrow \neg A \vee B$. Therefore $$ \neg(A\wedge B) \wedge \neg(A\wedge \neg B) \Leftrightarrow (\neg A \vee \neg B) \wedge (\neg A \vee B) \overset{DP}{\Leftrightarrow} \neg A \vee (B\wedge \neg B) \Leftrightarrow \neg A $$ Here DP is the distributive property. The last equivalence holds because $B\wedge \neg B$ is a contradiction.

$\endgroup$
7
  • $\begingroup$ Hello, I understand DeMorgan's law AND double negation as a concept and can definitely follow ¬(𝐴∧𝐵)∧¬(𝐴∧¬𝐵)⇔(¬𝐴∨¬𝐵)∧(¬𝐴∨𝐵)⇔¬𝐴∨(𝐵∧¬𝐵)⇔¬𝐴. It's just I can't quite figure out how to write the whole thing out as a formal proof. $\endgroup$
    – brando
    Feb 24 '19 at 3:51
  • 1
    $\begingroup$ You're also using the distributive property in the last line. It might be a good idea to add it to your answer for the OP to know what is exactly done. $\endgroup$ Feb 24 '19 at 3:51
  • 2
    $\begingroup$ @brando This is a formal proof. If you want to prove De Morgan's law or the distributive property, you have to resort to truth tables. Truth tables can always be drawn for showing two Boolean expressions are the same, yet there are some well-known facts derived from them (like De Morgan's law or the distributive property) that make life easier like in Alan Muniz's answer. $\endgroup$ Feb 24 '19 at 3:52
  • $\begingroup$ I suppose I meant a formal proof using proof by cases. $\endgroup$
    – brando
    Feb 24 '19 at 3:58
  • 1
    $\begingroup$ I believe we are not talking the same language here. Please include a reference to a book or whatever you are using to study this topic. $\endgroup$
    – Alan Muniz
    Feb 24 '19 at 4:33
1
$\begingroup$

What appears to be a problem with the proof is that "# Elim" (explosion) should not discharge a assumption (or close a subproof) as what done on lines 7 and 10. Here is what the attempted proof looks like in a Fitch-style proof checker:

enter image description here

Here is a proof that should work using De Morgan's laws as suggested by Alan Muniz's answer:

enter image description here

I converted the two premises using De Morgan's laws (DeM) on lines 3 and 4. Then I attempted to eliminate the disjunction on line 4 by considering both cases. In each case, I had to derive $\neg A$. The first case was already $\neg A$ so there was nothing I needed to do. For the second case, $\neg \neg B$ I used disjunctive syllogism (DS) to derive from line 3 the desired result $\neg A$. When I used disjunction elimination on line 8, I was permitted to discharge the assumptions on lines 5 and 6 which closed the two subproofs.


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

$\endgroup$
1
$\begingroup$

As Frank Hubeny has stated in his answer, the $\#\textsf{Elim}$ rule (a.k.a. negation elimination, ex falso quadlibet, explosion) does not discharge the assumption.

What the OP was attempting was to introduce a negation, which does; (just not with assumptions attempted).   This would have required assuming the positive with the aim of contradicting a premise, so that assumption may be discharged and its negation infered.   Eg, assume $A$ on line $3$ and $B$ on line $4$.

$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~~{\sim}(A\& B)\quad\textsf{Premise}\\~~2.~~{\sim}(A\&{\sim}B)\quad\textsf{Premise}}{\fitch{~~3.~A\quad\textsf{Assumption}}{\fitch{~~4.~~B\quad\textsf{Assumption}}{~~5.~~A\& B\quad\&\textsf{Intro }3,4\\~~6.~~\#\quad\#\textsf{Intro }1,5}\\~~7.~~{\sim}B\quad{\sim}\textsf{Intro }4{-}6\\~~8.~~A\&{\sim}B\quad\&\textsf{Intro }3,7\\~~9.~~\#\quad\#\textsf{Intro }2,8}\\10.~~{\sim}A\quad{\sim}\textsf{Intro }3{-}9}$$

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.