\begin{frame}{Models Formally}
  Let \vspace{-.5ex}
  \begin{itemize}\setlength{\itemsep}{0ex}
    \item $\asetfuncs$ be a set of function symbols,  
    \item $\asetpreds$ a set of predicate symbols.
  \end{itemize}
  \pause
  
  \begin{block}{}  
    A \emph{model} $\model{\amodel}$ for $\pair{\asetfuncs}{\asetpreds}$
    consists of:
    \begin{itemize}
      \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
        \alert{$\interpretin{f}{\model{\amodel}} : A^n \to A$}
        for every $n$-ary function symbol $f \in \asetfuncs\,$ 
        \vspace*{0.75ex}
      \item
        \alert{$\interpretin{P}{\model{\amodel}} \subseteq A^n$}
        for every $n$-ary predicate symbols $P \in \asetpreds$
      \end{enumerate}
    \end{itemize}
  \end{block}
  A symbol is \alert{$n$-ary} if it has $n$ arguments.      
  \pause
  
  \only<-7>{
  \begin{exampleblock}{}
  \begin{itemize}\setlength{\itemsep}{0ex}
    \item 
      \alert{$\interpretin{\const{c}}{\model{\amodel}} \in \model{\adomain}$}
      for nullary function symbols (constants) $c \in \asetfuncs$
    \pause
    \item 
      \alert{$\interpretin{f}{\model{\amodel}} \funin \model{\adomain} \to \model{\adomain}$}
      for 1-ary (unary) symbols $f \in \asetfuncs$
    \pause
    \item 
      \alert{$\interpretin{f}{\model{\amodel}} \funin \model{\adomain} \times \model{\adomain} \to \model{\adomain}$}
      for 2-ary (binary) symbols $f \in \asetfuncs$
    \pause
    \item 
      \alert{$\interpretin{P}{\model{\amodel}} \subseteq \model{\adomain}$}
      for 1-ary (unary) predicate symbols $P \in \asetpreds$
    \pause
    \item 
      \alert{$\interpretin{P}{\model{\amodel}} \subseteq \model{\adomain} \times \model{\adomain}$}
      for 2-ary (binary) predicate symbols $P \in \asetpreds$
  \end{itemize}
  \end{exampleblock}
  }
  \pause[8]\bigskip
  
  \begin{goal}{}
  \emph{Note:} concept of model is \alert{extremely liberal}
  \begin{itemize}
    \smallskip
    \item
      universe $A$ can be \emph{any non-empty set} 
    \smallskip
    \item
      \emph{only one requirement} for interpretations:\\
      $\intin{\sfunc{f}}{\model{\amodel}}$ and $\intin{\spred{P}}{\model{\amodel}}$
      have \emph{same number of arguments} as $\sfunc{f}$ and $\spred{P}$
  \end{itemize}
  \end{goal}
          
  \vspace{10cm}
\end{frame}