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