\begin{frame}[t]{Validity is Undecidable}
  \begin{block}{Theorem}
    The \emph{validity problem} in predicate logic is \alert{undecidable}.
  \end{block} 
  
  \begin{proof}[Proof structure]
    There is a computable function $\dm{r}$ (\forestgreen{see previous slides}) that maps
    instances of PCP to instances of the validity problem:
    \begin{talign}
      \dm{r} \funin \;\; \forestgreen{I} \;\; & \longmapsto \;\; \aformi{\forestgreen{I}}
      \\[-1ex]
    \intertext{such that it holds:}
      \\[-3ex]
      \text{$\forestgreen{I}$ has a solution}   
      \;\; & {\color{red}\Longleftrightarrow} \;\;
      \satisfies \!\! \aformi{\forestgreen{I}}
      \text{$\;\;$ (i.e.\ $\aformi{\forestgreen{I}}$ is valid}) \tag{$\star$} \label{eq:correctness:reduction}
    \end{talign}
    \vspace*{-2ex}
    
    Then if we had a program \emph{deciding validity} for predicate logic,
    we would obtain a PCP-solver. $\;$ \alert{$\xmark$}
    \renewcommand{\qed}{}
  \end{proof} 
  
  \begin{description}
  \pause
    \item[`$\alert{\Longleftarrow}$' in \eqref{eq:correctness:reduction}:]
      just shown \alert{\checkmark}
  \pause
    \item[`$\alert{\Longrightarrow}$' in \eqref{eq:correctness:reduction}:]  
      see Huth \& Ryan p.\ 134, 135
  \end{description}
\end{frame}