# Unsure how to solve this proof with natural deduction.

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?

updated proof from row 4 onwards with or elimination

• Welcome to MSE. I suggest that you learn MathJax and that you use it, instead of posting images. – José Carlos Santos Sep 19 '17 at 9:41
• Looks to me like you want to go about $f \vdash \lnot k \vdash \lnot t \vdash s$ – DanielV Sep 19 '17 at 12:29

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

• Thank you. So is there a rule that I can use that says that if I prove the falsified statement $(t \land \lnot s$ I can infer the other? – Gurkang Sep 19 '17 at 10:19
• Or elimination. – quasi Sep 19 '17 at 10:28
• Okay. So it would be that on line 10 I could write $\lnot t \land s (\lor e 5-9, 1)$ ? – Gurkang Sep 19 '17 at 10:30
• Well, perhaps not. As user482338 notes, "or elmination" doesn't work as simply as that. I've edited my answer accordingly. – quasi Sep 19 '17 at 10:52
• I've updated my original question with a new revised proof and tried to apply your help – Gurkang Sep 19 '17 at 11:07

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.

• The rules I have are the basic rules for $\land , \lor , \to , \bot and \lnot \lnot$. Would I be able to do after line 9: $s (5-9$? – Gurkang Sep 19 '17 at 10:38
• @user482338: Agreed, your objection to my "or elimination" claim is valid. – quasi Sep 19 '17 at 10:40
• @user482338: Thanks for straightening me out on "or elimination". I gave you credit (+1) for each of your answers. It appears you're new to MSE. You're a welcome addition. – quasi Sep 19 '17 at 12:10

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

• 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? – Gurkang Sep 19 '17 at 10:24

There are many different formal proof systems, all with slightly different rules. Here is a proof in my favorite system, Fitch: