= Solution
Write $D(\phi,\psi)=\neg(\neg\phi\land\neg\psi)$. We derive the two <disjunction introduction rules> and the <disjunction elimination rule> without using any disjunction rule inside the derivations.
For left introduction, start with $\phi$ and temporarily assume $\neg\phi\land\neg\psi$. The <conjunction elimination rule> gives $\neg\phi$, and the <negation elimination rule> gives $\bot$. Discharge the temporary conjunction by the <negation introduction rule>, concluding $D(\phi,\psi)$. For right introduction, start with $\psi$ and use the right <conjunction elimination rule> to obtain $\neg\psi$ instead. Thus either input derives the required encoded disjunction.
For elimination, suppose $D(\phi,\psi)$ is available, together with a derivation of $\kappa$ from an additional assumption $\phi$ and a derivation of $\kappa$ from an additional assumption $\psi$. Keep their common external context fixed. Temporarily assume $\neg\kappa$ under label $a$. Temporarily assume $\phi$ under label $b$ and insert the supplied first branch derivation to obtain $\kappa$. <Negation elimination rule> gives $\bot$, so <negation introduction rule> discharges $b$ and gives $\neg\phi$. Repeat with a temporary assumption $\psi$ under label $c$ and the supplied second branch derivation, discharging $c$ to obtain $\neg\psi$.
<Conjunction introduction rule> now gives $\neg\phi\land\neg\psi$. Its negation $D(\phi,\psi)$ gives $\bot$ by <negation elimination rule>. The supplied <reductio ad absurdum> rule discharges $a$ and yields \b[$\kappa$]. This discharges the two branch assumptions as required and proves the encoded elimination rule. Its last step uses <classical propositional logic>; the same encoded elimination principle is not generally available in <Intuitionistic propositional logic>.
Back to article page
