\begin{frame}[t]{Undecidability of $\textcolor{red}{\satisfies}$ and $\textcolor{red}{\derives}$}
  \begin{block}{Deduction Theorem}
    \pause
    Easy connection between $\satisfies$ and validity:
    \pause
    \begin{talign}
      \aformi{1}\black{,}\aformi{2}\black{,}\ldots\black{,}\aformi{n} \satisfies \bform
      \mpause[1]{
        \;\;&\Longleftrightarrow\;\;
        \satisfies \formula{\aformi{1} \logandinf \aformi{2} \logandinf \ldots \logandinf \aformi{n} \logimpinf \bform}
      } \\  
      \mpause{
        \;\;&\Longleftrightarrow\;\;
        \text{$\formula{\aformi{1} \logandinf \aformi{2} \logandinf \ldots \logandinf \aformi{n} \logimpinf \bform}\;\:$ is valid}
      }
    \mpause{ \intertext{and between $\derives$ and provability:} }
      \mpause{
        \aformi{1}\black{,}\aformi{2}\black{,}\ldots\black{,}\aformi{n} \derives \bform
      }
      \mpause{
        \;\;&\Longleftrightarrow\;\;
        \derives \formula{\aformi{1} \logandinf \aformi{2} \logandinf \ldots \logandinf \aformi{n} \logimpinf \bform} 
      } \\
      \mpause{
        \;\;&\Longleftrightarrow\;\;
        \text{$\formula{\aformi{1} \logandinf \aformi{2} \logandinf \ldots \logandinf \aformi{n} \logimpinf \bform}\;\:$ is provable }
      }
    \end{talign}
  \end{block}
  \updatepause\medskip
  
  \begin{block}{Corollary (Undecidability of entailment relations $\ssatisfies$ and $\sderives$)}
    The relations $\ssatisfies$ and $\sderives$ in predicate logic are \alert{undecidable}.
    \medskip
    
    There cannot be a program that, given formulas $\aformi{1}$, \ldots, $\aformi{n}$, $\bform$
    decides whether or not 
    $\satstmt{\aformi{1}\black{,}\ldots\black{,}\aformi{n} \satisfies \bform}$
    (or $\satstmt{\aformi{1}\black{,}\ldots\black{,}\aformi{n} \derives \bform}$).
  \end{block}
\end{frame}