7/183
\begin{frame}[t]{Logical Equivalence}

\renewcommand{\slogequiv}{\textcolor{firebrick}{\equiv}}

\begin{block}{Theorem}
\begin{malign}
\aform \logequiv \bform \;\;\;\iff\;\;\;
\aform \satisfies \bform
\;\text{ and }\;
\bform \satisfies \aform
\end{malign}
\end{block}

Therefore, logical equivalence is sometimes denoted $\mathrel{\reflectbox{$\ssatisfies$}}\satisfies$.
\bigskip

\begin{proof}
\begin{malign}
& \aform \logequiv \bform \\
& \;\;\iff\;\; \text{for all $\model{\amodel}$ and $\saluf\,$:} \\[-0.75ex]
& \phantom{\;\;\iff\;\;} \;\,
(\model{\amodel} \satisfieslookup{\saluf} \aform \;\Rightarrow\; \model{\amodel} \satisfieslookup{\saluf} \bform)
\text{ and }
(\model{\amodel} \satisfieslookup{\saluf} \bform \;\Rightarrow\; \model{\amodel} \satisfieslookup{\saluf} \aform) \\
& \;\;\iff\;\; \text{for all $\model{\amodel}$ and $\saluf\,$:} \;\;
\model{\amodel} \satisfieslookup{\saluf} \aform \;\Rightarrow\; \model{\amodel} \satisfieslookup{\saluf} \bform) \\[-0.75ex]
& \phantom{\;\;\iff\;\;} \;\, \text{and for all $\model{\amodel}$ and $\saluf\,$:} \;\;
\model{\amodel} \satisfieslookup{\saluf} \bform \;\Rightarrow\; \model{\amodel} \satisfieslookup{\saluf} \aform) \\
& \;\;\iff\;\; \aform \satisfies \bform \;\;\text{and}\;\; \bform \satisfies \aform \;\;
\text{(that is, $\aform \:\mathrel{\reflectbox{$\ssatisfies$}}\satisfies\: \bform$)}
\end{malign}
\end{proof}
\end{frame}