\begin{frame} \frametitle{Natural Deduction: Quantifiers} \begin{goal}{Introduction of Universal Quantification} \vspace{-1ex} \begin{align*} \infer[\rulename{\forall_i}] {\myall{x}{\phi}} { \framebox{\parbox{1.8cm}{\hint{$x_0$}\\\centerline{$\vdots$}\\\centerline{$\phi\;[x_0/x]$}}} } \end{align*} \emph{Condition} for application of this rule: `$x_0$ is arbitrary'.\\ That is: $x_0$ occurs only inside the box (in particular not in $\phi$) \end{goal} \pause\medskip \begin{exampleblock}{$\vdash\; \myall{x}{(P(x) \to P(x))}$} \begin{tikzpicture} \naturaldeduction{ \mpause[1]{ \namedproofbox{$x_0$}{ \mpause{ \proofbox{ \mpause{ \proofstep{$P(x_0)$}{assumption}; } } } \mpause{ \proofstep{$P(x_0) \to P(x_0)$}{$\to_i$ 1--1}; } } } \mpause{ \proofstep{$\myall{x}{(P(x)\to P(x))}$}{$\forall_i$ 1--2}; } } \end{tikzpicture} \end{exampleblock} \end{frame}