\begin{frame} \small \vspace{-1ex} \begin{definition} \smallskip An ES $\EE$ is \alert{consistent} if $\exists$ terms $s$, $t$ such that $s \mathrel{\not\approx}_\EE t$. \end{definition} \pause\medskip \begin{block}{Validity Problem} \begin{tabbing} instance: \quad \= ES $\ES$ \quad terms $s, t \in \TT(\FF,\VV)$ \\ question: \> $\EE \vDash s \approx t$ ? \quad (or equivalently $\EE \vdash s \approx t$?) \end{tabbing} \end{block} \medskip\pause \begin{theorem} \smallskip The validity problem is \alert{undecidable}. \end{theorem} \medskip \begin{example}<4->[Combinatory Logic] \vspace{-2ex} \GREEN{\begin{align*} \m{I} \cdot x &\approx x \\ (\m{K} \cdot x) \cdot y &\approx x \\ ((\m{S} \cdot x) \cdot y) \cdot z &\approx (x \cdot z) \cdot (y \cdot z) \end{align*}} \vspace{-3ex} \end{example} \end{frame}