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