= Solution
<Implication introduction> assumes $\phi$ temporarily, derives $\psi$, and discharges that assumption to conclude $\phi\to\psi$. <Disjunction elimination> starts from $\phi\lor\psi$ and derives the same conclusion $\kappa$ in two separate branches, one assuming $\phi$ 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.
Back to article page
