\begin{frame} \frametitle{MT and $\neg\neg_i$ as ``derived rules''} \begin{goal}{} The $\neg\neg_i$ rule derives \;$\neg\neg \alpha$\; from \;$\alpha$. \medskip\pause We can derive it using other rules as follows: \smallskip \begin{tikzpicture} \naturaldeduction{ \mpause[1]{ \proofstep{$\alpha$}{premise}; } \mpause{ \proofbox{ \mpause{ \proofstep{$\neg \alpha$}{assumption}; } \mpause{ \proofstep{$\bot$}{$\neg_e$ 1,2}; } } } \mpause{ \proofstep{$\neg\neg \alpha$}{$\neg_i$ 2--3}; } } \end{tikzpicture} \pause\pause\pause\pause\pause\pause \smallskip Thus: $\alpha \;\vdash \neg\neg\alpha$\;. \end{goal} \end{frame}