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} $$

  • $\begingroup$ Please copy-paste the formulas into the text... they are only two. $\endgroup$ Jan 18, 2021 at 15:12
  • $\begingroup$ I added the formulas as mathjax. There's a tutorial and reference here $\endgroup$ Jan 18, 2021 at 16:12

2 Answers 2



  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)$

  1. Contradiction !

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)$.

  • $\begingroup$ Thanks boss, ended up getting it because of you. u the man $\endgroup$
    – algebruh
    Jan 18, 2021 at 17:30

My proof here. Let me know if you see anything wrong with it, or if there's a more efficient way

  • $\begingroup$ 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. $\endgroup$ Jan 19, 2021 at 0:40
  • $\begingroup$ 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. $\endgroup$ Jan 19, 2021 at 0:50

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .