Weakly Aggregative Modal Logic: Characterization and Interpolation

Abstract

Weakly Aggregative Modal Logic ($\textsf {WAML}$) is a collection of disguised polyadic modal logics with n-ary modalities whose arguments are all the same. $\textsf {WAML}$ has some interesting applications on epistemic logic and logic of games, so we study some basic model theoretical aspects of $\textsf {WAML}$ in this paper. Specifically, we give a van Benthem-Rosen characterization theorem of $\textsf {WAML}$ based on an intuitive notion of bisimulation and show that each basic $\textsf {WAML}$ system $\mathbb {K}_n$ lacks Craig Interpolation.

The main work of the first author was completed during his Ph.D. at Peking University.

1 Introduction

You are invited to a dinner party for married couples after a logic conference in China. The host tells you the following facts:

• at least one person of each couple is a logician and

• at least one person of each couple is Chinese.

Given these two facts, can you infer that at least one person of each couple is a Chinese logician? The answer is clearly negative, since there might be a couple consisting of a foreign logician and a Chinese spouse who is not a logician.

Now, suppose that the host adds another fact:

• at least one person of each couple likes spicy food.

What do you know now? Actually, you can infer that for each couple, one of the two people must be either:

• a Chinese logician, or

• a logician who likes spicy food, or

• a Chinese who likes spicy food.

This can be verified by the Pigeonhole Principle: for each couple, there is a logician, a Chinese, and a fan for spicy food, thus there must be at least one person of the couple who has two of those three properties. This can clearly be generalized to n-tuples of things w.r.t. $n+1$ properties.

Now, going back to logic, if we express “at least one person of each couple has property $\varphi$” by $\Box \varphi$ then the above reasoning shows that the following is not valid:

$$ \mathtt {C}: \Box p\wedge \Box q\rightarrow \Box (p\wedge q).$$

On the other hand, the following should be valid:

$$\mathtt {K}_2: \Box p\wedge \Box q\wedge \Box r\rightarrow \Box ((p\wedge q)\vee (p\wedge r)\vee (q\wedge r)).$$

In general, if $\Box \varphi$ expresses “at least one thing of each (relevant) n-tuple of things has property $\varphi$” then the following is intuitively valid:

$$\mathtt {K}_n: \Box p_{0}\wedge \cdots \wedge \Box p_{n}\rightarrow \Box \bigvee _{(0\le i<j\le n)}(p_{i}\wedge p_{j}).$$

Note that $\mathtt {K}_1$ is just $\mathtt {C}$, which is a theorem in the weakest normal modal logic $\mathbb {K}$. $\mathtt {C}$ is sometimes called the Closure of Conjunction [11], or Aggregative Axiom [20], or Adjunctive Axiom [6]. Clearly, when $n\ge 2$, $\mathtt {K}_n$ are weaker versions of $\mathtt {C}$. The resulting logics departing from the basic normal modal logics by using weaker aggregative axioms $\mathtt {K}_n$ instead of $\mathtt {C}$ are called Weakly Aggregative Modal Logics (WAML) [32]. There are various readings of $\Box p$ under which it is intuitive to reject $\mathtt {C}$ besides the one we mentioned in our motivating party story. For example, if we read $\Box p$ as “p is obligatory” as in deontic logic, then $\mathtt {C}$ is not that reasonable since one may easily face two conflicting obligations without having any single contradictory obligation [32]. As another example, in epistemic logic of knowing how [16, 35], if $\Box p$ expresses “knowing how to achieve p”, then it is reasonable to make $\mathtt {C}$ invalid: you may know how to open a door and know how to close the door, but you can never know how to make the door both open and closed.

Coming back to our setting where $\mathtt {K}_n$ are valid, the readings of $\Box \varphi$ in those axioms may sound complicated, but they are actually grounded in a more general picture of Polyadic Modal Logics (${{\textsf {\textit{PML}}}}$) which studies the logics with n-ary modalities. Polyadic modalities arose naturally in the literature of philosophical logic, particularly for the binary ones, such as the until modality in temporal logic [21], instantial operators in games-related neighborhood modal logics [34], relativized knowledge operators in epistemic logic [9, 36], Routley and Meyer’s ternary accessibility relation semantics in relevance logics [29, 30], and the conditional operators in the logics of conditionals [8]. Following the notation in [10], we use $\nabla$ for the n-ary generalization of the $\Box$ modality when $n>1$.¹ The semantics of $\nabla (\varphi _1, \dots , \varphi _n)$ is based on Kripke models with $n+1$-ary relations R [10, 20]:

$\nabla (\varphi _1, \dots , \varphi _n)$ holds at s iff for all $s_1, ..., s_n$ such that $Rss_1\dots s_n$ there exists some $i\in [1,n]$ such that $\varphi _i$ holds at $s_i$.

We will call $\nabla$ the normal polyadic modal operator and one should also notice that, by contrast, in those examples with unary operators we just mentioned above, the unary operators are not normal.² However, the reading we mentioned for $\Box \varphi$ in our motivating story is simply the semantics for $\nabla (\varphi _1, \dots , \varphi _n)$ where $\varphi _1=\dots =\varphi _n$: notice how they share the same $\forall \exists$ quantifier alternation pattern. Thus, the formulas $\Box \varphi$ under the new reading can be viewed as special cases of the modal formulas in polyadic modal languages. Due to the fact that the arguments are the same in $\nabla (\varphi , \dots , \varphi )$, we can also call the $\Box$ the diagonal n-modalities.³ In this light, we may call the new semantics for $\Box \varphi$ the diagonal n-semantics (given frames with $n+1$-ary relations).

Diagonal modalities also arise in other settings in disguise. For example, in epistemic logic of knowing value [18], the formula $\mathsf {Kv}(\varphi , c)$ says that the agent knows the value of c given $\varphi$, which semantically amounts to that for all the pairs of $\varphi$ worlds that the agent cannot distinguish from the actual worlds, c has the same value. In other words, in every pair of the indistinguishable worlds where c has different values, there is a $\lnot \varphi$ world, which can be expressed by $\Box ^c \lnot \varphi$ with the diagonal 2-modality ($\Box ^c$) based on intuitive ternary relations (see details in [18]). As another example in epistemic logic, [13] proposed a local reasoning operator based on models where each agent on each world may have different frames of mind (sets of indistinguishable worlds). That one agent believes $\varphi$ then means that in one of his current frame of mind, $\varphi$ is true everywhere. This belief modality can also be viewed as the dual of a diagonal 2-modality (noticing the quantifier alternation $\exists \forall$ in the informal semantics).

Yet another important reason to study diagonal modalities comes from the connection with paraconsistent reasoning established by Schotch and Jennings [32]. In a nutshell, [32] introduces a notion of n-forcing where a set of formulas $\varGamma$ n-forces $\varphi$ ($\varGamma \vdash _n\varphi$) if for each n-partition of $\varGamma$ there is a cell $\varDelta$ such that $\varphi$ follows from $\varDelta$ classically w.r.t. some given logic ($\varGamma \vdash \varphi$). This leads to a notion of n-coherence relaxing the notion of consistency: $\varGamma \nvdash _n \bot$ ($\varGamma$ is n-coherent) iff there exists an n-partition of $\varGamma$ such that all the cells are classically consistent. These notions led the authors of [32] to the discovery of the diagonal semantics for $\Box$ based on frames with $n+1$-ary relations, by requiring $\Box (u)=\{\varphi \mid u\vDash \Box \varphi \}$ to be an n-theory based on the closure over n-forcing, under some other minor conditions. Since the derivation relation of basic normal modal logic $\mathbb {K}$ can be characterized by a proof system extending the propositional one with the rule $\varGamma \vdash \varphi /\Box (\varGamma )\vdash \Box \varphi$ where $\Box (\varGamma )=\{\Box \varphi \mid \varphi \in \varGamma \}$, it is interesting to ask whether adding $\varGamma \vdash _{n} \varphi /\Box (\varGamma )\vdash _n \Box \varphi$ characterizes exactly the valid consequences for modal logic under the diagonal semantics based on frames with n-ary relations. Apostoli and Brown answered this question positively in [5] 15 years later, and they characterize $\vdash _n$ by a Gentzen-style sequent calculus based on the compactness of $\vdash _n$ proved by using a compact result for coloring hypergraphs.⁴ Moreover, they show that the WAML proof systems with $\mathtt {K}_n$ are also complete w.r.t. the class of all frames with $n+1$-ary relations respectively. The latter proof is then simplified in [26] without using the graph theoretical compactness result. This completeness result is further generalized to the extensions of WAML with extra one-degree axioms in [4]. The computational complexity issues of such logics are discussed in [1], and this concludes our relatively long introduction to WAML, which might not be that well-known to many modal logicians.

In this paper, we continue the line of work on WAML by looking at the model theoretical aspects. In particular, we mainly focus on the following two questions:

• How to characterize the expressive power of WAML structurally within first-order logic over (finite) pointed models?

• Whether WAML has Craig Interpolation?

For the first question, we propose a notion of bisimulation to characterize WAML within the corresponding first-order logic. The answer for the second question is negative, and we will provide counterexamples in this paper to show WAML (in particular, each $\mathbb {K}_n$ for $n \ge 2$) does not have Craig Interpolation.

In the rest of the paper, we lay out the basics of WAML in Sect. 2, prove the characterization theorem based on a bisimulation notion in Sect. 3, and give counterexamples for the interpolation theorem in Sect. 4 before concluding with future work in Sect. 5.

2 Preliminaries

In this section we review some basic definitions and results in the literature.

2.1 Weakly Aggregative Modal Logic

The language for $\textsf {WAML}$ is the same as the language for basic (monadic) modal logic.

Definition 1

Given a set of propositional letters $\varPhi$ and a single unary modality $\Box$, the language of $\textsf {WAML}$ is defined by:

$$\varphi :=p\mid \lnot \varphi \mid (\varphi \wedge \varphi )\mid \Box \varphi $$

where $p\in \varPhi$. We define $\top$, $\varphi \vee \psi$, $\varphi \rightarrow \psi$, and $\Diamond \varphi$ as usual.

However, given n, $\textsf {WAML}$ can be viewed as a fragment of polyadic modal logic with a n-ary modality, since $\Box \varphi$ is essentially $\nabla (\varphi , \ldots , \varphi )$. Notation: in the sequel, we use $\textsf {WAML}^n$, where $n>1$, to denote the logical framework with the semantics based on n-models defined below:

Definition 2

(n-Semantics). An n-frame is a pair $\langle W, R \rangle$ where W is an nonempty set and R is an $n+1$-ary relation over W. An n-model $\mathcal {M}$ is a pair $\langle \mathcal {F}, V \rangle$ where the valuation function V assigns each $w\in W$ a subset of $\varPhi$. We say $\mathcal {M}$ is an image-finite model if there are only finitely many n-ary successors of each point. The semantics for $\Box \varphi$ (and $\Diamond \varphi$) is defined by:

$$\begin{array}{|lll|} \hline \mathcal {M},w\,\models \,\Box \varphi &{} \text {iff} &{} \text { for all } v_{1},\ldots v_{n}\in W \text { with } Rwv_{1}\ldots ,v_{n}, \mathcal {M},v_{i}\,\models \,\varphi \text { for some } i\le n.\\ \mathcal {M},w\,\models \,\Diamond \varphi &{} \text {iff} &{} \text { there are } v_{1},\ldots v_{n}\in W \text { st. } Rwv_{1}\ldots ,v_{n} \text { and } \mathcal {M},v_{i}\,\models \,\varphi \text { for all } i\le n.\\ \hline \end{array} $$

According to the above semantics, it is not hard to see that the aggregation axiom $\Box \varphi \wedge \Box \psi \rightarrow \Box (\varphi \wedge \psi )$ in basic normal modal logic is not valid on n-frames for any $n > 1$.

[32] proposed the following proof systems $\mathbb {K}_n$ for each n.

Definition 3

(Weakly aggregative modal logic). The logic $\mathbb {K}_n$ is a modal logic including propositional tautologies, the axiom $\mathtt {K}_n$ and closed under the rules⁵ $\mathtt {N}$ and $\mathtt {RM}$:

It is clear that $\mathtt {K}_1$ is just the aggregation axiom $\mathtt {C}$ and thus $\mathbb {K}_1$ is just the normal monadic modal logic $\mathbb {K}$. It can also be shown easily that for each $n > m$, $\mathbb {K}_n$ is strictly weaker than $\mathbb {K}_m$. In fact, many familiar equivalences in normal modal logics, like the equivalence between $\Diamond \top$ and $\Box p \rightarrow \Diamond p$, no longer hold in $\mathbb {K}_n$ for $n > 1$. Semantically speaking, while $\Box p \rightarrow \Diamond p$’s validity corresponds to seriality on 1-frames (usual Kripke frames), its correspondence on 2-frames is not even elementary ($\Diamond \top$ still corresponds to each point having at least a successor tuple).

After being open for more than a decade, the completeness for $\mathbb {K}_{n}$ over n-models was finally proved in [5] and [4], by reducing to the n-forcing relation proposed in [32]. In [26], a more direct completeness proof is given using some non-trivial combinatorial analysis to derive a crucial theorem of $\mathbb {K}_n$.

3 Characterization via Bisimulation

In this section, we introduce a notion of bisimulation for $\textsf {WAML}$ and prove the van Benthem-Rosen Characteristic Theorem for WAML.⁶

Definition 4

($wa^n$-bisimulation). Let $\mathcal {M}=(W,R,V)$ and $\mathcal {M}'=(W',R',V')$ be two n-models. A non-empty binary relation $Z\subseteq W\times W'$ is called a $wa^n$-bisimulation between $\mathcal {M}$ and $\mathcal {M}'$ if the following conditions are satisfied:

• inv If $wZw'$, then w and $w'$ satisfy the same propositional letters (in $\varPhi$).

• forth If $wZw'$ and $Rwv_{1},\ldots ,v_{n}$ then there are $v_{1}',\ldots ,v_{n}'$ in $W'$ s.t. $R'w'v_{1}',\ldots ,v_{n}'$ and for each $v'_j$ there is a $v_i$ such that $v_i Z v'_j$ where $1\le i,j\le n$.

• back If $wZw'$ and $R'w'v_{1}',\ldots ,v_{n}'$ then there are $v_{1},\ldots ,v_{n}$ in W s.t. $Rwv_{1},\ldots ,v_{n}$ and for each $v_i$ there is a $v'_j$ such that $v_i Z v'_j$ where $1\le i,j\le n$.

When Z is a bisimulation linking two states w in $\mathcal {M}$ and $w'$ in $\mathcal {M}'$ we say that w and $w'$ are $\varPhi$-$wa^n$-bisimilar .

Remark 1

Observe the two subtleties in the above definition: i, j in the forth and back conditions are not necessarily the same, thus we may not have an aligned correspondence of each $v_i$ and $v_i'$; in the second part of the forth condition, we require each $v_j'$ to have a corresponding $v_i$, not the other way around. Similar in the back condition. This reflects the quantifier alternation in the semantics of $\Box$ in $\textsf {WAML}^n$.

Example 1

Consider the following two 2-models where $\{\langle w,w_1,w_2 \rangle ,$ $\langle w,w_2,w_3 \rangle \}$ is the ternary relation in the left model, and $\{\langle v,v_1,v_2 \rangle \}$ is the ternary relation in the right model.

$Z=\{\langle w,v \rangle , \langle w_1, v_1 \rangle , \langle w_2, v_2 \rangle , \langle w_2, v_1 \rangle \}$ is a $wa^2$-bisimulation. A polyadic modal formula $\lnot \nabla \lnot (p, \lnot p)$, not expressible in $\textsf {WAML}^2$, can distinguish w and v.

It is easy to verify that is indeed an equivalence relation and we show $\textsf {WAML}^n$ is invariant under it.

Proposition 1

Let $\mathcal {M}=(W,R,V)$ and $\mathcal {M}'=(W',R',V')$ be two n-models. Then for every $w\in W$ and $w'\in W'$, implies $w\equiv _{\textsf {WAML}^n} w'$. In words, $\textsf {WAML}^n$ formulas are invariant under $wa^n$-bisimulation.

Proof

We consider only the modality case. Suppose that and $w\,\models \,\Diamond \varphi$. Then there are $v_{1},\ldots ,v_{n}$ s.t. $Rwv_{1},\ldots ,v_{n}$, and each $v_{i}\,\models \,\varphi$. By the forth condition, there are $v_{1}',\ldots ,v_{n}'$ in $W'$ s.t. $Rw'v_{1}',\ldots ,v_{n}'$ and for each $v'_j$ there is a $v_i$ such that $v_i Z v'_j$. From the I.H. we have each $v_{i}'\,\models \,\varphi$. As a result, $w'\,\models \,\Diamond \varphi$. For the converse direction just use the back condition.

Theorem 1

(Hennessy-Milner Theorem for ${\mathbf {\mathsf{{WAML}}}}^n$). Let $\mathcal {M}=(W,R,V)$ and $\mathcal {M}'=(W',R',V')$ be two image-finite n-models. Then for every $w\in W$ and $w'\in W'$, iff $w\equiv _{\textsf {WAML}^n} w'$.

Proof

As in basic modal logic, the crucial part is to show $\equiv _{\textsf {WAML}^n}$ is indeed a $wa^n$-bisimulation and we only verify the forth condition. Suppose towards contradiction that $Rwv_1\dots v_n$ but for each $v_1'\dots v'_n$ such that $R'w'v_1'\dots v'_n$ there is a $v'_j$ such that it is not $\textsf {WAML}^n$-equivalent to any of $v_i$. In image-finite models we can list such $v'_j$ as $u_1\dots u_m$. Now for each $u_k$ and $v_i$ we have $\varphi _k^i$ which holds on $v_i$ but not on $u_k$. Now we consider the formula $\psi =\Diamond (\bigvee _{1\le i\le n}\bigwedge _{1\le k\le m} \varphi _k^i)$. It is not hard to see that $\psi$ holds on w but not $w'$, hence contradiction.

Like in normal modal logic, we can also define a notion of k-bisimulation of $\textsf {WAML}^n$, by restricting the maximal depth we may go to.

Definition 5

(k-$wa^n$-bisimulation). Let $\mathcal {M}=(W,R,V)$ and $\mathcal {M}'=(W',R',$ $V')$ be two n-models. w and $w'$ are 0-$wa^n$-bisimilar () iff $V(v)=V'(v')$. iff and the follow two conditions are satisfied:

• forth If and $Rvv_{1},\ldots ,v_{n}$ then there are $v_{1}',\ldots ,v_{n}'$ in $W'$ s.t. $R'v'v_{1}',\ldots ,v_{n}'$ and for each $v'_j$ there is a $v_i$ such that where $1\le i,j\le n$.

• back If and $R'v'v_{1}',\ldots ,v_{n}'$ then there are $v_{1},\ldots ,v_{n}$ in W s.t. $Rvv_{1},\ldots ,v_{n}$ and for each $v_i$ there is a $v'_j$ such that where $1\le i,j\le n$.

We can translate each $\textsf {WAML}^n$ formula to an equivalent $\textsf {FOL}$ formula with one free variable and one $n+1$-ary relation symbol, thus $\textsf {WAML}^n$ is also compact.

Definition 6

(Standard translation). $ST:\textsf {WAML}^{n}\rightarrow \textsf {FOL}$:

$$\begin{array}{lcl} ST_x(p)&{}=&{}Px\\ ST_x(\lnot \varphi )&{}=&{} \lnot ST_x(\varphi )\\ ST_x(\varphi \wedge \psi )&{}=&{} ST_x(\varphi )\wedge ST_x(\psi ) \\ ST_x(\Box \varphi )&{}=&{} \forall y_1\forall y_2\dots \forall y_n (R xy_1y_2\dots y_n\rightarrow ST_{y_1}(\varphi )\vee \dots \vee ST_{y_n}(\varphi )) \end{array}$$

By following a similar strategy as in [27], we will show a van Benthem-Rosen characterization theorem for $\textsf {WAML}^n$: a $\textsf {FOL}$ formula is equivalent to the translation of a $\textsf {WAML}^n$ formula (over finite n-models) if and only if it is invariant under $wa^n$-bisimulations (over finite n-models).

First we need to define a notion of unraveling w.r.t. n-ary models similarly to models with binary relations. We use an example of a graph with ternary relations to illustrate the intuitive idea behind the general n-ary unraveling, which is first introduced in [28].

Example 2

Given the 2-model with ternary relations $\langle \{w,v,u,t\},$ $\{\langle w, u,t \rangle ,$ $\langle u,t,u \rangle ,$ $\langle t,w,v \rangle \}, V \rangle$. It is quite intuitive to first unravel it into a tree with pairs of states as nodes, illustrated below:

To turn it into a 2-model, we need to define the new ternary relations. For each triple $\langle s_0,s_1,s_2 \rangle$ of pairs, $\langle s_0, s_1, s_2 \rangle$ is in the new ternary relation iff $s_1$ and $s_2$ are successors of $s_0$ in the above graph and the triple of underlined worlds in $s_0, s_1, s_2$ respectively is in the original ternary relation, e.g., $\langle u,\underline{t} \rangle ,\langle \underline{w},v \rangle ,\langle w,\underline{v} \rangle$ is in the new ternary relation since $\langle t,w,v \rangle$ is in the original ternary relation.

In general, we can use the n-tuples of the states in the original model together with a natural number $k\in [1,n]$ as the basic building blocks for the unraveling of an n-model, e.g., $\langle w, v, u, 2 \rangle$ means the second the state is the underlined one. To make the definition uniform, we define the root as the sequence $\langle w,\dots ,w,1 \rangle .$ Like the unraveling for a binary graph, formally we will use sequences of such building blocks as the nodes in the unraveling of a n-model, e.g., the left-most node $\langle \underline{t},u \rangle$ in the above example will become $\langle \langle w,w,1 \rangle ,\langle u,t,1 \rangle ,\langle t, u ,1 \rangle \rangle$. This leads to the following definition.

Definition 7

Given an n-model $\mathcal {M}=\langle W,R,V\rangle$ and $w\in W$, we first define the binary unraveling $\mathcal {M}^b_{w}$ of $\mathcal {M}$ around w as $\langle W_w, R^b, V' \rangle$ where:

• $W_w$ is the set of sequences $\langle \langle \mathbf {v}_0,i_0\rangle ,\langle \mathbf {v}_{1},i_{1}\rangle ,\ldots ,\langle \mathbf {v}_{m},i_{m}\rangle \rangle$ where:

  • $m\in \mathbb {N}$;

  • for each $j\in [0,m]$, $\mathbf {v}_{j}\in W^n$ and $i_{j}\in [1, n]$ such that $R(\mathbf {v}_{j}[i_{j}])\mathbf {v}_{j+1}$;

  • $\mathbf {v}_0$ is the constant n-sequence $\langle w,\dots ,w\rangle$ and $i_0=1$;

• $R^bss'$ iff $s'$ extends s with some $\langle \mathbf {v}, i \rangle$

• $V'(s)=V(r(s))$, where $r(s)= \mathbf {v}_m[i_m]$ if $s=\langle \dots , \langle \mathbf {v}_m,i_m \rangle \rangle$.

The unraveling $\mathcal {M}_w=\langle W_w, R', V' \rangle$ is based on $\mathcal {M}^b_w$ by defining $R's_0 s_1\dots s_n$ iff $Rr(s_0)r(s_1)\dots r(s_n)$ and $R^bs_0s_i$ for all $i\in [1,n]$. Let the bounded unraveling $\mathcal {M}_w|_l$ be the submodel of $\mathcal {M}_w$ up to level l.

Remark 2

The unravelling $\mathcal {M}_w$ itself is not totally “tree-like”, since there may be some node w occurs in both an n-tuple successor of x and an n-tuple successor of y for $x \ne y$. But clearly $\mathcal {M}^b_w$ is a tree, and in $\mathcal {M}_w$, if $Rs_0\dots s_n$ then $s_1\dots s_n$ are at the next “level” of $s_0$. The latter property is crucial in the later proofs, but due to space issues, we have to omit the details here.

r defined above reveals the corresponding state of s in the original model $\mathcal {M}$. It is not hard to show the following.

Proposition 2

The above r (viewed as a relation) is a $wa^n$-bisimulation between $\mathcal {M}_{w}$ and $\mathcal {M}$. Actually r is a p-morphism (over n-models) from $\mathcal {M}_w$ to $\mathcal {M}$.

Now we have all the ingredients to prove the following characterization theorem. Note that the characterization works with or without the finite model constraints.

Theorem 2

A first-order formula $\alpha (x)$ is invariant under (over finite models) iff $\alpha (x)$ is equivalent to a $\textsf {WAML}^n$ formula (over finite models).

Following the general strategy in [27], the only non-trivial part is to show that the FOL formula $\alpha (x)$ that is invariant under $wa^n$-bisimulation has some locality property w.r.t. its bounded unraveling $\mathcal {M}_w|_l$ for some l. Due to lack of space, we only show the following lemma and give a proof sketch here. For other relatively routine parts of the proof, see [27].

Lemma 1

(locality). An FOL formula $\alpha (x)$ is invariant under (over finite models) implies that for some $l \in \mathbb {N}$, for any n-model $\mathcal {M},w$: $\mathcal {M},w\Vdash \alpha (x)[w]$ iff $\mathcal {M}_w|_{l}\Vdash \alpha (x)[(\langle \mathbf {w},1) \rangle ]$.

Here we explain the most important ideas behind the proof. First of all, like in [27], we take $l=2^q-1$ where q is the quantifier rank of $\alpha (x)$, and build two bigger models $\mathcal {M}^*, w^*$ and $\mathcal {N}^*, v^*$ which are $wa^n$-bisimilar to $\mathcal {M},w$ and $\mathcal {M}_w|_{l}, w$ respectively using our new unraveling notion. Then we show that in the q-round EF game between the bigger n-models Duplicator has a winning strategy. To specify the strategy, which is essentially letting the duplicator to keep some “safe zones” for extensions of partial isomorphisms, we need to define the distance of points in n-models. Let the distance between s and $s'$ (notation $d(s,s')$) be the length of the shortest (undirected) path between s and $s'$ via a new relation binary $R^{c}$ where $R^{c}xy$ iff $Rxy_{1}\ldots y_{n}$ and $y=y_{i}$ for some $i\in [1, n]$. We set $d(s, s')=\omega$ if s and $s'$ are not connected by any such path. It is easy to see that in the unraveling $\mathcal {M}_w$, $d(s, s')$ is exactly the distance in the usual sense between $s, s'$ in the tree $\mathcal {M}_w^b$. Then, the winning strategy looks exactly like the one in [27] for binary models. The key point to show that the same strategy is a winning strategy in the new setting is that when building the correct induction hypothesis, we need to define two “neighborhoods” of a node–a big one and a small one. In particular, first let $(a_{i},b_{i})$ be the pair selected at i round where each $a_{i}\in \mathcal {M}^{*}$ and $b_{i}\in \mathcal {N}^{*}$, where by the rule of the game, $a_{0}=w^{*}$ and $b_{0}=v^{*}$. Then define $S(m)=\{a_{i}\mid i\le m\}$, $N_{i}(m)$ to be the neighborhood of $a_{i}$ within distance of $2^{q-m}-1$, and $N_{i}^{^{\prime }}(m)$ to be the neighborhood of $a_{i}$ within distance of $2^{q-(m+1)}$. Here the N and $N^{^{\prime }}$ are the two “neighborhoods”. Then finally the induction hypothesis can be correctly formulated as the following.

After m rounds ($0\le m\le q$), the following two hold.

• 1. The selected points form a partial isomorphism I: $\mathcal {M}^{*}\rightarrow \mathcal {N}^{*}$.

• 2. If $m<q$ then there is a sequence $(I_{0},\ldots ,I_{m})$ s.t. for each $i\le m$,

  • (a) $I_{i}\supseteq I$ is a partial isomorphism with $Dom(I_{i})=N_{i}(m)\cup S(m)$;

  • (b) $\forall h,j\le m\forall x\in N_{h}^{^{\prime }}(m)\cap N_{j}^{^{\prime }}(m)(I_{h}(x)=I_{j}(x))$.

In Otto’s original proof in [27], the induction hypothesis is not very clear, and we think it is necessary to give such an explicit formulation here.

Remark 3

It is not hard to show that under our distance notion, for each x, y, z in the model, $d(x,z) \ge d(x,y)-d(y,z)$, i.e., $d(x,z)+d(z,y) \ge d(x,y)$ which is a more usual form of the triangle inequality. This justifies the new distance notion. To see why a similar strategy like the one in [27] for binary models works, note that our unraveling $\mathcal {M}_w$ is essentially based on a tree $\mathcal {M}_w^b$ by definition, and the n-ary relation over such a tree structure has a very special property: if $Rs_0\dots s_n$ then $s_1\dots s_n$ are immediate successors of $s_0$ in the binary unraveling as mentioned in Remark 2. This leads to the following crucial property we will use repeatedly: if we already established a partial isomorphism I between S and N (w.r.t. also n-ary relations), and $x\not \in S$ is not directly connected to anything in S, and $y\not \in N$ is also not directly connected to anything in N then $I\cup \{(x,y)\}$ extending I is again a partial isomorphism.

Finally, the bound $l=2^{q}-1$ in the above proof, which we choose uniformly for every n, is actually not “optimal”, since for a larger n, we can have a lower bound. Especially, when $n > q$, even $l=1$, the Duplicator could have a winning strategy, since any bijection will be a partial isomorphism. So the distance we define here is not a appropriate one for us to find the minimal bound l. Here we conjecture that the bound should be the least integer l s.t. $l \ge (2^{q}-1)/n$.

4 Interpolation

By a standard strategy in [19], we know that the basic polyadic modal logics ($\textsf {PML}$) have the Craig Interpolation theorem. What’s more, in [31], the authors proved that the minimal monotonic modal logic M has Uniform Interpolation. Furthermore, we know that the basic modal logic $\mathbb {K}$ also has Uniform Interpolation from [3] and [2]. From the following three aspects we may conjecture that the basic $\textsf {WAML}$ systems $\mathbb {K}_{n}$ should have interpolation too:

• 1 $\textsf {WAML}$ can be treated as a fragment of $\textsf {PML}$.

• 2 $\mathbb {K}_{n}$ is regarded as a general version of $\mathbb {K}$, since $\mathbb {K}$ is just $\mathbb {K}_{1}$.

• 3 $\mathbb {K}_{n}$ can be viewed as a special kind of monotonic modal logics.

But in fact no $\mathbb {K}_{n}$ has the Craig Interpolation Property for $n \ge 2$. The first counterexample for interpolation we found is for $\mathbb {K}_{3}$, which is relatively easy to understand and can be readily generalized to all $\mathbb {K}_{n}$ for $n \ge 3$. Later we found a counterexample for $\mathbb {K}_{2}$, which is slightly more complicated. Here we first give the two counterexamples for $\mathbb {K}_2$ and $\mathbb {K}_3$ and then provide the general construction for $\mathbb {K}_n$ ($n \ge 3$). But before we state the counterexamples, let us first clarify what do we mean by “a counterexample” of the Craig Interpolation Property for $\mathbb {K}_n$.

Lemma 2

Let n be a non-zero natural number. If there are two pointed n-models $\mathcal {M}, w$ and $\mathcal {N}, v$ and two formulas $\varphi$ and $\psi$ such that

• 1. $\mathcal {M}, w\,\models \,\varphi$ and $\mathcal {N}, v\,\models \,\psi$;

• 2. $\mathbb {K}_n \vdash \varphi \rightarrow \lnot \psi$;

• 3. letting $\varPhi '$ be the set of all the propositional letters that appear both in $\varphi$ and $\psi$, for any formula $\gamma$ in $\textsf {WAML}$ such that only letters in $\varPhi '$ appear, $\mathcal {M}, w\,\models \,\gamma$ iff $\mathcal {N}, v\,\models \,\gamma$;

then $\mathbb {K}_n$ lack the Craig Interpolation Property.

Proof

Assume for contradiction that $\mathbb {K}_n$ has the Craig Interpolation Property. Then since $\mathbb {K}_n \vdash \varphi \rightarrow \lnot \psi$, there is a interpolant $\gamma$ such that

• $\mathbb {K}_n \vdash \varphi \rightarrow \gamma$ and $\mathbb {K}_n \vdash \gamma \rightarrow \lnot \psi$;

• only letters in $\varPhi '$ appear in $\gamma$.

Now since $\mathcal {M}, w\,\models \,\varphi$ with $\mathcal {M}$ being an n-model and $\mathbb {K}_n \vdash \varphi \rightarrow \gamma$, by soundness, $\mathcal {M}, w\,\models \,\gamma$. Then $\mathcal {N}, v\,\models \,\gamma$ by 3. Then using $\mathbb {K}_n \vdash \gamma \rightarrow \lnot \psi$ and soundness again, $\mathcal {N}, v\,\models \,\lnot \psi$, contradicting $\mathcal {N}, v\,\models \,\psi$.

Given this proposition, a pair of pointed n-models and a pair of formulas satisfying the antecedent constitute a counterexample of the Craig Interpolation property. Now we proceed to provide them for each $\mathbb {K}_n$ with $n \ge 2$.

Example 3

Consider the following two 2-models where $\{\langle w,w_1,w_1 \rangle ,$ $\langle w,w_2,w_3 \rangle \}$ is the ternary relation in the left model $\mathcal {M}_2$, and $\{\langle v,v_1,v_2 \rangle \}$ is the ternary relation in the right model $\mathcal {N}_2$, where the valuations are as in the diagram.

Then set $\varphi _2 = \Box (\lnot p \vee \lnot q) \wedge \Diamond q$ and $\psi _2 = \Box (p \wedge r) \wedge \Box (p \wedge \lnot r)$. It is easy to see that $\mathcal {M}_2, w\,\models \,\varphi _2$ and $\mathcal {N}_2, v\,\models \,\psi _2$. To see that $\mathbb {K}_2\vdash \varphi _2 \rightarrow \lnot \psi _2$, consider the following derivation, where to make long Boolean combinations readable, we write negation of propositional letters as overline, omit $\wedge$ between purely Boolean formulas and replace $\vee$ with |.

Here PL means propositional reasoning. Hence we are done with the first two points for this pair of models and formulas to be a counterexamples. For the last point, note that $Z=\{\langle w,v \rangle , \langle w_1, v_1 \rangle , \langle w_1, v_2 \rangle , \langle w_2, v_1 \rangle ,\langle w_2, v_2 \rangle \}$ is a $wa^2$-bisimulation when $\varPhi = \{p\}$. Hence by Proposition 1, for any formula $\gamma$ with p the only propositional letter, $\mathcal {M}_2, w\,\models \,\gamma$ iff $\mathcal {N}_2, v\,\models \,\gamma$. But p is the only common propositional letters in $\varphi _2$ and $\psi _2$. Clearly, now $\mathcal {M}, w$, $\mathcal {N}, v$, $\varphi _2$, and $\psi _2$ form a counterexample to the Craig Interpolation Property for $\mathbb {K}_2$.

Example 4

Consider the following two 3-models where $\{\langle w,w_1,w_2,w_3 \rangle \}$ is the relation in $\mathcal {M}_3$ and $\{\langle v,v_1,v_2,v_3 \rangle \}$ is the relation in $\mathcal {N}_3$.

Then set $\varphi _3= \Box p\bar{q} \wedge \Box pq \wedge \Diamond (p|\bar{p})$, $\psi _3= \Box \bar{p}r \wedge \Box \bar{p}\bar{r} \wedge \Diamond (p|\bar{p})$. Clearly $\mathcal {M}_3, w\,\models \,\varphi _3$ and $\mathcal {N}_3, v\,\models \,\psi _3$. Further, $\mathbb {K}_2 \vdash \varphi _3 \rightarrow \lnot \psi _3$ since we have the following derivation.

Finally, note that $Z=\{\langle w,v \rangle , \langle w_1, v_3 \rangle , \langle w_2, v_3 \rangle , \langle w_3, v_1 \rangle ,\langle w_3, v_2 \rangle \}$ is a $wa^3$-bisimulation if $\varPhi = \{p\}$.

The above example can be naturally generalized for each $\mathbb {K}_n$ with $n > 3$. Let m be the least natural number s.t. $2^{m} \ge n-1$ and pick m many distinct propositional letters $r_1, \ldots , r_m$ from $\varPhi$. Then for each i from 1 to $n-1$, we can associate a distinct conjunction of literals $\rho _i$ using $r_j$’s so that $\rho _i \wedge \rho _{i'}$ are incompatible for each $i \not = i'$. Then we can state the general counterexample.

Example 5

Consider the following two n-models where $\{\langle w,w_1,...,w_n \rangle \}$ is the relation in $\mathcal {M}_n$, and $\{\langle v,v_1,...,v_n \rangle \}$ is the relation in $\mathcal {N}_n$.

Set $\varphi _n = \Box (p \wedge \lnot q) \wedge \Box (p \wedge q) \wedge \Diamond \top$ and $\psi _n = \bigwedge _{i = 1}^{n-1}\Box (\lnot p \wedge \rho _{i}) \wedge \Diamond \top$. Clearly $\mathcal {M}_n, w\,\models \,\varphi _n$ and $\mathcal {N}_n, v\,\models \,\psi _n$. It is also easy to see that by $\mathtt {K}_n$, we can derive $(\Box (p \wedge \lnot q) \wedge \Box (p \wedge q) \wedge \bigwedge _{i = 1}^{n-1}\Box (\lnot p \wedge \rho _i)) \rightarrow \Box \bot$. With this we can then easily derive $\varphi _n \rightarrow \lnot \psi _n$ in $\mathbb {K}_n$. Finally, note that p is the only common propositional letter in $\varphi _n$ and $\psi _n$ and that $Z=\{\langle w,v \rangle , \langle w_1, v_1 \rangle , \langle w_2, v_1 \rangle \} \cup \{w_3,...,w_n\} \times \{v_2,...,v_n\}$ is a $wa^n$-bisimulation when $\varPhi = \{p\}$.

With the examples and Lemma 2, the main theorem of this section follows.

Theorem 3

For any $n \ge 2$, $\mathbb {K}_n$ does not have the Craig Interpolation Property.

Remark 4

Note that the Lemma 2 uses only the soundness of the logics. Hence for any extension of $\mathbb {K}_n$ that is sound on $\mathcal {M}_n$ and $\mathcal {N}_n$, it still lacks the Craig Interpolation Property. For example, we may extend $\mathbb {K}_n$ with $\mathtt {4}$ and our examples still work since $\mathtt {4}$ is valid on the underlying frames.

5 Conclusion

In this paper, we proved two results about $\textsf {WAML}$: first, $\textsf {WAML}$ have a van Benthem-Rosen characterization, and second, $\textsf {WAML}$ do not have Craig Interpolation Property (CIP). We conclude with two potentially promising lines of further investigation.

First, the main part of the completeness proof of $\mathbb {K}_n$ over n-models is to solve some combinatorial puzzle [26]. Due to the semantics of $\textsf {WAML}$ there is a natural link between combinatorics and $\textsf {WAML}$ as also shown in the use of graph coloring problem in [5]. As future work, we would like to explore the possibility of using $\textsf {WAML}$ to express interesting combinatorial properties in graph theory, like the one in [25].

Second, even though we proved that $\textsf {WAML}$ do not have Craig Interpolation Property, it doesn’t mean that the same must be the case under further constraints (stronger logics). For instance, the counterexample in our paper cannot show that $\mathbb {K}_n \oplus \mathtt {T}$ lacks CIP since the logic is not sound on the frames of the models we provided. What remains to be done then is to chart the map of CIP among the logics extending $\mathbb {K}_n$’s and look for more general methods.

Lastly, if we change all the $\Box$ in $\mathbb {K}_n$ into $\Diamond$, we get the following formula:

$$\mathtt {K}_{n}^{*}: \Diamond p_{0}\wedge \cdots \wedge \Diamond p_{n}\rightarrow \Diamond \bigvee \limits _{(0\le i<j\le n)}(p_{i}\wedge p_{j}).$$

In basic normal modal logics, this formula characterizes frames where each world has at most n accessible worlds and is equivalent (assuming the normality of $\Box$) to what is commonly called the $\mathtt {Alt}_n$ in the literature [33]. It is not too hard to observe that the strategy we gave in Sect. 4 can be used to show that for each $n \ge 3$, normal modal logic $\mathtt {K}\oplus \mathtt {K}_{n}^{*}$ lacks CIP. It seems that, more abstractly speaking, the counterexamples exist because the logic can reason about with the help of extra propositional letters, but cannot express directly, whether there are many accessible worlds satisfying a property. Note that counting the number of accessible worlds satisfying a property is intuitively important and has been studied in Description Logics (DL) [7] and Graded Modal Logics (GML) [12, 15, 17]. There are already some CIP work in those logics, like [23], and we conjecture that CIP may return when we add modalities that talk directly about numbers.