202/270
\begin{frame}[t]{Quantification by Varying the Environment}
\begin{minipage}{0.49\textwidth}
Model and environment:
\medskip

\scalebox{.75}{
\begin{tikzpicture}[dom/.style={circle,draw=orange!50!black,very thick,fill=orange!50!white,inner sep=2pt}]
\node (1) [dom] {1};
\node (2) [below of=1,dom] {2};
\node (3) [below of=2,dom] {3};
\node (4) [below of=3,dom] {4};
\begin{scope}[node distance=30mm]
\node (x) [left of=2] {$x$};
\node (y) [left of=3] {$y$};
\node (z) [left of=4] {$z$};
\end{scope}
\begin{scope}[shorten <= 2mm, shorten >= 2mm, very thick, >=stealth]
\draw [->] (x) to (2);
\draw [->] (y) to[bend left=20] (4);
\draw [->] (z) to[bend right=20] (4) ;     %node [pos=.5] {A};
\end{scope}
\end{tikzpicture}
}
\end{minipage}
\begin{minipage}{0.49\textwidth}
\begin{itemize}
\item domain: $\model{\adomain} = \{1,2,3,4\}$
\item $\intin{\sunpred{L}}{\model{\amodel}} = {<}$
\medskip
\item environment $\saluf$:
\begin{itemize}
\item $\aluf{\freevar{x}} = 2$
\item $\aluf{\freevar{y}} = \saluf(\freevar{z}) = 4$
\end{itemize}
\end{itemize}
\end{minipage}

\hspace*{-4ex}
\begin{minipage}{.51\textwidth}
\bigskip
\bigskip
\begin{itemize}
\item<2>
Now $\model{\amodel} \satisfiesnotlookup{\saluf} \formula{\binpred{L}{y}{x}}$
% $\M \;\not\mw_\saluf Lyx$
\item<3>
But: $\model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{y}{\,\binpred{L}{y}{\freevar{x}}}}$
% $\M \;\mw_\saluf \eris y Lyx$,
\\
because
$\model{\amodel} \satisfieslookup{\saluf[\freevar{y}\mapsto 1]} \formula{\binpred{L}{\freevar{y}}{\freevar{x}}}$
% $\M \;\mw_{\saluf[y\mapsto 1]} Lyx$
\item<4->
Also
$\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\existsst{y}{\, \binpred{L}{y}{x}}}}$ $\;\;$?
%$\M \;\mw_\saluf \alle x\eris y Lyx$?
\item<5->
No:
$\model{\amodel} \satisfiesnotlookup{\saluf[\freevar{x}\mapsto 1]} \formula{\existsst{y}{\,\binpred{L}{y}{\freevar{x}}}}$
%$\M \;\not\mw_{\saluf[x\mapsto 1]} \eris y Lyx$
\end{itemize}
\end{minipage}
%
\hspace*{2ex}
\begin{minipage}{.25\textwidth}
\onslide<3>{\scalebox{.6}{
\begin{tikzpicture}[
dom/.style={circle,draw=orange!50!black,very thick,fill=orange!50!white,
inner sep=2pt}]
\node (1) [dom] {1};
\node (2) [below of=1,dom] {2};
\node (3) [below of=2,dom] {3};
\node (4) [below of=3,dom] {4};
\begin{scope}[node distance=30mm]
\node (x) [left of=2] {$x$};
\node (y) [left of=3] {$y$};
\node (z) [left of=4] {$z$};
\end{scope}
\begin{scope}[shorten <= 2mm, shorten >= 2mm, very thick, >=stealth]
\draw [->] (x) to (2);
\draw [green!60!black,->] (y) to[bend left=10] (1);
\draw [->] (z) to[bend right=20] (4) ;     %node [pos=.5] {A};
\end{scope}
\end{tikzpicture}
}}
\end{minipage}
%\hspace*{1ex}
\begin{minipage}{.23\textwidth}
\bigskip
\bigskip
\bigskip

\onslide<5->{\scalebox{.6}{
\begin{tikzpicture}[
dom/.style={circle,draw=orange!50!black,very thick,fill=orange!50!white,
inner sep=2pt}]
\node (1) [dom] {1};
\node (2) [below of=1,dom] {2};
\node (3) [below of=2,dom] {3};
\node (4) [below of=3,dom] {4};
\node (a) at (y) [xshift=20mm, yshift=-3mm] {\Large ?};
\begin{scope}[node distance=30mm]
\node (x) [left of=2] {$x$};
\node (y) [left of=3] {$y$};
\node (z) [left of=4] {$z$};
\end{scope}
\begin{scope}[shorten <= 2mm, shorten >= 2mm, very thick, >=stealth]
\draw [red,->] (x) to[bend left=10] (1);
\draw [green!60!black,->] (y) to[bend right=10] (a);
\draw [->] (z) to[bend right=20] (4);
\end{scope}
\end{tikzpicture}
}}
\end{minipage}
\end{frame}