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 (resit) / 7 / a / Solution

The implication introduction rule opens a subproof under a temporary assumption $\varphi$, derives $\psi$, then performs assumption discharge to conclude $\varphi \to \psi$. The negation introduction rule instead derives logical falsity $\perp$ under a temporary assumption $\varphi$, discharges it, and concludes $\neg \varphi$:The rectangular boxes delimit these subproofs and the scope of their temporary assumptions. A line depending on the boxed temporary assumption cannot simply be used outside the box. The relevant introduction rule exports the indicated logical implication or negation; other surrounding assumptions $\Gamma$ stay in force.