\begin{frame}{Usefulness of Semantics}
  
  Assume we have a logic with syntax and semantics
  and with a \emph{soundness and completeness theorem}:
  \begin{talign}
    \aformi{1}, \ldots, \aformi{n} \derives \aform
      \;\;\;\;\Longleftrightarrow\;\;\;
    \aformi{1}, \ldots, \aformi{n} \satisfies \aform  
  \end{talign}
  \pause

  \begin{goal}{}
    If we want to show 
    \begin{equation}\label{eq:derives}
      \aformi{1}, \ldots, \aformi{n} \derives \aform
      \tag{\mbox{$\star$}}
    \end{equation}\pause{}
    but don't succeed despite best efforts.
    \pause\medskip
    
    We might want to \emph{change tactics}, and try to show:
    \begin{equation*}
      \aformi{1}, \ldots, \aformi{n} \satisfiesnot \aform
    \end{equation*}
    by a \alert{counter model} to $\aformi{1}, \ldots, \aformi{n} \satisfies \aform$.
    \pause\medskip 
    
    If we succeed here, then \eqref{eq:derives} \alert{cannot} hold.
  \end{goal}
\end{frame}