\begin{frame}{Logical Equivalence}
  \begin{definition}[Logical equivalence \firebrick{$\,\slogequiv$}]
    Formulas $\aform$ and $\bform$ are \emph{logically equivalent}, denoted by
    \begin{talign}
      \firebrick{\aform \logequiv \bform}
    \end{talign}
    if for all models $\model{\amodel}$ and environments $\saluf$:
    \begin{center}
      $
      \model{\amodel} \satisfieslookup{\saluf} \aform
        \;\;\Longleftrightarrow\;\;
      \model{\amodel} \satisfieslookup{\saluf} \bform  
      $
    \end{center}
    That is,
    $\aform$ and $\bform$ are true in precisely the same models
    when interpreted with the same environments.
  \end{definition}
\end{frame}