\begin{frame}{Free Variables and Environments}
  \begin{exampleblock}{}
    For a formula with free variables such as
    \begin{talign}
      \formula{\unpred{L}{\freevar{x}}}\;,
    \end{talign}
    its validity depends on the interpretation of $\freevar{x}$:
    %
    \begin{talign}
      \model{\amodel} \satisfieslookup{\saluf[\freevar{x} \mapsto m]} \formula{\unpred{L}{\freevar{x}}}
      \;\;\;\Longleftrightarrow\;\;\;
      m \in \intin{\sunpred{L}}{\model{\amodel}}      
    \end{talign}
    \pause
    Since we chose $\intin{\sunpred{L}}{\model{\amodel}}$ to be the set of logicians,
    $\unpred{L}{x}$ thus says:
    \begin{center}
      \sentence{$x$ is a logician}.
    \end{center} 
  \end{exampleblock}
  \pause\medskip

  \begin{exampleblock}{}
    A formula such as 
    \begin{talign}
      \formula{\existsst{y}{(\logand{\binpred{K}{\freevar{x}}{y}}{\unpred{L}{y}})}}
    \end{talign}
    with free variable $\freevar{x}$ expresses a property:
    \begin{talign}
      \sentence{$x$ knows a logician}
    \end{talign}
  \end{exampleblock}  
\end{frame}