\begin{frame}{Model Informally (1)}
  
  \begin{exampleblock}{}
    \vspace{-1ex}
    \begin{talign}
      \formula{\existsst{x}{\,\unpred{P}{x}}}
    \end{talign}
    \pause%
    If we interpret $\formula{\unpred{P}{x}}$ as `\sentence{\black{$x$} is green}', this expresses:
    \begin{scenter}
      There is something that is green.
    \end{scenter}      
    \pause\smallskip
    
    This formula has a \emph{model}:
    \begin{itemize}
      \item universe $\{1,2,3\}$ 
      \item $\unpred{P}{1}$,\; $\lognot{\unpred{P}{2}}$,\; $\lognot{\unpred{P}{3}}$
    \end{itemize}
    \medskip
    \pause
    
    In a picture, this looks as follows:
    \begin{scenter}
      \begin{tikzpicture}[dot/.style={minimum size=4mm, circle, draw=none, fill=black, inner sep=0, outer sep=1mm, text=white}]
        \node [dot,fill=forestgreen] (1) {1};
        \node [dot,below right of=1] (2) {2};
        \node [dot,above right of=2] (3) {3};
        %
        \draw [rounded corners=5mm,thick,dashed] 
               ($(1) + (-6mm,7mm)$) rectangle ($(3) + (6mm,-13mm)$);
      \end{tikzpicture}
    \end{scenter}
    A \forestgreen{green dot} indicates that $\sunpred{P}$ is $\T$.
  \end{exampleblock}
\end{frame}