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

The conjunction introduction rule derives $\varphi \wedge \psi$ from proofs of $\varphi$ and $\psi$ in the current context. The disjunction elimination rule derives a common conclusion $\kappa$ from $\varphi \vee \psi$, a subproof of $\kappa$ under temporary assumption $\varphi$, and a subproof of $\kappa$ under temporary assumption $\psi$. The implication introduction rule derives $\varphi \to \psi$ by temporarily assuming $\varphi$ and proving $\psi$.

The rectangular boxes delimit subproofs and the scope of their temporary assumptions. The disjunction elimination rule discharges the two case assumptions; the implication introduction rule discharges its antecedent assumption. Formulas depending on a boxed assumption cannot simply escape that box. Other undischarged assumptions remain in force, and nested boxes can access the assumptions of enclosing boxes.