\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}