54/116
\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

\item $\myex{y}{R(x,y)} \;\; [y/x] \quad\RED{\neq}\quad \myex{y}{R(y,y)}$
This substitution is \aemph{forbidden} since $y$
is not \aemph{free for $x$} in $\myex{y}{R(x,y)}$.