38/205
\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}