50/116
\begin{frame}
\frametitle{Bound and Free Variables}

\begin{goal}{}
A quantifier
\emph{binds} the \aemph{free (not yet bound)} variables of the same name
\aemph{in the scope} of the quantifier.
\end{goal}
\pause

\begin{goal}{}
The \quad$\forall x$\quad or \quad$\exists x$\quad in \vspace{-.5ex}
\begin{talign}
\myall{x}{(\phi)} && \myex{x}{(\phi)}
\end{talign}
\vspace{-3ex}

binds all $x$ in $\phi$ that are free, that is, not already bound.
\end{goal}
\pause

\smallskip
\begin{exampleblock}{}
\vspace{-2ex}
\begin{talign}
\myex{\BLUE{y}}{ \myall{\GREEN{z}}{ (\myex{\DARKRED{x}}{R(\DARKRED{x},\GREEN{z})} \to (R(x,\GREEN{z}) \wedge R(\BLUE{y},\GREEN{z}))) }}
\end{talign}
\vspace{-4ex}

\begin{center}
\tikz[level distance=6mm,outer sep=1mm,inner sep=0,
level 1/.style={sibling distance=20mm},
level 2/.style={sibling distance=35mm},
level 3/.style={sibling distance=30mm},
level 4/.style={sibling distance=17mm},
level 5/.style={sibling distance=8mm},
]
\node {$\exists \BLUE{y}$}
child {node {$\forall \GREEN{z}$}
child {node   {$\to$}
child {node {$\exists \DARKRED{x}$}
child {node {$R$}
child {node {$\DARKRED{x}$} }
child {node {$\GREEN{z}$} }
}
}
child {node  {$\wedge$}
child {node {$R$}
child {node {$x$} }
child {node {$\GREEN{z}$} }
}
child {node {$R$}
child {node {$\BLUE{y}$ }}
child {node {$\GREEN{z}$} }
}
}
}
};
\end{center}
\vspace{-2ex}

The only black $x$ is \emph{not bound}, a \aemph{free variable}.
\vspace{-.5ex}
\end{exampleblock}
\end{frame}