33/270
\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
}

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

\theme{Models}