Arrow Logic

In this chapter, we continue the study of two-dimensional frames. Here we look at these frames from a slightly different perspective, namely apart from taking the states in the two-dimensional frames to be just pairs (u,v), we will view them as arrows leading from u to v. We will study a similarity type which, interpreted on squares, is very expressive. This similarity type consists of the following three modalities, a dyadic ○ a monadic ⊗ and a constant ι δ. All of these were discussed before; we recall their definitions on squares, $$\begin{array}{*{20}{l}} {\mathfrak{M}, (u,\upsilon ) \Vdash \varphi \circ \psi }&{\mathop \Leftrightarrow \limits^{def} }&{(\exists w) : \mathfrak{M}, (u,w) \Vdash \varphi \& \mathfrak{M},(w,\upsilon ) \Vdash \psi } \\ {\mathfrak{M},(u,\upsilon ) \Vdash \otimes \varphi }&{\mathop \Leftrightarrow \limits^{def} }&{\mathfrak{M},(\upsilon ,u) \Vdash \varphi } \\ {\mathfrak{M},(u,\upsilon ) \Vdash \iota \delta }&{\mathop \Leftrightarrow \limits^{def} }&{u = \upsilon .} \end{array}$$