\begin{frame}{Encoding a PCP-Instance into a Formula} \begin{goal}{} Now given a PCP instance \begin{talign} \forestgreen{I} = \tuple{\pair{\forestgreen{w_1}}{\forestgreen{v_1}}, \pair{\forestgreen{w_2}}{\forestgreen{v_2}}, \ldots, \pair{\forestgreen{w_k}}{\forestgreen{v_k}}} \end{talign} \pause we encode $\forestgreen{I}$ into a formula $\aformi{\!\forestgreen{I}}$ of predicate logic as follows: \pause{} % \begin{align*} \aformi{\!\forestgreen{I}} & \:\defdby\: \formula{\logimp{\logand{\aformi{1}}{\aformi{2}}}{\aformi{3}}} \\[2ex] \mpause[1]{ \aformi{1} & \:\defdby\: \formula{\bigwedge_{i=1,\ldots,k} \!\!\! \binpred{P}{\unfunci{f}{\forestgreen{w_i}}{\const{e}}}{\unfunci{f}{\forestgreen{v_i}}{\const{e}}}} } \\ \mpause{ \aformi{2} & \:\defdby\: \formula{\forallst{x}{\forallst{y}{ \bigl( \binpred{P}{x}{y} \logimpinf \bigwedge_{i=1,\ldots,k} \!\!\! \binpred{P}{\unfunci{f}{\forestgreen{w_i}}{x}}{\unfunci{f}{\forestgreen{v_i}}{y}} \bigr) }}} } \\ \mpause{ \aformi{3} & \:\defdby\: \formula{\existsst{z}{\:\binpred{P}{z}{z}}} } \end{align*} \end{goal} \smallskip\updatepause The idea behind $\sbinpred{P}$ is: \begin{talign} \binpred{P}{x}{y} \;\iff\; \text{$\pair{x}{y}$ can be constructed using dominos in $\forestgreen{I}$} \end{talign} \end{frame}