\begin{frame}{Predicate Logic with Equality}
  \begin{goal}{}
  Fixed binary predicate symbol $\sequalto$ for equality.
  \end{goal}
  \pause\medskip
  
  Notation:
  \begin{itemize}
    \item infix notation $\equalto{x}{y}$ instead of ${\sequalto}(x,y)$
    \item the notation $\notequalto{x}{y}$ is an abbreviation of $\lognot{\equalto{x}{y}}$
  \end{itemize}
  \pause\medskip
  
  \begin{goal}{}
    Uniform, fixed interpretation of $\sequalto$ in every model.
    \pause\medskip
    
    If the model $\amodel$ has domain $A$, then the interpretation of $\sequalto$ is
    \begin{talign}
      \intin{\sequalto}{\model{\amodel}} \;\; = \;\; \descsetexp{\pair{a}{a}}{a\in\model{\adomain}} 
    \end{talign}
  \end{goal}
  \pause\medskip
  
  Formulas may use $\sequalto$ like a predicate symbol (but ${\sequalto} \notin \asetpreds$).
\end{frame}