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