I’m working on a practice question on my logic textbook. And I’m stuck at this question.

This is what I have so far:

1. ~(P & Q)   Assumption/ Negated Eelimination 
2.     P          Assumption/Negated Introduction 
3.       Q          Assumption/Negated Introduction 
4.       P&Q        2,3 conjunction Introduction
5.     ~(P&Q)       1 Reteration 
6.    ~Q            2-5 Negated Introduction 

Now, as long as I can derive a Q, then I will be able to Derive (P&Q) I’m wondering if some one can give me some insight.

Thanks in Advance

  • Isn't this just logic, not philosophy of logic or logic with any philosophical dimension ? – Geoffrey Thomas Jul 19 '18 at 20:37
  • 1
    Can't you use de Morgan? Just open the brackets of NAND part. – rus9384 Jul 19 '18 at 20:45
  • So this is philosophy of logic or logic with a philosophical dimension ? Interesting. – Geoffrey Thomas Jul 19 '18 at 21:45
  • What is the question that you are stuck on and what is the name of the logic book you are using. Do you use any software for proof checking? – Frank Hubeny Jul 19 '18 at 22:13
  • 1
    As you can see from the answers below, the details depend on the proof systems you are allowed to use: if, e.g. SD is Natural Deduction, you have not a "prinmitive rule" for De Morgan. You have to use instead Double Negation. So, please, specify what system SD stands for. – Mauro ALLEGRANZA Jul 20 '18 at 7:31

You won’t be able to prove either disjunct, as neither is a logical truth. Instead, assume the negation of what you want to prove and then derive a contradiction. I’m sure others can format this much more beautifully than I can, but here’s a proof. I use ‘F’ to mean the falsum/contradiction and I rely on a DeMorgan equivalence, but this, of course, be eliminated.

|1. ~((P&Q)∨(~P∨~Q))........Assume
||2. P&Q................................Assume
||3. (P&Q)∨(~P∨~Q)...........2, ∨Intro
||4. F ................................... 1,3
|5. ~(P&Q).......................... 2-4, ~Intro
|6. ~P ∨ ~Q........................ 5,DeMorgan
|7. (P&Q)∨(~P∨~Q).......... 6, ∨Intro
|8. F.................................... 1,7
9. (P&Q)∨(~P∨~Q).......... 1-8, ~Elim


another approach giving the minimum number of steps (though not a formal proof):

1. (P & Q) v ~(P & Q)              law of excluded middle
2. (P & Q) v (~P v ~Q)             DeM 1

Using the natural deduction and proof checker associated with forall x: Calgary Remix, I get the following proof:

enter image description here

In line 1 begin a subproof by assuming the negation of what you want to prove.

In line 2 apply DeMorgan's rule to line 1.

In line 3 eliminate the first part of the conjunction in line 2.

In line 4 apply DeMorgan's rule to line 3.

In line 5 eliminate the second part of the conjunction in line 2.

In line 6 introduce a contradiction based on lines 4 and 5.

In line 7 discharge the assumption in line 1 and exit the subproof using indirect proof (IP) to reach the desired conclusion.


I would like to offer the following "proof."

1 - If (A) V ~(A) is a SD theorem,
2 - A = (P & Q) : definition
3 - (P & Q) V (~P V ~Q) : given
4 - (P & Q) V ~(P & Q) : DeMorgan (on 2nd part)
5 - (A) V ~(A) : substitution
6 - Therefore (P & Q) V (~P V ~Q), is a SD theorem.


Strategy: Demonstrate that assuming the target is false leads to a contradiction no matter what we assume about the literals.

The Fitch Style proof is as follows: Assume some stuff and, then, deny everything. Basically.

 1.|  |_ ~((p & q) v (~p v ~q))      : Assumption
 2.|  |  |_ p                        : Assumption
 3.|  |  |  |_ q                     : Assumption

 6.|  |  |  | #                      : Negation Elimination (1,5)
 7.|  |  | ~q                        : Negation Introduction (3-6)

10.|  |  | #                         : Negation Elimination (1,9)
11.|  | ~p                           : Negation Introduction(2-10)

14.|  | #                            : Negation Elimination (1,13)
15.| ~~((p & q) v (~p v ~q))         : Negation Introduction (1-14)
16.| ((p & q) v (~p v ~q))           : Double Negation Elimination (15)

Opps. I missed a few steps. :)

NB: The DNE at the end suggests this is not a constructively valid theorem. Indeed, it is not. Still ((p & q) v (~p v ~q)) is a theorem of classical logic, as shown by using only the basic rules of inference for natural deduction.

PS: Using # as the falsum constant

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.