\begin{frame}
  \frametitle{Proof by Contradiction as a Rule}

  \begin{goal}{Proof by Contradiction Rule}
    \vspace{-1ex}
    \begin{align*}
      \infer[\rulename{PBC} \quad (or \rulename{RAA})]
      {\alpha}
      {
        \framebox{\parbox{.8cm}{\centerline{$\neg\alpha$}\centerline{$\vdots$}\centerline{$\bot$}}} 
      }
    \end{align*}
  \end{goal}
  \pause
  
  \begin{exampleblock}{}
    We now can derive the rule \quad$\neg\neg_e$\quad:
    \medskip
    
    \begin{tikzpicture}
    \naturaldeduction{
      \mpause[1]{
        \proofstep{$\neg\neg \alpha$}{premise};
      }
      \mpause{
        \proofbox{
          \mpause{
            \proofstep{$\neg \alpha$}{assumption};
          }
          \mpause{
            \proofstep{$\bot$}{$\neg_e$ 2,1};
          }
        }
      }
      \mpause{
        \proofstep{$\alpha$}{PBC 2--3};
      }
    }
    \end{tikzpicture}
  \end{exampleblock}
\end{frame}