\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:
      \asetforms \satisfies \aform \;\;\;\Longrightarrow\;\;\; \asetforms \derives \aform  
  Reformulation and explanation:
    The derivations rules are \emph{strong enough}
    to derive \emph{all valid semantic entailment statements}.
    Thus \emph{more} derivation rules are \emph{not necessary},\\
    and in this sense these rules are \emph{complete}.
  Proof of the theorem: non-trivial (first one by Kurt G\"{o}del, 1930)