= Solution
Only $\psi$ requires a <natural deduction> proof. Assume $h:(A\lor B)\to C$. Within that assumption, temporarily assume $a:A$. By disjunction introduction, obtain $A\lor B$; applying $h$ by the <implication elimination rule> gives $C$. Discharge $a$ by the <implication introduction rule> to derive $A\to C$. Disjunction introduction now gives $(A\to C)\lor(B\to C)$. Finally discharge $h$ by the <implication introduction rule>:
$$
\frac{
\begin{array}{c}
[(A\lor B)\to C]^1\qquad
\dfrac{[A]^2}{A\lor B}\ {\lor I_L}\\[3pt]
\dfrac{(A\lor B)\to C\qquad A\lor B}{C}\ {\to E}\\[5pt]
\dfrac{C}{A\to C}\ {\to I}^{,2}\\[5pt]
\dfrac{A\to C}{(A\to C)\lor(B\to C)}\ {\lor I_L}
\end{array}}
{\bigl((A\lor B)\to C\bigr)\to\bigl((A\to C)\lor(B\to C)\bigr)}\ {\to I}^{,1}.
$$
All temporary assumptions are discharged. No classical rule is needed; the same proof works in <Intuitionistic propositional logic>. The false <propositional formula> $\varphi$ has no proof in this sound <natural deduction> system.
Back to article page
