= Solution
The <implication introduction rule> opens a <subproof> with a <temporary assumption> $\phi$, derives $\psi$, and discharges that assumption to conclude \b[$\phi\to\psi$]. The <negation introduction rule> opens a <subproof> with a <temporary assumption> $\phi$, derives <logical falsity> $\bot$, and discharges it to conclude \b[$\neg\phi$].
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.
Back to article page
