Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof / 7 / e

Only $\psi$ requires a natural deduction proof. Assume $h:(A\vee B)\to C$. Within that assumption, temporarily assume $a:A$. By disjunction introduction, obtain $A\vee 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)\vee (B\to C)$. Finally discharge $h$ by the implication introduction rule:All temporary assumptions are discharged. No classical rule is needed; the same proof works in Intuitionistic propositional logic. The false propositional formula $\phi$ has no proof in this sound natural deduction system.