\begin{frame} \frametitle{Natural Deduction: Quantifiers} \vspace{-1ex} \begin{goal}{Elimination of Existential Quantification} \vspace{-1ex} \begin{align*} \infer[\rulename{\exists_e}] {\psi} { \myex{x}{\phi} && \framebox{\parbox{1.8cm}{\hint{$x_0$}\\\centerline{$\phi[x_0/x]$}\\\centerline{$\vdots$}\\\centerline{$\psi$}}} } \end{align*}\vspace{-3.5ex} \emph{Condition}: $x_0$ nowhere outside the box (in particular not in $\psi$). \end{goal} \pause \begin{exampleblock}{$\myex{x}{(P(x) \wedge Q(x))} \;\vdash\; \myex{x}{P(x)}$} \begin{tikzpicture} \naturaldeduction{ \mpause[1]{ \proofstep{$\myex{x}{(P(x) \wedge Q(x))}$}{premise}; } \mpause{ \namedproofbox{$x_0$}{ \mpause{ \proofstep{$P(x_0) \wedge Q(x_0)$}{assumption}; } \mpause{ \proofstep{$P(x_0)$}{$\wedge_e$ 2}; } \mpause{ \proofstep{$\myex{x}{P(x)}$}{$\exists_i$ 3}; } } } \mpause{ \proofstep{$\myex{x}{P(x)}$}{$\exists_e$ 1,2--4}; } } \end{tikzpicture}\vspace{-1ex} \end{exampleblock} \end{frame}