\begin{frame}[t] \frametitle{Distribution of $\,\formula{\sforall}\,$ over $\,\formula{\slogand}\,$ and $\,\formula{\slogor}\:$?} \begin{alertblock}{} Does it work for $\,\formula{\slogand}\,$ and $\,\formula{\slogor}\,$? \begin{itemize}\vspace*{0.45ex}\setlength{\itemsep}{0.45ex} \item $\formula{\forallst{x}{(\logand{\unpred{LL}{x}}{\unpred{C}{x}}})} \;\logequiv\; \formula{\logand{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$ $\;$ \alert{?} \item $\formula{\forallst{x}{(\logor{\unpred{LL}{x}}{\unpred{C}{x}})}} \;\logequiv\; \formula{\logor{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$ $\;$ \alert{?} \end{itemize} \end{alertblock} \pause\bigskip Are there counter models? \pause\medskip In the first case, no, in the second case, yes! \pause\medskip \begin{block}{ $\; \formula{\forallst{x}{\logand{(\unpred{LL}{x}}{\unpred{C}{x})}}} \;\logequiv\; \formula{\logand{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$ } \begin{itemize}\vspace*{0.45ex}\setlength{\itemsep}{0.45ex} \item For every model $\model{\amodel}$ with domain $\adomain$ it holds that: \begin{talign} \model{\amodel} \satisfies \formula{\forallst{x}{\logand{(\unpred{LL}{x}}{\unpred{C}{x})}}} \;\;\;\Longleftrightarrow\;\;\; \intin{\sunpred{LL}}{\model{\amodel}} = \intin{\sunpred{C}}{\model{\amodel}} = \adomain \end{talign} \item The same is the case for $\; \model{\amodel} \satisfies \formula{\logand{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}} \;$ \item Thus the two formulas hold in precisely the same models. \end{itemize} \end{block} \end{frame}