# Natural Deduction proof using basic rules only

I need some assistance solving what seems to be a very intuitive problem, but becomes tough when only using strict natural deduction and not assuming De Morgan laws.

Laws allowed: Implication, And, Or, MT, PBC, Copy Rule, Negation, Double Negation, Contradictions, law of excluded middle

I'm thinking it uses the law of excluded middle but I can't quite figure it out.

$$\lnot(P \land \lnot Q), \; (\lnot P \to S) \land \lnot Q \;\;\; \text{premises} \tag{1}$$

$$T \lor S \;\;\; \text{conclusion} \tag{2}$$

• Please copy-paste the formulas into the text... they are only two. – Mauro ALLEGRANZA Jan 18 at 15:12
• I added the formulas as mathjax. There's a tutorial and reference here – Gregory Nisbet Jan 18 at 16:12

Hint

1. $$\lnot (P \land \lnot Q)$$ --- premise

2. $$(\lnot P \to S) \land \lnot Q$$ --- premise

3. $$\lnot Q$$ --- from 2) by $$(\land \text E)$$

4. $$P$$ --- assumed [a]

5. $$(P \land \lnot Q)$$ --- from 4) and 3) by $$(\land \text I)$$

and so on, deriving the sought conclusion: $$T \lor S$$.
The Natural Deduction rules needed, in addition to the $$\land$$-rules above, are $$(\lnot \text I), (\to \text E)$$ and $$(\lor \text I)$$.
• On line 4, just assert ¬P∨P and so on line 8 you need only assume P. There is no need for the double negation elimination. – Graham Kemp Jan 19 at 0:40
• Indeed you do not need LEM at all. Since you can derive a contradiction when you assume P, you have an Indirect Proof of ¬P and so may infer S from ¬P →S. – Graham Kemp Jan 19 at 0:50