Abstract

We introduce inquisitive action logic, InqAL, a multi-agent modal logic for reasoning about action. While traditional approaches focus on what properties of the outcome an agent can force, InqALalso captures what aspects of the outcome an agent determines through their actions. As we argue, such claims of agentive determination are naturally analyzed as modal claims involving questions.

Technically, InqALis a multi-agent extension of inquisitive neighborhood logic [@Ciardelli:25neighborhood] based on concurrent game structures. With respect to statements, it is expressively equivalent to the individual-agent fragment of the socially friendly coalition logic recently proposed by Goranko and Enqvist [@GorankoEnqvist:18].

We present an axiomatization of InqALand prove completeness and decidability via the finite model property. Along the way, we establish a representation theorem for actual effectivity functions, associating to an agent the sets of outcomes corresponding to their possible actions; we give exact conditions under which a multi-agent neighborhood frame arises from a concurrent game structure.

1 Introduction↩︎

There is a long tradition of using modal logics to reason about actions, outcomes, and abilities (for surveys, see [@Agotnes:15; @Segerberg:16]). This enterprise is motivated by philosophical, juridical, and computational concerns: logics of agency have been used, e.g., to spell out precise notions of responsibility [@Lorini:14; @Baltag:21], and for the automated verification of software properties [@Demri:16]. Logics in this tradition typically focus on the powers of agents (or coalitions) in an interactive situation, i.e., on the facts they are able to force through their actions. Something which is just as important, however, is what aspects of the world an agent determines, or influences, through their actions. For an illustration, imagine that Alice and Bob are creating clay animals together; Alice moulds an animal with the clay, and Bob paints it. While Alice works, Bob picks a color, without looking at what Alice is moulding. In this scenario, it is natural to say the following:

. . Alice determines the shape of the animal (but not its color). .̱ Bob determines the color of the animal (but not its shape).

These facts matter, among other things, for ascribing responsibility: suppose little Charlie asks his siblings to make a red cat for him; if what he gets is a blue cat, he should complain to Bob, not to Alice.

How can we analyze a statement like ? More precisely, what is the thing that Alice determines? Standardly, in modal logic, modalities apply to propositions. However, “the shape of the animal” does not denote a proposition; rather, it is associated with a set of propositions: that the animal is a dog, that the animal is a cat, etcetera. What Alice determines is not a specific one of these propositions, but which among these propositions is going to be actualized. In other words, what Alice determines is the answer to a question, namely, the question “what the shape is”. Determining, then, can be seen as a relation between an agent and a question. What does this relation amount to? Here is a natural idea: an agent can be said to determine a question if the answer to the question is not settled a priori, but it becomes settled once we fix the agent’s action. Implementing this idea takes us into the realm of inquisitive modal logic, a quickly growing research area that combines inquisitive logic and modal logic.

Inquisitive logic [@Ciardelli:23book] is a framework that allows one to build logical systems including not only, as usual, formulas expressing propositions (e.g., that the animal is a cat), but also formulas expressing questions (e.g., what the shape of the animal is). One can then define inquisitive modalities that apply to such formulas (see, a.o., [@Ciardelli:14aiml; @CiardelliRoelofsen:15idel; @Ciardelli:18aiml; @Gessel:20action; @Gessel:21; @PuncocharSedlar:21epistemic; @PuncocharSedlar:21pdl; @CiardelliOtto:21; @MeissnerOtto:22; @MaricPerkov:24; @Ciardelli:25neighborhood]). In our case, the idea is to capture agentive determination in terms of an inquisitive modality \(\boxtimes\) indexed by agents which, when applied to formulas shape and color formalizing the questions what is the shape and what the color, delivers modal statements \(\boxtimes_{\text{Alice}}\textsf{shape}\) and \(\boxtimes_{\text{Bob}}\textsf{color}\) capturing, respectively, the claims in and .

In this paper, we will develop this idea in detail. We will define an inquisitive action logic, InqAL, which allows us to analyze statements like and along the lines we described, but which also recovers the modal account of ability familiar from the classical work of Brown [@Brown:88] and more recent work on coalition logic, CL [@Pauly:02]. Our logic is a multi-agent version of a recently developed system, inquisitive neighborhood logic, InqNL[@Ciardelli:22aiml; @Ciardelli:25neighborhood]. InqNLis based on a binary modality \(\Rrightarrow\), acting semantically as a strict conditional quantifying over neighborhoods; analogously, our multi-agent extension InqALcontains one such modality \(\Rrightarrow_{a}\!\) for each agent \(a\); in terms of this modality, some derivative unary modalities (including the modality \(\boxtimes_a\) mentioned above) can be defined. Besides being multi-agent, InqALis geared specifically towards an interpretation in terms of action; as a consequence, while InqNLis interpreted over arbitrary neighborhood models, InqALstarts with more concrete structures known as concurrent game structures or multi-agent transition systems [@Alur:02; @Pauly:02; @GorankoDrimmelen:06; @Bulling:16], modeling processes in which a system transitions from a state to another based on the joint actions of multiple agents. Now, from such models one can extract a corresponding neighborhood model, where the neighborhoods for a given agent correspond to the actions available to them, each neighborhood encoding the range of outcomes that may possibly result if the agent performs that action. The neighborhood maps induced in this way are known in the literature as actual effectivity functions [@Bulling:16] (in contrast with the effectivity functions studied in coalition logic [@Pauly:02; @Goranko:13], which are upward-closed sets of neighborhoods). The problem of characterizing which families of neighborhood maps are the actual effectivity functions of some concurrent game structure is currently open. In this paper, we settle this problem for the case in which we only consider single agents, and not proper coalitions. This result is interesting in its own right, but it also plays a key role in our study of InqAL, giving us a characterization of the relevant class of neighborhood models.

Our logic InqALis also connected to socially friendly coalition logic (SFCL), an extension of coalition logic recently proposed by Goranko and Enqvist [@GorankoEnqvist:18]. Whereas standard coalition logic focuses on what outcomes agents can force through their actions, SFCL also captures what outcomes agents can enable for others, while still forcing their own goals. These properties are crucial for the possibility of cooperation between agents (hence the name socially friendly). Technically, SFCL is a multi-agent extension of instantial neighborhood logic, INL [@Benthem:17]. As proved in [@Ciardelli:25neighborhood], inquisitive neighborhood logic has, with respect to statements, the same expressive power as INL. In the same vein, our inquisitive action logic has, with respect to statements, the same expressive power as SFCL. Still, as we will see, the way modal claims are expressed in these logics is very different; in particular, the translation from InqALto SFCL can lead to an exponential increase in the size of the formula.

The paper is structured as follows. In §2 we provide a characterization of those neighborhood frames that arise as actual effectivity functions from some concurrent game structure. In §3 we introduce \(\textsf{InqNL}_{\mathcal{A}}\), a multi-agent version of inquisitive neighborhood logic. In §4 we introduce InqAL, which interprets \(\textsf{InqNL}_{\mathcal{A}}\)over concurrent game models, and discuss how this logic allows us to express interesting properties relating to what agents can force, enable, or determine in an interactive situation. In §5 we give an axiomatization of InqALand prove completeness and decidability. In §6 we compare the expressive power of our logic with that of Socially Friendly Coalition Logic. §7 concludes.

2 Characterizing actual effectivity functions of agents↩︎

Concurrent game structures [@Alur:02; @Pauly:02; @Bulling:16] model processes in which the transition from one stage to the next is determined by the simultaneous actions of multiple agents. The formal definition is as follows.

Definition 1. Let \(\mathcal{A}=\{a_1,\dots,a_k\}\) be a finite set of agents. A concurrent game structure* (or CGS for short) for \(\mathcal{A}\) is a triple \(\mathcal{S}=(W,\textsf{act},\textsf{out})\) where:*

\(W\) is a non-empty set of worlds, representing stages of the process;
\(\textsf{act}\) is a function which assigns to each agent \(a\) and world \(w\) a non-empty set \(\textsf{act}(a,w)\) of actions.

A function \(\tau\) assigning to each agent \(a_i\) a corresponding action \(\tau(a_i)\in\textsf{act}(a_i,w)\) is called an action profile at \(w\); the set of action profiles at \(w\) is denoted \(\textsf{ActP}(w)\).
\(\textsf{out}\) is a function that, given a world \(w\) and an action profile \(\tau\) at \(w\), returns a world \(\textsf{out}(w,\tau)\); intuitively, \(\textsf{out}(w,\tau)\) is the world that results from \(w\) when each agent \(a_i\) performs the action \(\tau(a_i)\).

At a world \(w\) in a CGS, a range of outcomes are possible, depending on the choices of the agents, namely: \[O(w)=\{\textsf{out}(w,\tau)\mid\tau\in\textsf{ActP}(w)\}\] By picking a particular action, an agent typically narrows down the set of possible outcomes. The set of outcomes which are possible from \(w\) given that agent \(a\) performs action \(\tau_a\in\textsf{act}(a,w)\) is: \[O_{a}(w,\tau_a)=\{\textsf{out}(w,\tau)\mid\tau\in\textsf{ActP},\tau(a)=\tau_a\}\] We call this the output set of action \(\tau_a\) for \(a\) at \(w\). By collecting the output sets of all actions available to an agent, we obtain their actual effectivity function. More precisely, the actual effectivity function of agent \(a\) in a CGS \(\mathcal{S}\) is the map \(\Sigma_a^\mathcal{S}:W\to\wp\wp(W)\) given by: \[\Sigma_a^\mathcal{S}(w)=\{O_a(w,\tau_a)\mid \tau_a\in\textsf{act}(a,w)\}\] In this way, a CGS determines a corresponding multi-agent neighborhood frame \(F_\mathcal{S}=(W,(\Sigma_a^\mathcal{S})_{a\in\mathcal{A}})\). But not just any neighborhood frame \(F=(W,(\Sigma_a)_{a\in\mathcal{A}})\), where \(\Sigma_a:W\to\wp\wp(W)\), can be a system of actual effectivity functions of some CGS. This raises a natural question: which neighborhood frames arise from some CGS? The following theorem provides an answer to this question.¹

Theorem 1. Let \(\mathcal{A}=\{a_1,\dots,a_k\}\) be a finite set of agents with \(k>1\).² For a multi-agent neighborhood frame \(F=(W,(\Sigma_a)_{a\in\mathcal{A}})\) the following are equivalent:

\(F=F_\mathcal{S}\) for some concurrent game structure \(\mathcal{S}\).
The following three conditions are satisfied for each world \(w\in W\):
1. Existence of actions: for all \(a\in\mathcal{A}\), \(\Sigma_a(w)\neq\emptyset\);
2. Uniform range: for all \(a,b\in\mathcal{A}\), \(\bigcup\Sigma_a(w)=\bigcup\Sigma_b(w)\);
3. Independence: for all \(s_1\in\Sigma_{a_1}(w),\dots,s_k\in\Sigma_{a_k}(w): s_1\cap\dots\cap s_k\neq\emptyset\).

Proof. \(1\Rightarrow 2\) amounts to the claim that the actual effectivity functions of a CGS satisfy conditions (a)-(c) in 2. Condition (a) follows from the fact that \(\textsf{act}(a,w)\) is non-empty by definition. Condition (b) is due to the observation that for every \(a\), \(\bigcup\Sigma_a^\mathcal{S}(w)\) coincides with the set of all possible outcomes at \(w\), \(O(w)\). Condition (c) is due to the fact that whenever we take neighborhoods \(O_{a_i}(w,\tau_{a_i})\in\Sigma_{a_i}^\mathcal{S}(w)\) for \(i=1,\dots,k\), the function \(\tau\) defined by \(\tau(a_i)=\tau_{a_i}\) is an action profile, and we have \(\textsf{out}(w,\tau)\in O_{a_i}(w,\tau_{i})\) for each \(i\).

To show \(2\Rightarrow 1\), suppose \(F=(W,(\Sigma_a)_{a\in\mathcal{A}})\) is a neighborhood frame satisfying (a)-(c). Our aim is to define a CGS \(\mathcal{S}=(W,\textsf{act},\textsf{out})\) with \(F_\mathcal{S}=F\), i.e., such that for each agent \(a\), \(\Sigma_a\) coincides with the actual effectivity function \(\Sigma_a^\mathcal{S}\) of agent \(a\) in \(\mathcal{S}\).

For this, equip the set \(W\) with a group structure, so that \((W,e,*,(\cdot)^{-1})\) is a group. Also, fix a well-ordering of \(W\), and for any non-empty \(s\subseteq W\), let \(\min(s)\) denote the least element of \(s\) according to this well-ordering.³ We define the actions available to an agent \(a\) at a world \(w\) as pairs consisting of a neighborhood for \(a\), and a world: \[\textsf{act}(a,w)=\{(s,v)\mid s\in\Sigma_a(w), v\in W\}\] Condition (a) guarantees that this is a non-empty set, as required by the definition of a CGS.

Now given a world \(w\), an action profile at \(w\) can be identified with a sequence \(\tau=((s_1,v_1),\dots,(s_k,v_k))\) where \(s_i\in\Sigma_{a_i}(w)\) for \(i\le k\). We define the outcome of \(\tau\) at \(w\) in the following way: \[\textsf{out}(w,\tau)=\left\{ \begin{array}{ll} v_1*\dots*v_k &\text{if }(v_1*\dots*v_k)\in (s_1\cap\dots\cap s_k)\\ \min(s_1\cap\dots\cap s_k) & \text{otherwise} \end{array} \right.\] Condition (c) guarantees that \(s_1\cap\dots\cap s_k\) is non-empty, so that \(\min(s_1\cap\dots\cap s_k)\) exists, which ensures that \(\textsf{out}(w,\tau)\) is well-defined. Note further that, by definition, \(\textsf{out}(w,\tau)\in s_1\cap\dots \cap s_k\).

We claim that the CGS so defined induces \(F\). To show this, the key step is to prove that for each agent \(a\) and action \((s,v)\in\textsf{act}(a,w)\), the set of outputs that may result from \(a\) performing \((s,v)\) is simply \(s\): \[\label{eq:key32step} O_a(w,(s,v))=s\tag{1}\] The inclusion \(\subseteq\) is clear: whenever \(\tau\) is an action profile that includes the action \((s,v)\), the corresponding outcome \(\textsf{out}(w,\tau)\) is bound to be in \(s\) by definition of \(\textsf{out}\). To show the inclusion \(\supseteq\), consider an arbitrary world \(u\in s\). We need to show that there is an action profile \(\tau\) including \((s,v)\) whose outcome is \(u\).

For simplicity, suppose \(a=a_1\) and let us write \((s_1,v_1)\) for \((s,v)\). Since \(u\in s_1\) and \(s_1\in\Sigma_{a_1}(w)\), we have \(u\in\bigcup\Sigma_{a_1}(w)\). By condition (b), for each \(i>1\) we have \(u\in\bigcup\Sigma_{a_i}(w)\), so we can pick a neighborhood \(s_i\in\Sigma_{a_i}(w)\) with \(u\in s_i\). Now for \(1<i<k\), pick some worlds \(v_i\in W\) arbitrarily. Finally, let \(v_k\) be the element \((v_1*\dots*v_{k-1})^{-1}*u\). Now consider the action profile \(\tau=((s_1,v_1),\dots,(s_k,v_k))\). We have \(v_1*\dots*v_k=(v_1*\dots*v_{k-1})*(v_1*\dots*v_{k-1})^{-1}*u=u\). By the way the sets \(s_i\) were chosen we know that \(u\in s_1\cap\dots\cap s_k\), and so by definition of \(\textsf{out}\) we have \(\textsf{out}(w,\tau)=u\). Since the profile \(\tau\) includes the action \((s,v)\), this shows that \(u\in O_a(w,(s,v))\), as required to complete the proof of (1 ).

Finally, using (1 ), the actual effectivity function for agent \(a\) turns out to be \[\Sigma_a^\mathcal{S}(w)= \{O_a(w,\tau_a)\mid\tau_a\in\textsf{act}(a,w)\}= \{O_a(w,(s,v))\mid s\in \Sigma_a(w),v\in W\}= \{s\mid s\in \Sigma_a(w)\}= \Sigma_a(w)\] which shows that indeed, \(F_\mathcal{S}=F\), as desired. ◻

3 Inquisitive multi-agent neighborhood logic↩︎

In this section we present a multi-agent version of inquisitive neighborhood logic, InqNL[@Ciardelli:25neighborhood]. We call this logic \(\textsf{InqNL}_{\mathcal{A}}\) where \(\mathcal{A}=\{a_1,\dots,a_k\}\) is a finite set of agents. The proofs of the results in this section are the same as for InqNL; we do not repeat them here, but include pointers to the results in [@Ciardelli:25neighborhood].

Syntax. Given a finite set \(\mathcal{P}\) of atoms, the set \(\mathcal{L}_{\mathcal{A}}\) of \(\textsf{InqNL}_{\mathcal{A}}\)-formulas is given by: \[\varphi\;::=\;p\mid\bot\mid(\varphi\land\varphi)\mid(\varphi\to\varphi)\mid(\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\varphi)\mid(\varphi\Rrightarrow_{a}\!\varphi)\] where \(p\in\mathcal{P}\) and \(a\in\mathcal{A}\). As standard in inquisitive logic, we also use the following abbreviations: \(\neg\varphi:=(\varphi\to\bot)\); \(\top:=\neg\bot\); \((\varphi\lor\psi):=\neg(\neg\varphi\land\neg\psi)\); \({?\varphi}:=(\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\neg\varphi)\). The connective \(\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\), called inquisitive disjunction, is regarded as a question-forming disjunction. Thus, e.g., the formula \({?p}\) (short for \(p\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\neg p\)) is regarded as the question whether or not \(p\). The operators \(\Rrightarrow_a\) are indexed versions of the binary modality \(\Rrightarrow\) InqNL. Two unary modalities (read “window” and “kite”) are defined in terms of \(\Rrightarrow_{a}\!\) as follows: \[\boxplus_a\varphi:=(\top\Rrightarrow_{a}\!\varphi)\qquad \diamondplus_a\varphi:=\neg(\varphi\Rrightarrow_{a}\!\bot)\] An important fragment of the language is given by declarative formulas (or declaratives, for short), where inquisitive disjunction occurs only in the scope of a modal operator. More formally, the set \(\mathcal{L}_{\mathcal{A}}^!\)of declaratives is defined as follows, where \(\varphi\) can be rewritten as any formula from \(\mathcal{L}_{\mathcal{A}}\): \[\alpha\;::=\;p\mid\bot\mid(\alpha\land\alpha)\mid(\alpha\to\alpha)\mid(\varphi\Rrightarrow_{a}\!\varphi)\] Intuitively, declaratives stand for statements (as we will see, this is reflected in a key semantic property). We will use the meta-variables \(\varphi,\psi,\chi\) for arbitrary formulas, and \(\alpha,\beta,\gamma\) for declaratives.

The modal depth of a formula is defined as usual as the maximum number of nestings of modal operators in it. More precisely, we set: \(\text{md}(p)=\text{md}(\bot)=0\); \(\text{md}(\varphi\land\psi)=\text{md}(\varphi\to\psi)=\text{md}(\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi)=\max(\text{md}(\varphi),\text{md}(\psi))\); \(\text{md}(\varphi\Rrightarrow_{a}\!\psi)=\max(\text{md}(\varphi),\text{md}(\psi))+1\). The set of formulas in \(\mathcal{L}_{\mathcal{A}}\) with modal depth up to \(n\) is denoted \(\mathcal{L}_{\mathcal{A}}^n\); the set of declaratives with modal depth up to \(n\) is denoted \(\mathcal{L}_{\mathcal{A}}^{!n}\).

Semantics. We interpret formulas relative to multi-agent inhabited neighborhood models (main-models, for short), which are triples \(M=(W,(\Sigma_a)_{a\in\mathcal{A}},V)\) where \(W\neq\emptyset\) is a set of worlds, \(\Sigma_a:W\to\wp\wp_{0}(W)\) is a map assigning to each \(w\in W\) a set \(\Sigma_a(w)\) of non-empty subsets of \(W\) (called the neighborhoods of \(w\)) and \(V:\mathcal{P}\to\wp(W)\) is a valuation function. As customary in inquisitive logic, the semantics of \(\textsf{InqNL}_{\mathcal{A}}\)is not given in terms of truth relative to possible worlds, but instead in terms of support relative to sets of possible worlds, called information states (or simply states).

Definition 2 (Support in main-models). Let \(M=(W,(\Sigma_a)_{a\in\mathcal{A}},V)\) be a main-model. The relation of support between information states \(s\subseteq W\) and formulas \(\varphi\in\mathcal{L}_{\mathcal{A}}\) is defined as follows:

\(M,s\models p\iff s\subseteq V(p)\)
\(M,s\models\bot\iff s=\emptyset\)
\(M,s\models\varphi\land\psi\iff M,s\models\varphi\) and \(M,s\models\psi\)
\(M,s\models\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi\iff M,s\models\varphi\) or \(M,s\models\psi\)
\(M,s\models\varphi\to\psi\iff \forall t\subseteq s: M,t\models\varphi\) implies \(M,t\models\psi\)
\(M,s\models\varphi\Rrightarrow_{a}\!\psi\iff \forall w\in s\forall t\in\Sigma_a(w):M,t\models\varphi\) implies \(M,t\models\psi\)

All the clauses except for the last one are standard in inquisitive logic (see [@Ciardelli:23book] for discussion), while the clause for the modality \(\Rrightarrow_{a}\!\) is a direct multi-agent adaptation of the one for \(\Rrightarrow\) in InqNL[@Ciardelli:25neighborhood]. Entailment and equivalence are defined in the obvious way: a set of formulas \(\Phi\) entails a formula \(\psi\), denoted \(\Phi\models_{\textsf{InqNL}_{\mathcal{A}}}\psi\), if for every main-model \(M\) and state \(s\) that supports all formulas in \(\Phi\), \(s\) also supports \(\psi\). Two formulas \(\varphi,\psi\) are equivalent, denoted \(\varphi\equiv_{\textsf{InqNL}_{\mathcal{A}}}\psi\), if they are supported by the same states in every main-model. To ease notation, throughout this section we drop the subscript \(\textsf{InqNL}_{\mathcal{A}}\).

As usual in inquisitive logic, support is persistent (if \(M,s\models\varphi\) and \(t\subseteq s\), then \(M,t\models\varphi\)), and the empty state trivially supports every formula. Moreover, we retrieve a notion of truth at a world \(w\) by defining it as support relative to the corresponding singleton \(\{w\}\).

Definition 3 (Truth). \(\varphi\) is true* at a world \(w\) of a main-model \(M\), denoted \(M,w\models\varphi\), in case \(M,\{w\}\models\varphi\). The set of worlds at which \(\varphi\) is true in a model \(M\) is denoted \(|\varphi|_M\).*

Some simple calculations show that the Boolean connectives have their usual truth-functional behavior (for instance, \(M,w\models\neg\varphi\iff M,w\not\models\varphi\)), and that modal formulas have the following truth conditions:

\(M,w\models(\varphi\Rrightarrow_{a}\!\psi)\iff \forall s\in\Sigma_a(w):M,s\models\varphi\) implies \(M,s\models\psi\)
\(M,w\models\boxplus\varphi\iff \forall s\in\Sigma_a(w):M,s\models\varphi\)
\(M,w\models\diamondplus\varphi\iff \exists s\in\Sigma_a(w):M,s\models\varphi\)

Declaratives have a special semantic property: for them, support boils down to truth at each world. In fact, up to equivalence, declaratives are exactly the formulas for which this holds.

Definition 4 (Truth-conditionality). A formula \(\varphi\in\mathcal{L}_{\mathcal{A}}\) is truth-conditional* if for every model \(M\) and state \(s\) we have \(M,s\models\varphi\iff \forall w\in s: M,w\models\varphi\).*

Every declarative \(\alpha\in\mathcal{L}_{\mathcal{A}}^!\) is truth-conditional. Conversely, every truth-conditional formula of \(\mathcal{L}_{\mathcal{A}}\) is equivalent to a declarative.

Not all formulas of \(\textsf{InqNL}_{\mathcal{A}}\)are truth-conditional. As a simple example, consider the formula \(?p\) (which abbreviates \(p\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\neg p\)). A simple calculation yields the following support conditions: \[M,s\models{?p}\iff p\text{ has the same truth value in all worlds in }s\] Intuitively, \({?p}\) is supported at \(s\) if it is settled in \(s\) whether \(p\) is true or false. Clearly, \({?p}\) is supported at every singleton state, and so true at each world, in every model; yet, it is not supported by every state.

Obviously, formulas that are not truth-conditional cannot be equivalent to a declarative. However, any formula \(\varphi\) is equivalent to a finite inquisitive disjunction of declaratives, called the resolutions of \(\varphi\).

Definition 5 (Resolutions). The set \(\mathcal{R}(\varphi)\) of resolutions* of a formula \(\varphi\in\mathcal{L}_{\mathcal{A}}\) is defined as follows:*

\(\mathcal{R}(\alpha)=\{\alpha\}\) if \(\alpha\) is an atom, \(\bot\), or a modal formula \((\varphi\Rrightarrow_{a}\!\psi)\);
\(\mathcal{R}(\varphi\land\psi)=\{\alpha\land\beta\mid\alpha\in\mathcal{R}(\varphi),\beta\in\mathcal{R}(\psi)\}\);
\(\mathcal{R}(\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi)=\mathcal{R}(\varphi)\cup\mathcal{R}(\psi)\);
\(\mathcal{R}(\varphi\to\psi)=\{\bigwedge_{\alpha\in\mathcal{R}(\varphi)}(\alpha\to f(\alpha))\mid f:\mathcal{R}(\varphi)\to\mathcal{R}(\psi)\}\).

Note that \(\mathcal{R}(\varphi)\) is always a finite non-empty set of declaratives, and for any declarative \(\alpha\), \(\mathcal{R}(\alpha)=\{\alpha\}\).

For any \(\varphi\in\mathcal{L}_{\mathcal{A}}\), \(\varphi\equiv\mathlarger{\mathbin{{\setminus}\mspace{-5mu}{\setminus}}/}\mathcal{R}(\varphi)\).

In terms of resolutions we may also define a further modal operator, \(\Box_a\), which will play a role below: \[\Box_a\varphi\::=\;\bigvee\{\boxplus_a\alpha\mid\alpha\in\mathcal{R}(\varphi)\}\] This operator has been considered in previous work on inquisitive modal logic [@CiardelliRoelofsen:15idel; @Ciardelli:14aiml; @Ciardelli:25].⁴ In particular, it has been argued to give a natural generalization of the standard knowledge modality of epistemic logic, allowing for a uniform analysis of knowledge ascriptions involving declarative complements (knowing that) and interrogative complements (knowing whether/who/what, etc).

Note that \(\Box_a\varphi\) is a declarative. A simple calculation yields the following truth conditions:

\(M,w\models\Box_a\varphi\iff M,\bigcup\Sigma_a(w)\models\varphi\)

To conclude, we mention a fact that will be useful later on: given that we start with a finite set of atoms, there are only finitely many formulas of a given modal depth, up to logical equivalence.

The quotient of \(\mathcal{L}_{\mathcal{A}}^n\) under equivalence is finite.

4 Inquisitive action logic↩︎

In this section we turn to the logic which is the focus of this paper: inquisitive action logic, InqAL. This logic is a special case of the multi-agent inquisitive neighborhood logic \(\textsf{InqNL}_{\mathcal{A}}\)introduced in the previous section, obtained by focusing on a particular class of neighborhood models: those whose neighborhood functions represent actual effectivity functions of some concurrent game structure. For simplicity, we focus on the multi-agent case, i.e., we assume from now on that \(\mathcal{A}\) contains at least two agents; for some comments on the trivial, but somewhat special, single-agent case, see Footnote 7.

Definition 6. A concurrent game model* (or cg-model, for short) is a pair \(\mathcal{M}=(\mathcal{S},V)\) consisting of a concurrent game structure \(\mathcal{S}=(W,\textsf{act},\textsf{out})\) and a valuation function \(V:\mathcal{P}\to\wp(W)\).*

A concurrent game model \(\mathcal{M}=(\mathcal{S},V)\) with \(\mathcal{S}=(W,\textsf{act},\textsf{out})\) determines a corresponding main-model \(M_\mathcal{M}=(W,(\Sigma_a^\mathcal{S})_{a\in\mathcal{A}},V)\), whose neighborhood functions are the actual effectivity functions of agents. We can thus interpret the formulas of \(\mathcal{L}_{\mathcal{A}}\) relative to a cg-model, via its associated main-model.

Definition 7. Let \(\mathcal{M}\) be a cg-model, \(s\) a state in \(\mathcal{M}\), and \(\varphi\in\mathcal{L}_{\mathcal{A}}\). We write \(\mathcal{M},s\models\varphi\) if \(M_\mathcal{M},s\models\varphi\).

Entailment and equivalence in InqAL, denoted \(\models_\textsf{InqAL}\) and \(\equiv_\textsf{InqAL}\) respectively, are defined in the same way as for \(\textsf{InqNL}_{\mathcal{A}}\), but with respect to cg-models instead of main-models. Note that, being determined by a smaller class of models, the logic InqALis an extension of \(\textsf{InqNL}_{\mathcal{A}}\).

In the setting of concurrent game models, our modal formulas take on a specific significance. We will illustrate this by means of some examples (for the sake of space, we omit the simple calculations involved). First, consider a modal formula of the form \(\diamondplus_a\alpha\), where \(\alpha\in\mathcal{L}_{\mathcal{A}}^!\). We have: \[\mathcal{M},w\models\diamondplus_a\alpha\iff\exists \tau_a\in\textsf{act}(a,w):O_a(w,\tau_a)\subseteq|\alpha|_\mathcal{M}\] Thus, \(\diamondplus_a\alpha\) expresses the fact that agent \(a\) has an action available that guarantees the truth of \(\alpha\) (i.e., if that action is executed, the outcome will make \(\alpha\) true, regardless what the other agents do). In short, \(\diamondplus_a\alpha\) says that \(a\) can force \(\alpha\), recovering the standard semantics for ability familiar from [@Brown:88] and [@Pauly:02].⁵

As a second example, consider the modal formula \((\alpha\Rrightarrow_{a}\!\beta)\), where \(\alpha,\beta\in\mathcal{L}_{\mathcal{A}}^!\). We have: \[\mathcal{M},w\models(\alpha\Rrightarrow_{a}\!\beta)\iff \forall\tau_a\in\textsf{act}(a,w): O_a(w,\tau_a)\subseteq|\alpha|_\mathcal{M}\text{ implies }O_a(w,\tau_a)\subseteq|\beta|_\mathcal{M}\] What this formula expresses is that, in order to force \(\alpha\), agent \(a\) necessarily has to force \(\beta\) as well. By negating such statements, we can express the fact that the agent can force certain outcomes without precluding others. Consider, e.g., the formula \(\neg(\alpha\Rrightarrow_{a}\!\neg\beta)\). We have: \[\mathcal{M},w\models\neg(\alpha\Rrightarrow_{a}\!\neg\beta)\iff \exists\tau_a\in\textsf{act}(a,w): O_a(w,\tau_a)\subseteq|\alpha|_\mathcal{M}\text{ and }O_a(w,\tau_a)\cap|\beta|_\mathcal{M}\neq\emptyset\] The formula expresses the fact that agent \(a\) can perform an action which forces \(\alpha\) without precluding \(\beta\). More generally, a formula of the form \(\neg(\alpha\Rrightarrow_{a}\!\neg\beta_1\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\dots\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\neg\beta_n)\) expresses the fact that it is possible for \(a\) to force \(\alpha\) without precluding any of \(\beta_1,\dots,\beta_n\). In this way, the central properties that the Socially Friendly Coalition Logic of Goranko and Enqvist [@GorankoEnqvist:18] is designed to capture can be expressed in InqAL.

Let us now consider formulas involving the modalities \(\boxplus_a\) and \(\Box_a\). First consider the case in which the argument is a declarative \(\alpha\in\mathcal{L}_{\mathcal{A}}^!\). In this case, \(\mathcal{R}(\alpha)=\{\alpha\}\), and so the two modalities coincide: by definition of \(\Box_a\), we have \(\Box_a\alpha=\boxplus_a\alpha\). Recall from Section 2 that, in the case of actual effectivity functions, the union of the neighborhoods simply coincides with the set \(O(w)\) of all outcomes possible at \(w\): for any agent \(a\), \(\bigcup\Sigma_a^\mathcal{S}(w)=O(w)\). Using this fact, we obtain the following: \[\mathcal{M},w\models\Box_a\alpha\iff\mathcal{M},w\models\boxplus_a\alpha\iff O(w)\subseteq|\alpha|_\mathcal{M}\] Thus, regardless of the agent \(a\), the (identical) formulas \(\boxplus_a\alpha\) and \(\Box_a\alpha\) express the fact that \(\alpha\) is unavoidable: it will be true at the next stage regardless what the agents do.

When the argument is not a declarative, however, the modalities \(\Box_a\) and \(\boxplus_a\) come apart. Let us illustrate this with the case of a polar question \(?\alpha\), where \(\alpha\in\mathcal{L}_{\mathcal{A}}^!\). Since \(\mathcal{R}(?\alpha)=\{\alpha,\neg\alpha\}\), the formula \(\Box_a{?\alpha}\) amounts to \(\boxplus_a\alpha\lor\boxplus_a\neg\alpha\), which says that either \(\alpha\) is unavoidably true at the next stage, or it is unavoidably false. More formally: \[\mathcal{M},w\models \Box_a{?\alpha}\iff\text{\alpha has the same truth value in all worlds in }O(w)\] Thus, \(\Box_a{?\alpha}\) says that whether \(\alpha\) will be true at the next stage is predetermined, i.e., settled a priori regardless of the actions of the agents. By contrast, for the modal formula \(\boxplus_a{?\alpha}\) we have the following: \[\mathcal{M},w\models\boxplus_a{?\alpha}\iff \forall \tau_a\in\textsf{act}(a,w): \text{\alpha has the same truth value in all worlds in }O_a(w,\tau_a)\] Thus, what \(\boxplus_a{?\alpha}\) expresses is that once we fix the action of \(a\), the truth value of \(\alpha\) at the next stage is settled: the actions of other agents cannot affect it. These findings generalize: if \(\varphi\) denotes a question, then \(\Box_a\varphi\) expresses the fact that \(\varphi\) is settled a priori, regardless of what the agents do, while \(\boxplus_a\varphi\) expresses the fact that \(\varphi\) is settled once we fix the action of agent \(a\).

We can now see how the analysis of agentive determination we suggested in the introduction can be formalized in InqAL. Our guiding idea was this: at a certain stage in a process, an agent \(a\) determines a question \(\varphi\) if (i) the answer to \(\varphi\) is not settled a priori but (ii) it becomes settled once we fix the action of agent \(a\). In our logic, (i) is captured by \(\neg\Box_a\varphi\), and (ii) by \(\boxplus_a\varphi\). We can thus define a modality \(\boxtimes_a\) capturing agentive determination in the following way: \[\boxtimes_a\varphi\;:=\;\neg\Box_a\varphi\land \boxplus_a\varphi\] For instance, the claim that agent \(a\) determines whether \(\alpha\) will be true at the next stage is expressed by \(\boxtimes_a{?\alpha}:=\neg\Box_a{?\alpha}\land\boxplus_a{?\alpha}\), which says that the truth value of \(\alpha\) is not predetermined (i.e., not the same in all possible outcomes), but it is determined once we fix the action of \(a\) (i.e., it is constant within each neighborhood for \(a\)). This is, in my view, a very natural analysis of the determination claim.⁶

To illustrate this analysis further, consider the scenario from the introduction, where Alice (\(a\)) and Bob (\(b\)) are creating clay animals together. Let’s say that there are three shapes that Alice is able to mould—cat, dog, and cow—and three colors available to Bob—red, blue, and green. A simple modeling of the scenario is one where Alice has three actions available to her: \(\tau_{\text{cat}}\) (mould a cat), \(\tau_{\text{dog}}\) (mould a dog), and \(\tau_{\text{cow}}\) (mould a cow); similarly, Bob has three actions: \(\tau_{\text{red}}\) (paint red), \(\tau_{\text{blue}}\) (paint blue), \(\tau_{\text{green}}\) (paint green). Each joint action by Alice and Bob, for instance \(\tau_{\text{cat}}\tau_{\text{red}}\), results in a specific outcome, for instance \(\textsf{out}(w,\tau_{\text{cat}}\tau_{\text{red}})=\text{red cat}\). In total, there are \(3\times 3=9\) possible outcomes (red cat, blue dog, etc.) which make up the total set \(O(w)\). For each agent, fixing an action leaves us with only 3 possible outcomes; for instance, \(O_a(w,\tau_{cat})=\{\text{red cat},\text{blue cat},\text{green cat}\}\), while \(O_b(w,\tau_{red})=\{\text{red cat},\text{red dog},\text{red cow}\}\). The neighborhoods corresponding to these outcome sets for Alice and Bob are depicted in Figure [fig:1].

Figure 1: The neighborhoods (i.e., outcome sets) associated to Alice’s actions (left) and Bob’s action (right) in our toy example.

Now we can consider a language with six propositional atoms, cat, dog, cow, red, blue, green, with the obvious interpretation (e.g., cat expresses the proposition “the animal is a cat”). Using inquisitive disjunction, we can build two formulas shape and color expressing, respectively, the questions “what the shape is” and “what the color is”: \[\textsf{shape}:=(\textsf{cat}\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\textsf{dog}\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\textsf{cow})\qquad\textsf{color}:=(\textsf{red}\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\textsf{blue}\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\textsf{green})\] An information state \(s\) in our model supports the question shape just in case in all worlds in \(s\), the animal has the same shape; similarly, \(s\) supports color if in all worlds in \(s\), the animal has the same color.

By embedding these questions under modalities we can now describe what aspects of the outcome Alice and Bob respectively determine through their actions: Alice determines the shape (\(\boxtimes_a\textsf{shape}\)) but not the color (\(\neg\boxtimes_a\textsf{color}\)), while Bob determines the color (\(\boxtimes_b\textsf{color}\)) but not the shape (\(\neg\boxtimes_b\textsf{shape}\)).

In order to see that \(\boxtimes_a\textsf{shape}\) (i.e., \(\neg\Box_a\textsf{shape}\land\boxplus_a\textsf{shape}\)) is true at our world \(w\), we reason as follows. First, since the shape of the animal is not constant across all possible outcomes, we have \(\mathcal{M},O(w)\not\models\textsf{shape}\), which ensures \(\mathcal{M},w\models\neg\Box_a\textsf{shape}\); this captures the fact that in our scenario, the shape is not predetermined, but depends on the actions of the agents. Second, within each of the three outcome sets \(O_a(w,\tau_{cat}),O_a(w,\tau_{dog}),O_a(w,\tau_{cow})\), corresponding to the three actions for \(a\), the shape of the animal is constant; therefore, each of these sets supports shape, ensuring \(\mathcal{M},w\models\boxplus_a\textsf{shape}\); this captures the fact that once we fix Alice’s action, the shape of the outcome is settled, regardless of what Bob does.

By contrast, \(\boxtimes_a\textsf{color}\) (i.e., \(\neg\Box_a\textsf{color}\land\boxplus_a\textsf{color}\)) is false at \(w\), since its second conjunct is false. Consider any outcome set for \(a\), for instance \(O_a(w,\tau_{cat})\). The color of the animal is not constant across this set, and so this set does not support \(\textsf{color}\). Since not all the outcome sets for \(a\) (in fact, none of them) support \(\textsf{color}\), \(\mathcal{M},w\not\models\boxplus_a\textsf{color}\). This reflects the fact even if we fix Alice’s action, the color of the outcome is not settled—it depends in part (and in fact, in our case, completely) on what Bob does.

5 Axiomatization and decidability↩︎

We start by presenting an axiomatization of \(\textsf{InqNL}_{\mathcal{A}}\), which is the basis for our axiomatization of InqAL.

The propositional axioms include instances of axioms for intuitionistic propositional logic, with \(\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\) in the role of intuitionistic disjunction, and all instances of the following, where \(\alpha\in\mathcal{L}_{\mathcal{A}}^!\) and \(\varphi,\psi\in\mathcal{L}_{\mathcal{A}}\):

\(\neg\neg\alpha\to\alpha\)(Declarative double negation)
\((\alpha\to\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi)\to(\alpha\to\varphi)\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}(\alpha\to\psi)\)(Split)

The modal axioms include all instances of the following schemata, capturing the behavior of the modalities \(\Rrightarrow_{a}\!\) as strict conditionals (see [@Ciardelli:25neighborhood] for discussion of these axioms in the uni-modal case and [@LitakVisser:18] for a more general study of strict conditionals on an intuitionistic basis):

\((\varphi\Rrightarrow_{a}\!\psi)\land(\psi\Rrightarrow_{a}\!\chi)\to(\varphi\Rrightarrow_{a}\!\chi)\)(Transitivity)
\((\varphi\Rrightarrow_{a}\!\psi)\land(\varphi\Rrightarrow_{a}\!\chi)\to(\varphi\Rrightarrow_{a}\!(\psi\land\chi))\)(Right conjunction)
\((\varphi\Rrightarrow_{a}\!\chi)\land(\psi\Rrightarrow_{a}\!\chi)\to((\varphi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi)\Rrightarrow_{a}\!\chi)\)(Left disjunction)

The inference rules are modus ponens (\(\varphi,\varphi\to\psi/\psi\)) and conditional necessitation (\(\varphi\to\psi/\varphi\Rrightarrow_{a}\!\psi\)).

If \(\psi\in\mathcal{L}_{\mathcal{A}}\) is derivable in this system we write \(\vdash_{\textsf{N}}\psi\). For \(\Phi,\Psi\subseteq\mathcal{L}_{\mathcal{A}}\), we write \(\Phi\vdash_{\textsf{N}}\Psi\) in case for some finite \(\Phi_0\subseteq\Phi\) and \(\Psi_0\subseteq\Psi\) we have \(\vdash_{\textsf{N}}\bigwedge\Phi_0\to\mathlarger{\mathbin{{\setminus}\mspace{-5mu}{\setminus}}/}\Psi_0\). Instead of \(\{\varphi_1,\dots,\varphi_n\}\vdash_{\textsf{N}}\{\psi_1,\dots,\psi_m\}\) we write simply \(\varphi_1,\dots,\varphi_n\vdash_{\textsf{N}}\psi_1,\dots,\psi_m\). We write \(\varphi\dashv\vdash_{\textsf{N}}\psi\) if we have both \(\varphi\vdash_{\textsf{N}}\psi\) and \(\psi\vdash_{\textsf{N}}\varphi\).

The following soundness and strong completeness theorem generalizes the one for InqNL. The proof is the obvious multi-agent adaptation of the one for InqNLgiven in [@Ciardelli:25neighborhood].

Theorem 2. For all \(\Phi\subseteq\mathcal{L}_{\mathcal{A}}\) and \(\psi\in\mathcal{L}_{\mathcal{A}}\), \(\Phi\models_{\textsf{InqNL}_{\mathcal{A}}}\psi\iff\Phi\vdash_{\textsf{N}}\psi\).

To obtain a system for InqAL, we add three axiom schemata reflecting the properties of actual effectivity functions we identified in Theorem 1. For all declaratives \(\alpha\), all formulas \(\varphi_1,\dots,\varphi_n\), all agents \(a,b\), and all pairwise distinct agents \(a_1,\dots,a_{n+1}\), the following are axioms:⁷

\(\diamondplus_a\top\)(Existence of actions)
\(\boxplus_a\alpha\leftrightarrow\boxplus_b\alpha\;\)⁸ (Uniform range)
\(\diamondplus_{a_1}\varphi_1\land\dots\land\diamondplus_{a_n}\varphi_n\,\to\,\neg{\diamondplus_{a_{n+1}}}\neg(\varphi_1\land\dots\land\varphi_n)\) (Independence)

We write \(\vdash_{\textsf{A}}\psi\) if \(\psi\) is derivable in this extended system. Similarly, the notations \(\Phi\vdash_{\textsf{A}}\Psi\) and \(\varphi\dashv\vdash_{\textsf{A}}\psi\) are defined as for \(\vdash_{\textsf{N}}\), but with reference to the extended axiom system. Our task is now to prove that this extended system is sound and (weakly) complete for InqAL.⁹

Theorem 3 (Soundness and completeness for InqAL). For all \(\varphi\in\mathcal{L}_{\mathcal{A}}\), \(\models_{\textsf{InqAL}}\varphi\iff\vdash_{\textsf{A}}\varphi\).

For soundness, we just have to check that the axioms are valid and the inference rules preserve validity. We leave this as an exercise, noting only that the three extra axioms for InqALowe their validity to the three corresponding properties of actual effectivity functions listed in Theorem 1. Towards completeness, we adapt a finite canonical model construction from [@Ciardelli:25neighborhood] (in turn building on ideas from [@Ciardelli:14aiml]).

Definition 8. For \(n\in\mathbb{N}\), an \(n\)-bounded complete theory of declaratives* (or \(n\)CTD for short), is a set of declaratives \(\Gamma\subseteq\mathcal{L}_{\mathcal{A}}^{!n}\) satisfying three conditions: (i) deductive closure relative to \(\mathcal{L}_{\mathcal{A}}^{!n}\): if \(\Gamma\vdash_{\textsf{A}}\alpha\) and \(\alpha\in\mathcal{L}_{\mathcal{A}}^{!n}\), then \(\alpha\in\Gamma\); (ii) consistency: \(\bot\not\in\Gamma\); and (iii) completeness: for all \(\alpha\in\mathcal{L}_{\mathcal{A}}^{!n}\), \(\alpha\in\Gamma\) or \(\neg\alpha\in\Gamma\). We denote the set of all \(n\)CTDs by \(\mathcal{K}_n\).*

We now show that each \(\mathcal{K}_n\) is a non-empty finite set, and that the sets \(\mathcal{K}_n\) and \(\mathcal{K}_m\) are disjoint for \(n\neq m\).

Lemma 1. If \(\Delta\subseteq\mathcal{L}_{\mathcal{A}}^{!n}\) and \(\Delta\not\vdash_{\textsf{A}}\bot\), then \(\Delta\subseteq\Gamma\) for some \(\Gamma\in\mathcal{K}_n\). In particular, \(\mathcal{K}_n\neq\emptyset\).

Proof. A simple adaptation of the usual saturation argument. ◻

Lemma 2. Each set \(\mathcal{K}_n\) is finite.

Proof. Since \(\vdash_{\textsf{A}}\) extends \(\vdash_{\textsf{N}}\), the equivalence relation \(\dashv\vdash_{\textsf{N}}\) refines \(\dashv\vdash_{\textsf{A}}\). By Theorem 2, \(\dashv\vdash_{\textsf{N}}\) coincides with the semantic equivalence relation \(\equiv_{\textsf{InqNL}_{\mathcal{A}}}\). By Prop.[prop:finiteness], the quotient of \(\mathcal{L}_{\mathcal{A}}^n/\equiv_{\textsf{InqNL}_{\mathcal{A}}}\) is finite, and a fortiori, so is the quotient \(\mathcal{L}_{\mathcal{A}}^{!n}/\dashv\vdash_{\textsf{A}}\). Since an \(n\)CTD is a subset of \(\mathcal{L}_{\mathcal{A}}^{!n}\) which is deductively closed, it is fully determined by the equivalence classes of its elements modulo \(\dashv\vdash_{\textsf{A}}\), i.e., it is fully determined by a subset of the quotient \(\mathcal{L}_{\mathcal{A}}^{!n}/\dashv\vdash_{\textsf{A}}\). Since these subsets are finitely many, so are the \(n\)CTDs. ◻

Lemma 3. \(\mathcal{K}_n\cap\mathcal{K}_m=\emptyset\) for \(n\neq m\).

Proof. Let \(a\) be an arbitrary agent and let \(\boxplus_a^h\top\) abbreviate \(\boxplus_a\dots\boxplus_a\top\) with \(h\) occurrences of \(\boxplus_a\). If \(\Gamma\in\mathcal{K}_n\), by deductive closure relative to \(\mathcal{L}_{\mathcal{A}}^{!n}\) we have \(\boxplus_a^h\top\in\Gamma\iff h\le n\), and so \(n=\max\{h\mid \boxplus_a^h\top\in\Gamma\}\). As a consequence, if \(\Gamma\in \mathcal{K}_n\cap \mathcal{K}_m\) then \(n=\max\{h\mid \boxplus_a^h\top\in\Gamma\}=m\). ◻

We now define for each \(n\in\mathbb{N}\) a canonical model suitable for formulas in \(\mathcal{L}_{\mathcal{A}}^n\).

Definition 9. For \(n\in\mathbb{N}\), we define the main-model \(M_n=(W_n,(\Sigma_{a}^n)_{a\in\mathcal{A}},V_n)\) as follows: \(W_n=\bigcup_{m\le n}\mathcal{K}_m\); \(V_n(p)=\{\Gamma\in W_n\mid p\in\Gamma\}\); finally, the neighborhood map \(\Sigma_{a}^n\) is defined as follows:

if \(\Gamma\in\mathcal{K}_0\) then \(\Sigma_{a}^n(\Gamma)=\{\mathcal{K}_0\}\)
if \(\Gamma\in\mathcal{K}_{m+1}\) then \(\Sigma_{a}^n(\Gamma)=\{S\subseteq\mathcal{K}_m, S\neq\emptyset\mid \text{for all }(\psi\Rrightarrow_a\!\chi)\in\Gamma:\bigcap S\vdash_{\textsf{A}}\psi\text{ implies }\bigcap S\vdash_{\textsf{A}}\chi\}\)

For any \(n\in\mathbb{N}\), the model \(M_n\) is finite by Lemma 2. The following four lemmas play a key role in the completeness proof. The proofs are simple adaptations of those of the corresponding results for InqNL(Lemmas 6.10, 6.12, 6.15, and 6.16 in [@Ciardelli:25neighborhood]), We provide the details in Appendix A for completeness.

Lemma 4 (Intersection Lemma).
For a set \(\Delta\subseteq\mathcal{L}_{\mathcal{A}}^{!n}\), define \(S_\Delta^n=\{\Gamma\in\mathcal{K}_n\mid\Delta\subseteq\Gamma\}\). For every \(\varphi\in\mathcal{L}_{\mathcal{A}}^n\) we have \(\Delta\vdash_{\textsf{A}}\varphi\iff \bigcap S_\Delta^n\vdash_{\textsf{A}}\varphi\).¹⁰ In particular, since \(S_\emptyset^n=\mathcal{K}_n\), for every \(\varphi\in\mathcal{L}_{\mathcal{A}}^n\) we have \(\vdash_{\textsf{A}}\varphi\iff\bigcap\mathcal{K}_n\vdash_{\textsf{A}}\varphi\).

Lemma 5 (Existence Lemma).
For \(m\le n\), if \(\Gamma\in\mathcal{K}_m\) and \(\neg(\varphi\Rrightarrow_{a}\!\psi)\in\Gamma\), then there is \(S\in\Sigma_a^n(\Gamma)\) such that \(\bigcap S\vdash_{\textsf{A}}\varphi\) and \(\bigcap S\not\vdash_{\textsf{A}}\psi\).

Lemma 6 (Range Lemma).
For all \(\Gamma\in\mathcal{K}_{m}\) with \(m>0\) we have \(\bigcup\Sigma_a^n(\Gamma)=\{\Gamma'\in\mathcal{K}_{m-1}\mid\forall\alpha\in\mathcal{L}_{\mathcal{A}}^!:\boxplus_a\alpha\in\Gamma\text{ implies }\alpha\in\Gamma'\}\).

Lemma 7 (Support Lemma).
For all \(m\le n\), all non-empty states \(S\subseteq\mathcal{K}_m\), and all formulas \(\varphi\in\mathcal{L}_\mathcal{A}^m\): \(M_n,S\models\varphi\iff\bigcap S\vdash_{\textsf{A}}\varphi\).

The part of the proof which is genuinely novel, and crucial for our purposes, lies in showing that the canonical models \(M_n\) so constructed are induced by some corresponding concurrent game models.

Lemma 8 (Representation Lemma). For each \(n\in\mathbb{N}\) there is a CGM \(\mathcal{M}_n\) such that \(M_{\mathcal{M}_n}=M_n\).

Proof. It suffices to show that the maps \((\Sigma_a^n)_{a\in\mathcal{A}}\) of our canonical model satisfy the conditions (a)-(c) of Theorem 1. Consider a world \(\Gamma\in W_n\). We have \(\Gamma\in\mathcal{K}_m\) for some \(m\le n\). If \(m=0\) then \(\Sigma_a^n(\Gamma)=\{\mathcal{K}_0\}\) for every agent \(a\) and conditions (a)-(c) are obviously satisfied. So, we may assume \(m>0\).

(a) Existence of actions. Since \(\Gamma\) contains the axiom \(\diamondplus_a\top\), which is short for \(\neg(\top\Rrightarrow_{a}\!\bot)\), the existence of some \(S\in\Sigma_a^n(\Gamma)\) follows directly from Lemma 5.

(b) Uniform range. Take any agents \(a,b\in\mathcal{A}\). For any declarative \(\alpha\), \(\boxplus_a\alpha\leftrightarrow\boxplus_b\alpha\) is an axiom, so \(\boxplus_a\alpha\dashv\vdash_{\textsf{A}}\boxplus_b\alpha\). Since the formulas \(\boxplus_a\alpha\) and \(\boxplus_b\alpha\) also have the same modal depth, \(\Gamma\) contains one iff it contains the other. Now using Lemma 6 for both agents \(a\) and \(b\) we have: \[\begin{align} \bigcup\Sigma_a^n(\Gamma)&= & \{\Gamma'\in\mathcal{K}_{m-1}\mid\forall\alpha\in\mathcal{L}_{\mathcal{A}}^!:\boxplus_a\alpha\in\Gamma\text{ implies }\alpha\in\Gamma'\}\\ &= & \{\Gamma'\in\mathcal{K}_{m-1}\mid\forall\alpha\in\mathcal{L}_{\mathcal{A}}^!:\boxplus_b\alpha\in\Gamma\text{ implies }\alpha\in\Gamma'\}\quad =\quad \bigcup\Sigma_b^n(\Gamma) \end{align}\]

(c) Independence. Take any neighborhoods \(S_1\in\Sigma_{a_1}^n(\Gamma), \dots, S_k\in\Sigma_{a_k}^n(\Gamma)\). We must prove \(S_1\cap\dots\cap S_k\neq\emptyset\). We start by proving the following claim: \[\qquad\qquad\bigcap S_1 \cup \dots \cup \bigcap S_k\not\vdash_{\textsf{A}}\bot\qquad\quad(*)\] Towards a contradiction, suppose this is false. Then there are formulas \(\alpha_1\in\bigcap S_1,\dots,\alpha_k\in\bigcap S_k\) such that \(\alpha_1,\dots,\alpha_k\vdash_{\textsf{A}}\bot\) (it suffices to consider a single \(\alpha_i\) from each \(\bigcap S_i\), since \(\bigcap S_i\) is closed under conjunction).

By definition of \(\Sigma_{a_i}^n\), each \(S_i\) is non-empty and thus \(\bigcap S_i\not\vdash_{\textsf{A}}\bot\). Since \(S_i\in\Sigma_{a_i}^n(\Gamma)\) and \(\bigcap S_i\vdash_{\textsf{A}}\alpha_i\) but \(\bigcap S_i\not\vdash_{\textsf{A}}\bot\), again by definition of \(\Sigma_{a_i}^n\) it follows that \((\alpha_i\Rrightarrow_{a_i}\bot)\not\in\Gamma\). Also, since \(\Gamma\in\mathcal{K}_m\), by definition of \(\Sigma_{a_i}^n(\Gamma)\) we have \(S_i\subseteq\mathcal{K}_{m-1}\), which means that \(\text{md}(\alpha_i)\le m-1\), and thus \(\text{md}(\alpha_i\Rrightarrow_{a_i}\bot)\le m\). Since \(\Gamma\in\mathcal{K}_m\) and \((\alpha_i\Rrightarrow_{a_i}\bot)\in\mathcal{L}_\mathcal{A}^{!m}\), from \((\alpha_i\Rrightarrow_{a_i}\bot)\not\in\Gamma\) we can conclude by the completeness condition on \(\Gamma\) that \(\neg(\alpha_i\Rrightarrow_{a_i}\bot)\in\Gamma\), that is, \(\diamondplus_{a_i}\alpha_i\in\Gamma\). So, for each \(i\le k\) we have \(\diamondplus_{a_i}\alpha_i\in\Gamma\). But now, by deductive closure relative to \(\mathcal{L}_{\mathcal{A}}^{!m}\), \(\Gamma\) contains both the axiom \[\diamondplus_1\alpha_1\land\dots\land\diamondplus_{k-1}\alpha_{k-1}\to\neg\diamondplus_k\neg(\alpha_1\land\dots\land\alpha_{k-1})\] and its antecedent. So, \(\Gamma\) must contain the consequent, \(\neg\diamondplus_k\neg(\alpha_1\land\dots\land\alpha_{k-1})\).

On the other hand, from \(\alpha_1,\dots,\alpha_k\vdash_{\textsf{A}}\bot\) we have that \(\alpha_k\vdash_{\textsf{A}}\neg(\alpha_1\land\dots\land\alpha_{k-1})\), and since \(\alpha_k\in\bigcap S_k\), also \(\neg(\alpha_1\land\dots\land\alpha_{k-1})\in\bigcap S_k\). Reasoning again as in the previous paragraph, from this and the fact that \(S_k\in\Sigma_{a_k}^n(\Gamma)\) we may conclude that \(\Gamma\) contains \(\diamondplus_k\neg(\alpha_1\land\dots\land\alpha_{k-1})\).

So, \(\Gamma\) contains both \(\diamondplus_k\neg(\alpha_1\land\dots\land\alpha_{k-1})\) and the negation of this formula; by deductive closure, it must contain \(\bot\). But this is a contradiction, since \(\Gamma\) is consistent by assumption. Thus, \((*)\) is true.

Thus, \(\bigcap S_1 \cup \dots \cup \bigcap S_k\) is a consistent subset of \(\mathcal{L}_\mathcal{A}^{!m-1}\). By Lemma 1 there is a \(\Delta\in\mathcal{K}_{m-1}\) with \(\bigcap S_1\cup\dots\cup\bigcap S_k\subseteq \Delta\). To conclude, we show that \(\Delta\in S_1\cap \dots\cap S_k\), which implies that \(S_1\cap \dots\cap S_k\neq\emptyset\).

Take any \(i\le k\). We know that \(\bigcap S_i\subseteq\Delta\) and we want to prove \(\Delta\in S_i\). Towards a contradiction, suppose that \(\Delta\not\in S_i\). By Lemma 2, we know that \(S_i\) is a finite set, \(S_i=\{\Theta_1,\dots,\Theta_\ell\}\) for some \(\ell\) and \(\Theta_1,\dots,\Theta_\ell\in\mathcal{K}_{m-1}\). For \(j\le\ell\), \(\Theta_j\neq\Delta\) and therefore we can find \(\theta_j\in\mathcal{L}_{\mathcal{A}}^{!m-1}\) with \(\theta_j\in\Theta_j\) and \(\neg\theta_j\in\Delta\). Now let \(\theta=\theta_1\lor\dots\lor\theta_\ell\). We have \(\theta\in\bigcap S_i\) but \(\theta\not\in\Delta\), which is a contradiction since \(\bigcap S_i\subseteq\Delta\). ◻

Finally, we can now put everything together and establish completeness.

Proof of Theorem 3, left-to-right.. Suppose \(\not\vdash_{\textsf{A}}\varphi\) and let \(n=\text{md}(\varphi)\). By Lemma 4, we have that \(\bigcap \mathcal{K}_n\not\vdash_{\textsf{A}}\varphi\), which by Lemma 7 implies \(M_n,\mathcal{K}_n\not\models\varphi\). By Lemma 8, there is a CGM \(\mathcal{M}_n\) that induces \(M_n\), and so we have \(\mathcal{M}_n,\mathcal{K}_n\not\models\varphi\). Since \(\varphi\) can be falsified in some CGM, \(\not\models_{\textsf{InqAL}}\varphi\). ◻

Note that the proof yields, for any \(\varphi\) which is not provable in \(\vdash_{\textsf{A}}\), a finite countermodel. Therefore, our proof also establishes the finite model property of InqAL. In turn, the finite model property together with our (recursive) axiomatization yields the decidability of InqAL.

Corollary 1 (Finite model property). If \(\not\models_{\textsf{InqAL}}\varphi\), \(\varphi\) can be refuted within a finite cg-model.

Corollary 2 (Decidability). The problem of deciding if a given \(\varphi\in\mathcal{L}_{\mathcal{A}}\) is valid in \(\textsf{InqAL}\) is decidable.

6 Connection with Socially Friendly Coalition Logic↩︎

In this section we relate InqALto Socially Friendly Coalition Logic (SFCL) [@GorankoEnqvist:18], a generalization of coalition logic [@Pauly:02] developed by Goranko and Enqvist based on instantial neighborhood logic [@Benthem:17]. Modal formulas in SFCL have the form \([C](\sigma;\pi_1,\dots,\pi_n)\) where \(C\subseteq\mathcal{A}\) and \(\sigma,\pi_1,\dots,\pi_n\) are formulas. The primitive connectives are \(\neg\) and \(\lor\). To compare it with InqAL, we restrict to the individual-agent fragment of SFCL, where \(C\) is a singleton \(\{a\}\), which we may identify with the agent \(a\).¹¹ Formulas are interpreted relative to CGMs in a standard truth-conditional fashion. The clause for modal formulas is as follows: \[\mathcal{M},w\Vdash[a](\sigma;\pi_1,\dots,\pi_n)\iff \exists\tau_a\in\textsf{act}(a,w):O_a(w,\tau_a)\subseteq|\sigma|_\mathcal{M}\text{ and }O_a(w,\tau_a)\cap|\pi_i|_\mathcal{M}\neq\emptyset\text{ for }i\le n\] Based on the observations in §4, we can define a translation \((\cdot)^*\) from the individual-agent fragment of SFCL to InqALin the following way: \(p^*=p\); \((\neg\varphi)^*=\neg\varphi^*\); \((\varphi\lor\psi)^*=\varphi^*\lor\psi^*\); and, finally: \[[a](\sigma;\pi_1,\dots,\pi_n)^*=\neg(\sigma^*\Rrightarrow_{a}\!\neg\pi_1^*\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\dots\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\neg\pi_n^*)\] It is easy to check that the translation \(\sigma^*\) of a SFCL-formula is always a declarative with the same truth conditions as \(\sigma\). Translating in the opposite direction, from InqALto SFCL, is more tricky. First, since the language of SFCL includes only statements, we can only expect to faithfully translate declaratives, and not arbitrary formulas. Moreover, even though \(\varphi\Rrightarrow_{a}\!\psi\) is a declarative, the formulas \(\varphi\) and \(\psi\) need not be declarative, and so, they need not have a translation. Still, we can cook up a translation via their resolutions. We define a translation from the declarative fragment of InqALto SFCL as follows: \(p^\star=p\); \(\bot^\star=(p\land\neg p)\) for an arbitrary \(p\in\mathcal{P}\); \((\alpha\land\beta)^\star=\alpha^\star\land\beta^\star\); \((\alpha\to\beta)^\star=\neg(\alpha^\star\land\neg\beta^\star)\); and, crucially, \[(\varphi\Rrightarrow_{a}\!\psi)^\star=\bigwedge_{i=1}^n\neg[a](\alpha_i^\star;\neg\beta_1^\star,\dots,\neg\beta_m^\star)\] where \(\{\alpha_1,\dots,\alpha_n\}=\mathcal{R}(\varphi)\) and \(\{\beta_1,\dots,\beta_m\}=\mathcal{R}(\psi)\). One can prove that for any declarative \(\alpha\in\mathcal{L}_{\mathcal{A}}^!\), \(\alpha\) and its translation \(\alpha^*\) have the same truth conditions. The proof is identical to the one given for the translation of InqNLinto instantial neighborhood logic (Proposition 10.2 in [@Ciardelli:25neighborhood]).

In sum, InqALand SFCL are equi-expressive with respect to statements about individual agents. Still, the way things are expressed in these logics is rather different. Note, in particular, that the number of resolutions \(\mathcal{R}(\varphi)\) of a formula \(\varphi\) can grow exponentially relative to the size of \(\varphi\), and thus, so can the length of the translation of a modal formula containing \(\varphi\). It is plausible to conjecture that this blowup is unavoidable, and so, that InqALis in general exponentially more succinct than SFCL. It is also worth noting that there is currently no complete axiomatization of SFCL (an axiomatization is presented in [@GorankoEnqvist:18], but by the authors’ admission (p.c.) the completeness proof contains a mistake). It can be hoped that our Theorem 1 can be used to establish completeness at least for the individual-agent fragment of SFCL.

7 Conclusions and future work↩︎

We have motivated and investigated InqAL, a logic that allows us to reason not only about what agents can force through their actions, but also about what they enable or determine. An obvious goal for future work is to generalize InqALfrom individual agents to coalitions. Semantically, this is straightforward. The difficulty lies in establishing a characterization theorem analogous to Theorem 1, which played a crucial role in our proof of completeness and decidability. A further important goal is to extend InqALwith temporal operators, yielding an inquisitive version of strategic multi-agent logics like ATL [@Alur:02; @GorankoDrimmelen:06]. In a different direction, it would be interesting to ask if InqAL, or an extension, can regiment claims to the effect that an agent can partly influence (though perhaps not fully determine) the answer to a question.

7.0.0.1 Acknowledgements.

Funding from the European Research Council (ERC) under the Horizon Europe research and innovation programme (Project InqML, Grant Agreement No.) is gratefully acknowledged. Thanks to Valentin Goranko for detailed discussions on this topic, and to four anonymous reviewers for precious comments and suggestions.

8 Appendix: Proofs of standard results↩︎

8.1 Preliminaries↩︎

We start with some basic results about derivability and resolutions. Essentially the same results appear in many completeness results for inquisitive propositional logic [@Ciardelli:23book] and inquisitive modal logics [@Ciardelli:14aiml; @Ciardelli:18aiml; @Ciardelli:25neighborhood]. In each case, we outline the proof and provide a reference where an analogous proof is spelled out.

Lemma 9 (Provable normal form). For all \(\varphi\in\mathcal{L}_{\mathcal{A}}\), \(\varphi\dashv\vdash_{\textsf{A}}\mathlarger{\mathbin{{\setminus}\mspace{-5mu}{\setminus}}/}\mathcal{R}(\varphi)\).

Proof. This uses only the propositional component of the axiomatization. See Lemma 4.3.8 in [@Ciardelli:23book]. ◻

Lemma 10. For all \(\varphi\in\mathcal{L}_{\mathcal{A}}\), if \(\vdash_{\textsf{A}}\varphi\) then \(\vdash_{\textsf{A}}\alpha\) for some \(\alpha\in\mathcal{R}(\varphi)\).

Proof. It suffices to check that this property holds for axioms and is preserved by inference rules. When an axiom is a declarative \(\alpha\), the claim is trivially true since \(\mathcal{R}(\alpha)=\{\alpha\}\). Since all our modal axioms are declaratives, the only axioms we need to check are the propositional ones. This is a simple and standard exercise (see the proof of Lemma 5.6 in [@Ciardelli:18aiml]). As for the inference rules, if \(\varphi\) was obtained by Conditional Necessitation then \(\varphi\) is declarative and the claim is trivially true. If \(\varphi\) was obtained by Modus Ponens from \(\psi\) and \(\psi\to\varphi\), then by induction hypothesis some resolutions \(\alpha\in\mathcal{R}(\psi)\) and \(\beta\in\mathcal{R}(\psi\to\varphi)\) are derivable. By definition of resolutions of an implication, \(\beta\) is a conjunction with one conjunct of the form \(\alpha\to\gamma\) where \(\gamma\in\mathcal{R}(\varphi)\). Since \(\alpha\) and \(\alpha\to\gamma\) are derivable, \(\gamma\) is derivable by Modus Ponens. ◻

Lemma 11. If \(\Gamma\subseteq\mathcal{L}_{\mathcal{A}}^!\) and \(\Gamma\vdash_{\textsf{A}}\varphi\), then \(\Gamma\vdash_{\textsf{A}}\alpha\) for some \(\alpha\in\mathcal{R}(\varphi)\)

Proof. If \(\Gamma\vdash_{\textsf{A}}\varphi\), this means that there is a finite subset \(\Gamma_0\subseteq\Gamma\) such that \(\bigwedge\Gamma_0\to\varphi\) is derivable. Let \(\gamma=\bigwedge\Gamma_0\). Since \(\Gamma\) is a set of declaratives, \(\gamma\) is a declarative, so \(\mathcal{R}(\gamma)=\{\gamma\}\). Then, by definition of resolutions \(\mathcal{R}(\gamma\to\varphi)=\{\gamma\to\alpha\mid\alpha\in\mathcal{R}(\varphi)\}\). By the previous lemma, since \(\gamma\to\varphi\) is derivable, some particular resolution \(\gamma\to\alpha\) is derivable. This implies that \(\Gamma\vdash_{\textsf{A}}\alpha\), and since \(\alpha\in\mathcal{R}(\varphi)\) we are done. ◻

Definition 10 (Resolutions for sets). A resolution function* for a set \(\Phi\subseteq\mathcal{L}_{\mathcal{A}}\) is a function \(f\) assigning to each \(\varphi\in\Phi\) a corresponding resolution \(\alpha\in\mathcal{R}(\varphi)\). The image of \(\Phi\) under a resolution function is called a resolution of \(\Phi\). More formally, the set of resolutions of \(\varphi\) is defined in the following way: \(\mathcal{R}(\Phi)=\{f[\Phi]\mid f\text{ a resolution function for }\Phi\}\). Note that if \(\Gamma\in\Phi\), then for each \(\varphi\in\Phi\) there is some resolution \(\alpha\in\mathcal{R}(\varphi)\) with \(\alpha\in\Gamma\).*

Lemma 12. If \(\Phi,\Psi\subseteq\mathcal{L}_{\mathcal{A}}\) and \(\Phi\not\vdash_{\textsf{A}}\Psi\), then \(\Gamma\not\vdash_{\textsf{A}}\Psi\) for some \(\Gamma\in\mathcal{R}(\Phi)\).

Proof. Repeated application of Lemma 9, by standard properties of \(\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\). See Lemma 4.3.7 in [@Ciardelli:23book]. ◻

8.2 Intersection Lemma (Lemma 4)↩︎

Consider a set of declaratives \(\Delta\subseteq\mathcal{L}_{\mathcal{A}}^{!n}\) and its corresponding set of \(n\)-bounded complete extensions, \(S_\Delta^n=\{\Gamma\in\mathcal{K}_n\mid\Delta\subseteq\Gamma\}\). We want to show that for all \(\varphi\in\mathcal{L}_{\mathcal{A}}^n\): \(\Delta\vdash_{\textsf{A}}\varphi\iff\bigcap S_\Delta^n\vdash_{\textsf{A}}\varphi\).

The direction \(\Rightarrow\) is obvious since \(\Delta\subseteq\bigcap S_\Delta^n\). For the converse, suppose for a contradiction that for some \(\varphi\) we had \(\bigcap S_\Delta^n\vdash_{\textsf{A}}\varphi\) but \(\Delta\not\vdash_{\textsf{A}}\varphi\). Since \(\bigcap S_\Delta^n\) is a set of declaratives, by Lemma 11 we have \(\bigcap S_\Delta^n\vdash_{\textsf{A}}\alpha\) for some \(\alpha\in\mathcal{R}(\varphi)\). Since \(\Delta\not\vdash_{\textsf{A}}\varphi\), it follows by Lemma 9 that \(\Delta\not\vdash_{\textsf{A}}\alpha\). By the axiom \(\neg\neg\alpha\to\alpha\), this implies \(\Delta\not\vdash_{\textsf{A}}\neg\neg\alpha\), and therefore \(\Delta\cup\{\neg\alpha\}\not\vdash_{\textsf{A}}\bot\). Since \(\varphi\in\mathcal{L}_{\mathcal{A}}^n\) we have \(\alpha\in\mathcal{L}_{\mathcal{A}}^{!n}\) and thus also \(\Delta\cup\{\neg\alpha\}\subseteq\mathcal{L}_{\mathcal{A}}^{!n}\). So by Lemma 1 there is \(\Gamma\in\mathcal{K}_n\) such that \(\Delta\cup\{\neg\alpha\}\subseteq\Gamma\). Now since \(\Gamma\in S_\Delta^n\) and \(\bigcap S_\Delta^n\vdash_{\textsf{A}}\alpha\) we have \(\Gamma\vdash_{\textsf{A}}\alpha\). So we have \(\Gamma\vdash_{\textsf{A}}\neg\alpha\) and \(\Gamma\vdash_{\textsf{A}}\alpha\), whence \(\Gamma\vdash_{\textsf{A}}\bot\) and, by deductive closure relative to \(\mathcal{L}_{\mathcal{A}}^{!n}\), \(\bot\in\Gamma\). But this is a contradiction since \(\Gamma\in\mathcal{K}_n\) is consistent by assumption.\(\Box\)

8.3 Existence Lemma (Lemma 5)↩︎

We follow closely the proof of Lemma 6.12 in [@Ciardelli:25neighborhood], adapting it to our multi-agent setting and to our modal depth-bounded canonical model construction. We first establish some preliminary results.

Let \(\Gamma\) be an \(n\)CTD, with \(n>0\). Given two sets \(\Phi,\Psi\subseteq\mathcal{L}_\mathcal{A}^{n-1}\), we write \({\Phi\Rrightarrow_\Gamma^a\Psi}\) if there are finite subsets \(\Phi_0\subseteq\Phi\) and \(\Psi_0\subseteq\Psi\) such that the formula \(\bigwedge\Phi_0\Rrightarrow_{a}\!\mathlarger{\mathbin{{\setminus}\mspace{-5mu}{\setminus}}/}\Psi_0\) is in \(\Gamma\). Note the following fact.

Lemma 13. If \(\Phi,\Psi\subseteq\mathcal{L}_\mathcal{A}^{n-1}\) and \(\Phi\vdash_{\textsf{A}}\Psi\), then \(\Phi\Rrightarrow_\Gamma^a\Psi\).

Proof. If \(\Phi\vdash_{\textsf{A}}\Psi\), there are finite subsets \(\Phi_0\subseteq\Phi\) and \(\Psi_0\subseteq\Psi\) such that \(\vdash_{\textsf{A}}\bigwedge\Phi_0\to\mathlarger{\mathbin{{\setminus}\mspace{-5mu}{\setminus}}/}\Psi_0\). By Conditional Necessitation, also \(\vdash_{\textsf{A}}\bigwedge\Phi_0\Rrightarrow_{a}\!\mathlarger{\mathbin{{\setminus}\mspace{-5mu}{\setminus}}/}\Psi_0\). Since \(\Phi,\Psi\subseteq\mathcal{L}_\mathcal{A}^{n-1}\), the modal depth of the formula \(\Phi_0\Rrightarrow_{a}\!\mathlarger{\mathbin{{\setminus}\mspace{-5mu}{\setminus}}/}\Psi_0\) is at most \(n\), and so by deductive closure, this formula must be in \(\Gamma\), witnessing \(\Phi\Rrightarrow_\Gamma^a\Psi\). ◻

Importantly, the relation \(\Rrightarrow_\Gamma^a\) also enjoys the following cut-like property.

Lemma 14. For any two sets \(\Phi,\Psi\subseteq\mathcal{L}_\mathcal{A}^{n-1}\) and formula \(\chi\in\mathcal{L}_\mathcal{A}^{n-1}\): \(\Phi\cup\{\chi\}\Rrightarrow_\Gamma^a\Psi\) and \(\Phi\Rrightarrow_\Gamma^a\Psi\cup\{\chi\}\) implies \(\Phi\Rrightarrow_\Gamma^a\Psi\).

Proof. Suppose \(\Phi\cup\{\chi\}\Rrightarrow_\Gamma^a\Psi\) and \(\Phi\Rrightarrow_\Gamma^a\Psi\cup\{\chi\}\). This means that there are finite sets of formulas \(\Phi_0,\Phi_1\subseteq\Phi\) and \(\Psi_0,\Psi_1\subseteq\Psi\) such that \(\Gamma\) contains the following formulas: \[(\chi\land\bigwedge\Phi_0)\Rrightarrow_{a}\!\mathlarger{\mathbin{{\setminus}\mspace{-5mu}{\setminus}}/}\Psi_0\qquad\qquad \bigwedge\Phi_1\Rrightarrow_{a}\!(\chi\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\mathlarger{\mathbin{{\setminus}\mspace{-5mu}{\setminus}}/}\Psi_1)\] We prove that \(\Gamma\) must contain \(\bigwedge(\Phi_0\cup\Phi_1)\Rrightarrow_{a}\!\mathlarger{\mathbin{{\setminus}\mspace{-5mu}{\setminus}}/}(\Psi_0\cup\Psi_1)\), thus witnessing \({\Phi\Rrightarrow_\Gamma^a\Psi}\). To ease notation, we spell out the details for the case in which the relevant sets are all singletons \(\Phi_0=\{\varphi_0\},\Phi_1=\{\varphi_1\},\Psi_0=\{\psi_0\},\Psi_1=\{\psi_1\}\), but the general case is analogous.

So, we know that \(\Gamma\) contains the formulas \((\varphi_1\land\chi\Rrightarrow_{a}\!\psi_1)\) and \((\varphi_2\Rrightarrow_{a}\!\psi_2\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\chi)\), and we want to show that it contains \((\varphi_1\land\varphi_2\Rrightarrow_{a}\!\psi_1\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi_2)\). Since this formula is a declaratives with modal depth \(\le n\), and since \(\Gamma\) is closed under deduction relative to such formulas, it suffices to show that: \[(\varphi_1\land\chi\Rrightarrow_{a}\!\psi_1),(\varphi_2\Rrightarrow_{a}\!\psi_2\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\chi)\vdash_{\textsf{A}}(\varphi_1\land\varphi_2\Rrightarrow_{a}\!\psi_1\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi_2)\] A derivation is given in Figure [fig:derivation]. In the derivation, we indicate explicitly only the modal axioms and rules involved in the reasoning, omitting reference to propositional axioms. We write \((\texttt{MP})\) to indicate modus ponens and \((\texttt{CN})\) for conditional necessitation. For simplicity, we use the formulas \((\varphi_1\land\chi\Rrightarrow_{a}\!\psi_1)\) and \((\varphi_2\Rrightarrow_{a}\!\psi_2\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\chi)\) as if they were premises; this is legitimate since we will not use the conditional necessitation rule (CN) on these formulas or anything inferred from them. Rewriting the argument with the relevant formulas used throughout as conditional antecedents is tedious but straightforward. ◻

Figure 2: Sketch of a proof showing (\varphi_1\land\chi\Rrightarrow_{a}\!\psi_1),(\varphi_2\Rrightarrow_{a}\!\psi_2\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\chi)\vdash_{\textsf{A}}(\varphi_1\land\varphi_2\Rrightarrow_{a}\!\psi_1\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi_2) — Figure 2: Sketch of a proof showing \((\varphi_1\land\chi\Rrightarrow_{a}\!\psi_1),(\varphi_2\Rrightarrow_{a}\!\psi_2\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\chi)\vdash_{\textsf{A}}(\varphi_1\land\varphi_2\Rrightarrow_{a}\!\psi_1\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\psi_2)\)

Lemma 15 (Splitting lemma). Let \(\Gamma\) be a \(n\)CTD with \(n>0\) and take \(\Phi,\Psi\subseteq\mathcal{L}_\mathcal{A}^{n-1}\) with \(\Phi\not\Rrightarrow_\Gamma^a\Psi\). The set \(\mathcal{L}_\mathcal{A}^{n-1}\) can be partitioned into sets \(\textsf{L}\) and \(\textsf{R}\) such that \(\Phi\subseteq\textsf{L}\), \(\Psi\subseteq\textsf{R}\), and \(\textsf{L}\not\Rrightarrow_\Gamma^a\textsf{R}\).

Proof. Fix an enumeration \((\chi_i)_{i\in\mathbb{N}}\) of \(\mathcal{L}_\mathcal{A}^{n-1}\). Define a sequence of sets \((\textsf{L}_i)_{i\in\mathbb{N}}\) and \((\textsf{R}_i)_{i\in\mathbb{N}}\) as follows:

\(\textsf{L}_0=\Phi, \textsf{R}_0=\Psi\)
if \(\textsf{L}_i\cup\{\chi_i\}\not\Rrightarrow_\Gamma^a\textsf{R}_i\) we let \(\textsf{L}_{i+1}:=\textsf{L}_i\cup\{\chi_i\}\) and \(\textsf{R}_{i+1}=\textsf{R}_i\)
if \(\textsf{L}_i\cup\{\chi_i\}\Rrightarrow_\Gamma^a\textsf{R}_i\) we let \(\textsf{L}_{i+1}:=\textsf{L}_i\) and \(\textsf{R}_{i+1}=\textsf{R}_i\cup\{\chi_i\}\)

We show by induction on \(i\) that \(\textsf{L}_i\not\Rrightarrow_\Gamma^a\textsf{R}_i\). For \(n=0\) this is true by assumption. Now suppose this is true for \(i\) and consider \(i+1\). If \(\textsf{L}_i\cup\{\chi_i\}\not\Rrightarrow_\Gamma^a\textsf{R}_i\), the claim is obvious by definition of \(\textsf{L}_{i+1}\) and \(\textsf{R}_{i+1}\). So, suppose \(\textsf{L}_i\cup\{\chi_i\}\Rrightarrow_\Gamma^a\textsf{R}_i\). Since by induction hypothesis \(\textsf{L}_i\not\Rrightarrow_\Gamma^a\textsf{R}_i\), Lemma 14 implies \(\textsf{L}_i\not\Rrightarrow_\Gamma^a\textsf{R}_i\cup\{\chi_i\}\), which by definition amounts to \(\textsf{L}_{i+1}\not\Rrightarrow_\Gamma^a\textsf{R}_{i+1}\).

Now let \(\textsf{L}=\bigcup_{i\in\mathbb{N}}\textsf{L}_i\) and \(\textsf{R}=\bigcup_{i\in\mathbb{N}}\textsf{R}_i\). By construction, \(\Phi\subseteq\textsf{L}\) and \(\Psi\subseteq\textsf{R}\). We have \(\textsf{L}\not\Rrightarrow_\Gamma^a\textsf{R}\), otherwise there would be an \(i\in\mathbb{N}\) such that \(\textsf{L}_i\Rrightarrow_\Gamma^a\textsf{R}_i\), contrary to what we just saw. Moreover, \(\textsf{L}\) and \(\textsf{R}\) form a partition of \(\mathcal{L}_\mathcal{A}^{n-1}\). By construction, every formula of \(\mathcal{L}_\mathcal{A}^{n-1}\) occurs in either set. Moreover, no formula cannot occur in both: to see why, suppose for a contradiction that for some \(\chi\in\mathcal{L}_\mathcal{A}^{n-1}\) we have \(\chi\in\textsf{L}\cap\textsf{R}\); since \(\chi\Rrightarrow_{a}\!\chi\) is a valid declarative with modal depth \(\le n\), and since \(\Gamma\) is deductively closed with respect to such formulas, we would need to have \((\chi\Rrightarrow_{a}\!\chi)\in\Gamma\), contradicting \(\textsf{L}\Rrightarrow_\Gamma^a\textsf{R}\). ◻

With these preliminaries at hand, we are now ready to complete the proof of the existence lemma.

Proof of Lemma 5. Let \(\Gamma\) be an \(n\)CTD with \(\neg(\varphi\Rrightarrow_{a}\!\psi)\in\Gamma\). This implies \(n>0\) (otherwise \(\Gamma\) would contain only propositional formulas) and furthermore \(\varphi\) and \(\psi\) must be in \(\mathcal{L}_\mathcal{A}^{n-1}\). Since \(\Gamma\) is consistent, \((\varphi\Rrightarrow_{a}\!\psi)\not\in\Gamma\), and so \(\{\varphi\}\not\Rrightarrow_\Gamma^a\{\psi\}\). Now extend \(\{\varphi\}\) and \(\{\psi\}\) to sets \(\textsf{L}\) and \(\textsf{R}\) as in the previous lemma.

Since \(\textsf{L}\not\Rrightarrow_\Gamma^a\textsf{R}\), by Lemma 13 we have \(\textsf{L}\not\vdash_{\textsf{A}}\textsf{R}\). By Lemma 12 there is a set \(\Delta\in\mathcal{R}(\textsf{L})\) with \(\Delta\not\vdash_{\textsf{A}}\textsf{R}\). Since \(\textsf{L}\subseteq\mathcal{L}_\mathcal{A}^{n-1}\), we have \(\Delta\subseteq\mathcal{L}_\mathcal{A}^{!n-1}\). We can now take \(S=S_\Delta^{n-1}=\{\Gamma'\in\mathcal{K}_{n-1}\mid \Delta\subseteq\Gamma'\}\). We need to verify that (i) \(\bigcap S\vdash_{\textsf{A}}\varphi\), (ii) \(\bigcap S\not\vdash_{\textsf{A}}\psi\) and (iii) \(S\in\Sigma_a^n(\Gamma)\).

For (i), we have \(\varphi\in\textsf{L}\). Since \(\Delta\in\mathcal{R}(\textsf{L})\), for some \(\alpha\in\mathcal{R}(\varphi)\) we have \(\alpha\in\Delta\). By Lemma 9, \(\Delta\vdash_{\textsf{A}}\varphi\), and thus, since \(\varphi\in\mathcal{L}_\mathcal{A}^{n-1}\), by Lemma 4 also \(\bigcap S\vdash_{\textsf{A}}\varphi\).
For (ii), we have \(\psi\in\textsf{R}\). Since \(\Delta\not\vdash_{\textsf{A}}\textsf{R}\), also \(\Delta\not\vdash_{\textsf{A}}\psi\). Since \(\psi\in\mathcal{L}_\mathcal{A}^{n-1}\), Lemma 4 gives \(\bigcap S\not\vdash_{\textsf{A}}\psi\).
For (iii), first note that since \(\Delta\not\vdash_{\textsf{A}}\textsf{R}\), we have \(\Delta\not\vdash_{\textsf{A}}\bot\), so by Lemma 1, \(S\neq\emptyset\). Next, suppose \((\chi\Rrightarrow_{a}\!\xi)\in\Gamma\) and \(\bigcap S\vdash_{\textsf{A}}\chi\). We need to show that \(\bigcap S\vdash_{\textsf{A}}\xi\). Since \((\chi\Rrightarrow_{a}\!\xi)\in\Gamma\) and \(\Gamma\in\mathcal{K}_n\) we have \(\chi,\xi\in\mathcal{L}_\mathcal{A}^{n-1}\). Since \(\bigcap S\vdash_{\textsf{A}}\chi\) and \(\chi\in\mathcal{L}_\mathcal{A}^{n-1}\), Lemma 4 gives \(\Delta\vdash_{\textsf{A}}\chi\). Since by construction \(\Delta\not\vdash_{\textsf{A}}\textsf{R}\), it follows that \(\chi\not\in\textsf{R}\), and since \(\textsf{R}\) and \(\textsf{L}\) partition the set \(\mathcal{L}_\mathcal{A}^{n-1}\) we have \(\chi\in\textsf{L}\). Now we must have \(\xi\in\textsf{L}\) as well, for if we had \(\xi\in\textsf{R}\) it would follow from \((\chi\Rrightarrow_{a}\!\xi)\in\Gamma\) that \(\textsf{L}\Rrightarrow_\Gamma^a\textsf{R}\), contrary to what we know. Since \(\xi\in\textsf{L}\) and \(\Delta\in\mathcal{R}(\textsf{L})\), for some \(\alpha\in\mathcal{R}(\xi)\) we have \(\alpha\in\Delta\), so by Lemma 9, \(\Delta\vdash_{\textsf{A}}\xi\). Finally, since \(\xi\in\mathcal{L}_\mathcal{A}^{n-1}\), Lemma 4 implies \(\bigcap S\vdash_{\textsf{A}}\xi\), as desired.\(\Box\)

8.4 Range Lemma (Lemma 6)↩︎

We follow the proof of Lemma 6.15 in [@Ciardelli:25neighborhood], adapting it to our multi-agent and depth-bounded setting.

Consider a \(\Gamma\in\mathcal{K}_{m}\) with \(m>0\). We want to show the identity: \[\bigcup\Sigma_a^n(\Gamma)=\{\Gamma'\in\mathcal{K}_{m-1}\mid\forall\alpha\in\mathcal{L}_{\mathcal{A}}^!:\boxplus_a\alpha\in\Gamma\text{ implies }\alpha\in\Gamma'\}\]

Proof. \((\subseteq)\) Suppose \(\Gamma'\in\bigcup\Sigma_a^n(\Gamma)\), that is, \(\Gamma'\in S\) for some \(S\in\Sigma_a^n(\Gamma)\). By definition of \(\Sigma_a^n\), since \(\Gamma\in\mathcal{K}_m\) we have \(\Gamma'\in\mathcal{K}_{m-1}\). Now let \(\alpha\) be a declarative and suppose \(\boxplus_a\alpha\in\Gamma\), that is, \((\top\Rrightarrow_{a}\!\alpha)\in\Gamma\). Since \(S\in\Sigma_a^n(\Gamma)\) and \(\bigcap S\vdash_{\textsf{A}}\top\), it follows that \(\bigcap S\vdash_{\textsf{A}}\alpha\). Since \(\Gamma'\in S\), we have \(\bigcap S\subseteq\Gamma'\), and so also \(\Gamma'\vdash_{\textsf{A}}\alpha\). Since \(\boxplus_a\alpha\in\Gamma\) and \(\Gamma\in\mathcal{K}_m\), it follows that \(\alpha\in\mathcal{L}_\mathcal{A}^{!m-1}\). Since \(\Gamma'\vdash_{\textsf{A}}\alpha\) and \(\Gamma'\) is closed under deduction relative to \(\mathcal{L}_\mathcal{A}^{!m-1}\), we have \(\alpha\in\Gamma'\).

\((\supseteq)\) Consider \(\Gamma'\in\mathcal{K}_{m-1}\) and suppose for all \(\alpha\in\mathcal{L}_{\mathcal{A}}^!\), \(\boxplus_a\alpha\in\Gamma\text{ implies }\alpha\in\Gamma'\). We must show that \(\Gamma'\in S\) for some \(S\in\Sigma_a^n(\Gamma)\). First, we claim that \(\emptyset\not\Rrightarrow_\Gamma^a\{\neg\alpha\mid\alpha\in\Gamma'\}\). Towards a contradiction, suppose not: then there are \(\alpha_1,\dots,\alpha_n\in\Gamma'\) such that \((\top\Rrightarrow_{a}\!\neg\alpha_1\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\dots\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\neg\alpha_n)\in\Gamma\). Since \(\neg\alpha_1\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\dots\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\neg\alpha_n\vdash_{\textsf{A}}\neg(\alpha_1\land\dots\land\alpha_n)\), by Conditional Necessitation and Transitivity we have \((\top\Rrightarrow_{a}\!\neg\alpha_1\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\dots\mathbin{\rotatebox[origin=c]{-90}{\geqslant}}\neg\alpha_n)\vdash_{\textsf{A}}(\top\Rrightarrow_{a}\!\neg(\alpha_1\land\dots\land\alpha_n))\). Since \((\top\Rrightarrow_{a}\!\neg(\alpha_1\land\dots\land\alpha_n))\in\mathcal{L}_\mathcal{A}^{m}\) and \(\Gamma\) is deductively closed with respect to \(\mathcal{L}_\mathcal{A}^m\), we conclude \((\top\Rrightarrow_{a}\!\neg(\alpha_1\land\dots\land\alpha_n))\in\Gamma\), that is, \(\boxplus_a\neg(\alpha_1\land\dots\land\alpha_n)\in\Gamma\). By our assumption on \(\Gamma'\), we must have \(\neg(\alpha_1\land\dots\land\alpha_n)\in\Gamma'\). But this is impossible, since each \(\alpha_i\) is in \(\Gamma'\) and \(\Gamma'\) is consistent.

We have thus established the claim \(\emptyset\not\Rrightarrow_\Gamma^a\{\neg\alpha\mid\alpha\in\Gamma'\}\). By Lemma 15, we can partition the language \(\mathcal{L}_\mathcal{A}^{m-1}\) into sets \(\textsf{L},\textsf{R}\) with \(\textsf{L}\not\Rrightarrow_\Gamma^a\textsf{R}\) and \(\{\neg\alpha\mid\alpha\in\Gamma'\}\subseteq\textsf{R}\). Reasoning as in the previous lemma, we can find a \(\Delta\in\mathcal{R}(\textsf{L})\) with \(\Delta\not\vdash\textsf{R}\), and we can show that the corresponding set of \(m-1\)-bounded complete extensions \(S_\Delta^{m-1}\) is in \(\Sigma_a^n(\Gamma)\). We now claim that \(\Gamma'\in S_\Delta^{m-1}\). To show this, it suffices to show that \(\Delta\cup\Gamma'\not\vdash_{\textsf{A}}\bot\): if this holds, it follows by Lemma 1 that there is a \(\Gamma''\in\mathcal{K}_{m-1}\) with \(\Delta\cup\Gamma'\subseteq\Gamma''\). Since two bounded elements of \(\mathcal{K}_{m-1}\) cannot be properly included in one another, we must have \(\Gamma'=\Gamma''\), and therefore \(\Delta\subseteq\Gamma'\), showing that \(\Gamma'\in S_\Delta^{m-1}\) as desired.

So, towards a contradiction, suppose \(\Delta\cup\Gamma'\vdash_{\textsf{A}}\bot\). Since \(\Gamma'\) is closed under conjunction, this means that there is a single formula \(\alpha\in\Gamma'\) such that \(\Delta\cup\{\alpha\}\vdash_{\textsf{A}}\bot\), and so, \(\Delta\vdash_{\textsf{A}}\neg\alpha\). But this is impossible, since by construction \(\neg\alpha\in\textsf{R}\) and \(\Delta\not\vdash\textsf{R}\).

To conclude, we have found a state \(S_\Delta^{m-1}\) such that \(\Gamma'\in S_\Delta^{m-1}\) and \(S_\Delta^{m-1}\in\Sigma_a^n(\Gamma)\), thus showing that \(\Gamma'\in\bigcup \Sigma_a^n(\Gamma)\), as required. ◻

8.5 Support Lemma (Lemma 7)↩︎

We must show that for all \(m\le n\), all formulas \(\varphi\in\mathcal{L}_\mathcal{A}^m\), and all non-empty states \(S\subseteq\mathcal{K}_m\) we have \[M_n,S\models\varphi\iff\bigcap S\vdash_{\textsf{A}}\varphi\] The proof is by induction on \(\varphi\), simultaneously for all \(S\subseteq\mathcal{K}_m\). The cases for atoms and connectives are standard (see the proof of Lemma 4.3.15 in [@Ciardelli:23book]). We spell out the inductive step for a modal formula \(\varphi=(\psi\Rrightarrow_{a}\!\chi)\). Note that since we are assuming \(\varphi\in\mathcal{L}_\mathcal{A}^m\) we have \(m>0\) and \(\psi,\chi\in\mathcal{L}_\mathcal{A}^{m-1}\).

Suppose \(\bigcap S\vdash_{\textsf{A}}(\psi\Rrightarrow_{a}\!\chi)\). We must show \(M_n,S\models(\psi\Rrightarrow_{a}\!\chi)\). For this, take an arbitrary world \(\Gamma\in S\) and a state \(T\in\Sigma_a^n(\Gamma)\) with \(M_n,T\models\psi\). We need to show that \(M_n,T\models\chi\). By definition of \(\Sigma_a^n\) we have \(T\subseteq\mathcal{K}_{m-1}\). By induction hypothesis on \(\psi\), from \(M_n,T\models\psi\) we obtain \(\bigcap T\vdash_{\textsf{A}}\psi\). Since \(\Gamma\in S\) we have \(\bigcap S\subseteq\Gamma\), and since \(\bigcap S\vdash_{\textsf{A}}(\psi\Rrightarrow_{a}\!\chi)\) also \(\Gamma\vdash(\psi\Rrightarrow_{a}\!\chi)\). Since \((\psi\Rrightarrow_{a}\!\chi)\in\mathcal{L}_\mathcal{A}^{!m}\) and \(\Gamma\in\mathcal{K}_m\), it follows that \((\psi\Rrightarrow_{a}\!\chi)\in\Gamma\). By definition of \(\Sigma_a^n\), from \(T\in \Sigma_a^n(\Gamma)\), \((\psi\Rrightarrow_{a}\!\chi)\in\Gamma\), and \(\bigcap T\vdash_{\textsf{A}}\psi\) we can conclude \(\bigcap T\vdash_{\textsf{A}}\chi\). Finally, by induction hypothesis on \(\chi\), this gives \(M_n,T\models\chi\), as required.

For the converse, suppose \(\bigcap S\not\vdash_{\textsf{A}}(\psi\Rrightarrow_{a}\!\chi)\). Then there is some \(\Gamma\in S\) such that \((\psi\Rrightarrow_{a}\!\chi)\not\in\Gamma\). Since \((\psi\Rrightarrow_{a}\!\chi)\in\mathcal{L}_\mathcal{A}^{m}\) and \(\Gamma\in\mathcal{K}_m\), by completeness we have \(\neg(\psi\Rrightarrow_{a}\!\chi)\in\Gamma\). By the Existence Lemma (Lemma 5) there is a state \(T\in\Sigma_a^m(\Gamma)\) such that \(\bigcap T\vdash_{\textsf{A}}\psi\) and \(\bigcap T\not\vdash_{\textsf{A}}\chi\). By induction hypothesis on \(\psi\) and \(\chi\), this means that \(M_n,T\models\psi\) and \(M_n,T\not\models\chi\). Hence, \(M_n,S\not\models(\psi\Rrightarrow_{a}\!\chi)\).\(\Box\)

[@*]

A reviewer asks why it is difficult to extend this result from individual agents to coalitions. The reason is that coalitions can be related to each other by inclusion or overlap; in these cases, there are complex interplays between their effectivity functions.↩︎
When \(k=1\), i.e., in the single-agent case, the characterization is trivial: as the reader can readily verify, a neighborhood frame \(F=(W,\Sigma)\) is induced by a CGS if and only if \(\Sigma(w)\) is a non-empty set of singletons for every \(w\in W\). We therefore focus on the interesting multi-agent case with \(k>1\).↩︎
Given the axiom of choice, it is well-known that any set admits both a well-ordering and a group structure. No appeal to the axiom of choice is needed if \(W\) is finite or countably infinite, as will be the case in our completeness proof in Section 5.↩︎
In this previous work, \(\Box\) is taken as primitive, while here we take it as a defined operator. Either choice has advantages. The advantage of our present choice is that having fewer primitives simplifies the completeness proof below.↩︎
In fact, it is possible to show that the \(\diamondplus\)-fragment of our language is equi-expressive with the fragment of coalition logic that contains only modalities for individual agents. See §3 of [@Ciardelli:25neighborhood] for an analogous result in the case of InqNL.↩︎
Interestingly, exactly the same modal pattern, \(\neg\Box_a\varphi\land\boxplus_a\varphi\) is argued in inquisitive epistemic logic to capture the idea that an agent wonders about, or is interested in, a certain question [@CiardelliRoelofsen:15idel]. It is striking that such seemingly different notions across different modal domains plausibly share the same logical structure. Revealing this common structure is one of the payoffs of the formal analysis of question-oriented modal notions made possible by inquisitive modal logic.↩︎
Recall that we assume that \(\mathcal{A}\) contains at least two agents. If \(\mathcal{A}\) contains a single agent \(a\), an axiomatization of InqALis obtained by following two axioms: (i) \(\diamondplus_a\top\) (existence of actions); (ii) \(\boxplus_a?{\alpha}\) for any declarative \(\alpha\) (determinacy). The former captures the condition that \(\Sigma_a(w)\neq\emptyset\), the latter the condition that each \(s\in\Sigma_a(w)\) is a singleton. As mentioned in Footnote 2, these conditions guarantee that \(\Sigma_a\) is the actual effectivity function of some CGS. The completeness proof for this case follows the one below, except that the proof of the Lemma 8 needs to be adapted. We leave this as an exercise.↩︎
Note that the restriction to declaratives in this axiom is crucial; for instance, \(\boxplus_a{?p}\leftrightarrow\boxplus_b{?p}\) is not valid in InqAL. Alternatively, we may take as axioms all formulas of the form \(\Box_a\varphi\leftrightarrow\Box_b\varphi\); in this case, no restriction is needed.↩︎
An interesting question that we will leave open is whether Theorem 3 can be extended to a strong completeness result.↩︎
To be fully precise, for \(S\subseteq\mathcal{K}_n\), we define \(\bigcap S=\{\alpha\in\mathcal{L}_{\mathcal{A}}^{!n}\mid \alpha\in\Gamma\text{ for all }\Gamma\in S\}\). This definition implies that \(\bigcap\emptyset=\mathcal{L}_{\mathcal{A}}^{!n}\), ensuring that the lemma holds also when we have \(\Delta\vdash_{\textsf{A}}\bot\), and therefore \(S_\Delta^n=\emptyset\). In this case, the sets of formulas \(\Delta\) and \(\bigcap S_\Delta^n=\bigcap \emptyset=\mathcal{L}_{\mathcal{A}}^{!n}\) indeed derive the same formulas from \(\mathcal{L}_{\mathcal{A}}^n\): all of them.↩︎
The connection discussed in this section extends straighforwardly to one between full SFCL and the natural generalization of InqALwith coalitions. The translations would work in the same way, and in particular, the same exponential blowup discussed below would result when translating a formula from the coalitional version of InqALto SFCL.↩︎

Inquisitive Action Logic