Problem: Prove that $P \lor S$ follows from the premises: $P \lor (Q \land R)$ and $(\lnot Q \lor \lnot R) \lor S$
So far I have been able to prove that $(\lnot Q \lor \lnot R)$ equates to $\lnot (Q \land R)$ using De Morgan's theorem and want to prove that this cancels out $(Q \land R)$, but I have trouble taking it further. Here is what I have so far:
On
@lemontree gives a nice proof ... but I want to provide a general comment/piece of advice about your proof:
Whenever you start subproofs, you should always indicate what you want at the end of each subproof, before diving into the details of the subproof. This is what provides structure to the proof .... and without it, you're going to get lost, believe me!
From what you have, I can immediately tell that you are not doing this ... and thus get lost. Indeed, since the goal you have is $P \lor S$, you should try and get that as the last line of each subproof. So, for your very first subproof, where you assume $S$, the last line you are looking for is $P \lor S$. Of course, that is a simple $\lor I$ ... but the fact that you didn't speaks volumes. Indeed, for the second subproof, while you proved DeMorgan, you did once again not indicate what it is that you want at the end of the subproof ... which once again should be $P \lor S$.
So, your initial set-up should be:
Which you can then follow up with:
And go from there ... see how this works? First you do the proof set-up/organization/plan/skeleton .. and then you work out the details
You don't have to go the detour of proving the DeMorgan law $\neg Q \lor \neg R \leftrightarrow \neg(Q \land R)$ and then derive a contradiction to $Q \land R$, instead you can show the contradiction directly, where the main operation you do is a disjunction elmination on the premise $\neg Q \lor \neg R$. That is, you have two subproofs, one starting with the assumption $\neg Q$ and one starting with $\neg R$, and each of these assumptions will lead to a contradiction. One assumption will contradict $Q$, and one $R$, both of which we can get get out of $Q \land R$. And then, since you know that at least one out of $\neg Q$ or $\neg R$ holds and either of them leads to a contradiction, you may conclude that the formula $\neg Q \lor \neg R$ leads to a contradiction. You already were on the right track by doing disjunction elimination on $\neg Q \lor \neg R$ and starting two subprofos with $\neg Q$ and $\neg R$ respectively, it's just that you don't need the formula $\neg(\neg Q \lor \neg R)$ anywhere in your proof, you can just derive the contradiction between $\neg Q \lor \neg R$ and $Q \land R$ directly:
(You also could now derive one direction of one of the De Morgan laws in two more steps by doing $\neg$ Intro on one of the premises (either $Q \land R \vdash \neg(\neg Q \lor \neg R)$ or $\neg Q \lor\neg R \vdash \neg(Q \land R)$, but this is not necessary, because we already have the desired contradiction.)
From this contradiction we can then, by applying ex falso quodlibet, conclude whatever formula suits us. Here we're interested in the formula $P \lor S$. This should, by the way, also be the formula you derive from the assumption $S$ further above, since $P \lor S$ is the formula we need to show eventually, and we want to derive it by doing $\lor$ elimination on the premise $(\neg Q \lor \neg R) \lor S$, so we need $P \lor S$ to be the conclusion of both of the two subproofs starting with $S$ and with $\neg Q \lor \neg P$.
However, it is easier to do the nesting of the subproofs the other way round than you started it and instead have the $\lor$ elimination on $P \lor (Q \land R)$ be the outermost operation and the $ \lor$ elimination on $(\neg Q \lor R) \lor S$ inside it, so this is what the final proof then looks like: