= Solution
The <conjunction introduction rule> combines derivations of $\phi$ and $\psi$ into a derivation of $\phi\land\psi$. Both conclusions must be available under the current assumptions.
The <disjunction elimination rule> is reasoning by cases: from $\phi\lor\psi$, a <subproof> deriving the same conclusion $\kappa$ under $\phi$, and another <subproof> deriving $\kappa$ under $\psi$, conclude $\kappa$. It discharges the two case assumptions, not any surrounding premises.
The <implication introduction rule> derives $\phi\to\psi$ by temporarily assuming $\phi$ and deriving $\psi$; it then discharges that occurrence of the assumption $\phi$.
Thus
$$
\boxed{\text{the boxes delimit temporary assumptions, their dependent subproofs, and their discharge}.}
$$
A conclusion inside a box cannot simply be reused outside it without an appropriate <inference rule>. Any other undischarged assumptions continue to constrain the result. These are exactly the rules printed in Figure 1.<Digital systems, linear algebra, introduction to formal proof examination paper by the University of Oxford (2013)>[Printed p. 9, Figure 1]{ref}
Back to article page
