\begin{frame}[t]
  \frametitle{Inconsistent Set of Formulas (Example)}
  
  \exampleloverlover
  \pause\bigskip

  The set $\Gamma = \setexp{ \aform, \, \formula{{\binpred{loves}{\const{alma}}{\const{alma}}}} }$ is \emph{inconsistent}:
  \pause
  \begin{exampleblock}{}
    Suppose that $\model{\amodel}$ is a model with 
    $\model{\amodel} \satisfies  \formula{{\binpred{loves}{\const{alma}}{\const{alma}}}}$.
    \pause\smallskip
    
    Then in $\model{\amodel}$:
    \begin{itemize}\setlength{\itemsep}{0pt}
      \item
        Alma is a lover of Alma.\pause{} 
      \item 
        Alma is a lover of a lover of Alma.\pause{} 
      \item 
        Alma is a lover's lover of Alma who loves Alma.\pause{}
    \end{itemize}
    Consequently 
    $\model{\amodel} \satisfiesnot \aform$.
    \pause\smallskip
    
    Hence there is no model satisfying both formulas in the set.
  \end{exampleblock}
  \vspace{10cm}
\end{frame}

\theme{
  Translation into Predicate Logic\\[.75ex]
  and the Interplay of Quantifiers
}