\begin{frame}
  \frametitle{Proof Theory $(\,\sderives\,)$ $\,$ versus Semantics $\,$ $(\,\ssatisfies\,)$}
  
  \begin{block}{\emph{Proof theory} with entailment $\,\sderives$}
    \begin{itemize}
      \mpause[1]{
      \item 
        rules prove \alert{operative} explanation to logical symbols 
      }
      
      \mpause[3]{
      \item
        gives an \alert{existential characterisation} of the formulas\\ that are true in a logic:
        \begin{talign}
          \aformi{1}, \ldots, \aformi{n} \derives \aform
            \;\;\Longleftrightarrow\;\;
          &\text{\alert{there exists} a derivation of $\aform$} \\[-.5ex]
          &\text{from premises $\aformi{1},\ldots,\aformi{n}$}
        \end{talign}\vspace{-3ex} 
      }
      
      \mpause[5]{
      \item
        convenient for \alert{positive} arguments: give a derivation
      }
    \end{itemize}
  \end{block}
  
  \begin{block}{\emph{Semantics} with entailment $\,\ssatisfies$}
    %
    \begin{itemize}
      \mpause[2]{
      \item
        gives \alert{meaning} to logical symbols
      }
      
      \mpause[4]{
      \item
        gives a \alert{universal characterisation} of the formulas\\ that are true in a logic:
        \begin{talign}
          \aformi{1}, \ldots, \aformi{n} \satisfies \aform
            \;\;\Longleftrightarrow\;\;
          &\text{\alert{all} models that satisfy $\aformi{1},\ldots,\aformi{n}$,}\\[-.5ex]
          &\text{also satisfy $\aform$}   
        \end{talign}\vspace{-3ex}
      }
      
      \mpause[6]{  
      \item
        convenient for \alert{negative} arguments: give a counter model     
      }
    \end{itemize}
  \end{block}
  \bigskip
\end{frame}