\begin{frame}{Soundness and Completeness Theorem}
  \begin{block}{Theorem (Soundness and Completeness)}
    The syntactic version $\derives$ and the semantical version $\satisfies$\\
    of logical entailment \emph{coincide}:
    \begin{talign}
      \asetforms \derives \aform \;\;\iff\;\; \asetforms \satisfies \aform  
    \end{talign}
    holds for all formulas\/ $\aform$, and every set\/ $\asetforms$ of formulas.
  \end{block}
  \pause\medskip

  Two directions:
  \begin{talign}
    \Longrightarrow\;:&\;\; \text{correctness (soundness)} \\
    \Longleftarrow\;:&\;\; \text{completeness}
  \end{talign}
  \pause\medskip
  
  In a symbolic abbreviation:
  \begin{talign}
    \scalebox{1.5}{$\derives \;\, = \;\, \satisfies$}
  \end{talign}
\end{frame}