# Using Fitch proof system to for: Given ¬q, (¬p⇒(¬q⇒¬r)), (s∨r), (s⇒t), and (p⇒t), prove t.

I've been tasked with using the fitch proof system to do the to complete the following proof: Given ¬q, (¬p⇒(¬q⇒¬r)), (s∨r), (s⇒t), and (p⇒t), prove t. I'm experiencing difficulty getting this done. I've tried by assuming ¬t, proving a contradiction and thereby deriving ¬¬t, and then using negation elimination to get t. I've also tried to prove r⇒t and then use or elimination to prove t. I have unfortunately not yet been able to prove t using these approaches. If anyone has any ideas for how I may go about solving this proof, I'd appreciate your sharing them with me.

• You have premises $s \to t$ and $p \to t$; thus, in order to prove $t$, we have to derive either $s$ or $p$. From premise $s \lor r$ by Disjunction Elim one sub-proof gives us $s$ and it's fine. Now we have to work with the other sub-proof, starting with $r$, in order to derive either $s$ or $p$. This one is a little bit tricky... May 30 at 13:30
• Question for clarification: What rules do you have, in particular do you have Disjunctive Syllogism or LEM? May 30 at 19:46
• Andrew L, thank you for trying to help me. I'm able to use the following rules: Reiteration, Negation introduction, Negation elimination, And introduction, And elimination, Or introduction, Or elimination, Assumption, Implication elimination, Biconditional introduction, Biconditional elimination, Universal introduction, Universal elimination, Existential introduction, Existential elimination. May 31 at 11:47

Probably the easiest way forward is to assume $$P$$ and derive $$T$$, then assume $$\neg P$$ and derive $$T$$. Both of these derivations are straightforward. From there, depending on your exact rules, you should be able to extract $$T$$ by itself.

I think this is the easiest way to go about proving it pseudo-Fitch Style:

1. $$\neg q$$ (Assumption)
2. $$\neg p \to (\neg q \to \neg r)$$ (Assumption)
3. $$s \lor r$$ (Assumption)
4. $$s \to t$$ (Assumption)
5. $$p \to t$$ (Assumption)
6. $$r$$ (Hypothesis)
7. $$\neg t$$ (Hypothesis)
8. $$p$$ (Hypothesis)
9. $$t$$ (5,8 $$\to$$ Elim)
10. $$\bot$$ (7,9 $$\bot$$ Intro)
11. $$\neg p$$ (8-10, $$\neg$$ Intro)
12. $$\neg q \to \neg r$$ (2,11 $$\to$$ Elim)
13. $$\neg r$$ (1,12 $$\to$$ Elim)
14. .
15. .
16. $$r \to t$$ (6-15 $$\to$$ Intro)
17. $$t$$ (3,4,16 $$\lor$$ Elim)

I left some of it to fill in since I think that’s probably the trickiest part.

I've tried by assuming ¬t, proving a contradiction and thereby deriving ¬¬t, and then using negation elimination to get t. I've also tried to prove r⇒t and then use or elimination to prove t.

Combine both these approaches. Assume $$\lnot t$$ and then use $$\vee$$-elimination on $$(s\vee r)$$ where you derive contradictions in each case.

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{~~1.~~¬q\\~~2.~~(\lnot p\to(\lnot q\to\lnot r))\\~~3.~~(s\vee r)\\~~4.~~(s\to t)\\~~5.~~(p\to t) }{\fitch{~~6.~~\lnot t}{\fitch{~~7.~~s}{~~~~\vdots\\~~\mathrm h.~~\bot}\\\fitch{~~\mathrm i.~~r}{~~~~\vdots\\~~\mathrm j.~~\lnot r\\~~\mathrm k.~~\bot}\\~~\ell.~~\bot}\\~~\mathrm m.~~\lnot\lnot t\\~~\mathrm n.~~t}$$