\begin{frame} \frametitle{Substitution} \begin{goal}{Substitution of $t$ for $x$ in $\phi$} \begin{align*} \phi\;[t/x] \end{align*} is the result of replacing all free occurrences of the \emph{variable} $x$ in $\phi$ with the \emph{term} $t$. \end{goal} \pause \begin{exampleblock}{} \begin{itemize} \item $\myall{x}{P(x)} \wedge Q(x) \;\; [y/x] \quad=\quad \pause\myall{x}{P(x)} \wedge Q(y)$ \pause \item $\myex{y}{R(x,y)} \;\; [z/x] \quad=\quad \pause \myex{y}{R(z,y)}$ \pause \item $\myex{y}{R(x,y)} \;\; [z/y] \quad=\quad \pause \myex{y}{R(x,y)}$ \end{itemize} \end{exampleblock} \pause \begin{alertblock}{Attention!} \begin{itemize} \item $\myex{y}{R(x,y)} \;\; [y/x] \quad\RED{\neq}\quad \myex{y}{R(y,y)}$ \end{itemize} This substitution is \aemph{forbidden} since $y$ is not \aemph{free for $x$} in $\myex{y}{R(x,y)}$. \end{alertblock} \end{frame}