\begin{frame}{Models in Predicate Logic with Equality}
  Let \vspace{-.5ex}
  \begin{itemize}\setlength{\itemsep}{0ex}
    \item $\asetfuncs$ be a set of function symbols,  
    \item $\asetpreds$ a set of predicate symbols (not containing $\,\sequalto\,$).
  \end{itemize}
  
  \begin{block}{}  
    A \emph{model} $\model{\amodel}$ for $\pair{\asetfuncs}{\asetpreds}$
    in predicate logic with equality
    consists~of:
    \begin{itemize}
    \pause
      \item 
        a non-empty set~$\model{\adomain}$, called \emph{domain} or \emph{universe},
      \item
        an \emph{interpretation operation} $(\cdot)^{\model{\amodel}}$
        for the symbols in $\asetfuncs$, $\asetpreds$
        \begin{enumerate}[(i)]
        \item
          $\interpretin{f}{\model{\amodel}} : A^n \to A$
          for every $n$-ary function symbol $f \in \asetfuncs\,$ 
          \vspace*{0.75ex}
        \item
          $\interpretin{P}{\model{\amodel}} \subseteq A^n$
          for every $n$-ary predicate symbols $P \in \asetpreds$
        \end{enumerate}
    \pause
      \item
        the \emph{fixed interpretation} of $\sequalto$ in $\model{\amodel}$:
        \begin{talign}
          \intin{\sequalto}{\model{\amodel}} \;\; = \;\; \descsetexp{\pair{a}{a}}{a\in\model{\adomain}} 
        \end{talign}\vspace{-1ex}
    \end{itemize}
  \end{block}
\end{frame}