Simpler completeness proofs for modal logics with intersection

Intersection plays a role in several areas of modal logic, including epistemic logics with distributed knowledge [11, 7], propositional dynamic logic with intersection of programs [9], description logics with concept intersection [2, 3], and coalition logic [1]. It is well-known that intersection is not modally definable and that standard logics with intersection are not canonical (cf., e.g., [10]).

A method for proving completeness was introduced by [8, 10, 7, 11] for various (static) epistemic logics with distributed knowledge, and later explicated and extended in [13, 14, 12] as the unraveling-folding method which is applicable to various static or dynamic epistemic S5 logics with distributed knowledge with or without common knowledge.

Let us take a closer look at this technique for epistemic logic with distributed knowledge (S5D). It is known that the canonical S5 model built in the standard way is not a model for the classical axiomatization for this logic. This is because the accessibility relation $R_{G}$ (where $G$ is a set) that is (implicitly) used to interpret the interesection (distributed knowledge) modality is not necessarily the intersection of individual accessibility relations $R_{a}$ ($a\in G$). In the canonical S5 model we can ensure that ${R_{G}}\subseteq\bigcap_{a\in G}{R_{a}}$, but not that ${R_{G}}\supseteq\bigcap_{a\in G}{R_{a}}$.

The unraveling-folding method is carried out in the following way. A pre-model is a standard S5 model where $R_{G}$ is treated as a primitive relation for each group $G$. A pseudo model is a pre-model satisfying the following two constraints

1. 1.

   ${R_{\{a\}}}={R_{a}}$ for every agent $a$, and

2. 2.

   ${R_{G}}\subseteq{\bigcap_{a\in G}{R_{a}}}$ for every agent $a$ and group $G$

An S5D model is then a pseudo model that satisfies also a third constraint:

1. 3.

   ${R_{G}}\supseteq{\bigcap_{a\in G}{R_{a}}}$ for every agent $a$ and group $G$

A canonical pseudo model can be truth-preservingly translated to a treelike pre-model using an unraveling technique, and then folded to an S5D model while also preserving the truth of all formulas (for details of the two processes see [13]). Completeness is achieved by first building a canonical pseudo model for a given consistent set $\Phi$ of formulas, and then having it translated to an S5D model for $\Phi$ using the unraveling-folding method.

There are many subtleties not mentioned in this simplified overview, which in particular makes the method cumbersome to adapt to extensions of basic epistemic logic or to non-S5 based logics.

In this paper we demonstrate a simpler way to prove completeness for modal logics with intersection. Since we know that a treelike model typically works for such logics, the idea is to build a treelike model directly for a given consistent set of formulas. We call such a model a standard model. This eliminates having to deal with the details of the unraveling and folding processes, and dramatically simplifies the proofs.

We illustrate the technique by building the standard model for each of the modal logics, K, D, T, B, S4 and S5, extended with intersection. We furthermore demonstrate that the method is useful by showing that it is compatible with finitary methods based on Fischer-Ladner-style closures, and introduce finitary standard models for the mentioned logics further extended with the transitive closure of the union, using in, e.g., PDL and epistemic logic, as well. Some of these completeness results have been stated in the literature before, often without proof, some of them not. For example, to the best of our knowledge, no completeness results have been reported for D or B extended with intersection, and even less can be found for logics with both intersection and the transitive closure of union.

The rest of the paper is structured as follows. In the next section we introduce basic definitions and conventions. We study some modal logics with (only) intersection in Section 3, introduce an axiomatization for each of them and show its completeness, and then study the logics extended further with transitive closure of union in Section 4. We conclude in Section 5.

In this paper we study modal logics over multi-modal languages with countably many standard unary modal operators: $\Box_{0}$, $\Box_{1}$, $\Box_{2}$, etc. On top of these we focus on two types of modal operators, each indexed by a finite nonempty set $I$ of natural numbers:

• •

  Intersection modalities, denoted $\cap_{I}$;

• •

  Union⁺ modalities, denoted $\uplus_{I}$.

We mention some applications of these modalities below.

The languages are parameterized by a countably infinite set prop of propositional variables, and an at-most countable set $\mathcal{I}$ of primitive types. A finite non-empty subset $I\subseteq\mathcal{I}$ is called an index. We are interested in the following languages.

A Kripke model $M$ (over prop and $\mathcal{I}$) is a triple $(S,R,V)$, where $S$ is a nonempty set of states, $R:\mathcal{I}\to\wp(S\times S)$ assigns to every modality $\Box_{i}$ a binary relation $R_{i}$ on $S$, and $V:\textsc{prop}\to S$ is a valuation which associates with every propositional variable a set of states where it is true.

Thus, the intersection modalities are interpreted by taking the intersection, and the union⁺ modalities by taking the transitive closure of the union. We use “union⁺ modalities” as a short name to avoid the more awkward “transitive closure of union modalities”.

Given a formula $\varphi$ and a class $\mathscr{C}$ of models, we say $\varphi$ is valid in $\mathscr{C}$ iff $\varphi$ is valid in all models of $\mathscr{C}$. We usually do not choose a class of models arbitrarily, but are rather interested in those based on a certain set of conditions over the binary relations in a model. Such conditions are often called frame conditions. In this paper we are going to focus on some of the most well known frame conditions (see, e.g., [5]). These conditions are seriality, reflexivity, symmetry, transitivity and Euclidicity. It is well known that these frame conditions are characterized by the formulas D ($\Box_{i}\varphi\rightarrow\neg\Box_{i}\neg\varphi$), T ($\Box_{i}\varphi\rightarrow\varphi$), B ($\neg\varphi\rightarrow\Box_{i}\neg\Box_{i}\varphi$), 4 ($\Box_{i}\varphi\rightarrow\Box_{i}\Box_{i}\varphi$) and 5 ($\neg\Box_{i}\varphi\rightarrow\Box_{i}\neg\Box_{i}\varphi$), respectively. With respect to different combinations of these frame conditions, normal modal logics K, D (a.k.a. KD), T (a.k.a. KT), B (a.k.a. KTB), S4 (a.k.a., KT4) and S5 (a.k.a. KT5) based on the language $\mathcal{L}$ are well studied in the literature. We shall refer an “S5 model” to a Kripke model in which the binary relation is an equivalence relation, and likewise for a D, T, B or S4 model.

In this paper we will focus on the counterpart logics over the languages $\mathcal{L}^{\cap}$ and $\mathcal{L}^{\cap\uplus}$, and they will be named in a comprehensive way as follows:

There are well known applications of these logics, for example are $\text{S5}^{\cap}$ and $\text{S5}^{\cap\uplus}$ (under the restriction that $\mathcal{I}$ is finite) well known as S5D and S5CD respectively in the area of epistemic logic. The logics $\text{K}^{\cap}$ and $\text{S4}^{\cap}$ are known as $\mathcal{ALC}(\cap)$ (i.e., $\mathcal{ALC}$ with role intersection) and $\mathcal{S}(\cap)$ (where $\mathcal{S}$ is $\mathcal{ALC}$ with role transitivity) respectively in the area of description logic [2, 3].²²2The subscript $i$ of a unary modal operator $\Box_{i}$ typically stands for an agent in epistemic logic or a role in description logic. In epistemic logic, a finite number of agents is assumed, and the intersection modality (i.e., a distributed knowledge operator) is an arbitrary intersection over a finite domain. In description logic, the number of roles are typically unbounded, but the intersection is binary, which is in effect equivalent to finite intersection. The logic $\text{K}^{\cap\uplus}$ is close to propositional dynamic logic with intersection (IPDL) [9] or the description logic $\mathcal{ALC(\cap,\cup,*)}$, and similarly, $\text{S4}^{\cap\uplus}$ close to $\mathcal{S(\cap,\cup,*)}$.³³3There are two major differences however. First, the Kleene star in both logics are the reflexive-transitive closure, and we consider the transitive closure which is denoted by a “$+$” in the symbol $\uplus$. Second, $\uplus_{I}$ is a compound modality (union and then take the transitive closure), while in those logics the Kleene star is separated from the union, and as a result, the Kleene star applies to the intersection as well, which we do not consider here.

The minimal logic K can be axiomatized by the system K composed of the following axiom (schemes) and rules (where $\varphi,\psi\in\mathcal{L}$ and $i\in\mathcal{I}$):

• (PC)

  all instances of all propositional tautologies

• (MP)

  from $(\varphi\rightarrow\psi)$ and $\varphi$ infer $\psi$

• (K)

  $\Box_{i}(\varphi\rightarrow\psi)\rightarrow(\Box_{i}\varphi\rightarrow\Box_{i}\psi)$

• (N)

  from $\varphi$ infer $\Box_{i}\varphi$

Axiomatizations for D, T, B , S4 and S5, which are named D, T, B, S4 and S5 respectively, can be obtained by adding characterization axioms to K. In more detail, $\textbf{D}=\textbf{K}\oplus\text{D}$, $\textbf{T}=\textbf{K}\oplus\text{T}$, $\textbf{B}=\textbf{T}\oplus\text{B}$, $\textbf{S4}=\textbf{T}\oplus\text{4}$ and $\textbf{S5}=\textbf{T}\oplus\text{5}$, where the symbol $\oplus$ means combining the axioms and rules of the two parts. Details can be found in standard modal logic textbooks (see, e.g., [5, 4]).

A logic extended with the intersection modality is typically axiomatized by adding axioms and rules to the corresponding logic without intersection. The axioms and rules to be added are in total called the characterization of intersection, and depends on which logic we are dealing with. Similarly we can define the characterization of the transitive closure of union, which can be made independent to the concrete logic (will be made clear in Section 4).

Characterizations of intersection and transitive closure of union can be found in the literature for some of the logics, including $\text{K}^{\cap}$, $\text{T}^{\cap}$, $\text{S4}^{\cap}$, $\text{S5}^{\cap}$ and $\text{S5}^{\cap\uplus}$ in epistemic logic (see [7, 11, 12]). In particular, for the base logic S5, the characterizations are Int(S5) and Un(S5), respectively:

In this section we study the logics over the language $\mathcal{L}^{\cap}$, namely, $\text{K}^{\cap}$, $\text{D}^{\cap}$, $\text{T}^{\cap}$, $\text{B}^{\cap}$, $\text{S4}^{\cap}$ and $\text{S5}^{\cap}$, which means that in this section a “formula” stands for a formula of $\mathcal{L}^{\cap}$, and a “logic” without further explanation refers to one of the six. We shall provide a general method for proving completeness in these logics.

The axiomatization L we will provide for a logic L is an extension of the axiomatization for the corresponding logic without intersection, with the characterization of intersection. The characterization of intersection is dependent on the frame conditions. For a given class of models, the characterization of intersection is listed below:

• •

  $\textbf{Int({K})}=\textbf{Int({D})}=\{\text{K}\cap,\text{N}\cap,\cap 1,\cap 2\}$

• •

  $\textbf{Int({T})}=\{\text{K}\cap,\text{T}\cap,\text{N}\cap,\cap 1,\cap 2\}$

• •

  $\textbf{Int({B})}=\{\text{K}\cap,\text{T}\cap,\text{B}\cap,\text{N}\cap,\cap 1,\cap 2\}$

• •

  $\textbf{Int({S4})}=\{\text{K}\cap,\text{T}\cap,4\cap,\text{N}\cap,\cap 1,\cap 2\}$

• •

  $\textbf{Int({S5})}=\{\text{K}\cap,\text{T}\cap,5\cap,\text{N}\cap,\cap 1,\cap 2\}$

where Int(K) is the characterization of intersection for the class of all models, Int(D) for the class of all D models, Int(T) for the class of all T models, and so on. We stress that D$\cap$ is not included in Int(D): it is in fact invalid in $\text{D}^{\cap}$.

By adding the characterization of intersection to the axiomatization of a logic, we get an axiomatization for the corresponding logic over $\mathcal{L}^{\cap}$. To be precise, we list the axiomatizations as follows:

It is not hard to verify that all the above axiomatizations are sound in their corresponding logic, respectively.

Some of the above axiomatizations, in particular, ${\textbf{K}^{\cap}}$, ${\textbf{T}^{\cap}}$, ${\textbf{S4}^{\cap}}$ and ${\textbf{S5}^{\cap}}$, are given in [7]. An outline of proof of completeness is also found there, without details. Detailed proofs can be found for certain special cases, such as the ${\textbf{S5}^{\cap}}$ with only a single intersection modality for the set of all agents (which is assumed to be finite) [6]. A general and detailed proof based on this technique can be found in [13]. The proof goes through an unraveling-folding procedure, mentioned already in the introduction. Due to the subtleties in the unraveling and folding processes, it is diffucult to apply this technique directly to new logics, as definitions may differ already from the beginning (for example, the definition of a path is already different) all the way to the very end of the procedure. This in general becomes an obstacle for developers of new logics with the intersection modality.

We introduce a simpler method for proving completeness, that can easily be adapted to a range of different logics. This is a relatively simple variant of the standard canonical model method. For each of the logics L mentioned above, with corresponding axiomatization L, we shall show that L is a complete axiomatization of L, which is equivalent to finding an L model for every L-consistent set of formulas. The model we are going to build is called a standard model.

Let $\text{MCS}^{\textbf{L}}$ be the set of all maximal L-consistent sets of $\mathcal{L}^{\cap}$-formulas.⁴⁴4We refer to a modal logic textbook, say [4], for a definition of a (maximal) consistent set of formulas. Given L, given an index $I$, we shall write $\rhd_{I}$ to stand for a binary relation on $\text{MCS}^{\textbf{L}}$, such that $\Phi\rhd_{I}\Psi$ iff for all $\varphi$, $\cap_{I}\varphi\in\Phi$ implies $\varphi\in\Psi$. This type of relations is typically used in the definition of a canonical model (as found in modal textbooks), and are sometimes called canonical relations. We easily get the following proposition.

The standard models we will define for these logics are a bit different from the canonical model for a standard modal logic. As mentioned existing proofs are based on transforming the canonical model to a treelike model. We will construct a treelike model directly: in the standard model for a logic L, a state will be a canonical path for L. However, the binary relations in a standard model is dependent on the concrete logic we focus on. We now first define these binary relations and then introduce the definition of a standard model.

In this section we study the logics with both the intersection and union⁺ modalities. The language is set to be $\mathcal{L}^{\cap\uplus}$ in this section, and by a “logic” without further explanation we mean one of $\text{K}^{\cap\uplus}$, $\text{D}^{\cap\uplus}$, $\text{T}^{\cap\uplus}$, $\text{B}^{\cap\uplus}$, $\text{S4}^{\cap\uplus}$ or $\text{S5}^{\cap\uplus}$.

Compared with the characterization of intersection, that of transitive closure of union is better behaved:

These axioms are not new, as e.g., is found in [7], although as far as we know they have not been studied as additions to D and B in the literature. For simplicity we write Un this set of axioms. Additional axioms for union⁺ corresponding to specific frame conditions can be derived in specific logic systems. For instance, D$\uplus$ is a theorem of $\textbf{D}\oplus\textbf{Un}$.

By adding to the axiomatization of a logic over $\mathcal{L}^{\cap}$ the characterization of union⁺, we get a sound axiomatization for the corresponding logic over $\mathcal{L}^{\cap\uplus}$. To make it precise, we list the axiomatizations as follows:

In this section we will make extensive references to the names of logics and axiomatizations, and for simplicity we shall call a tuple $\sigma=(\text{L},\textbf{L},\alpha,\iota)$ a signature, when L is one of the logics $\text{K}^{\cap\uplus}$, $\text{D}^{\cap\uplus}$, $\text{T}^{\cap\uplus}$, $\text{B}^{\cap\uplus}$, $\text{S4}^{\cap\uplus}$ and $\text{S5}^{\cap\uplus}$, L is the corresponding axiomatization for L, $\alpha$ is a formula of $\mathcal{L}^{\cap\uplus}$, and $\iota$ is an index such that every index occurring in $\alpha$ is a subset of $\iota$. Moreover, we write $\sigma(\text{K})$ when the L in $\sigma$ is K, and similarly for $\sigma(\text{D})$, $\sigma(\text{T})$, $\sigma(\text{B})$, $\sigma(\text{S4})$ and $\sigma(\text{S5})$.

It is not hard to verify that $cl(\sigma)$ is finite and nonempty for any signature $\sigma$. Given $\sigma=(\text{L},\textbf{L},\alpha,\iota)$, a set of formulas is said to be maximal L-consistent in $cl(\sigma)$, if it is (i) a subset of $cl(\sigma)$, (ii) L-consistent and (iii) maximal in $cl(\sigma)$ (i.e., any proper superset which is a subset of $cl(\sigma)$ is inconsistent). We write $\text{MCS}^{\sigma}$ for the set of all maximal L-consistent sets of formulas in $cl(\sigma)$.

Now we extend the canonical relations to the finitary case. Given a signature $\sigma$ and an index $I$, we may try to define a canonical relation $\rhd_{I}$ to be a binary relation on $\text{MCS}^{\sigma}$, such that $\Phi\rhd_{I}\Psi$ iff for all $\varphi$, $\cap_{I}\varphi\in\Phi$ implies $\varphi\in\Psi$, like we did for the logics over $\mathcal{L}^{\cap}$. But there are subtleties regarding the closure. For example, transitivity may be lost in $\text{S4}^{\cap\uplus}$, if $\cap_{I}\varphi\in\Phi$ but ${\cap_{I}}{\cap_{I}}\varphi\notin\Phi$ in case the latter is not included in the closure. We introduce the formal definition below.

Note that for all the logics, from $\Phi\rhd_{I}\Psi$ we still get that $\cap_{I}\varphi\in\Phi$ implies $\varphi\in\Psi$, as the criteria above are at least not weaker. We can get the following proposition that is similar to Proposition 1.