= Solution
The <implication introduction rule> opens a <subproof> under a <temporary assumption> $\phi$, derives $\psi$, then performs <assumption discharge> to conclude $\phi\to\psi$. The <negation introduction rule> instead derives <logical falsity> $\bot$ under a <temporary assumption> $\phi$, discharges it, and concludes $\neg\phi$:
$$
\boxed{\frac{\Gamma,\phi\vdash\psi}{\Gamma\vdash\phi\to\psi}
\qquad
\frac{\Gamma,\phi\vdash\bot}{\Gamma\vdash\neg\phi}.}
$$
The rectangular boxes delimit these <subproofs> and the scope of their <temporary assumptions>. A line depending on the boxed <temporary assumption> cannot simply be used outside the box. The relevant introduction rule exports the indicated <logical implication> or <negation>; other surrounding assumptions $\Gamma$ stay in force.
Back to article page
