= Solution
The <conjunction introduction rule> derives $\phi\land\psi$ from proofs of $\phi$ and $\psi$ in the current context. The <disjunction elimination rule> derives a common conclusion $\kappa$ from $\phi\lor\psi$, a subproof of $\kappa$ under temporary assumption $\phi$, and a subproof of $\kappa$ under temporary assumption $\psi$. The <implication introduction rule> derives $\phi\to\psi$ by temporarily assuming $\phi$ 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.
$$
\boxed{\text{Boxes record local assumptions and their discharge, not additional premises}.}
$$
Back to article page
