I have a question about the methodology of natural deduction, more specifically finding a proof in natural deduction.
The assignment says:
Find a proof for the formula $(P \rightarrow \neg P) \rightarrow (P \rightarrow Q)$.
If I'm not entirely mistaken, this works as a bottom-rule (not sure of the correct translation), meaning that if you imply that something false is true, you can conclude anything on that premise.
Obviously, this being because $P$ can't imply the negation of $P$, but I suppose you can show how you could theoretically prove it in natural deduction.
(Correct me if I'm wrong, I am not particularly good with natural deduction!)
So let's imply that I'm right, how do I go on and make the proof for the deduction?
Do I simply just close the assumption of $P$, conclude $\neg P$ from that and then conclude $(P \rightarrow Q)$ from that again, before ending on the conclusion of $Q$?
Best Answer
Your intuition is absolutely correct. Below I formalized it in a derivation in natural deduction.
I assume that $\lnot P $ is a shorthand for $P \to \bot$, thus inference rules $\lnot_\text{intro}$ and $\lnot_\text{elim}$ are just special cases of $\to_\text{intro}$ and $\to_\text{elim}$.
The following is a derivation (without assumptions) of the formula $(P \to \lnot P) \to (P \to Q)$ in natural deduction. Symbols $*$ and $\circ$ mark which assumptions are discharged by the corresponding instance of the rule $\to_\text{intro}$. The rule $\text{efq}$ (ex falso quodlibet or principle of explosion) is the special case of the rule $\text{raa}$ that does not discharge any assumption.
\begin{equation} \dfrac{\dfrac{[P \to \lnot P]^\circ \qquad[P]^*}{\lnot P}\to_\text{elim} \qquad [P]^*}{\dfrac{\dfrac{\bot}{Q}\scriptsize{\ \text{efq}}}{\dfrac{P \to Q}{(P \to \lnot P) \to (P \to Q)}\to_\text{intro}^\circ}\to_\text{intro}^*}\lnot_\text{elim} \end{equation}