\begin{frame}[t] \frametitle{Termination is Undecidable (Structure of Argument)} \begin{block}{Theorem} The \emph{termination problem} is \alert{unsolvable} (\alert{undecidable}). \end{block} \vspace{-3ex} \begin{talign} \mhide[10]{ \mpause[1]{ \text{$\terminator$ outputs \alert{yes} on input $\pair{\forestgreen{P}}{\forestgreen{w}}$} \;\;& \overset{ \mat{time:undefined:fail}{\mpause[?+1]{ \textcolor{red}{\huge\xmark} }} }{ \Longleftrightarrow } \;\; \text{$\forestgreen{P}$ halts on input $\forestgreen{w}$} } \\[-.95ex] \mpause{ & \;\; \Downarrow } \\[-.95ex] \mpause{ \text{$\terminatoronitself$ outputs \alert{yes} on input $\forestgreen{P}$} \;\; & \Longleftrightarrow \;\; \text{$\forestgreen{P}$ halts on input $\forestgreen{P}$} } \\[-.95ex] \mpause{& \;\; \Downarrow} \\[-2.45ex] } \mpause{ \text{$\diagonalisator$ halts on input $\forestgreen{P}$} \;\; & \overset{ \mpause[?+5]{ \textcolor{red}{\huge\xmark} } }{ \Longleftrightarrow } \;\; \text{$\forestgreen{P}$ does \alert{not} halt on input $\forestgreen{P}$} } \\[-.95ex] \mpause{ & \;\; \Downarrow} \\[-.95ex] \mpause{ \text{$\diagonalisator$ halts on input $\diagonalisator$} \;\; & \underset{ \mpause[?+1]{\textcolor{red}{\huge\xmark}\mtime{time:undefined:fail}} }{ \Longleftrightarrow } \;\; \text{$\diagonalisator$ does \alert{not} halt on input $\diagonalisator$} } \mpause[+3]{ \intertext{Compare with \emph{Russell's barber paradox}:\vspace{-.75ex}} \text{\firebrick{barber} shaves $\forestgreen{x}$} \;\; & \overset{\textcolor{red}{\huge\xmark}}{\Longleftrightarrow} \;\; \text{$\forestgreen{x}$ does \alert{not} shave $\forestgreen{x}$} \\[-.95ex] & \;\; \Downarrow \\[-.95ex] \text{\firebrick{barber} shaves \firebrick{barber}} \;\; & \underset{\textcolor{red}{\huge\xmark}}{\Longleftrightarrow} \;\; \text{\firebrick{barber} does {\alert{not}} shave \firebrick{barber}} } \end{talign} \end{frame}