= Solution
In <natural deduction>, <conjunction introduction> combines derivations of $\phi$ and $\psi$ under the available assumptions into $\phi\land\psi$. <Disjunction elimination> takes $\phi\lor\psi$ and two <subproofs> of the same conclusion $\kappa$, one assuming $\phi$ and the other assuming $\psi$, and concludes $\kappa$. <Implication introduction> takes a <subproof> deriving $\psi$ from a <temporary assumption> $\phi$, and concludes $\phi\to\psi$.
The rectangular boxes mark the scopes of <temporary assumptions>. The <disjunction elimination rule> discharges its two case assumptions, while the <implication introduction rule> discharges the antecedent assumption. Other surrounding assumptions remain in force; intermediate results depending on the boxed assumptions cannot be exported arbitrarily. Schematically,
$$
\boxed{\frac{\phi\quad\psi}{\phi\land\psi},\qquad\frac{\phi\lor\psi\quad[\phi]\ \vdots\ \kappa\quad[\psi]\ \vdots\ \kappa}{\kappa},\qquad\frac{[\phi]\ \vdots\ \psi}{\phi\to\psi}.}
$$
Here the square brackets designate the assumptions discharged by the corresponding <inference rule>.
Back to article page
