\begin{frame}[t]{Completeness Theorem}
  \begin{block}{Theorem (Completeness of $\sderives$ with respect to $\ssatisfies$)}
    For all formulas\/ $\aform$, and every set\/ $\asetforms$ of formulas:
    \begin{talign}
      \asetforms \satisfies \aform \;\;\;\Longrightarrow\;\;\; \asetforms \derives \aform  
    \end{talign}
  \end{block}
  \pause\medskip
  
  Reformulation and explanation:
  \begin{goal}{}
    The derivations rules are \emph{strong enough}
    to derive \emph{all valid semantic entailment statements}.
    \pause\medskip
    
    Thus \emph{more} derivation rules are \emph{not necessary},\\
    and in this sense these rules are \emph{complete}.
  \end{goal}
  \pause\medskip
  
  Proof of the theorem: non-trivial (first one by Kurt G\"{o}del, 1930)
\end{frame}