\begin{frame} \frametitle{Transitive Frames: $\some\some p \to \some p$} \begin{goal}{Theorem} \begin{malign} \F \models \some\some p \to \some p \quad\iff\quad \text{the frame $\F$ is transitive} \end{malign} \end{goal} \pause \begin{block}{Proof ($\Rightarrow$)} \begin{itemize} \pause \item Let $\F = \pair{W}{R}$ be a frame with $\F \;\models\; \some\some p \to \some p$. \pause \item For a contradiction, assume that $R$ is not transitive. \pause \item Since $R$ is not transitive, there are $a,b,c \in W$ with \begin{malign} R(a,b) && R(b,c) && \neg R(a,c) \end{malign}\vspace{-1ex} \pause \item Define $\M = \langle W,R,\lab{L} \rangle$ with labelling $\lab{L}$ given by:\pause \begin{malign} \lab{L}(c) &= \{\;p\;\} &&& \lab{L}(w) &= \emptyset \quad \text{for every $w \neq c$} \end{malign}\vspace{-1ex} \pause \item Then \begin{itemize} \pause \item $b \fc \some p$ \tabto{2.7cm} since $c \fc p$ and $R(b,c)$ \pause \item $a \fc \some\some p$ \tabto{2.7cm} since $b \fc \some p$ en $R(a,b)$ \pause \item $a \not\fc \some p$ \tabto{2.7cm} since $p$ is valid only in $c$, and $\neg R(a,c)$ \end{itemize} \pause \item Thus $\;\M \not\models \some\some p \to \some p\;$; \pause contradicting $\F \models \some\some p \to \some p$. \end{itemize} \end{block} \vspace{10cm} \end{frame}