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