# How to show that (P & Q) v (~P v ~ Q) is a theorem in SD

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.

• Isn't this just logic, not philosophy of logic or logic with any philosophical dimension ? Jul 19, 2018 at 20:37
• Can't you use de Morgan? Just open the brackets of NAND part. Jul 19, 2018 at 20:45
• So this is philosophy of logic or logic with a philosophical dimension ? Interesting. Jul 19, 2018 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? Jul 19, 2018 at 22:13
• 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. Jul 20, 2018 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:

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

No answer so far has been purely in SD.

1. |~((P&Q)∨(~P∨~Q)) A/~E
2. | ~P A/~E
3. | (~Pv~Q) 2 vI
4. | (~Pv~Q)v(P&Q) 3 vI
5. | ~((P&Q)∨(~P∨~Q)) 1 R
6. |P 2-5 ~E
7. | ~Q A/~E
8. | (~Pv~Q) 7 vI
9. | (~Pv~Q)v(P&Q) 8 vI
10. | ~((P&Q)∨(~P∨~Q)) 1 R
11. |Q 7-10 ~E
12. |(P&Q)
13. |(P&Q)v(~P∨~Q) 12 vI
14. |~((P&Q)∨(~P∨~Q)) 1 R
15. (P&Q)∨(~P∨~Q) 1-14 ~E