= Solution
* The <implication introduction rule> assumes $\phi$ locally, derives $\psi$ under that assumption, then concludes $\phi\to\psi$ while discharging the temporary assumption.
* The <disjunction elimination rule> uses $\phi\lor\psi$ and two local cases: one derives a common conclusion $\kappa$ from $\phi$, and the other derives that same $\kappa$ from $\psi$. It concludes $\kappa$ and discharges both case assumptions.
* The <negation introduction rule> assumes $\phi$ locally and derives <logical falsity>. Discharging that assumption gives $\neg\phi$.
The boxes delimit a <subproof> and identify the lifetime of its temporary assumptions. A result depending on a boxed assumption is available inside that box and its nested boxes; it cannot simply be exported outside. The enclosing rule specifies what may be exported and which assumptions are discharged. Other premises on which the derivation depends remain undischarged. This <assumption discharge> discipline distinguishes a conditional argument from an unconditional <proof>.
Back to article page
