2/183
\begin{frame}{Reminder: Models and Environments}
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}

\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.
\medskip

\begin{goal}{}
An \emph{environment}~(look-up function)
\begin{talign}
\end{talign}
interprets \alert{free} variables in the domain.
\end{goal}
\end{frame}