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