2

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.

|improve this question
  • I made an edit to format the rules for easier reading. I assume I got the list right. You may roll this back or continue editing. I wonder if you have negation introduction or contradiction introduction. – Frank Hubeny Aug 24 '18 at 22:30
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.

|improve this 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]

|improve this answer
1

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

enter image description here

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.

enter image description here

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.

enter image description here

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:

enter image description here

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/

|improve this answer
  • By DeMorgan this is obvious as general algorithm is just to remove negation from outside, negate any element on the next step of hierarchy and flip conjunctions and disjunctions. – rus9384 Aug 25 '18 at 0:36
  • @rus9384 Yes, it is obvious. I would expect to do it in two lines, premise and conclusion, but this proof checker, assuming I used it efficiently, made me use 5 lines. – Frank Hubeny Aug 25 '18 at 1:40
  • @FrankHubeny Many thanks for your prompt reply. However, I do not know contradiction introduction yet. So would you mind showing me how to solve it without that one please? – Diego Ruiz Haro Sep 6 '18 at 20:13
  • @DiegoRuizHaro You have reductio ad absurdum (RAA) which is similar. I don't have that rule in the proof checker that I am using, but I imagine it goes the same way except instead of introducing the contradiction and then discharging the assumption with an indirect proof, you may have to reach something like P & ~P and then discharge the assumption with an RAA rule of some sort. – Frank Hubeny Sep 6 '18 at 20:22
  • @FrankHubeny Thanks again for the help. I am still stuck on the disjunction elimination. Which is the conclusion I have to derive from both disjuncts in order to validate the disjunction elimination? – Diego Ruiz Haro Sep 6 '18 at 21:28

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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