\begin{frame}
  \frametitle{Usefulness of Semantics}
  
  For example, the valuation 
  \begin{talign}
    \aval{\prop{p}} = \True &&
    \aval{\prop{q}} = \False &&
    \aval{\prop{r}} = \True
  \end{talign} 
  yields 
  \begin{talign}
    \aval{\formula{\logimp{\logor{\prop{p}}{\prop{q}}}{\prop{r}}}} & = \True
    &
    \aval{\formula{\lognot{(\logand{\prop{r}}{\lognot{\prop{q}})}}}} & = \False\\
    \aval{\formula{\logimp{\logand{\prop{q}}{\prop{r}}}{\lognot{\prop{p}}}}} & = \True
  \end{talign}
  \pause\vspace{-2ex}
  
  \begin{exampleblock}{}
  This valuation $\saval$ is a \alert{counter model} to:
  \begin{talign}
    \logimp{\logor{\prop{p}}{\prop{q}}}{\prop{r}}, \;\;
    \logimp{\logand{\prop{q}}{\prop{r}}}{\lognot{\prop{p}}}
      \;\;\satisfies\;\;
    \lognot{(\logand{\prop{r}}{\lognot{\prop{q}})}}
  \end{talign}
  \pause
  and hence justifies:
  \begin{talign}
    \logimp{\logor{\prop{p}}{\prop{q}}}{\prop{r}}, \;\;
    \logimp{\logand{\prop{q}}{\prop{r}}}{\lognot{\prop{p}}}
      \;\;\alert{\ssatisfiesnot}\;\;
    \lognot{(\logand{\prop{r}}{\lognot{\prop{q}})}}
  \end{talign}
  \pause
  This implies, by the soundness (and completeness) theorem:  
  \begin{center}
    $
    \formula{\logimp{\logor{\prop{p}}{\prop{q}}}{\prop{r}}}, \;\;
    \formula{\logimp{\logand{\prop{q}}{\prop{r}}}{\lognot{\prop{p}}}}
      \;\;\alert{\sderivesnot}\;\;
    \formula{\lognot{(\logand{\prop{r}}{\lognot{\prop{q}})}}}
    $
  \end{center}
  \pause
  Thus \alert{there is no} natural-deduction derivation!
  \end{exampleblock}
\end{frame}