32/77
\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}
`