21/160
\begin{frame}[t]{Consistency Theorem}
  \begin{block}{Theorem (Consistency)}
    For every set\/ $\asetforms$ of formulas it holds:
    \begin{talign}
      \text{$\asetforms$ is \emph{consistent}}
        \;\; & \Longleftrightarrow\;\;
      \text{$\asetforms$ is \emph{syntactically consistent}}  \tag{$\star$} \label{eq:consistency:theorem}
    \end{talign}
  \end{block}
  \pause\bigskip
  
  Reformulating this equivalence \eqref{eq:consistency:theorem}:
  \pause
  \begin{goal}{}
    \begin{malign}
      \exists \model{\amodel}\exists \saluf \;\; \model{\amodel} \satisfieslookup{\saluf} \asetforms
      \;\; &\iff\;\; 
      \asetforms \derivesnot \formula{\false}
    \end{malign}
  \end{goal}
  \pause

  \begin{goal}{}
    \begin{malign}
      \text{$\asetforms$ has a model}
      \;\; &\iff\;\; 
      \text{there is no derivation of $\false$ from $\asetforms$}
    \end{malign}
  \end{goal}
  \pause\bigskip
  
  The proof will utilise $\,\satisfies \; = \; \derives\,$ (soundness and completeness).
\end{frame}