211/270
\begin{frame}[t]
  \frametitle{Well-definedness of $\,\ssatisfies$}
  
  \begin{proposition}
    If $\saluf$ and $\salufacc$ coincide on the free variables of $\aform$, then:
    \begin{align*}
      \model{\amodel} \satisfieslookup{\saluf} \aform
      \;\;\iff\;\;
      \model{\amodel} \satisfieslookup{\salufacc} \aform  
    \end{align*}
  \end{proposition}\pause{} 
  \bigskip
  
  A formula $\aform$ is a \emph{sentence} if $\aform$ does not have free variables.
  \begin{proposition}
    Let $\aform$ be a sentence. Then it holds for all enviroments $\saluf$ and $\salufacc$:
    \begin{align*}
      \model{\amodel} \satisfieslookup{\saluf} \aform
      \;\;\iff\;\;
      \model{\amodel} \satisfieslookup{\salufacc} \aform  
    \end{align*}
  \end{proposition}
  \pause\medskip
  
  Hence for sentences $\aform$, we can write
  \begin{scenter}
    $\model{\amodel} \satisfies \aform$
    \;\;for\;\; 
    $\model{\amodel} \satisfieslookup{\saluf} \aform$,
  \end{scenter} 
  since $\saluf$ is irrelevant. 
\end{frame}