\begin{frame}{PCP is Undecidable} \begin{block}{Theorem} \emph{Post's Correspondence Problem} is \alert{undecidable}. \end{block} \pause \begin{proof}[Idea of the Proof] The termination problem can be \emph{reduced to} PCP.\pause{} \medskip More precisely, there is a computable function $\dm{r}$ that maps instances of the termination problem to instances of PCP:\vspace*{-1ex} \begin{align*} \dm{r} \funin \;\; \pair{\forestgreen{P}}{\forestgreen{w}} \;\; & \longmapsto \;\; \mediumblue{I_{\pair{\forestgreen{P}}{\forestgreen{w}}}} \\[-1ex] \intertext{such that it holds:} \\[-4ex] \text{$\forestgreen{P}$ terminates on input $\forestgreen{w}$} \;\; &\Longleftrightarrow \;\; \text{$\mediumblue{I_{\pair{\forestgreen{P}}{\forestgreen{w}}}}$ has a solution} \end{align*} \pause\vspace*{-3ex} Then if we had a \emph{PCP-solver} (decides solvability of PCP-inst.) % (a solver for PCP-instances), we would obtain a \alert{solver for the termination problem.} $\;$ \alert{$\xmark$} \end{proof} \end{frame}