\begin{frame}
  \frametitle{Rules for $\neg\neg$ and $\to$}
  
  \begin{goal}{Rules for $\neg\neg$}
    \vspace{-1ex}
    \begin{align*}
      \infer[\rulename{\neg\neg_e}]
      {\alpha}
      {\neg\neg\alpha}
      &&
      \infer[\rulename{\neg\neg_i}]
      {\neg\neg\alpha}
      {\alpha}
    \end{align*}
  \end{goal}
  \pause\medskip

  \begin{goal}{Elimination rules for $\to$}
    This rule is called ``Modus Ponens'' (MP):
    \begin{align*}
      \infer[\rulename{\to_e} \;\; (or \rulename{MP})]
      {\beta}
      {\alpha && \alpha \to \beta}
    \end{align*}
    \pause
    This rule is called ``Modus Tollens'' (MT):
    \begin{align*}
      \infer[\rulename{MT}]
      {\neg\alpha}
      {\alpha \to \beta && \neg\beta}
    \end{align*}
  \end{goal}
\end{frame}