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