\begin{frame}
  \frametitle{Examples}

  \begin{exampleblock}{$\myall{x}{(P(x) \to \neg P(x))} \;\vdash\; \neg \myex{x}{P(x)}$}
  \begin{tikzpicture}
    \naturaldeduction{
      \proofstep{$\myall{x}{(P(x) \to \neg P(x))}$}{premise};
      \proofbox{
        \proofstep{$\myex{x}{P(x)}$}{assumption};
        \namedproofbox{$y$}{
          \proofstep{$P(y)$}{assumption};  
          \proofstep{$P(y) \to \neg P(y)$}{$\forall_e\;$ 1};
          \proofstep{$\neg P(y)$}{$\to_e\;$ 2,3};
          \proofstep{$\bot$}{$\neg_e\;$ 2,4};
        }
        \proofstep{$\bot$}{$\exists_e\;$ 2, 3--6};
      }
      \proofstep{$\neg \myex{x}{P(x)}$}{$\neg_i\;$ 2--7};
    }
  \end{tikzpicture}
  \end{exampleblock}
  \bigskip
  
  Similar to an example we have seen before
  $$\myall{x}{(P(x) \to \neg P(x))} \;\vdash\; \myall{x}{ \neg P(x)}$$
\end{frame}