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