Orthogonal Frames and Indexed Relations

Abstract

We define and study the notion of an indexed frame. This is a bi-dimensional structure consisting of a Cartesian product equipped with relations which only relate pairs if they coincide in one of their components. We show that these structures are quite ubiquitous in modal logic, showing up in the literature as products of Kripke frames, subset spaces, or temporal frames for STIT logics. We show that indexed frames are completely characterised by their ‘orthogonal’ relations, and we provide their sound and complete logic. Using these ‘orthogonality’ results, we provide necessary and sufficient conditions for an arbitrary Kripke frame to be isomorphic to certain well-known bi-dimensional structures.

1 Introduction

This text is concerned with a certain type of bi-dimensional relational structure which shows up in multiple areas of modal logic. The ubiquity of these structures, we wish to argue, should motivate an independent study of their properties and their logic, towards which we take the first steps in this paper.

In the text we will call these structures indexed frames. Let us start off by providing two distinct (but ultimately equivalent) definitions of what we mean by that.

Definition 1

By indexed frame we refer indistinctly to any of the following structures:

(IF1) Frames $(W_1\times W_2, R_1, R_2)$ where $R_1$ and $R_2$ are binary relations on $W_1\times W_2$ such that $(w_1,w_2)R_i(w'_1,w'_2)$ implies $w_j=w'_j$ for $i\ne j$;

(IF2) Tuples $(W_1,W_2,R^1, R^2)$ where, for $i\ne j$, $R^i=\{R^i_w:w\in W_j\}$ is a family of binary relations on $W_i$ indexed by the elements of $W_j$.

It is straightforward to see how these two definitions refer to the same type of structure. Given a frame of the form (IF1), we define $w_2 R^1_w w'_2$ iff $(w,w_2) R_1 (w,w'_2)$ and $w_1 R^2_w w'_1$ iff $(w_1,w) R_2 (w'_1,w)$ to obtain a frame of the form (IF2); conversely, given a frame in the form (IF2) we obtain a (IF1) frame by setting $(w_1,w_2)R_i(w'_1,w'_2)$ iff $w_j =w'_j$ and $w_i R^i_{w_j}w'_i$.

Having these bi-dimensional structures at hand, one can interpret formulas over a bi-modal language

$$\phi \,{:}{:}{=}\, p|\bot |(\phi \wedge \phi )|\lnot \phi |\square _1\phi |\square _2\phi $$

with respect to pairs in $W_1\times W_2$ as follows:

It can be easily seen how these semantics are equivalent.

We start this paper by illustrating that indexed frames show up quite often in the literature. In order to put forward this argument, we provide in the next section examples of well-known models in different areas of modal logic which are indexed frames. In Sect. 3 we show that the property of ‘orthogonality’ (i.e., the fact that each point in the model is uniquely determined by the pair of connected components to which it belongs) is necessary and sufficient to characterize indexed frames, and we use this property to provide their sound and complete logic. In Sect. 4 we enrich our language with modalities $\blacksquare _1$ and $\blacksquare _2$ which fix $w_2$ (resp. $w_1$) and quantify over all points in $W_1$ (resp. $W_2$). We provide the sound and complete logic for this extended language. In Sect. 5, we come back to the examples presented in Sect. 2 with the results on orthogonality previously discussed, showing necessary and sufficient conditions for a bi-relational Kripke frame to be isomorphic to several well-known types of indexed frames. We conclude in Sect. 6.

The proofs of some minor Propositions and Lemmas have been moved to the Appendix; this is indicated with the symbol .

2 Examples of Indexed Frames

Let us see some well-known structures that are either indexed frames or generated subframes thereof. We will use the term “indexed relation” to informally refer to a relation defined on a Cartesian product that respects one of the coordinates.

Example 1 (Products)

[7, Chapter 3] The product of two Kripke frames $(W_1,R_1)$ and $(W_2,R_2)$ (wherein $R_i$ is a binary relation defined on $W_i$ for $i=1,2$) is the frame

$$(W_1,R_1)\times (W_2,R_2) = (W_1\times W_2, R_H, R_V),$$

where $R_H$ and $R_V$ are binary relations on $W_1\times W_2$ (called the ‘horizontal’ and ‘vertical’ relations respectively) defined as:

Products very closely adjust to the (IF1) definition. In fact, indexed frames can be seen as a generalization of products. Indeed, a product can be seen as an (IF2) indexed frame $(W_1, W_2, R^1, R^2)$ with the extra property that, for all $w_1,w'_1\in W_1$ and $w_2,w'_2\in W_2$, $R^1_{w_2} = R^1_{w'_2}$ and $R^2_{w_1} = R^2_{w'_1}$.

It is of note that, while the logic of bidimensional products of frames (as studied in [7]) contains axioms making both modalities interact (such as $\Diamond _1\Diamond _2 p\leftrightarrow \Diamond _2\Diamond _1 p$), this will not the case for the logic of indexed frames.

Example 2 (Subset spaces)

In its most basic form [12], a subset space is a tuple consisting of a set X and some collection $\mathcal {O}$ of nonempty subsets of X.

One can interpret formulas of a bimodal language including $\square$ and K modalities on a subset space with respect to a pair (x, U) such that $x\in U$ and $U\in \mathcal {O}$ as follows:

The semantics above naturally defines two indexed relations on the graph $\mathcal {O}_X : = \{(x,U): x\in U \; \& \; U\in \mathcal {O}\}$, namely:

Clearly, the standard Kripke semantics on the frame $(\mathcal {O}_X, \equiv _K, \ge _\square )$ (let us call this a subset space frame) are the exact semantics above, and moreover this subset space frame is (a generated subframe of) an indexed frame.

Example 3 (Social Epistemic Logic)

Social Epistemic Logic (SEL) is a multi-modal framework to model knowledge within social networks, introduced in [15]. Its language contains, in addition to atomic propositional variables p, q..., nominal variables n, m, ..., an artefact borrowed from Hybrid Logic [1]. It has operators $K\phi$ and $F\phi$ to express things such as “I know $\phi$” and “all my friends $\phi$”, and, in addition, it presents an operator $@_n\phi$ for each nominal n to express “$\phi$ is true of the agent named by n”.

The models for SEL are of the form $(W,A,\{\sim _a\}_{a\in A}, \{\asymp _w\}_{w\in W}, V)$, where each $\sim _a$ is an ‘epistemic indistinguishability’ equivalence relation for agent a on the set of possible worlds W, and each $\asymp _w$ is a ‘social’ symmetric and irreflexive relation, representing which pairs of agents in the set A are ‘friends’ at world w. The valuation V assigns subsets of $W\times A$ to propositional variables p and, for a nominal n, V(n) is of the form $W\times \{a\}$ for some a; it is then said that “n is the name of a”, denoted $a=\underline{n}_V$.

For the semantics, we read formulas with respect to a pair of a world and an agent as follows: $(w,a)\models K\phi$ iff $(v,a)\models \phi$ for all v such that $w\sim _a v$; $(w,a)\models F\phi$ iff $(w,b)\models \phi$ for all b such that $a\asymp _w b$, and $(w,a)\models @_n\phi$ iff $(w,\underline{n}_V)\models \phi$.

$(W,A,\{\sim _a\}_{a\in A}, \{\asymp _w\}_{w\in W})$ is clearly an (IF2) indexed frame and even the $@_n$ modality can be interpreted via the “indexed” relation: $(w,a) R_n (v,b)$ iff $w=v$ and $b=\underline{n}_V$.

Its equivalent (IF1) form is $(W\times A, \sim , \asymp )$, where $(w,a) \sim (v,b)$ iff $a=b$ and $w\sim _a v$, and $(w,a)\asymp (v,b)$ iff $w=v$ and $a\asymp _w b$.

Example 4 (STIT logic)

The logic of seeing-to-it-that or STIT was studied in [3] and has shown up in the literature with many variations; in most cases, the different models for STIT are quite explicitly indexed frames, or present indexed relations. The one we showcase here is (a slightly simplified version of) a Kamp frame, discussed in [5, 17].

A Kamp frame is a tuple $(W,\mathcal {O}, \{\sim _t\}_{t\in T}, \{\sim _{t,i}\}_{t\in T, i\in Agt})$, where each world has a ‘timeline’ associated to it, this being a linear order $\mathcal {O}(w) = (T_w, <_w)$. T is the union of all the $T_w$’s. For each t, the relations $\sim _t$ and $\sim _{t,i}$ are equivalence relations defined on the set $\{w: t\in T_w\}$.

Sentences in a language including a necessity operator $\square$, agency operators [i] for $i\in Agt$ and a temporal operator G are read with respect to pairs (t, w) such that $t\in T_w$ as follows:

While this does not exactly adjust to the definitions of indexed frame above, one sees how this structure can be defined as (a generated subframe of) the (IF2) indexed frame

$$ (W,T, \{\sim _t\}_{t\in T}, \{\sim _{t,i}\}_{t\in T, i\in Agt}, \{<_w\}_{w\in W}).$$

(We are slightly bending our definition of ‘indexed frame’ here and allowing for multiple families of relations indexed by the elements of T.)

We can easily ‘rewrite’ these relations to be defined on (a subset of) $W\times T$ in the (IF1) way:

All the frames showcased in this section share one property: namely that of orthogonality. We explain and study this in the next section.

3 Orthogonal Frames

The relations $R_1$ and $R_2$ in an indexed frame $(W_1\times W_2, R_1, R_2)$ are “orthogonal” to each other, in the sense that there cannot be two distinct points connected by both $R_1$ and $R_2$. Indeed, if there is an $R_i$ path from $(w_1,w_2)$ to $(w'_1,w'_2)$ (i.e. if they belong to the same $R_i$-connected component), then $w_j = w'_j$ for $j\ne i$ and, in consequence, if there are both $R_1$ paths and $R_2$ paths between these pairs, then $(w_1,w_2)=(w'_1,w'_2)$. In the present section we shall see that this property fully characterises indexed frames.

For the rest of this paper, given a relation R, we let $R^*$ denote the least equivalence relation containing R, i.e., the equivalence relation induced by the connected components of R. By $\mathrm {Id}_W$ we refer to the identity relation $\{(w,w): w\in W\}$.

Definition 2

A birelational Kripke frame $(W,R_1,R_2)$ is orthogonal if there exist equivalence relations $\equiv _1$ and $\equiv _2$ on W satisfying:

A frame $(W,R_1, R_2)$ is said to be full orthogonal if there exist equivalence relations $\equiv _1$ and $\equiv _2$ on W satisfying (O1), (O2) and

We leave it to the reader to check that:

Lemma 1

$(W,R_1, R_2)$ is orthogonal if and only if $R^*_1\cap R^*_2 = \mathrm {Id}_W$.

Note that, if such a pair of equivalence relations exists, it is not necessarily unique: consider the frame $(W,R_1,R_2)$ where $W=\mathbb {N}^2$ and $R_1 = R_2 = \mathrm {Id}_W$; the pair of equivalence relations $(\equiv _1,\equiv _2)$, where $(n_1,n_2) \equiv _i (m_1,m_2)$ iff $n_i=m_i$ satisfies properties O1 – O3; however, the pair $(W^2, \mathrm {Id}_W)$ does as well.

Proposition 1

$(W,R_1,R_2)$ is isomorphic to an indexed frame if and only if it is full orthogonal.

Proof

Let $(W_1\times W_2,R_1,R_2)$ be an indexed frame. Then the relations $(w_1,w_2)\equiv _i(w'_1,w'_2)$ iff $w_j =w'_j$ (where $\{i,j\}=\{1,2\}$) satisfy O1, O2, and O3.

Conversely, suppose such relations exist, and let $[w]_i$ denote the equivalence class of w under $\equiv _i$. By O2 and O3, given any pair $(w,v)\in W^2$, there is exactly one element in the intersection $[w]_2\cap [v]_1$: let $x_{w,v}$ denote this unique element. Consider the frame $(W/_{\equiv _2}\times W/_{\equiv _1},\mathsf {R}_1,\mathsf {R}_2)$, where

$$([w]_2,[v]_1) \mathsf {R}_i ([w']_2,[v']_1)\text { if and only if }x_{w,v} R_i x_{w',v'}.$$

This in an indexed frame, for if $x_{w,v} R_1 x_{w',v'}$, then $x_{w,v} \equiv _1 x_{w',v'}$, and since $v\equiv _1 x_{w,v} \equiv _1 x_{w',v'} \equiv _1 v'$, this gives $[v]_1 = [v']_1$. We reason analogously for $\mathsf {R}_2$. It is isomorphic to $(W,R_1,R_2)$ via the map $f([w]_2,[v]_1) = x_{w,v}$. For injectivity, note that if $x_{w,v} \ne x_{w',v'}$, then either $w\not \equiv _2 w'$ or $v\not \equiv _1 v'$. For surjectivity, note that $w = x_{w,w}$ for all $w\in W$. Finally, note that we have defined the map in such a way that $([w]_2,[v]_1) \mathsf {R}_i ([w']_2,[v']_1)$ iff $f([w]_2,[v]_1) R_i f([w']_2,[v']_1)$.

Definition 3

Given two Kripke-complete unimodal logics $L_1$ and $L_2$ we say that a birelational frame $(W,R_1,R_2)$ is a $[L_1,L_2]$-frame if $(W,R_i)\models L_i$, for $i=1,2$.

Recall that the fusion logic $L_1\oplus L_2$ is the least normal modal logic containing the axioms and rules of $L_1$ for $\square _1$ and of $L_2$ for $\square _2$ and that:

Theorem [7, Thm. 4.1]. $L_1 \oplus L_2$ is the logic of $[L_1,L_2]$-frames.

We have:

Proposition 2

An orthogonal $[L_1,L_2]$-frame $(W,R_1,R_2)$ is a generated subframe of a full orthogonal $[L_1,L_2]$-frame.

Proposition 3

The fusion logic $L_1\oplus L_2$ is the logic of orthogonal $[L_1,L_2]$-frames.

Proof

The proof in [7, Thm. 4.1] of the fact that

the logic of frames $(W,R_1,R_2)$ such that $(W,R_i)\models L_i$ for $i=1,2$ is the fusion $L_1\oplus L_2$

utilises the construction of a dovetailed frame in order to prove that any formula $\phi$ consistent in $L_1\oplus L_2$ is satisfiable in an $[L_1,L_2]$-frame. It is a recursive process done as follows: first, one obtains a consistent formula in the language of $L_1$ by rewriting $\phi$ with ‘surrogate’ propositional variables $p^1_{\Diamond _2 \psi _1},...,p^1_{\Diamond _2 \psi _n}$ in place of its maximal subformulas preceded by $\Diamond _2$. Then one constructs a rooted $L_1$-frame satisfying $\phi$. Whenever a point in this frame satisfies a surrogate variable $p^1_{\Diamond _2\psi }$, one rewrites $\psi$ in the language of $L_2$ by using surrogates $q^2_{\Diamond _1\theta _1}, ..., q^2_{\Diamond _1\theta _n}$ and makes this point the root of an $L_2$-frame satisfying this formula. One repeats this process, alternating between $L_1$-formulas and $L_2$-formulas until one obtains a rooted frame satisfying $\phi$ at the root.

We point the interested reader to [7] for more precise details about this construction; for clarity, we provide a simple example from [7], using the formula $\phi = p\wedge \Diamond _1 (\lnot p \wedge \Diamond _2 p) \wedge \Diamond _2(\lnot p\wedge \Diamond _1(p\wedge \Diamond _2 p))$.

We rewrite $\phi$ as $p\wedge \Diamond _1 (\lnot p \wedge \mathbf {q}^2) \wedge \mathbf {r}^2$, where $\mathbf {q}^2$ is a ‘surrogate’ for $\Diamond _2 p$, $\mathbf {r}^2$ for $\Diamond _2(\lnot p\wedge \mathbf {q}^1)$, $\mathbf {q}^1$ for $\Diamond _1(p\wedge \mathbf {s}^2)$, and $\mathbf {s}^2$ for $\Diamond _2 p$.

We construct a rooted $L_1$-frame satisfying the rewritten formula (top left of Fig. 1); we make the node satisfying $\mathbf {r}^2$ into the root of an $L_2$-frame satisfying its surrogate formula $\Diamond _2(\lnot p\wedge \mathbf {q}^1)$ and the $\mathbf {q}^2$ node into frame satisfying $\Diamond _2 p$ (top right); we then proceed similarly with $\mathbf {q}^1$ (bottom left) and finally with $\mathbf {s}^2$ (bottom right) to find a $[L_1,L_2]$-frame satisfying $\phi$ at its bottom point.

Fig. 1.

‘Dovetailed’ construction of a frame for $p\wedge \Diamond _1 (\lnot p \wedge \Diamond _2 p) \wedge \Diamond _2(\lnot p\wedge \Diamond _1(p\wedge \Diamond _2 p))$.

For our current purposes it suffices to point out that the ‘dovetailed’ frames obtained by this method are always orthogonal, for this construction does not allow for two distinct points x and y to be reachable from each other by both $R_1$ and $R_2$. As an immediate consequence of Propositions 2 and 3:

Theorem 1

The logic of $[L_1,L_2]$-indexed frames is the fusion $L_1\oplus L_2$.

4 Orthogonal Structures

In the definition for full orthogonal frames (Definition 2) we demand the existence of equivalence relations which are supersets of the two given relations and satisfy the properties of full orthogonality. These relations are not made explicitly part of the structure and are not taken into account when defining the logic.

In this section we consider structures $(X,R_1,R_2,\equiv _1,\equiv _2)$ satisfying O1, O2 and O3, and we study the logic of these frames when we add modal operators to our language to explicitly account for the orthogonal equivalence relations.

Let us first note the following fact:

Lemma 2 (Generalized orthogonal frames)

If $(W,R_1,R_2)$ is a Kripke frame such that there exist equivalence relations $\equiv _1$ and $\equiv _2$ on W satisfying

then $(W,R_1,R_2)$ is a disjoint union of full orthogonal frames.

Definition 4

An orthogonal structure is a tuple $(W,R_1,R_2, \equiv _1, \equiv _2)$, where $(W,R_1,R_2)$ is a birelational Kripke frame and $\equiv _1$ and $\equiv _2$ are equivalence relations on W satisfying (O1), (O2), and (O3’) above. A standard orthogonal structure satisfies moreover (O3) $\equiv _1\circ \equiv _2 = W^2$.

A tuple satisfying (O1) and (O3’) is called a semistructure.

We define a semantics for (semi)structures $(W,R_{1,2},\equiv _{1,2})$ with respect to a language containing operators $\square _i$ and $\blacksquare _i$ for $i=1,2$ as follows:

A very standard canonical model argument shows that:

Proposition 4

The sound and complete logic of semistructures is

$$K_{\square _1} + K_{\square _2} + S5_{\blacksquare _1} + S5_{\blacksquare _2} + \blacksquare _1\blacksquare _2 \phi \leftrightarrow \blacksquare _2\blacksquare _1\phi + \blacksquare _i\phi \rightarrow \square _i\phi .$$

Moreover, if $L_1$ and $L_2$ are canonical unimodal logics, the logic of semistructures $(W,R_{1,2},\equiv _{1,2})$ such that $(W,R_i)\models L_i$ for $i=1,2$ is

$$L_{1} + L_2 + S5_{\blacksquare _1} + S5_{\blacksquare _2} + \blacksquare _1\blacksquare _2 \phi \leftrightarrow \blacksquare _2\blacksquare _1\phi + \blacksquare _i\phi \rightarrow \square _i\phi .$$

Let us call these logics $Log_\dashv$ and $Log^{L_1L_2}_\dashv$ respectively. Let us now see that $Log_\dashv$ is also the logic of orthogonal structures (and, in turn, of “standard” structures).

Recall that a bounded morphism between Kripke frames $F = (W,R_1,...,R_n)$ and $F' = (W',R'_1,..., R'_n)$ is a map $f:W\rightarrow W'$ satisfying the forth condition ($wR_i v$ implies $f(w) R'_i f(v)$) and the back condition ($f(w) R'_i v$ implies there is an $w\in f^{-1}(w')$ such that $wR_i v$). If the bounded morphism is surjective, then every formula which is refutable in $F'$ can be refuted in F. (See [4, Thm. 3.14] for details).

We shall show that a semistructure is always the image of a bounded morphism departing from an orthogonal structure, which in turn will let us prove that the logic of orthogonal structures is the above.

The proof below utilises the notion of a matrix enumeration. Given sets I and X, an I-matrix enumeration of X is a map $f:I\times I\rightarrow X$ such that, for any fixed $i_0\in I$, both maps

$$j\in I \mapsto f(i_0,j)\in X \text { and } j\in I \mapsto f(j, i_0)\in X$$

are surjective.

Lemma 3

If $|I| \ge |X|$, there exists an I-matrix enumeration of X.

With this:

Proposition 5

A semistructure is a bounded morphic image of an orthogonal structure.

Proof

Let $(W,R_{1,2},\equiv _{1,2})$ be a semistructure. Let I be a set of indices with the same cardinality as W.

Let us consider the quotient set $W/_{\equiv _1\cap \equiv _2}$. Let us fix a matrix enumeration $f_{[w]}: I\times I\rightarrow [w]$ of each equivalence class $[w]\in W/_{\equiv _1\cap \equiv _2}$. We use $w_{ij}$ as a shorthand for $f_{[w]}(i,j)$. Note that it is always the case that $w\equiv _k w_{ij}$ for $k=1,2$.

We define the following relations on the set $W'= W/_{\equiv _1\cap \equiv _2} \times I^2$:

Let us see that this is an orthogonal structure. Indeed,

(O1) $([w],i_1,i_2)R'_k([v],j_1,j_2)$ implies $w_{i_1 i_2} R_k v_{j_1 j_2}$ and $i_l=j_l$ (for $k\ne l$), which in turn implies $w_{i_1 i_2} \equiv _k v_{j_1 j_2}$ and $i_l=j_l$. This means that $w\equiv _k v$ and $i_l =j_l$, and thus $([w],i_1,i_2)\equiv '_k([v],j_1,j_2)$.

(O2) If $([w],i_1,i_2)\equiv '_k ([v],j_1,j_2)$ for $k=1$ and 2, then $i_1 = j_1$, and $i_2 = j_2$, and $(w,v)\in \equiv _1\cap \equiv _2$, which implies $[w] = [v]$. Therefore, $\equiv '_1\cap \equiv '_2 = Id_{W'}$.

(O3’) If $([w],i_1,i_2) (\equiv '_1 \circ \equiv '_2) ([u], j_1, j_2)$, then $w(\equiv _1 \circ \equiv _2) u$. This, plus property (O3’) of the semistructure, implies that there exists some $v'$ such that $w\equiv _2 v' \equiv _1 u$. But then

$$([w],i_1,i_2) \equiv '_2 ([v'], i_1, j_2) \equiv '_1 ([u], j_1, j_2).$$

This shows that $(\equiv '_1\circ \equiv '_2) \subseteq (\equiv '_2\circ \equiv '_1)$; the converse inclusion is analogous.

Finally, the map

$$([w], i_1, i_2) \in W/_{\equiv _1\cap \equiv _2} \times I^2 \mapsto w_{i_1 i_2} \in W$$

is a bounded morphism. For the forth condition, $([w],i_1,i_2)\equiv '_k([v],j_1,j_2)$ implies $w_{i_1 i_2} \equiv _k v_{j_1 j_2}$ and $([w],i_1,i_2)R'_k([v],j_1,j_2)$ implies $w_{i_1 i_2} R_k v_{j_1 j_2}$, by definition. For the back condition, if $w_{i_1 i_2} R_1 v$, then there exists an index $j\in I$ such that $f_{[v]}(j,i_2) = v$ and, by definition,

$$([w], i_1, i_2) R'_1 ([v], j, i_2).$$

An analogous argument can be made for $R_2$, $\equiv _1$ and $\equiv _2$.

As a consequence:

Theorem 2

The sound and complete logic of standard orthogonal structures is $Log_\dashv$,

$$K_{\square _1} + K_{\square _2} + S5_{\blacksquare _1} + S5_{\blacksquare _2} + \blacksquare _1\blacksquare _2 \phi \leftrightarrow \blacksquare _2\blacksquare _1\phi + \blacksquare _i\phi \rightarrow \square _i\phi .$$

Proof

Consequence of Propositions 4 and 5.

Remark 1

The construction in the proof above respects many properties of the $R_i$ relations: for instance, if $R_i$ is reflexive, transitive, symmetric, Euclidean, etc., then so is $R'_i$. This means that this technique can be used to prove that $Log^{L_1L_2}_\dashv$ is the logic of indexed structures $(W,R_i,\equiv _i)$ where $(W,R_i)\models L_i$ for a large family of logics that includes S4, S5, KD45, etc. We conjecture that the result is true for any pair $L_1, L_2$ of Kripke-complete unimodal logics.

Let us now define a semantics for this extended language directly on indexed frames $(W_1\times W_2, R_1, R_2)$, taking advantage of the isomorphism between indexed frames and full orthogonal frames given in the proof of Proposition 1. The fact that the isomorphic image of the equivalence classes of the ‘orthogonal’ equivalence relations are sets of the form $W_1\times \{w_2\}$ and $\{w_1\}\times W_2$ allows us to consider the $\blacksquare$ modalities as coordinate-wise ‘universal modalities’; that is to say, if we interpret formulas of the extended language on indexed frames as follows:

then we have that:

Proposition 6

$Log_\dashv$ is the sound and complete logic of indexed frames for the language including $\square _i$ and $\blacksquare _i$ operators.

We finish this Section by pointing out the fact that $Log_\dashv$ enjoys the Finite Model Property with respect to semistructures, orthogonal structures and indexed frames, in the following sense:

Proposition 7

If $\phi \notin Log_\dashv$, then there exists a finite indexed frame refuting $\phi$.

We conjecture that, if $L_1$ and $L_2$ have the Finite Model Property, then for all $\phi \notin Log^{L_1 L_2}_\dashv$ there exists a finite $[L_1,L_2]$-semistructure (perhaps a finite $[L_1,L_2]$-indexed frame) refuting $\phi$; this problem, however, remains open.

5 Some Case Studies

In the present section we return to the Examples in Sect. 2 and, with the help of our orthogonality results above, we abstract from the “indexed frame” definition and give necessary and sufficient conditions on orthogonal frames to be isomorphic to these structures.

Products (Example 1). We have:

Proposition 8

A frame $(X,R_1,R_2)$ is isomorphic to a product of Kripke frames if and only if there exist two equivalence relations $\equiv _1$ and $\equiv _2$ such that:

Proof

That a product $(W_1,R_2) \times (W_2,R_2)$ satisfies these properties (with the equivalence relations $(w_1,w_2) \equiv _i (v_1,v_2)$ iff $w_j = v_j$) is trivial.

Now let us consider a frame $(W,R_1,R_2)$ satisfying the properties above and let $x_{wv}$ denote the unique element in $[w]_2\cap [v]_1$ (as in the proof of Proposition 1). This frame satisfies, for all $w,w',v,v'\in W$: $x_{wv} R_1 x_{w'v}$ iff $x_{wv'} R_1 x_{w'v'}$. Indeed, if $x_{wv} R_1 x_{w'v}$, since $x_{w'v} \equiv _2 x_{w'v'}$, then by (P1) there must exist some y such that $x_{wv'} \equiv _2 y R_1 x_{w'v'}$, and this y can be no other than $x_{wv'}$. We thus can define a relation on $W/_{\equiv _2}$ as $[w]_2 R'_1 [w']_2$ iff $x_{wv} R_1 x_{w'v}$ for some (equiv.: for all) v. We proceed similarly to define a relation $R'_2$ on $W/_{\equiv _1}$: $[v]_1 R'_2 [v']_1$ iff $x_{wv} R_1 x_{wv'}$ for some (for all) w.

The product $(W/_{\equiv _2}, R'_1) \times (W/_{\equiv _1}, R'_2)$ is equal to $(W/_{\equiv _2} \times W/_{\equiv _1}, \mathsf {R}_1, \mathsf {R}_2),$ isomorphic to $(W,R_1,R_2)$ as per Proposition 1.

Subset spaces (Example 2). Recall the notion of a subset space frame from Example 2. We have:

Proposition 9

A frame $(W,R_K,R_\square )$ is isomorphic to a subset space frame if an only if

and there exists an equivalence relation $\equiv _\square$ such that

and, moreover,

Social Epistemic Logic (Example 3). Let us define a semantics for Social Epistemic Logic on full orthogonal structures $(X,R_K,R_F,\equiv _A,\equiv _W)$, where $R_K\subseteq \equiv _A$ and $R_F\subseteq \equiv _W$. The equivalence classes of these relations will represent agents and worlds respectively.

Recall that the only constraints on a SEL model $(W,A,\sim ,\asymp )$ are that $\sim$ must be an equivalence relation and $\asymp$ must be symmetric and irreflexive. Therefore, via the isomorphism in Proposition 1, one easily sees that:

Lemma 4

Let $(X,R_K,R_F,\equiv _A,\equiv _W)$ be a full orthogonal structure. The full orthogonal frame $(X, R_K, R_F)$ is isomorphic to a SEL frame if and only if, on top of (O1) – (O3), it satisfies:

Recall (Proposition 1) that the corresponding isomorphic SEL model will be $(X/_{\equiv _W}, X/_{\equiv _A}, \mathsf {R}_K, \mathsf {R}_F)$, where $\mathsf {R}_K$ relates two pairs of equivalence classes if an only if the unique elements in the intersection of each pair are related by $R_K$ (and likewise for $\mathsf {R}_F$).

Now let us consider how a valuation must act upon this model. For a SEL model we demand that each V(n) must be of the form $W\times \{a\}$ for some unique agent $a\in A$. Via the isomorphism outlined above, we can see, for the image of a valuation V defined on an orthogonal structure $(X,R_K,R_F,\equiv _A,\equiv _W)$ to be a valid valuation on a SEL model, we want the image of the set V(n) to be $X/_{\equiv _W} \times \{[y]_A\}$ for some $y\in X$. But the pre-image of this set is precisely $[y]_A$.

We thus demand the following property:

For each nominal n and $x\in X$, we let $n_x$ denote the unique element in $[x]_W \cap V(n)$.

Models of SEL must be named. A named model is a model wherein every agent has a name, i.e., for all $a\in A$, there exists a nominal n such that $a = \underline{n}$. In these isomorphic structures, the notion of named model translates to: for all $y\in X$, there exists n such that $V(n) = [y]_A$, or, equivalently,

With all this we can define a semantics for Social Epistemic Logic on full orthogonal models $(X,R_K,R_F,\equiv _A,\equiv _W, V)$ where $R_K$, $R_F$ and V satisfy the constraints (SEL1) – (SEL4) above as follows:

The ‘non-rigid’ variant of SEL [18] assigns different names to agents in each possible world. This is imposed via the following, weaker, constraint of the valuation: for every nominal n and each world w, there exists a unique agent $a\in A$ such that $(w,a)\in V(n)$. In the isomorphic structures above, this translates to a constraint weaker than (SEL3), namely:

A proof of completeness of (standard, rigid) SEL using ‘indexed’ canonical models was recently given in [2] (it had been proven in [14] with a different method). Completeness of ‘non-rigid’ SEL was proven in [18] by means of an involved step-by-step construction, but a proof of this result using canonical models remains an open problem. We conjecture that the semantics above could assist in this endeavour.

STIT logic (Example 4). [5] compares three distinct semantics for STIT logic. One of them, in the form of ‘Kamp frames’, was briefly alluded to in Example 4. Another one, introduced in [10], interprets sentences on T-STIT frames: these are one-dimensional Kripke frames

$$ (X, \equiv _\square , \{\equiv _i\}_{i\in Agt}, \prec _G) $$

wherein two different sorts of relations allow to reason, respectively, about time ($\prec _G$) and necessity/agency (the equivalence relations, with $\equiv _i \subseteq \equiv _\square$). These relations are defined to be orthogonal, for they satisfy ‘$x\equiv _\square y$ implies $x\nprec _G y$’.

In [5] it is shown that both T-STIT frames and Kamp frames satisfy the same formulas, via an argument which involves transforming one structure into the other in a truth-preserving manner. However, thanks to the isomorphism in Proposition 1 (and the (IF1) redefinition of a Kamp frame of Example 4) one can go beyond and show that a Kamp frame is always a T-STIT frame and that a T-STIT frame is isomorphic to a Kamp frame, wherein the set of ‘timelines’ W is defined by the connected components of $\prec$ and the set of ‘moments’ T is given by the equivalence classes of $\equiv _\square$.

6 Discussion and Future Work

We have identified a structure that shows up with relative frequency in different areas of modal logic; we have argued that an independent study of this structure is warranted and have taken the first steps towards it.

We have shown that these structures are completely characterised by the ‘orthogonality’ of their relations. Proofs of completeness of frameworks based on indexed frames are not particularly easy to tackle; as an example, we point the reader to the completeness proof of SEL in [14]. We hope that the above observations about orthogonality will help facilitate some of these proofs.

Some work remains to be done and many questions are open. Among these are the following:

Is $Log_\dashv ^{L_1 L_2}$ the logic of orthogonal structures $(W,R_{1},R_2,\equiv _{1},\equiv _2)$ such that $(W,R_i)\models L_i$, for any pair of Kripke-complete logics $L_1$ and $L_2$? Can a formula $\phi \notin Log_\dashv ^{L_1 L_2}$ be refuted in a finite indexed frame whenever $L_1$ and $L_2$ have the FMP? We conjecture an affirmative answer to these questions, and we plan further research to resolve them.

Some variations on subset space logics consider families of subsets which are closed under intersection [12] or which are topologies [6, 8, for instance]. What further restrictions does one have to add to obtain a result analogous to Proposition 9 for these structures? In the latter case, is there a relation between these properties and the point-free topologies of [13]?

Perhaps the most obvious question: how does one generalise the definitions and results in this paper to the n-dimensional case? The reader may find that there are two reasonable generalisations of this framework to the n-th dimension:

Out of these two, we suggest (A) is more appropriate, for it does not make much sense to apply (B) to $n=1$, and (A) is the only one which still generalises n-dimensional products. Many of the results of this paper may translate relatively easily to the n-dimensional case, whereas some may not. We plan to devote future work to this question.

Appendix

Proof of Proposition 2. Given an orthogonal $[L_1,L_2]$-frame $(W,R_1,R_2)$, we extend W to the set

$$W' = W \cup \{ x_{wv}: w,v\in W, R^*_2(w)\cap R^*_1(v) = \varnothing \},$$

i.e., we add one element for each pair of connected components which have an empty intersection, and we extend the relations $R_i$ as follows:

• if $F_\bullet \models L_i$, then $R'_i = R_i$;

• if $F_\circ \models L_i$, then $R'_i = R_i \cup \{(x,x):x\in W'\setminus W\}$;

where $F_\bullet$ is the irreflexive singleton frame $(\{*\}, \varnothing )$, and $F_\circ$ is the reflexive singleton frame $(\{*\}, \{(*,*)\})$. (Recall that every logic is satisfied in either $F_\bullet$ or $F_\circ$; this is a consequence of a classical result by Makinson [11].)

Note that, in either case, no elements of W are related to any elements of $W'\setminus W$ and thus $(W,R_1,R_2)$ is a generated subframe of $(W',R'_1, R'_2)$.

We define

Note that $\equiv '_1$ and $\equiv '_2$ satisfy conditions O1 – O3 of Definition 2, and therefore $(W',R'_1,R'_2)$ is a full orthogonal frame. Finally, for $i=1,2$, $(W',R'_i)$ is the disjoint union of the $L_i$-frame $(W,R_i)$ with a family of singleton $L_i$-frames, and thus it is an $L_i$-frame.

Proof of Lemma 2. We leave it to the reader to check that (O3’) implies that $\equiv _1 \circ \equiv _2$ is an equivalence relation. Let $W'$ be an equivalence class of $\equiv _1\circ \equiv _2$. Let $R'_i$ and $\equiv '_i$ be the restrictions of $R_i$ and $\equiv _i$ to $W'$. It is routine to check that (O1) $R'_i\subseteq \equiv '_i$, (O2) $\equiv '_1\cap \equiv '_2 = Id_{W'}$, and (O3) $\equiv '_1 \circ \equiv '_2 = (W')^2$. Each of these is therefore a full orthogonal frame and $(W,R_1,R_2)$ is equal to the disjoint union $\bigcup _{W'\in W/_{\equiv _1\circ \equiv _2}} (W',R'_1,R'_2)$.

Proof (sketch) of Proposition 4. This uses the very standard technique of canonical models; we point the reader to [4, Chapter 4] for full details and we simply offer a sketch here:

Let X be the set of maximal consistent sets of formulas in the language. We define the relations $xR_i y$ iff, for all $\phi$, $\square _i\phi \in x$ implies $\phi \in y$ and $x\equiv _i y$ iff, for all $\phi$, $\blacksquare _i\phi \in x$ implies $\phi \in y$.

The Truth Lemma shows that, given the valuation $V(p) = \{x\in X:p\in x \}$, it is the case that $x\models \phi$ iff $\phi \in x$.

We note that the logic $Log_\dashv ^{L_1 L_2}$ is canonical, for canonicity is preserved by fusions [9, Cor. 6] and the addition of Sahlqvist axioms [4, Chapter 4]. This canonicity ensures that $(X,R_i)\models L_i$; the S5 axioms for the $\blacksquare _i$’s ensure that $\equiv _i$ is an equivalence relation; $\blacksquare _1\blacksquare _2\phi \leftrightarrow \blacksquare _2\blacksquare _1\phi$ ensures that (O3’) is satisfied; finally, the axioms $\blacksquare _i\phi \rightarrow \square _i\phi$ ensure (O1).

Therefore $(X,R_{1,2},\equiv _{1,2})$ is a semistructure and any consistent formula $\phi$ can be satisfied in it.

Proof of Lemma 3. We simply show the existence of a matrix enumeration $f:X\times X\rightarrow X$ whenever X is infinite; we leave further details to the reader. Let $\{X_1, X_2\}$ be a partition of X into two sets which are equipotent to X itself (note that the existence of such partition requires the Axiom of Choice for uncountable cardinalities [16]). Let $f_1:X_1\rightarrow X$ and $f_2:X_2\rightarrow X$ be two surjections. The map

$$f(x,y) = {\left\{ \begin{array}{ll} f_i(x) &{} \text { if } x,y\in X_i \\ f_j(y) &{} \text { if } x\in X_i, y\in X_j, i\ne j \end{array}\right. }$$

is the desired enumeration.

Proof of Proposition 6. Soundness is routine. For completeness, given a formula $\phi \notin Log_\dashv$, it suffices to use Theorem 2 to find a standard orthogonal structure $(W,R_{1,2},\equiv _{1,2})$ that refutes $\phi$, construct the indexed frame $(W/_{\equiv _2}\times W/_{\equiv _1}, \mathsf {R}_1, \mathsf {R}_2)$ isomorphic to $(W,R_1,R_2)$ via Proposition 1 and note that the equivalence relation $([w]_2,[v]_1) \cong _i ([w']_2,[v']_1)$ iff $x_{wv}\equiv _i x_{w'v'}$ relates two pairs if and only if their j-th coordinate coincides, for $j\ne i$.

Proof (sketch) of Proposition 7. This involves a rather standard filtration argument. (See [4, Chapter 2] for details on this technique).

Given a consistent formula $\phi$, we let $(W,R_{1,2},\equiv _{1,2})$ be a semistructure satisfying $\phi$ at a point $w_0$, and $\varGamma$ be a finite set of formulas closed under subformulas such that $\phi \in \varGamma$, and we define an equivalence relation $w\sim _\varGamma v$ iff for all $\psi \in \varGamma$, ($w\models \psi$ iff $v\models \psi$). We define relations in the quotient set $W/_{\sim _\varGamma }$ as follows: for $i=1,2$,

• $[w]_\varGamma \equiv '_i [v]_\varGamma$ iff, for all $\blacksquare _i\psi \in \varGamma$, ($w\models \blacksquare _i\psi$ iff $v\models \blacksquare _i\psi$), and

• $[w]_\varGamma R'_i [v]_\varGamma$ iff $[w]_\varGamma \equiv '_i [v]_\varGamma$ and for all $\square _i\psi \in \varGamma$ ($w\models \square _i\psi$ implies $v\models \psi$).

We leave it to the reader to check that the resulting tuple is a semistructure and a filtration and therefore that $[w_0]_\varGamma \models \phi$. We can then use Proposition 5 and Lemma 2 to obtain an indexed frame satisfying $\phi$.

Proof of Proposition 9. For the left-to-right direction, given a subset space frame we consider the relations $(x,U) R_K (y,V)$ iff $U=V$, $(x,U) R_\square (y,V)$ iff $x=y$ and $U\supseteq V$, and $(x,U)\equiv _\square (y,V)$ iff $x=y$. We note that $(R_K\circ \equiv _\square )(x,U) = \{ (x',U')\in \mathcal {O}_X: x'\in U \}$, and we leave it to the reader to check that this satisfies all the properties in Proposition 9.

Let us now consider a frame with these properties. We let $[.]_\square$ and $[.]_K$ denote the equivalence classes of $\equiv _\square$ and $R_K$. Let us define the subset space

Note that $[w]_\square \in U_v$ if and only if $[w]_\square \cap [v]_K \ne \varnothing$.

By (O2), an intersection $[w]_\square \cap [v]_K$ of two equivalence classes is at most a singleton. Let us map and element $([w]_\square , U_v)$ in the graph of $(X,\mathcal {O})$ to the unique element in $[w]_\square \cap [v]_K$. This is a bijection whose inverse maps each $w\in W$ to $([w]_\square , U_w)$. We define relations $\equiv _K$ and $\ge _\square$ on this graph as in Example 2 and, to show that this map is an isomorphism, it suffices to show that

We start with the second item. From left to right, if $w R_\square v$, then $[w]_\square = [v]_\square$ by (O1), and let us see that $U_w \supseteq U_v$. If $[y]_\square \in U_v$, then there is a unique element $x\in [y]_\square \cap [v]_K$. But since $wR_\square v R_K x$, it follows by (SS3) that there must exist some $x'$ such that $wR_K x'R_\square x$. Since $x'\equiv _\square x$, by (O1), and $x\equiv _\square y$, it follows that $x'\in [w]_K \cap [y]_\square$, and thus $[y]_\square \in U_w$. From right to left, it suffices to see that $U_w\supseteq U_v$ and $w\equiv _\square v$ implies $wR_\square v$. But this follows directly from (SS4), noting that $U_w \supseteq U_v$ implies $[R_k \circ \equiv _\square ](w) \supseteq [R_k \circ \equiv _\square ](v)$.

For the first item it suffices to show that $wR_K v$ iff $U_w = U_v$. The left-to-right direction is immediate from the definition of $U_w$, whereas the right-to-left direction follows from (SS5).