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

Implication introduction assumes $\varphi$ temporarily, derives $\psi$, and discharges that assumption to conclude $\varphi \to \psi$. Disjunction elimination starts from $\varphi \vee \psi$ and derives the same conclusion $\kappa$ in two separate branches, one assuming $\varphi$ and the other assuming $\psi$.

The boxes delimit subproofs: a locally assumed formula is available inside its box but cannot be used unconditionally outside it. Discharging a box records exactly which dependency has been removed. The proofs below use a vertical bar to mark each active box.