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 / 7 / a

The implication introduction rule opens a subproof with a temporary assumption $\varphi$, derives $\psi$, and discharges that assumption to conclude $\varphi \to \psi$. The negation introduction rule opens a subproof with a temporary assumption $\varphi$, derives logical falsity $\perp$, and discharges it to conclude $\neg \varphi$.

The boxes record the scopes and dependencies of the temporary assumptions. A result derived inside a box cannot be used outside it without the appropriate discharge rule; it may depend on the boxed assumption. Other, surrounding assumptions remain in force. This is how the natural deduction rules distinguish a conditional derivation from an unconditional assertion.