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