Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof / 7 / a / i / Solution

In natural deduction, conjunction introduction combines derivations of $\varphi$ and $\psi$ under the available assumptions into $\varphi \wedge \psi$. Disjunction elimination takes $\varphi \vee \psi$ and two subproofs of the same conclusion $\kappa$, one assuming $\varphi$ and the other assuming $\psi$, and concludes $\kappa$. Implication introduction takes a subproof deriving $\psi$ from a temporary assumption $\varphi$, and concludes $\varphi \to \psi$.

The rectangular boxes mark the scopes of temporary assumptions. The disjunction elimination rule discharges its two case assumptions, while the implication introduction rule discharges the antecedent assumption. Other surrounding assumptions remain in force; intermediate results depending on the boxed assumptions cannot be exported arbitrarily. Schematically,Here the square brackets designate the assumptions discharged by the corresponding inference rule.