1

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!

Improve this question
4
  • I made an edit which you may roll back or continue editing. You can see the versions by clicking on the "edited" link above.
    – Frank Hubeny
    Commented Aug 2, 2018 at 20:49
  • As showned by the answer below: when you do not know how to proceed... use a proof by contradiction.
    – Mauro ALLEGRANZA
    Commented Aug 3, 2018 at 5:58
  • Hint: Prove ~[p & ~q] => [p => q]. Then apply the contrapositive.
    – Dan Christensen
    Commented Aug 13, 2018 at 15:08
  • How can I proof: (p ∧ ¬q) ⊢ ¬(p → q)
    – Amela Sultanovic
    Commented Nov 25, 2019 at 13:35

1 Answer 1

Reset to default
3

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.

enter image description here

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/

Improve this answer
5
  • 2
    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.
    – Mauro ALLEGRANZA
    Commented Aug 3, 2018 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.
    – Frank Hubeny
    Commented Aug 3, 2018 at 8:37
  • Line 2 assumes a definition for --> that wasn't in the OP's list of rules.
    – Dan Christensen
    Commented Aug 13, 2018 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.
    – Frank Hubeny
    Commented Aug 13, 2018 at 15:25
  • I see. I wasn't familiar with your notation. Makes sense now. Thanks.
    – Dan Christensen
    Commented Aug 13, 2018 at 15:51

You must log in to answer this question.

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