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