I'm really new to natural deduction and proofs with this. But I've been trying to solve the problem on the attached paper for a while and I just don't feel my solution is correct.
Can someone help me with this and explain how I should be attacking these problems.
I want to prove that $(T ∧ ¬S) ∨ (¬T ∧ S), ¬(K ∧ F), T → K ∴ F → S$.
I'm trying to prove that F -> S
I've updated parts of the proof from row 4 with the information given to me below. Does it look better?
On
The justification for the seventh row is missing the reference to the sixth row (where the antecedent of the conditional in row three is).
Up until the ninth row, everything else is correct. Your tenth row is wrong in more ways than I care to explain. What I would do instead is continue the subproof that started in row 5 by inferring $s$ from $\bot$ and end the subproof there.
Then I would start another subproof with $\neg t \land s$ as a premise and try to derive $s$. By this point you will have derived $s$ at the end of both "parts" of the premise on the first row. Thus you can use disjunction elimination to find $s$.
On
Answering Gurgank's comments as I'm unable to do so.
Thank you for the input. When you say infer s from the assumption that I start at row 5, how exactly would I do that? Doesn't the assumption end with the falsum that disproves the assumption? Can I continue after that even though its a false?
Yes, probably can proceed. That depends on which rules you have at your disposal, but I'll venture in saying that you can use $\bot$ elimination to infer whatever you want in that subproof, namely $s$.
So is there a rule that I can use that says that if I prove the falsified statement $t∧¬s$ I can infer the other? – Gurkang 9 mins ago
Or elimination. – quasi just now
It is very unlikely that you have such a rule at your disposal and $\lor$ elimination doesn't work that way.
Line $10\;$of your original proof attempt is wrong. The operation $\lnot$ is not distributive over $\land$.
Instead, just use the fact that you've falsified the assumption $(t \land \lnot s)$.
That, together with the premise $(t \land \lnot s) \lor (\lnot t \land s)$, yields $(\lnot t \land s)$, which then yields $s$.
EDIT:
As user482338 correctly observes, after falsifying $(t \land \lnot s)$, you can't immediately use "or elimination".
Instead, since in the subproof you proved $\bot$, you can follow that with anything (since $\bot \rightarrow\;$"anything"). In particular, you can get $\bot \rightarrow s$, so that subproof yields $(t \land \lnot s) \rightarrow s$.
To make use of "or elimination", your next goal is to prove $(\lnot t \land s) \rightarrow s$, which can be accomplished with an easy subproof.
Then you can apply "or elimination" to get $s$.
Here's a modified version of your proof, with appropriate corrections . . . \begin{align*} 1.&\;\;\;(t \land \lnot s) \lor (\lnot t \land s)&&(\text{P})\\[4pt] 2.&\;\;\;\lnot(k \land f)&&(\text{P})\\[4pt] 3.&\;\;\;t \rightarrow k&&(\text{P})\\[4pt] 4.&\;\;\;f&&(\text{A})\\[4pt] 5.&\;\;\;\;\qquad t \land \lnot s&&(\text{A})\\[4pt] 6.&\;\;\;\;\qquad t&&(\land\,\text{E})&&5\\[4pt] 7.&\;\;\;\;\qquad k&&(\rightarrow\text{E})&&6,3\\[4pt] 8.&\;\;\;\;\qquad k \land f&&(\land\,\text{I})&&4,7\\[4pt] 9.&\;\;\;\;\qquad \bot &&(\bot\,\text{I})&&8,2\\[4pt] 10.&\;\;\;\;\qquad s &&(\bot\,\text{E})&&9\\[4pt] 11.&\;\;\;(t \land \lnot s) \rightarrow s&&(\rightarrow\text{I})&&5\text{$-$}10\\[4pt] 12.&\;\;\;\;\qquad \lnot t \land s&&(\text{A})\\[4pt] 13.&\;\;\;\;\qquad s&&(\land\,\text{E})&&12\\[4pt] 14.&\;\;\;(\lnot t \land s) \rightarrow s&&(\rightarrow\text{I})&&12\text{$-$}13\\[4pt] 15.&\;\;\;s&&(\lor\,\text{E})&&1,11,14\\[4pt] 16.&\;\;\;f \rightarrow s&&(\rightarrow\text{I})&&4,15\\[4pt] \end{align*}