Natural deduction proof of $p \lor (p\implies q)$ with propositional calculus

Question

I'm having a bit of trouble proving this with the propositional calculus rules. $$p \lor (p\implies q)$$ Would someone mind helping me and showing which rules they've used with an explanation! Thanks!

Answer 1

Assume $p$.$\;$Then we get

• $p$$\\[4pt]$
• $p\lor (p\rightarrow q)$

Next, assume $\lnot p$.$\;$Then we get

• $\lnot p$$\\[4pt]$
• $\lnot p \lor q$$\\[4pt]$
• $p\rightarrow q$$\\[4pt]$
• $p\lor (p\rightarrow q)$

In either case, we have $p\lor (p\rightarrow q)$.

Answer 2

Formulas with a disjunction as the main connective are often a bit difficult to derive, if the last step was not simply weakening by $\lor I$. You could try the following stategy:

Base your proof on an analysis by cases -- that is, apply as the final step $\lor E$ -- on $p \lor \neg p$. The formula $p \lor \neg p$ is itself derivable in natural deduction (though a bit difficult as well).
For the case with assumption $p$, you can derive $p \lor (p \to q)$ in one step by application of $\lor I$.
For the case with assumption $\neg p$, derive $p \to q$ via the formula $\neg p \lor q$ obtained in a similar manner.
The proof skeleton then looks as follows:

It now just remains for you to fill in the question marks, that is, the subderivations of $\vdash p \lor \neg p$ and $\neg p \lor q \vdash p \to q$. (Hint: The latter will again end in an $\lor E$ step, with assumptions $\neg p$ and $q$ from which both times you derive $p \to q$).