# Fitch natural deduction proof of $\vdash (\neg P \lor Q) \to (P \to Q)$

I have been working on a problem for hours now - trying to prove a statement which has no premises. This is what the problem looks like:

You can see that so far I've tried to work my way backwards, starting with the answer, but without premises I am finding it very difficult to move forward. I've gone through my textbook back and forth and the examples in there are much less complex than this one. I'm pretty sure this is a rather obvious one, but I just can't seem to figure it out.

Thanks so much.

• Here is is the almost the exact same question with answers: philosophy.stackexchange.com/questions/46774/… "Almost the same" because your statement is weaker (you only need to show $\to$, not $\leftrightarrow$), so simply leave away the subproof of the other direction and make $\to I$ the last rule application (lines 1-8 in the answer by Frank Huberny). – lemontree May 4 at 18:05
• Thanks @lemontree - I guess a little searching will go a long way! I just have one other question - I understand the use of Modus Tollens (MT) (if you can disprove the consequent of a conditional you can disprove the antecedent). However, in the realm of the course I'm doing (working from the Language Proof And Logic textbook), there is no use of the so-called 'derived rules', only the basic rules. Modus Tollens is not covered in that book, therefore I can't use that rule in my exam. So I'm not sure what alternative there is to using MT in that situation? – Gerhardus Carinus May 4 at 18:43
• I see MT nowhere used in the proof of $(¬P ∨ Q) → (P → Q)$, so I guess that's a different question? If you are not allowed to presuppose derived rules, you just have to show their derivability yourslelf. That is, start with the assumptions $P \to Q, \neg Q$, and derive $\neg P$ directly (this will be a proof by contradicton on a new assumption $\neg P$). – lemontree May 4 at 18:59
• You could also ask your instructer whether it's allowed to "source out" the derivation of $P \to Q, \neg Q \therefore \neg P$ into a separate proof, name it (e.g. $\mathcal{D}_1$ - D for derivation) and reference that proof in the larger proof. This is useful especially in proofs that are already large enough or when you need the derived rule for more than one proof. – lemontree May 4 at 19:02
• You will see line 8 states the MT rule: {2,3} 8. ~~Q 2,7 MT – Gerhardus Carinus May 4 at 19:07

I'd go about it a bit differently: we need a rule to eliminate the $$\lor$$, in the system I learnt there was a $$\lor$$-elimination rule of the form (see also here:

If $$P \lor Q$$ holds, and we can prove $$R$$ from the assumption $$P$$ in some subproof (so $$P \to R$$ from the introduction of $$\to$$ rule) and also $$Q \to R$$ (via the same rule and some subproof), then we can conclude $$R$$; if $$R$$ follows from both members of a disjunction and the disjunction holds we conclude $$R$$.

So

1. $$\lnot P \lor Q$$ (base assumption we will eliminate at the end)
2. $$P$$ (we want to show $$P \to Q$$ eventually so we assume this, so a start of a subproof).
3. $$\lnot P$$ (assumption 1 for the elimination of $$\lor$$).
4. $$\bot$$ ((2+3: introduction of falsum $$\bot$$), or maybe in your system you need to go via $$P \land \lnot P$$ first?)
5. $$Q$$ (from 4: Ex Falso Quodlibet, or whatever you call the rule).
6. $$\lnot P \to Q$$ (from 3-5), end of subproof that started at 3).
7. $$Q$$ (assumption, new subproof).
8. $$Q$$ (trivial conclusion/copy from 7., I used to have to do this explicitly)
9. $$Q \to Q$$ (intro $$\to$$) from 7-8 end of subproof 2.
10. $$Q$$ ( from elimination of $$\lor$$, we have 1. holding, and combining with 6. and 9. we apply the rule I described above.)
11. $$P \to Q$$ from the subproof that started at 2. and ended at 10. asumption 2. can be dropped now).
12. $$\lnot P \lor Q) \to (P \to Q)$$ (from 1. - 11., assumption 1 is now dropped and we have an assumptionless proof of the statement.

On line 3 what you appear to be wanting to use is disjunctive syllogism (DS). This rule is available in this proof checker but it may require you to first construct $$\lnot\lnot P$$. However, that is easy to do as shown on lines 3-5 below. Once that is done, you can use disjunctive syllogism on lines 1 and 5 to derive $$Q$$. Then follow your approach to complete the proof.

Here is what the proof might look like:

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/