164/183
\begin{frame}{$\formula{\slognot}\,$ versus $\,\formula{\exists}$, $\,\formula{\forall}$}
  \begin{proposition}
    For all variables $\formula{\avarsynvar}$ and formulas $\aform$ it holds:  
    \begin{enumerate}[(i)]\setlength{\itemsep}{0.4ex}
      \item \; $\formula{\lognot{\forallst{\avarsynvar}{\,\aform}}}
                \logequiv
                \formula{\existsst{\avarsynvar}{\,\lognot{\aform}}}$ 
      \item \; $\formula{\lognot{\existsst{\avarsynvar}{\,\aform}}}
                \logequiv
                \formula{\forallst{\avarsynvar}{\,\lognot{\aform}}}$ 
      \item \; $\formula{\forallst{\avarsynvar}{\,\aform}}
                \logequiv
                \formula{\lognot{\existsst{\avarsynvar}{\,\lognot{\aform}}}}$  
      \item \; $\formula{\existsst{\avarsynvar}{\,\aform}}
                \logequiv
                \formula{\lognot{\forallst{\avarsynvar}{\,\lognot{\aform}}}}$ 
    \end{enumerate}  
  \end{proposition}  
  \pause\medskip  
    
  Equivalently, the following formulas are valid:
  \begin{enumerate}[(i)]\setlength{\itemsep}{0.4ex}
    \item \; $\formula{\lognot{\forallst{\avarsynvar}{\,\aform}}
              \logbiimpinf
              \exists{\avarsynvar}{\,\lognot{\aform}}}$  
    \item \; $\formula{\lognot{\existsst{\avarsynvar}{\,\aform}}
              \logbiimpinf
              \forallst{\avarsynvar}{\,\lognot{\aform}}}$ 
    \item \; $\formula{\forallst{\avarsynvar}{\,\aform}
              \logbiimpinf
              \lognot{\existsst{\avarsynvar}{\,\lognot{\aform}}}}$  
    \item \; $\formula{\existsst{\avarsynvar}{\,\aform}
              \logbiimpinf
              \lognot{\forallst{\avarsynvar}{\,\lognot{\aform}}}}$ 
  \end{enumerate}
\end{frame}