\begin{frame}[t]{Validity is Undecidable}
  \begin{block}{Theorem}
    The \emph{validity problem} in predicate logic is \alert{undecidable}.
    \medskip
    
    There cannot be a program that, given any formula $\aform$,
    decides whether or not $\;\ssatisfies\: \aform\,$ holds.
  \end{block} 
  \pause
  
  \begin{proof}[Proof structure]
    PCP can be \emph{encoded into} (\emph{reduced to}) the validity problem.
    \medskip\pause
    
    We will describe a computable function $\dm{r}$ 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}   
      \;\; & \Longleftrightarrow \;\;
      \satisfies \!\! \aformi{\forestgreen{I}}
      \text{$\;\;$ (i.e.\ $\aformi{\forestgreen{I}}$ is valid})
    \end{talign}
    \pause\vspace*{-2ex}
    
    Then if we had a program \emph{deciding validity} for predicate logic,
    we would obtain a \alert{PCP-solver.} $\;$ \alert{$\xmark$}
    \renewcommand{\qed}{}
  \end{proof} 
\end{frame}