\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 ($\Leftarrow$)} \begin{itemize} \pause \item Let $\F = (W,R)$ be a frame where $R$ is transitive. \pause \item Let $L$ be an arbitrary labelling, and $x$ a world in $W$. \pause \item We show $x \fc \some\some p \to \some p$.\\ \pause That is, if $x\fc \some\some p$, then also $x\fc \some p$. \pause \item Thus assume that $x \fc \some\some p$. \pause \item Then there exists $y\in W$ with $R(x,y)$ and $y \fc \some p$. \pause \item Then there exists $z \in W$ with $R(y,z)$ and $z \fc p$. \pause \item Because of transitivity of $R$ we have $R(x,z)$. \pause \item Hence $x \fc \some p$. \end{itemize} \end{block} \vspace{10cm} \end{frame}