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