8/183
\begin{frame}<10>
\frametitle{Proving Logical Equivalence}

\begin{exampleblock}
{\begin{center}
\black{%
$\satstmt{% \formula{\lognot{\forallst{x}{\,\unpred{P}{x}}}} \logequiv \formula{\existsst{x}{\,\lognot{\unpred{P}{x}}}}}$}
\end{center}}\pause{}

\medskip
For all models $\model{\amodel}$ with domain $\model{\adomain}$ and environments $\saluf$ we find:\pause{}
\begin{align*}
&
\model{\amodel} \satisfieslookup{\saluf} \formula{\lognot{\forallst{x}{\,\unpred{P}{x}}}}
\\
& \uncover<4->{%
\hspace*{2ex} \;\;\Longleftrightarrow\;\;
\text{not:} \;\;
\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\,\unpred{P}{x}}}}
\\
& \uncover<5->{%
\hspace*{2ex} \;\;\Longleftrightarrow\;\;
\text{not for all $\forestgreen{a}\in\model{\adomain}\,$:} \;\;
\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}}
\\
& \uncover<6->{%
\hspace*{2ex} \;\;\Longleftrightarrow\;\;
\text{there exists $\forestgreen{a}\in\model{\adomain}$ such that not:} \;\;
\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}}
\\
& \uncover<7->{%
\hspace*{2ex} \;\;\Longleftrightarrow\;\;
\text{there exists $\forestgreen{a}\in\model{\adomain}$ such that:} \;\;
\model{\amodel} \satisfiesnotlookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}}
\\
& \uncover<8->{%
\hspace*{2ex} \;\;\Longleftrightarrow\;\;
\text{there exists $\forestgreen{a}\in\model{\adomain}$ such that:} \;\;
\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\lognot{\unpred{P}{\freevar{x}}}}}
\\
& \uncover<9->{%
\hspace*{2ex} \;\;\Longleftrightarrow\;\;
\model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{x}{\,\lognot{\unpred{P}{x}}}}}
\end{align*}

\uncover<10->{%
Hence we can conclude:
$\satstmt{% \formula{\lognot{\forallst{x}{\,\unpred{P}{x}}}} \logequiv \formula{\existsst{x}{\,\lognot{\unpred{P}{x}}}}}$.}

\end{exampleblock}

Note that each step is a bi-implication, so we have $\reflectbox{$\satisfies$}$ and $\satisfies$.
%   \begin{exampleblock}
%         {\begin{center}
%           \black{%
%           $\satstmt{% % \formula{\lognot{\existsst{x}{\,\unpred{P}{x}}}} % \logequiv % \formula{\forallst{x}{\,\lognot{\unpred{P}{x}}}}}$}
%          \end{center}}
%
%   \medskip
%   For all models $\model{\amodel}$ with domain $\model{\adomain}$ and all environments $\saluf$ we find:
%   \begin{align*}
%     &
%     \model{\amodel} \satisfieslookup{\saluf} \formula{\lognot{\existsst{x}{\,\unpred{P}{x}}}}
%     \\
%     & \uncover<1->{%
%       \hspace*{2ex} \;\;\Longleftrightarrow\;\;
%       \text{not:} \;\;
%         \model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{x}{\,\unpred{P}{x}}}}
%     \\
%     & \uncover<1->{%
%       \hspace*{2ex} \;\;\Longleftrightarrow\;\;
%       \text{there does not exist $\forestgreen{a}\in\model{\adomain}\,$:} \;\;
%          \model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}}
%     \\
%     & \uncover<1->{%
%       \hspace*{2ex} \;\;\Longleftrightarrow\;\;
%       \text{for all $\forestgreen{a}\in\model{\adomain}$ it holds:} \;\;
%          \model{\amodel} \satisfiesnotlookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}}
%     \\
%     & \uncover<1->{%
%       \hspace*{2ex} \;\;\Longleftrightarrow\;\;
%       \text{for all $\forestgreen{a}\in\model{\adomain}$ it holds:} \;\;
%          \model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\lognot{\unpred{P}{\freevar{x}}}}}
%     \\
%     & \uncover<1->{%
%       \hspace*{2ex} \;\;\Longleftrightarrow\;\;
%       \model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\,\lognot{\unpred{P}{x}}}}}
%   \end{align*}
%
%   \uncover<1->{%
%   Hence we can conclude:
%   $\satstmt{% % \formula{ % \lognot{\existsst{x}{\,\unpred{P}{x}}}} % \logequiv % \formula{\forallst{x}{\,\lognot{\unpred{P}{x}}}}}$.}
%
%   \end{exampleblock}
\end{frame}