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

Question

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.

Answer 1

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.

Answer 2

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/