\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}