Segerberg Squares of Modal Logics and Theories of Relation Algebras

Abstract

The paper studies two-dimensional modal logics with additional connectives (so-called Segerberg squares) and can be regarded as a continuation of Shehtman (Russian Mathematical Surveys, 67(4):721–778, 2012). It gives a new simpler proof of the finite model property of minimal Segerberg squares using bisimulation games. It proves the square finite model property for Segerberg squares of polymodal $\mathbf{T}$ and $\mathbf{D}$. It also constructs a faithful embedding of Segerberg squares in the equational theory of relation algebras.

Appendix

In this part we prove a simple syntactic fact from modal logic and recall the proof of some standard identities in relation algebras (for the readers who are less familiar with the subject).

Proposition 1

$\mathbf{K}+\Diamond ^2p\,{\leftrightarrow }\, p\vdash \square p\,{\leftrightarrow }\,\Diamond p$, and thus

$\mathbf{K}+\Diamond ^2p\,{\leftrightarrow }\, p\vdash \lnot \Diamond p\,{\leftrightarrow }\,\Diamond \lnot p$.

Proof

In this logic we have $\Diamond ^2\top \,{\leftrightarrow }\, \top$, i.e., $\Diamond ^2\top$. So it contains $\mathbf{D}$ and proves $\square p\rightarrow \Diamond p$.

For the converse we first obtain $\square ^2p\,{\leftrightarrow }\, p$ (by substituting $\lnot p$ for p in the axiom). So $p\rightarrow \square ^2p$, and by substitution, $\Diamond p\rightarrow \square ^2\Diamond p$. From $\square p\rightarrow \Diamond p$ by substitution and monotonicity we have $\square ^2\Diamond p\rightarrow \square \Diamond ^2 p$. Thus $\Diamond p\rightarrow \square \Diamond ^2 p$, and by applying the axiom, $\Diamond p\rightarrow \square p$. $\boxtimes$

Proposition 2

The following identities and quasiidentities hold in $\mathbf{R}{} \mathbf{A}$:

• (1) $x\leqslant y\Rightarrow x^{-1}\leqslant y^{-1}$,

• (2) $\mathbf{1}^{-1}=\mathbf{1}$,

• (3) $z\circ (x\cup y)=(z\circ x)\cup (z\circ y)$,

• (4) ${\delta }^{-1}={\delta }$,

• (5) ${\delta }\circ x=x$,

• (6) $x\leqslant y\Rightarrow z\circ x\leqslant z\circ y$,

• (7) $x\circ \mathbf{0}=\mathbf{0}$,

• (8) $x\cap (\mathbf{1}\circ y)\leqslant x\circ y^{-1}\circ y$,

• (9) $x\leqslant y\Rightarrow x\circ z\leqslant y\circ z$,

• (10) $x\leqslant {\delta }\Rightarrow x=x^{-1}$.

Proof

(1) $x\leqslant y$ implies $y=x\cup y$, and so $y^{-1}=(x\cup y)^{-1}=x^{-1}\cup y^{-1}$ by (RA2). Hence $x^{-1}\leqslant y^{-1}$.

(2) $\mathbf{1}^{-1}\leqslant \mathbf{1}$ implies $(\mathbf{1}^{-1})^{-1}\leqslant \mathbf{1}^{-1}$ by (1), and so $\mathbf{1}\leqslant \mathbf{1}^{-1}$ by (RA5).

(3) From (RA1), (RA2), (RA6) we have:

$$ z^{-1}\circ (x^{-1}\cup y^{-1})= (z^{-1}\circ x^{-1})\cup (z^{-1}\circ y^{-1}). $$

Now replace x, y, z by their converses and use (RA5).

(4) ${\delta }^{-1}\circ {\delta }={\delta }^{-1}$ by (RA4); hence

$$({\delta }^{-1}\circ {\delta })^{-1}=({\delta }^{-1})^{-1}, $$

and so

$${\delta }^{-1}\circ {\delta }={\delta }, $$

by (RA6) and (RA5). Thus ${\delta }^{-1}={\delta }$.

(5) (RA5) and (RA6) imply ${\delta }^{-1}\circ x^{-1}=x^{-1}$. Then replace x by $x^{-1}$ and use (4) and (RA5).

(6) Replace y by $x\cup y$ and apply (3).

(7) Obviously,

$$ \mathbf{0}\leqslant -(x\circ \mathbf{1}). $$

Hence by (6) and (RA7)

$$ x^{-1}\circ \mathbf{0}\leqslant x^{-1}\circ (-(x\circ \mathbf{1}))\leqslant -\mathbf{1}=\mathbf{0}. $$

Now replace x by $x^{-1}$.

(8) As mentioned in the proof of Lemma 12.8.6, this is a translation of the $\mathbf{K.t}$-theorem

$$ p\wedge \blacklozenge ^{-1}\top \rightarrow \blacklozenge ^{-1}\blacklozenge p. $$

To prove the latter, we first obtain

$$ p\wedge \blacklozenge ^{-1}\top \rightarrow \blacksquare ^{-1}\blacklozenge p\wedge \blacklozenge ^{-1}\top $$

from a temporal axiom, and then apply the $\mathbf{K}$-theorem

$$ \blacksquare ^{-1}q\wedge \blacklozenge ^{-1}\top \rightarrow \blacklozenge ^{-1}q. $$

(9) Similar to (6)

(10) Apply (5), (9) and (8) for $y={\delta }$:

$$ x=x\cap ({\delta }\circ x)\leqslant x\cap (\varvec{1}\circ x)\leqslant x\circ x^{-1}\circ x. $$

So for $x\leqslant {\delta }$ we have by monotonicity and (6), (9)

$$ x\leqslant {\delta }\circ x^{-1}\circ {\delta }\leqslant x^{-1}. $$

Hence by taking the converses we obtain

$$ x^{-1}\leqslant x, $$

and thus $x^{-1}= x$. $\boxtimes$