\begin{frame}{Models in Predicate Logic with Equality}
  \begin{block}{}
  \emph{Truth} of a formula $\formula{\aform}$ in a model $\model{\amodel}$ with universe $\model{\adomain}$
  {\it with respect to environment $\saluf$}
  is defined by induction on the structure of $\formula{\aform}$:
  \medskip
  
  Atomic formulas:
  \begin{itemize}\setlength{\itemsep}{0.4ex}
    \item
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\narypredsynvar{P}{\ateri{1},\ldots,\ateri{n}}}
       \;\iff\; \tuple{\interpretin{\formula{\ateri{1}}}{\model{\amodel},\saluf},
                       \ldots,
                       \interpretin{\formula{\ateri{n}}}{\model{\amodel},\saluf}} 
                \in \interpretin{\snarypredsynvar{P}}{\model{\amodel}} $  
    \mpause[1]{
    \item 
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\equalto{\ateri{1}}{\ateri{2}}}
       \iff
         \pair{ \intin{\formula{\ateri{1}}}{\model{\amodel},\saluf} }{ \intin{\formula{\ateri{2}}}{\model{\amodel},\saluf} }
         \in {\intin{\sequalto}{\model{\amodel}}}
       \iff
         \intin{\formula{\ateri{1}}}{\model{\amodel},\saluf} = \intin{\formula{\ateri{2}}}{\model{\amodel},\saluf}$
    }
  \end{itemize}
  \smallskip
  
  Logic connectives:
  \begin{itemize}\setlength{\itemsep}{0.4ex}
    \item    
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\lognot{\aform}}
       \;\iff\; \model{\amodel} \satisfiesnotlookup{\saluf} \formula{\aform}$
    \item
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\logand{\aform}{\bform}}
       \;\iff\; \model{\amodel} \satisfieslookup{\saluf} \formula{\aform}
                \;\text{ and }\;
                \model{\amodel} \satisfieslookup{\saluf} \formula{\bform}$
    \item
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\logor{\aform}{\bform}}
       \;\iff\; \model{\amodel} \satisfieslookup{\saluf} \formula{\aform}
                \;\text{ or }\;
                \model{\amodel} \satisfieslookup{\saluf} \formula{\bform}$                    
    \item
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\logimp{\aform}{\bform}}
       \;\iff\; (\text{if }\; \model{\amodel} \satisfieslookup{\saluf} \formula{\aform}
                 \;\text{ then }\; \model{\amodel} \satisfieslookup{\saluf} \formula{\bform} )$          
  \end{itemize}
  \smallskip
  
  Quantifiers:
  \begin{itemize}\setlength{\itemsep}{0.4ex}
    \item  
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\,\aform}}
       \;\iff\; \text{for all $\forestgreen{a} \in \model{\adomain}$ it holds: }
                \model{\amodel} \satisfieslookup{\saluf\alert{[x\mapsto \forestgreen{a}]}} \formula{\aform}$    
    \item      
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{x}{\,\aform}}
       \;\iff\; \text{for some $\forestgreen{a} \in \model{\adomain}$ it holds: }
                \model{\amodel} \satisfieslookup{\saluf\alert{[x\mapsto \forestgreen{a}]}} \formula{\aform}  $    
  \end{itemize}
  \end{block}
\end{frame}