6/183
\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}