\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}