\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}