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