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 ? – Geoffrey Thomas Jul 19 '18 at 20:37
• 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
• 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:

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