\begin{frame}[fragile] \frametitle{Examples} \begin{exampleblock}{$\myall{x}{A(x)} \;\vdash\; \neg \myex{x}{\neg A(x)}$} \mpause[1]{ \begin{tikzpicture} \naturaldeduction{ \proofstep{$\myall{x}{A(x)}$}{premise}; \proofbox{ \proofstep{$\myex{x}{\neg A(x)}$}{assumption}; \namedproofbox{$x_0$}{ \proofstep{$\neg A(x_0)$}{assumption}; \proofstep{$A(x_0)$}{$\forall_e\; 1$}; \proofstep{$\bot$}{$\neg_e\; 3,4$}; } \proofstep{$\bot$}{$\exists_e\;$ 2, 3--5}; } \proofstep{$\neg \myex{x}{\neg A(x)}$}{$\neg_i\;$ 2--6}; } \end{tikzpicture} } \end{exampleblock} \begin{exampleblock}{} {\scriptsize% \begin{verbatim}Theorem ex8 : all x, A(x) -> ~(exi x, ~A(x)). \end{verbatim} \pause\pause\vspace{-4.5ex} \begin{verbatim}Proof. imp_i H. neg_i H2. f_exi_e H2 y Hny. insert Hy (A(y)). f_all_e H. f_neg_e Hny Hy. Qed.\end{verbatim}% } \end{exampleblock} \end{frame}