250/270
\begin{frame}{Disproving Semantic Entailment: Counter Models}
  \begin{exampleblock}{}
    \begin{malign}
      \formula{\forallst{x}{\existsst{y}{\,\binpred{R}{x}{y}}}}
      \satisfiesnot
      \formula{\existsst{y}{\forallst{x}{\,\binpred{R}{x}{y}}}}
    \end{malign}
    \pause

    We can give a model $\model{\amodel}$ such that:
    \begin{center}
      $\model{\amodel} \satisfies \formula{\forallst{x}{\existsst{y}{\,\binpred{R}{x}{y}}}}\,$,
      \hspace*{3ex} 
      $\model{\amodel} \satisfiesnot \formula{\existsst{y}{\forallst{x}{\,\binpred{R}{x}{y}}}}\,$.
    \end{center}
    \pause
    We choose $\model{\amodel}$ as follows:
    \begin{center}
      \scalebox{0.8}{  
      \begin{tikzpicture}[point/.style={circle,fill=black!60!white,draw=none,inner sep=2pt},
                          node distance=26mm]
        \node (1) [point] {};
        \node (2) [point, right of=1] {};
        \node at (1) [yshift=4mm] {$a_1$};
        \node at (2) [yshift=4mm]  {$a_2$};
        \begin{scope}[shorten <= 2mm, shorten >= 2mm, very thick, >=stealth]
        \draw [->] (1) to[out=-140,in=-40,looseness=30] (1);
        \draw [->] (2) to[out=-140,in=-40,looseness=30] (2);
        \end{scope}
        \node [right of=2,node distance=20mm,yshift=10mm] {\Large $\model{\model{\amodel}}$};
        \draw [rounded corners=5mm,thick,dashed] 
                   ($(1) + (-14mm,12mm)$) rectangle ($(2) + (14mm,-15mm)$);
      \end{tikzpicture}
      }
    \end{center}
  \end{exampleblock}
  \pause\smallskip
  
  \begin{goal}{}
    This is a \emph{counter model}:\\
    it satisfies the premise, but not the conclusion. 
  \end{goal}
\end{frame}