# How to prove ¬(p→q) ⊢ p &¬q

This is the first time I have posted anything on this forum. I am using Tomassi's Logic. Unfortunately I have been unable to solve some of the problems. One I can't solve is this one:

¬(p → q) ⊢ p & ¬q

I have to use natural deduction. The only rules I know are: assumptions, modus ponendo ponens, modus tollendo tollens, double negation, reductio ad absurdum, conditional proof, v-introduction, v-elimination, &-introduction, and &-elimination. Tomassi's proof consists of 12 steps.

Moreover, I don't see how to proceed because of the negations on the outside of the parentheses.

Thanks for the help!

• I made an edit which you may roll back or continue editing. You can see the versions by clicking on the "edited" link above. Aug 2 '18 at 20:49
• As showned by the answer below: when you do not know how to proceed... use a proof by contradiction. Aug 3 '18 at 5:58
• Hint: Prove ~[p & ~q] => [p => q]. Then apply the contrapositive. Aug 13 '18 at 15:08
• How can I proof: (p ∧ ¬q) ⊢ ¬(p → q) Nov 25 '19 at 13:35

Here is one way to show this using natural deduction. Of the rules, I used contradiction introduction (⊥I) which I did not see on your list, but I suspect is permitted because reduction ad absurdum is permitted. On line 1 is the assumption. I attempted an indirect proof (IP) or reductio ad absurdum beginning on the second line. This completed on line 10 which also completed the proof.

In between I assumed "P" in a subproof and then immediately assumed "¬Q" in another subproof. In line 5 I combined these two assumptions to get "P ∧ ¬Q" on line 5. That contradicted the assumption on line 2 and I completed an indirect proof on line 7 discharging the "¬Q" assumption on line 4. The set of lines from 3 to 7 represented a conditional introduction (→I) or conditional proof on line 8 which allowed me to discharge the "P" assumption in line 3. That contradicted line 1 and so I introduced a contradiction in line 9.

References

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

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

• Tomassi's system has no ⊥ symbol and thus neither (⊥I) rule. But your proof is easily "adapted" to the system. Replace step 6 with (∧I) to get ¬(P∧¬Q) ∧ (P∧¬Q) and then use RAA to get ¬¬Q from 4 and 6. Then derive Q with DNE (Double Negation Elim). The same for steps 9-10. In this way, the total number of steps are 12, as required by the OP. Aug 3 '18 at 8:25
• @MauroALLEGRANZA Thank you. I don't think this particular proof checker's rules will allow me to proceed in that manner, but I can see that the result is the same. Aug 3 '18 at 8:37
• Line 2 assumes a definition for --> that wasn't in the OP's list of rules. Aug 13 '18 at 15:15
• @DanChristensen Line 2 is an assumption starting a subproof. I will have to discharge that assumption (end the subproof) before I finish. That subproof ends with a contradiction on line 9 which allows me to discharge the assumption (close the subproof) with an indirect proof (IP). That step on line 10 is also the desired conclusion and so the proof completes. Line 2 is not coming from a definition of the conditional statement in line 1, but from negating the conclusion. Aug 13 '18 at 15:25
• I see. I wasn't familiar with your notation. Makes sense now. Thanks. Aug 13 '18 at 15:51