8/77
\begin{frame}
  \frametitle{Natural Deduction: Quantifiers}

  \begin{goal}{Introduction of Existential Quantification}
    \vspace{-1ex}
    \begin{align*}
      \infer[\rulename{\exists_i}]
      {\myex{x}{\phi}}
      {\phi\;[t/x]}
    \end{align*}
    \pause
    \emph{Condition} for application of this rule: $t$ free for $x$ in $\phi$.
  \end{goal}
  \pause\medskip

  \begin{exampleblock}{$\vdash\; R(a,a) \to \myex{x}{R(x,x)}$}
  \begin{tikzpicture}
  \naturaldeduction{
    \mpause[1]{
      \proofbox{
        \mpause{
        \proofstep{$R(a,a)$}{assumption};
        }
        \mpause{
        \proofstep{$\myex{x}{R(x,x)}$}{$\exists_i$ 1};
        }
      }
    }
    \mpause{
    \proofstep{$R(a,a) \to \myex{x}{R(x,x)}$}{$\to_i$ 1--2};
    }
  }
  \end{tikzpicture}
  \\
  \mpause[3]{\hint{For line 2:\quad $R(a,a) = R(x,x) [a/x]$}}
  \end{exampleblock}
\end{frame}