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