\begin{frame}{Consistency and Syntactical Consistency}
  We already know a \emph{semantical} notion of consistency.
  
  \begin{definition}[reminder]
    A set $\asetforms$ of formulas is \emph{consistent} (also: \emph{satisfiable}) 
    if there is a model $\model{\amodel}$ and an environment $\saluf$
    such that $\model{\amodel} \satisfies \aform$ for all $\aform\in\asetforms$:
    \begin{talign}
      \exists \model{\amodel}\; \exists \saluf\;\; \forall \aform\in \asetforms\;
         (\, \model{\amodel} \satisfieslookup{\saluf} \aform \,)
    \end{talign}
    \pause
    or equivalently
    \begin{talign}
      \exists \model{\amodel} \exists \saluf\;\; \model{\amodel} \satisfieslookup{\saluf} \asetforms      
    \end{talign}
  \end{definition}
  \pause\medskip
  
  There is also a \emph{syntactical}\/ variant:
  \begin{definition}
    A set $\asetforms$ of formulas is \emph{syntactically consistent} if:
    \begin{talign}
      \asetforms & \derivesnot \formula{\false}
    \end{talign}
    (That is, there is no derivation of $\formula{\bot}$ from $\asetforms$.)
  \end{definition}
\end{frame}