Natural Deduction proof using basic rules only

Question

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

Answer 1

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

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

Answer 2

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