\begin{frame}[t]{Example (Interpretation of Quantifiers)}
  \examplemodel
  \pause\medskip
    
  \begin{itemize} 
     \item $\mpause[1]{\model{\amodel} \satisfiesnot} \formula{\forallst{x}{\,\unpred{P}{x}}}$
     \updatepause
     \item $\mpause{\model{\amodel} \satisfies} \formula{\lognot{\forallst{x}{\,\unpred{P}{x}}}}$     
       % $\M \;\mw\; \niet \alle x Px$
     \updatepause
     \item $\mpause{\model{\amodel} \satisfies} \formula{\existsst{x}{\unpred{P}{x}}}$
        %$\M \;\mw\; \eris x Px$  \pause
     \updatepause
     \item $\mpause{\model{\amodel} \satisfiesnot}
            \formula{\forallst{x}{( \logimp{\unpred{P}{x}}
                                           {\existsst{y}{\,\binpred{R}{x}{y}}} )}}$
        %$\M \;\mw\; \alle x (Px \dan \eris y Rxy)$?  
     \updatepause
     \item $\mpause{\model{\amodel} \satisfies} 
            \formula{\forallst{x}{( \logor{\unpred{P}{x}}
                                          {\binpred{R}{x}{x}})}}$
        %$\M \;\mw\; \alle x (Px \of  Rxx)$?  
     \updatepause
     \item $\mpause{\model{\amodel} \satisfiesnot} 
            \formula{\existsst{x}{\forallst{y}{\,\binpred{R}{x}{y}}}}$
        %$\M \;\mw\; \eris x \alle y Rxy$?  
     \updatepause
     \item $\mpause{\model{\amodel} \satisfies} 
            \formula{\forallst{x}{( \logimp{\existsst{y}{\binpred{R}{x}{y}}}
                                           {\existsst{y}{(\logand{\binpred{R}{x}{y}}{\unpred{P}{y}})}} )}}$ 
  \end{itemize}    
\end{frame}