\begin{frame}[t]{Example (Interpretation of Free Variables)} 
  \examplemodelwith{
    What about: 
    % 
    \begin{itemize}
      \item $\model{\amodel} \satisfies \formula{\unpred{P}{\freevar{x}}}$ \hfill ?
        % $\M \;\mw\; Px$ $\;$?  
      \pause
      \item $\model{\amodel} \satisfies   \formula{\binpred{R}{\freevar{x}}{\freevar{x}}}$ \hfill ?
        % $\M \;\mw\;  Rxx$ $\;$?
      \pause
      \item $\model{\amodel} \satisfies \formula{\binpred{R}{\freevar{x}}{\freevar{y}}}$ \hfill ?
        % $\M \;\mw\; Rxy$ $\;$?
      \pause
      \item $\model{\amodel} \satisfies \formula{\existsst{y}{\,\binpred{R}{\freevar{x}}{y}}}$ \hfill ?
        % $\M \;\mw\; \eris y Rxy$ $\;$? 
     \end{itemize}  
  }
  \pause\bigskip
  
  This depends on the interpretation of the \firebrick{free variables} $\freevar{x}$ and $\freevar{y}$:%
  \pause
  \begin{itemize}\vspace*{0.75ex}\setlength{\itemsep}{0.75ex}
    \item   
      \parbox{22ex}{$\model{\amodel} \satisfieslookup{[\freevar{x} \mapsto a_1]} \formula{\unpred{P}{\freevar{x}}} $}
        % $\M \;\mw_{\,[\freevar{x} \mapsto a_1]} \; P\freevar{x}$  \hspace{3em} 
       \hspace*{1em}
       \pause{}
      $\model{\amodel} \satisfiesnotlookup{[\freevar{x} \mapsto a_3]} \formula{\unpred{P}{\freevar{x}}}$  
        % $\M \;\not\mw_{\,[\freevar{x} \mapsto a_3]} \; P\freevar{x}$   \pause
      \pause
    \item   
      \parbox{22ex}{$\model{\amodel} \satisfiesnotlookup{[\freevar{x} \mapsto a_1]} \formula{\binpred{R}{\freevar{x}}{\freevar{x}}}$}
        % $\M \;\not\mw_{\,[\freevar{x} \mapsto a_1]} \; R\freevar{x}\freevar{x}$  
      \hspace{1em}
      \pause{}
      $\model{\amodel} \satisfieslookup{[\freevar{x} \mapsto a_3]} \formula{\binpred{R}{\freevar{x}}{\freevar{x}}}$ \pause{} 
        % $\M \;\mw_{\,[\freevar{x} \mapsto a_3]} \; R\freevar{x}\freevar{x}$  \pause
    \item 
      \parbox{22ex}{$\model{\amodel} \satisfiesnotlookup{[\freevar{x} \mapsto a_2][\freevar{y}\mapsto a_3]} \formula{\binpred{R}{\freevar{x}}{\freevar{y}}}$}  
        % $\M \;\not\mw_{[\freevar{x} \mapsto a_2][y\mapsto a_3]} \; R\freevar{x}y$  
      \pause
    \item 
      \parbox{22ex}{$\model{\amodel} \satisfieslookup{[\freevar{x}\mapsto a_3]} \formula{\existsst{y}{\, \binpred{R}{\freevar{x}}{y}}}$}
        %$\M \;\mw_{\,[y\mapsto a_3]}\; \eris x Rxy$ 
      \hspace{1em}  
      \pause{}
      $\model{\amodel} \satisfiesnotlookup{[\freevar{x}\mapsto a_2]} \formula{\existsst{y}{\, \binpred{R}{\freevar{x}}{y}}}$
        % $\M \;\not\mw_{\,[x\mapsto a_2]}\; \eris y Rxy$
  \end{itemize}  
\end{frame}