\begin{frame} \frametitle{Law of Excluded Middle is Derivable} \begin{exampleblock}{} The LEM rule \quad$\vdash\; \alpha \vee \neg \alpha$\quad is derivable: \medskip \begin{tikzpicture} \naturaldeduction{ \mpause[1]{ \proofbox{ \mpause{ \proofstep{$\neg (\alpha \vee \neg \alpha) $}{assumption}; } \mpause{ \proofbox{ \mpause{ \proofstep{$\alpha$}{assumption}; } \mpause{ \proofstep{$\alpha \vee \neg \alpha$}{$\vee_{i_1}$ 2}; } \mpause{ \proofstep{$\bot$}{$\neg_e$ 3,1}; } } } \mpause{ \proofstep{$\neg \alpha$}{$\neg_i$ 2--4}; } \mpause{ \proofstep{$\alpha \vee \neg \alpha$}{$\vee_{i_2}$ 5}; } \mpause{ \proofstep{$\bot$}{$\neg_e$ 6,1}; } } } \mpause{ \proofstep{$\alpha \vee \neg \alpha$}{PBC 1--7}; } } \end{tikzpicture} \end{exampleblock} \end{frame}