How to prove P ∨ Q : ~ (~P & ~Q) with natural deduction

Question

Here's another Tomassi's problem I can't solve (Logic, Exercise 3.9.1.17, page 106):

P ∨ Q : ~ (~P & ~Q)

I have to use natural deduction and the only rules I know are:

• assumptions,
• modus ponendo ponens,
• modus tollendo tollens,
• double negation,
• reductio ad absurdum,
• conditional proof,
• v-introduction,
• v-elimination,
• and introduction,
• and elimination.

Tomassi's proof consists of 11 steps.

So far this is my solution:

[1] (1) P ∨ Q Premise

[2] (2) ~P & ~Q Assumption for RAA

[2] (3) ~P 2 &E

[4] (4) P Assumption and Conclusion from 1st disjunct for vE

[5] (5) Q Assumption 2nd disjunct for vE

[2,5] (6) ~P-->Q 2,5 CP

[2] (7) ~Q 2 &E

[2,5] (8) ~~P 6,7 MT

[2,5] (9) P 8 DNE

[1,2] (10) P 1,4,4,5,9 vE (discharging 4 & 5)

[1,2] (11) ~P&p 2,10 &I

[1] (12) ~(~P & ~Q) 2,11 RAA (discharging 2)

Tomassi's is not given.

Answer 1

This answer will provide a proof based on Paul Tomassi's Logic. The problem is 1.17 in Exercise 3.9 on page 106.

P v Q : ~(~P & ~Q)

P v Q ⊦ ~(~P & ~Q)
{1}    1.   P v Q      Premise
{2}    2.   P          Assumption for vElimination
{3}    3.   ~P & ~Q    Assumption for RAA
{3}    4.   ~P         3 &E
{2,3}  5.   P & ~P     2,4 &I
{2}    6.   ~(~P & ~Q) 3,5 RAA
{7}    7.   Q          Assumption for VElimination
{8}    8.   ~P & ~Q    Assumption for RAA
{8}    9.   ~Q         8 &E
{7,8} 10.   Q & ~Q     7,9 &I
{7}   11.   ~(~P & ~Q) 8,10 RAA
{1}   12.   ~(~P & ~Q) 1,2,6,7,11 vE

The description of reductio ad absurdum (RAA) is on pages 101-5.

The description of vElimination (vE) is on pages 86-9.

The description of &Elimiantion (&E) and &Introduction (&I) is on pages 50-2.

This proof used 12 rather than 11 lines.

---

Reference

Tomassi, P. (1999). Logic (London and New York.

Answer 2

Here is your proof slightly modified...

[1] P ∨ Q --- Premise

[2] ~P & ~Q --- Assumption for RAA

[3] ~P --- from 2 by &E

[4] ~Q --- from 2 by &E

[5] P --- Assumption from [1] for vE (1st one)

[6] ~P & P --- from [3] and [5] by &I

[7] ~(~P & ~Q) --- from [2] and contradiction [6] by RAA

[8] Q --- Assumption from [1] for vE (2nd one)

[9] ~Q & Q --- from [4] and [8] by &I

[10] ~(~P & ~Q) --- from [2] and contradiction [9] by RAA, discharging assumption [2]

[11] ~(~P & ~Q) --- from [5]-[7] and [8]-[10] and [1] by vE, discharging assumptions [5] and [8]

Answer 3

Here is one way to prove this based on Klement's proof checker:

On line 2 I assume the negation of what I want to show. This is a reductio ad absurdum argument designed to allow me to introduction a negation on 10. Although I do not see the negation introduction rule in your list this may give you an idea how to proceed.

On lines 3 and 4 I used conjunction elimination and on lines 5 through 8 I set up a disjunction elimination that completed online 9. It did involve introducing a contradiction on lines 6 and 8. I did not see contradiction introduction on your list of rules, but the reductio ad absurdum suggested to me it might be acceptable.

Here is a proof using disjunction syllogism (DS) a derived rule to cut short the disjunction elimination. This is not on your list. I provide it just to give another perspective on how this might be proven.

Finally, here is a shorter proof (at least in the proof checker I am using) that uses the De Morgan Rule (DeM). That is not on the list of permitted rules, but I offer it as another perspective on the problem when that derived rule becomes available.

The OP provided an attempted proof. This seems to work. Using the rules for the proof checker that I am using I get the following:

There are two differences. For line 6 in the OP's proof I needed three lines, my 6, 7 and 8. For line 11 to reach the contraction, I needed to use a contradiction introduction (⊥I) in my line 13. Otherwise the proofs are similar.

---

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/