Paper deep dive
Inquisitive Action Logic
Ivano Ciardelli
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 99%
Last extracted: 7/5/2026, 1:37:17 AM
Summary
The paper introduces Inquisitive Action Logic (InqAL), a multi-agent modal logic designed to reason about agentive determination. Unlike traditional logics that focus on what an agent can force, InqAL captures what aspects of an outcome an agent determines through their actions, treating determination as a modal claim involving questions. InqAL is a multi-agent extension of inquisitive neighborhood logic (InqNL) based on concurrent game structures (CGS). The authors provide an axiomatization, prove completeness and decidability via the finite model property, and establish a representation theorem for actual effectivity functions, showing that InqAL is expressively equivalent to the individual-agent fragment of socially friendly coalition logic (SFCL).
Entities (6)
Relation Signals (4)
Ivano Ciardelli → authored → Inquisitive Action Logic
confidence 100% · Ivano Ciardelli University of Padua, Italy... Inquisitive Action Logic
Inquisitive Action Logic → isbasedon → Concurrent Game Structure
confidence 100% · InqAL is a multi-agent extension of inquisitive neighborhood logic based on concurrent game structures.
Inquisitive Action Logic → isextensionof → Inquisitive Neighborhood Logic
confidence 100% · InqAL is a multi-agent extension of inquisitive neighborhood logic
Inquisitive Action Logic → isequivalentto → Socially Friendly Coalition Logic
confidence 90% · it is expressively equivalent to the individual-agent fragment of the socially friendly coalition logic
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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, InqAL also 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, InqAL is a multi-agent extension of inquisitive neighborhood logic 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. We present an axiomatization of InqAL and 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.
Tags
Links
- Source: https://arxiv.org/abs/2606.31866v1
- Canonical: https://arxiv.org/abs/2606.31866v1
Trouble viewing inline? Open PDF directly →
Full Text
64,752 characters extracted from source content.
Expand or collapse full text
M. Bílková, M. Gattinger, I. van der Giessen, M. Girlando, Y. Wang (Eds.): Advances in Modal Logic 2026 (AiML 2026) EPTCS 447, 2026, p. 222–241, doi:10.4204/EPTCS.447.13 © I. Ciardelli This work is licensed under the Creative Commons Attribution License. Inquisitive Action Logic Ivano Ciardelli University of Padua, Italy ivano.ciardelli@unipd.it We introduceinquisitive action logic,InqAL, a multi-agent modal logic for reasoning about action. While traditional approaches focus on whatpropertiesof the outcome an agent canforce,InqALalso captures whataspectsof the outcome an agentdeterminesthrough 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 [12] 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 [20]. We present an axiomatization ofInqALand prove completeness and decidability via the finite model property. Along the way, we establish a representation theorem foractual 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 sur- veys, see [1, 29]). 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 [23, 3], and for the automated verification of software properties [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 agentdetermines, orinfluences, through their actions. For an illustration, imagine that Alice and Bob are creating clay an- imals 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: (1)a.Alice determines the shape of the animal (but not its color). b.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 sib- lings 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 (1-a)? More precisely, what is thethingthat 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, butwhich 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 settleda priori, but it becomes settled once we fix the agent’s action. Implementing this idea takes us into the realm ofinquisitive modal logic, a quickly growing research area that combines inquisitive logic and modal logic. I. Ciardelli223 Inquisitive logic [10] 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., [7, 15, 8, 17, 18, 27, 28, 14, 25, 24, 12]). In our case, the idea is to capture agentive determination in terms of an inquisitive modality⊠indexed by agents which, when applied to formulasshapeandcolorformalizing the questionswhat is the shapeandwhat the color, delivers modal statements⊠ Alice shapeand⊠ Bob colorcapturing, respectively, the claims in (1-a) and (1-b). In this paper, we will develop this idea in detail. We will define aninquisitive action logic,InqAL, which allows us to analyze statements like (1-a) and (1-b) along the lines we described, but which also recovers the modal account of ability familiar from the classical work of Brown [5] and more recent work on coalition logic,CL[26]. Our logic is a multi-agent version of a recently developed system, inquisitive neighborhood logic,InqNL[9, 12].InqNLis based on a binary modality⇛, acting seman- tically as a strict conditional quantifying over neighborhoods; analogously, our multi-agent extension InqALcontains one such modality⇛ a for each agenta; in terms of this modality, some derivative unary modalities (including the modality⊠ a mentioned above) can be defined. Besides being multi-agent,In- qALis geared specifically towards an interpretation in terms of action; as a consequence, whileInqNL is interpreted over arbitrary neighborhood models,InqALstarts with more concrete structures known as concurrent game structuresormulti-agent transition systems[2, 26, 19, 6], 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 asactual effectivity functions[6] (in contrast with theeffectivity functionsstudied in coalition logic [26, 21], which are upward-closed sets of neighborhoods). The problem of character- izing 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 ofInqAL, giving us a characterization of the relevant class of neighborhood models. Our logicInqALis also connected tosocially friendly coalition logic(SFCL), an extension of coali- tion logic recently proposed by Goranko and Enqvist [20]. Whereas standard coalition logic focuses on what outcomes agents canforcethrough their actions,SFCLalso captures what outcomes agents can enablefor others, while still forcing their own goals. These properties are crucial for the possibility of cooperation between agents (hence the namesocially friendly). Technically,SFCLis a multi-agent ex- tension ofinstantial neighborhood logic,INL[4]. As proved in [12], inquisitive neighborhood logic has, with respect to statements, the same expressive power asINL. In the same vein, our inquisitive action logic has, with respect to statements, the same expressive power asSFCL. Still, as we will see, the way modal claims are expressed in these logics is very different; in particular, the translation fromInqALto SFCLcan 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 InqNL A , a multi-agent version of inquisitive neighborhood logic. In §4 we introduceInqAL, which interpretsInqNL A over concurrent game models, and discuss how this logic allows us to express inter- esting properties relating to what agents can force, enable, or determine in an interactive situation. In §5 we give an axiomatization ofInqALand prove completeness and decidability. In §6 we compare the expressive power of our logic with that of Socially Friendly Coalition Logic. §7 concludes. 224Inquisitive Action Logic 2 Characterizing actual effectivity functions of agents Concurrent game structures [2, 26, 6] 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 2.1.LetA=a 1 ,...,a k be a finite set of agents. Aconcurrent game structure(or CGS for short) forAis a tripleS= (W,act,out)where: •Wis a non-empty set ofworlds, representing stages of the process; •actis a function which assigns to each agentaand worldwa non-empty setact(a,w)of actions. A functionτassigning to each agenta i a corresponding actionτ(a i )∈act(a i ,w)is called anaction profileatw; the set of action profiles atwis denotedActP(w). •outis a function that, given a worldwand an action profileτatw, returns a worldout(w,τ); intuitively,out(w,τ)is the world that results fromwwhen each agenta i performs the actionτ(a i ). At a worldwin a CGS, a range of outcomes are possible, depending on the choices of the agents, namely: O(w) =out(w,τ)|τ∈ActP(w) By picking a particular action, an agent typically narrows down the set of possible outcomes. The set of outcomes which are possible fromwgiven that agentaperforms actionτ a ∈act(a,w)is: O a (w,τ a ) =out(w,τ)|τ∈ActP,τ(a) =τ a We call this theoutput setof actionτ a foraatw. By collecting the output sets of all actions available to an agent, we obtain theiractual effectivity function. More precisely, the actual effectivity function of agentain a CGSSis the mapΣ S a :W→℘(W)given by: Σ S a (w) =O a (w,τ a )|τ a ∈act(a,w) In this way, a CGS determines a corresponding multi-agent neighborhood frameF S = (W,(Σ S a ) a∈A ). But not justanyneighborhood frameF= (W,(Σ a ) a∈A ), whereΣ a :W→℘(W), can be a system of actual effectivity functions of some CGS. This raises a natural question:whichneighborhood frames arise from some CGS? The following theorem provides an answer to this question. 1 Theorem 2.2.LetA=a 1 ,...,a k be a finite set of agents with k>1. 2 For a multi-agent neighborhood frame F= (W,(Σ a ) a∈A )the following are equivalent: 1. F=F S for some concurrent game structureS. 2. The following three conditions are satisfied for each world w∈W : (a) Existence of actions: for all a∈A,Σ a (w)̸=/0; (b) Uniform range: for all a,b∈A, S Σ a (w) = S Σ b (w); (c) Independence: for all s 1 ∈Σ a 1 (w),...,s k ∈Σ a k (w):s 1 ∩·∩s k ̸=/0. 1 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. 2 Whenk=1, i.e., in the single-agent case, the characterization is trivial: as the reader can readily verify, a neighborhood frameF= (W,Σ)is induced by a CGS if and only ifΣ(w)is a non-empty set of singletons for everyw∈W. We therefore focus on the interesting multi-agent case withk>1. I. Ciardelli225 Proof.1⇒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 thatact(a,w)is non-empty by definition. Condition (b) is due to the observation that for everya, S Σ S a (w)coincides with the set of all possible outcomes atw,O(w). Condition (c) is due to the fact that whenever we take neighborhoodsO a i (w,τ a i )∈Σ S a i (w)fori=1,...,k, the functionτdefined byτ(a i ) =τ a i is an action profile, and we haveout(w,τ)∈O a i (w,τ i )for eachi. To show 2⇒1, supposeF= (W,(Σ a ) a∈A )is a neighborhood frame satisfying (a)-(c). Our aim is to define a CGSS= (W,act,out)withF S =F, i.e., such that for each agenta,Σ a coincides with the actual effectivity functionΣ S a of agentainS. For this, equip the setWwith a group structure, so that(W,e,∗,(·) −1 )is a group. Also, fix a well- ordering ofW, and for any non-emptys⊆W, let min(s)denote the least element ofsaccording to this well-ordering. 3 We define the actions available to an agentaat a worldwas pairs consisting of a neighborhood fora, and a world: act(a,w) =(s,v)|s∈Σ a (w),v∈W Condition (a) guarantees that this is a non-empty set, as required by the definition of a CGS. Now given a worldw, an action profile atwcan be identified with a sequenceτ= ((s 1 ,v 1 ),...,(s k ,v k )) wheres i ∈Σ a i (w)fori≤k. We define the outcome ofτatwin the following way: out(w,τ) = v 1 ∗·∗v k if(v 1 ∗·∗v k )∈(s 1 ∩·∩s k ) min(s 1 ∩·∩s k )otherwise Condition (c) guarantees thats 1 ∩·∩s k is non-empty, so that min(s 1 ∩·∩s k )exists, which ensures thatout(w,τ)is well-defined. Note further that, by definition,out(w,τ)∈s 1 ∩·∩s k . We claim that the CGS so defined inducesF. To show this, the key step is to prove that for each agent aand action(s,v)∈act(a,w), the set of outputs that may result fromaperforming(s,v)is simplys: O a (w,(s,v)) =s(1) The inclusion⊆is clear: wheneverτis an action profile that includes the action(s,v), the corresponding outcomeout(w,τ)is bound to be insby definition ofout. To show the inclusion⊇, consider an arbitrary worldu∈s. We need to show that there is an action profileτincluding(s,v)whose outcome isu. For simplicity, supposea=a 1 and let us write(s 1 ,v 1 )for(s,v). Sinceu∈s 1 ands 1 ∈Σ a 1 (w), we have u∈ S Σ a 1 (w). By condition (b), for eachi>1 we haveu∈ S Σ a i (w), so we can pick a neighborhood s i ∈Σ a i (w)withu∈s i . Now for 1<i<k, pick some worldsv i ∈Warbitrarily. Finally, letv k be the element(v 1 ∗·∗v k−1 ) −1 ∗u. Now consider the action profileτ= ((s 1 ,v 1 ),...,(s k ,v k )). We have v 1 ∗·∗v k = (v 1 ∗·∗v k−1 )∗(v 1 ∗·∗v k−1 ) −1 ∗u=u. By the way the setss i were chosen we know thatu∈s 1 ∩·∩s k , and so by definition ofoutwe haveout(w,τ) =u. Since the profileτincludes the action(s,v), this shows thatu∈O a (w,(s,v)), as required to complete the proof of (1). Finally, using (1), the actual effectivity function for agentaturns out to be Σ S a (w) =O a (w,τ a )|τ a ∈act(a,w)=O a (w,(s,v))|s∈Σ a (w),v∈W=s|s∈Σ a (w)=Σ a (w) which shows that indeed,F S =F, as desired. 3 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 ifWis finite or countably infinite, as will be the case in our completeness proof in Section 5. 226Inquisitive Action Logic 3 Inquisitive multi-agent neighborhood logic In this section we present a multi-agent version of inquisitive neighborhood logic,InqNL[12]. We call this logicInqNL A whereA=a 1 ,...,a k is a finite set of agents. The proofs of the results in this section are the same as forInqNL; we do not repeat them here, but include pointers to the results in [12]. Syntax.Given a finite setPof atoms, the setL A ofInqNL A -formulas is given by: φ::=p|⊥|(φ∧φ)|(φ→φ)|(φ ⩾ φ)|(φ⇛ a φ) wherep∈Panda∈A. As standard in inquisitive logic, we also use the following abbreviations:¬φ:= (φ→⊥);⊤:=¬⊥;(φ∨ψ):=¬(¬φ∧¬ψ); ?φ:= (φ ⩾ ¬φ). The connective ⩾ , calledinquisitive disjunction, is regarded as a question-forming disjunction. Thus, e.g., the formula ?p(short forp ⩾ ¬p) is regarded as the questionwhether or not p. The operators⇛ a are indexed versions of the binary modality ⇛InqNL. Two unary modalities (read “window” and “kite”) are defined in terms of⇛ a as follows: ⊞ a φ:= (⊤⇛ a φ)| a φ:=¬(φ⇛ a ⊥) An important fragment of the language is given bydeclarative formulas(ordeclaratives, for short), where inquisitive disjunction occurs only in the scope of a modal operator. More formally, the setL ! A of declaratives is defined as follows, whereφcan be rewritten as any formula fromL A : α::=p|⊥|(α∧α)|(α→α)|(φ⇛ a φ) Intuitively, declaratives stand for statements (as we will see, this is reflected in a key semantic property). We will use the meta-variablesφ,ψ,χfor arbitrary formulas, andα,β,γfor declaratives. Themodal depthof a formula is defined as usual as the maximum number of nestings of modal operators in it. More precisely, we set: md(p) =md(⊥) =0; md(φ∧ψ) =md(φ→ψ) =md(φ ⩾ ψ) = max(md(φ),md(ψ)); md(φ⇛ a ψ) =max(md(φ),md(ψ))+1. The set of formulas inL A with modal depth up tonis denotedL n A ; the set of declaratives with modal depth up tonis denotedL !n A . Semantics.We interpret formulas relative tomulti-agent inhabited neighborhood models(main-models, for short), which are triplesM= (W,(Σ a ) a∈A ,V)whereW̸=/0 is a set of worlds,Σ a :W→℘ 0 (W)is a map assigning to eachw∈Wa setΣ a (w)of non-empty subsets ofW(called theneighborhoodsofw) andV:P→℘(W)is a valuation function. As customary in inquisitive logic, the semantics ofInqNL A is not given in terms of truth relative to possible worlds, but instead in terms ofsupportrelative to sets of possible worlds, calledinformation states(or simplystates). Definition 3.1(Support in main-models).LetM= (W,(Σ a ) a∈A ,V)be a main-model. The relation of support between information statess⊆Wand formulasφ∈L A is defined as follows: •M,s|=p⇐⇒s⊆V(p) •M,s|=⊥ ⇐⇒s=/0 •M,s|=φ∧ψ⇐⇒M,s|=φandM,s|=ψ •M,s|=φ ⩾ ψ⇐⇒M,s|=φorM,s|=ψ •M,s|=φ→ψ⇐⇒ ∀t⊆s:M,t|=φimpliesM,t|=ψ •M,s|=φ⇛ a ψ⇐⇒ ∀w∈s∀t∈Σ a (w):M,t|=φimpliesM,t|=ψ I. Ciardelli227 All the clauses except for the last one are standard in inquisitive logic (see [10] for discussion), while the clause for the modality⇛ a is a direct multi-agent adaptation of the one for⇛inInqNL[12]. Entailment and equivalence are defined in the obvious way: a set of formulasΦentails a formula ψ, denotedΦ|= InqNL A ψ, if for every main-modelMand statesthat supports all formulas inΦ,salso supportsψ. Two formulasφ,ψare equivalent, denotedφ≡ InqNL A ψ, if they are supported by the same states in every main-model. To ease notation, throughout this section we drop the subscriptInqNL A . As usual in inquisitive logic, support is persistent (ifM,s|=φandt⊆s, thenM,t|=φ), and the empty state trivially supports every formula. Moreover, we retrieve a notion of truth at a worldwby defining it as support relative to the corresponding singletonw. Definition 3.2(Truth).φistrueat a worldwof a main-modelM, denotedM,w|=φ, in caseM,w|=φ. The set of worlds at whichφis true in a modelMis denoted|φ| M . Some simple calculations show that the Boolean connectives have their usual truth-functional behavior (for instance,M,w|=¬φ⇐⇒M,w̸|=φ), and that modal formulas have the following truth conditions: •M,w|= (φ⇛ a ψ)⇐⇒ ∀s∈Σ a (w):M,s|=φimpliesM,s|=ψ •M,w|=⊞φ⇐⇒ ∀s∈Σ a (w):M,s|=φ •M,w|=|φ⇐⇒ ∃s∈Σ a (w):M,s|=φ Declaratives have a special semantic property: for them, support boils down to truth at each world. In fact, up to equivalence, declaratives areexactlythe formulas for which this holds. Definition 3.3(Truth-conditionality).A formulaφ∈L A istruth-conditionalif for every modelMand stateswe haveM,s|=φ⇐⇒ ∀w∈s:M,w|=φ. Proposition 3.4(cf. Prop. 2.7 in [12]).Every declarativeα∈L ! A is truth-conditional. Conversely, every truth-conditional formula ofL A is equivalent to a declarative. Not all formulas ofInqNL A are truth-conditional. As a simple example, consider the formula ?p(which abbreviatesp ⩾ ¬p). A simple calculation yields the following support conditions: M,s|=?p⇐⇒phas the same truth value in all worlds ins Intuitively, ?pis supported atsif it issettledinswhetherpis true or false. Clearly, ?pis 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φis equivalent to a finite inquisitive disjunction of declaratives, called theresolutionsofφ. Definition 3.5(Resolutions).The setR(φ)ofresolutionsof a formulaφ∈L A is defined as follows: •R(α) =αifαis an atom,⊥, or a modal formula(φ⇛ a ψ); •R(φ∧ψ) =α∧β|α∈R(φ),β∈R(ψ); •R(φ ⩾ ψ) =R(φ)∪R(ψ); •R(φ→ψ) = V α∈R(φ) (α→f(α))|f:R(φ)→R(ψ). Note thatR(φ)is always a finite non-empty set of declaratives, and for any declarativeα,R(α) =α. Proposition 3.6(Normal form, cf. Prop. 2.9 in [12]).For anyφ∈L A ,φ≡\\/R(φ). 228Inquisitive Action Logic In terms of resolutions we may also define a further modal operator,□ a , which will play a role below: □ a φ:= _ ⊞ a α|α∈R(φ) This operator has been considered in previous work on inquisitive modal logic [15, 7, 11]. 4 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□ a φis a declarative. A simple calculation yields the following truth conditions: •M,w|=□ a φ⇐⇒M, S Σ a (w)|=φ 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. Proposition 3.7(cf. Corollary 5.17 in [12]).The quotient ofL n A 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 logicInqNL 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 thatAcontains at least two agents; for some comments on the trivial, but somewhat special, single-agent case, see Footnote 7. Definition 4.1.Aconcurrent game model(orcg-model, for short) is a pairM= (S,V)consisting of a concurrent game structureS= (W,act,out)and a valuation functionV:P→℘(W). A concurrent game modelM= (S,V)withS= (W,act,out)determines a corresponding main-model M M = (W,(Σ S a ) a∈A ,V), whose neighborhood functions are the actual effectivity functions of agents. We can thus interpret the formulas ofL A relative to a cg-model, via its associated main-model. Definition 4.2.LetMbe a cg-model,sa state inM, andφ∈L A . We writeM,s|=φifM M ,s|=φ. Entailment and equivalence inInqAL, denoted|= InqAL and≡ InqAL respectively, are defined in the same way as forInqNL A , but with respect to cg-models instead of main-models. Note that, being determined by a smaller class of models, the logicInqALis an extension ofInqNL 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| a α, whereα∈L ! A . We have: M,w|=| a α⇐⇒ ∃τ a ∈act(a,w):O a (w,τ a )⊆|α| M Thus,| a αexpresses the fact that agentahas an action available that guarantees the truth ofα(i.e., if that action is executed, the outcome will makeαtrue, regardless what the other agents do). In short, | a αsays thatacan forceα, recovering the standard semantics for ability familiar from [5] and [26]. 5 4 In this previous work,□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. 5 In fact, it is possible to show that the|-fragment of our language is equi-expressive with the fragment of coalition logic that contains only modalities for individual agents. See §3 of [12] for an analogous result in the case ofInqNL. I. Ciardelli229 As a second example, consider the modal formula(α⇛ a β), whereα,β∈L ! A . We have: M,w|= (α⇛ a β)⇐⇒ ∀τ a ∈act(a,w):O a (w,τ a )⊆|α| M impliesO a (w,τ a )⊆|β| M What this formula expresses is that, in order to forceα, agentanecessarily has to forceβ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¬(α⇛ a ¬β). We have: M,w|=¬(α⇛ a ¬β)⇐⇒ ∃τ a ∈act(a,w):O a (w,τ a )⊆|α| M andO a (w,τ a )∩|β| M ̸=/0 The formula expresses the fact that agentacan perform an action which forcesαwithout precludingβ. More generally, a formula of the form¬(α⇛ a ¬β 1 ⩾ · ⩾ ¬β n )expresses the fact that it is possible for ato forceαwithout precluding any ofβ 1 ,...,β n . In this way, the central properties that the Socially Friendly Coalition Logic of Goranko and Enqvist [20] is designed to capture can be expressed inInqAL. Let us now consider formulas involving the modalities⊞ a and□ a . First consider the case in which the argument is a declarativeα∈L ! A . In this case,R(α) =α, and so the two modalities coincide: by definition of□ a , we have□ a α=⊞ a α. Recall from Section 2 that, in the case of actual effectivity functions, the union of the neighborhoods simply coincides with the setO(w)of all outcomes possible atw: for any agenta, S Σ S a (w) =O(w). Using this fact, we obtain the following: M,w|=□ a α⇐⇒M,w|=⊞ a α⇐⇒O(w)⊆|α| M Thus, regardless of the agenta, the (identical) formulas⊞ a αand□ a αexpress the fact thatαisunavoid- able: it will be true at the next stage regardless what the agents do. When the argument is not a declarative, however, the modalities□ a and⊞ a come apart. Let us illustrate this with the case of a polar question ?α, whereα∈L ! A . SinceR(?α) =α,¬α, the formula □ a ?αamounts to⊞ a α∨⊞ a ¬α, which says that eitherαis unavoidably true at the next stage, or it is unavoidably false. More formally: M,w|=□ a ?α⇐⇒αhas the same truth value in all worlds inO(w) Thus,□ a ?αsays that whetherαwill be true at the next stage ispredetermined, i.e., settleda priori regardless of the actions of the agents. By contrast, for the modal formula⊞ a ?αwe have the following: M,w|=⊞ a ?α⇐⇒ ∀τ a ∈act(a,w):αhas the same truth value in all worlds inO a (w,τ a ) Thus, what⊞ a ?αexpresses is that once we fix the action ofa, the truth value ofαat the next stage is settled: the actions of other agents cannot affect it. These findings generalize: ifφdenotes a question, then□ a φexpresses the fact thatφis settleda priori, regardless of what the agents do, while⊞ a φ expresses the fact thatφis settled once we fix the action of agenta. We can now see how the analysis of agentive determination we suggested in the introduction can be formalized inInqAL. Our guiding idea was this: at a certain stage in a process, an agentadetermines a questionφif (i) the answer toφis not settleda prioribut (i) it becomes settled once we fix the action of agenta. In our logic, (i) is captured by¬□ a φ, and (i) by⊞ a φ. We can thus define a modality⊠ a capturing agentive determination in the following way: ⊠ a φ:=¬□ a φ∧⊞ a φ For instance, the claim that agentadetermines whetherαwill be true at the next stage is expressed by ⊠ a ?α:=¬□ a ?α∧⊞ a ?α, which says that the truth value ofαis not predetermined (i.e., not the same 230Inquisitive Action Logic red dog red cat red cow blue dog blue cat blue cow green dog green cat green cow Σ S a (w) red dog red cat red cow blue dog blue cat blue cow green dog green cat green cow Σ S b (w) Figure 1: The neighborhoods (i.e., outcome sets) associated to Alice’s actions (left) and Bob’s action (right) in our toy example. in all possible outcomes), but it is determined once we fix the action ofa(i.e., it is constant within each neighborhood fora). This is, in my view, a very natural analysis of the determination claim. 6 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:τ cat (mould a cat),τ dog (mould a dog), andτ cow (mould a cow); similarly, Bob has three actions:τ red (paint red),τ blue (paint blue),τ green (paint green). Each joint action by Alice and Bob, for instanceτ cat τ red , results in a specific outcome, for instance out(w,τ cat τ red ) =red cat. In total, there are 3×3=9 possible outcomes (red cat, blue dog, etc.) which make up the total setO(w). For each agent, fixing an action leaves us with only 3 possible outcomes; for instance,O a (w,τ cat ) =red cat,blue cat,green cat, whileO b (w,τ red ) =red cat,red dog,red cow. The neighborhoods corresponding to these outcome sets for Alice and Bob are depicted in Figure 1. Now we can consider a language with six propositional atoms,cat,dog,cow,red,blue,green, with the obvious interpretation (e.g.,catexpresses the proposition “the animal is a cat”). Using inquisitive disjunction, we can build two formulasshapeandcolorexpressing, respectively, the questions “what the shape is” and “what the color is”: shape:= (cat ⩾ dog ⩾ cow)color:= (red ⩾ blue ⩾ green) An information statesin our model supports the questionshapejust in case in all worlds ins, the animal has the same shape; similarly,ssupportscolorif in all worlds ins, 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 (⊠ a shape) but not the color (¬⊠ a color), while Bob determines the color (⊠ b color) but not the shape (¬⊠ b shape). In order to see that⊠ a shape(i.e.,¬□ a shape∧⊞ a shape) is true at our worldw, we reason as follows. First, since the shape of the animal is not constant across all possible outcomes, we haveM,O(w)̸|= shape, which ensuresM,w|=¬□ a shape; this captures the fact that in our scenario, the shape is not 6 Interestingly, exactly the same modal pattern,¬□ a φ∧⊞ a φis argued in inquisitive epistemic logic to capture the idea that an agentwonders about, or isinterested in, a certain question [15]. 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. I. Ciardelli231 predetermined, but depends on the actions of the agents. Second, within each of the three outcome sets O a (w,τ cat ),O a (w,τ dog ),O a (w,τ cow ), corresponding to the three actions fora, the shape of the animalis constant; therefore, each of these sets supportsshape, ensuringM,w|=⊞ a 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,⊠ a color(i.e.,¬□ a color∧⊞ a color) is false atw, since its second conjunct is false. Con- sider any outcome set fora, for instanceO a (w,τ cat ). The color of the animal is not constant across this set, and so this set does not supportcolor. Since not all the outcome sets fora(in fact, none of them) sup- portcolor,M,w̸|=⊞ a 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 ofInqNL A , which is the basis for our axiomatization ofInqAL. The propositional axioms include instances of axioms for intuitionistic propositional logic, with ⩾ in the role of intuitionistic disjunction, and all instances of the following, whereα∈L ! A andφ,ψ∈L A : •¬α→α(Declarative double negation) •(α→φ ⩾ ψ)→(α→φ) ⩾ (α→ψ)(Split) The modal axioms include all instances of the following schemata, capturing the behavior of the modal- ities⇛ a as strict conditionals (see [12] for discussion of these axioms in the uni-modal case and [22] for a more general study of strict conditionals on an intuitionistic basis): •(φ⇛ a ψ)∧(ψ⇛ a χ)→(φ⇛ a χ)(Transitivity) •(φ⇛ a ψ)∧(φ⇛ a χ)→(φ⇛ a (ψ∧χ))(Right conjunction) •(φ⇛ a χ)∧(ψ⇛ a χ)→((φ ⩾ ψ)⇛ a χ)(Left disjunction) The inference rules aremodus ponens(φ,φ→ψ/ψ) andconditional necessitation(φ→ψ/φ⇛ a ψ). Ifψ∈L A is derivable in this system we write⊢ N ψ. ForΦ,Ψ⊆L A , we writeΦ⊢ N Ψin case for some finiteΦ 0 ⊆ΦandΨ 0 ⊆Ψwe have⊢ N V Φ 0 →\\/Ψ 0 . Instead ofφ 1 ,...,φ n ⊢ N ψ 1 ,...,ψ m we write simplyφ 1 ,...,φ n ⊢ N ψ 1 ,...,ψ m . We writeφ⊣⊢ N ψif we have bothφ⊢ N ψandψ⊢ N φ. The following soundness and strong completeness theorem generalizes the one forInqNL. The proof is the obvious multi-agent adaptation of the one forInqNLgiven in [12]. Theorem 5.1.For allΦ⊆L A andψ∈L A ,Φ|= InqNL A ψ⇐⇒Φ⊢ N ψ. To obtain a system forInqAL, we add three axiom schemata reflecting the properties of actual effectivity functions we identified in Theorem 2.2. For all declarativesα, all formulasφ 1 ,...,φ n , all agentsa,b, and all pairwise distinct agentsa 1 ,...,a n+1 , the following are axioms: 7 •| a ⊤(Existence of actions) •⊞ a α↔⊞ b α 8 (Uniform range) 7 Recall that we assume thatAcontains at least two agents. IfAcontains a single agenta, an axiomatization ofInqALis obtained by following two axioms: (i)| a ⊤(existence of actions); (i)⊞ a ?αfor any declarativeα(determinacy). The former captures the condition thatΣ a (w)̸=/0, the latter the condition that eachs∈Σ a (w)is a singleton. As mentioned in Footnote 2, these conditions guarantee thatΣ 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 5.12 needs to be adapted. We leave this as an exercise. 8 Note that the restriction to declaratives in this axiom is crucial; for instance,⊞ a ?p↔⊞ b ?pis not valid inInqAL. Alterna- tively, we may take as axioms all formulas of the form□ a φ↔□ b φ; in this case, no restriction is needed. 232Inquisitive Action Logic •| a 1 φ 1 ∧·∧| a n φ n → ¬| a n+1 ¬(φ 1 ∧·∧φ n )(Independence) We write⊢ A ψifψis derivable in this extended system. Similarly, the notationsΦ⊢ A Ψandφ⊣⊢ A ψ are defined as for⊢ N , but with reference to the extended axiom system. Our task is now to prove that this extended system is sound and (weakly) complete forInqAL. 9 Theorem 5.2(Soundness and completeness forInqAL).For allφ∈L A ,|= InqAL φ⇐⇒⊢ A φ. 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 forInqALowe their validity to the three corresponding properties of actual effectivity functions listed in Theorem 2.2. Towards complete- ness, we adapt a finite canonical model construction from [12] (in turn building on ideas from [7]). Definition 5.3.Forn∈N, ann-bounded complete theory of declaratives(ornCTD for short), is a set of declarativesΓ⊆L !n A satisfying three conditions: (i) deductive closure relative toL !n A : ifΓ⊢ A αand α∈L !n A , thenα∈Γ; (i) consistency:⊥̸∈Γ; and (i) completeness: for allα∈L !n A ,α∈Γor¬α∈Γ. We denote the set of allnCTDs byK n . We now show that eachK n is a non-empty finite set, and that the setsK n andK m are disjoint forn̸=m. Lemma 5.4.If∆⊆L !n A and∆̸⊢ A ⊥, then∆⊆Γfor someΓ∈K n . In particular,K n ̸=/0. Proof.A simple adaptation of the usual saturation argument. Lemma 5.5.Each setK n is finite. Proof.Since⊢ A extends⊢ N , the equivalence relation⊣⊢ N refines⊣⊢ A . By Theorem 5.1,⊣⊢ N coincides with the semantic equivalence relation≡ InqNL A . By Prop. 3.7, the quotient ofL n A /≡ InqNL A is finite, and a fortiori, so is the quotientL !n A /⊣⊢ A . Since annCTD is a subset ofL !n A which is deductively closed, it is fully determined by the equivalence classes of its elements modulo⊣⊢ A , i.e., it is fully determined by a subset of the quotientL !n A /⊣⊢ A . Since these subsets are finitely many, so are thenCTDs. Lemma 5.6.K n ∩K m =/0for n̸=m. Proof.Letabe an arbitrary agent and let⊞ h a ⊤abbreviate⊞ a ...⊞ a ⊤withhoccurrences of⊞ a . IfΓ∈ K n , by deductive closure relative toL !n A we have⊞ h a ⊤∈Γ⇐⇒h≤n, and son=maxh|⊞ h a ⊤∈Γ. As a consequence, ifΓ∈K n ∩K m thenn=maxh|⊞ h a ⊤∈Γ=m. We now define for eachn∈Na canonical model suitable for formulas inL n A . Definition 5.7.Forn∈N, we define the main-modelM n = (W n ,(Σ n a ) a∈A ,V n )as follows:W n = S m≤n K m ; V n (p) =Γ∈W n |p∈Γ; finally, the neighborhood mapΣ n a is defined as follows: • ifΓ∈K 0 thenΣ n a (Γ) =K 0 • ifΓ∈K m+1 thenΣ n a (Γ) =S⊆K m ,S̸=/0|for all(ψ⇛ a χ)∈Γ: T S⊢ A ψimplies T S⊢ A χ For anyn∈N, the modelM n is finite by Lemma 5.5. The following four lemmas play a key role in the completeness proof. The proofs are simple adaptations of those of the corresponding results forInqNL (Lemmas 6.10, 6.12, 6.15, and 6.16 in [12]), We provide the details in Appendix A for completeness. 9 An interesting question that we will leave open is whether Theorem 5.2 can be extended to a strong completeness result. I. Ciardelli233 Lemma 5.8(Intersection Lemma). For a set∆⊆L !n A , define S n ∆ =Γ∈K n |∆⊆Γ. For everyφ∈L n A we have∆⊢ A φ⇐⇒ T S n ∆ ⊢ A φ. 10 In particular, since S n /0 =K n , for everyφ∈L n A we have⊢ A φ⇐⇒ T K n ⊢ A φ. Lemma 5.9(Existence Lemma). For m≤n, ifΓ∈K m and¬(φ⇛ a ψ)∈Γ, then there is S∈Σ n a (Γ)such that T S⊢ A φand T S̸⊢ A ψ. Lemma 5.10(Range Lemma). For allΓ∈K m with m>0we have S Σ n a (Γ) =Γ ′ ∈K m−1 |∀α∈L ! A :⊞ a α∈Γimpliesα∈Γ ′ . Lemma 5.11(Support Lemma). For all m≤n, all non-empty states S⊆K m , and all formulasφ∈L m A : M n ,S|=φ⇐⇒ T S⊢ A φ. The part of the proof which is genuinely novel, and crucial for our purposes, lies in showing that the canonical modelsM n so constructed are induced by some corresponding concurrent game models. Lemma 5.12(Representation Lemma).For each n∈Nthere is a CGMM n such that M M n =M n . Proof.It suffices to show that the maps(Σ n a ) a∈A of our canonical model satisfy the conditions (a)-(c) of Theorem 2.2. Consider a worldΓ∈W n . We haveΓ∈K m for somem≤n. Ifm=0 thenΣ n a (Γ) =K 0 for every agentaand conditions (a)-(c) are obviously satisfied. So, we may assumem>0. (a)Existence of actions.SinceΓcontains the axiom| a ⊤, which is short for¬(⊤⇛ a ⊥), the existence of someS∈Σ n a (Γ)follows directly from Lemma 5.9. (b)Uniform range.Take any agentsa,b∈A. For any declarativeα,⊞ a α↔⊞ b αis an axiom, so ⊞ a α⊣⊢ A ⊞ b α. Since the formulas⊞ a αand⊞ b αalso have the same modal depth,Γcontains one iff it contains the other. Now using Lemma 5.10 for both agentsaandbwe have: [ Σ n a (Γ) =Γ ′ ∈K m−1 |∀α∈L ! A :⊞ a α∈Γimpliesα∈Γ ′ =Γ ′ ∈K m−1 |∀α∈L ! A :⊞ b α∈Γimpliesα∈Γ ′ = [ Σ n b (Γ) (c)Independence.Take any neighborhoodsS 1 ∈Σ n a 1 (Γ),...,S k ∈Σ n a k (Γ). We must proveS 1 ∩·∩S k ̸=/0. We start by proving the following claim: \ S 1 ∪·∪ \ S k ̸⊢ A ⊥(∗) Towards a contradiction, suppose this is false. Then there are formulasα 1 ∈ T S 1 ,...,α k ∈ T S k such that α 1 ,...,α k ⊢ A ⊥(it suffices to consider a singleα i from each T S i , since T S i is closed under conjunction). By definition ofΣ n a i , eachS i is non-empty and thus T S i ̸⊢ A ⊥. SinceS i ∈Σ n a i (Γ)and T S i ⊢ A α i but T S i ̸⊢ A ⊥, again by definition ofΣ n a i it follows that(α i ⇛ a i ⊥)̸∈Γ. Also, sinceΓ∈K m , by definition ofΣ n a i (Γ)we haveS i ⊆K m−1 , which means that md(α i )≤m−1, and thus md(α i ⇛ a i ⊥)≤m. Since Γ∈K m and(α i ⇛ a i ⊥)∈L !m A , from(α i ⇛ a i ⊥)̸∈Γwe can conclude by the completeness condition on Γthat¬(α i ⇛ a i ⊥)∈Γ, that is,| a i α i ∈Γ. So, for eachi≤kwe have| a i α i ∈Γ. But now, by deductive closure relative toL !m A ,Γcontains both the axiom | 1 α 1 ∧·∧| k−1 α k−1 →¬| k ¬(α 1 ∧·∧α k−1 ) and its antecedent. So,Γmust contain the consequent,¬| k ¬(α 1 ∧·∧α k−1 ). 10 To be fully precise, forS⊆K n , we define T S=α∈L !n A |α∈Γfor allΓ∈S. This definition implies that T /0=L !n A , ensuring that the lemma holds also when we have∆⊢ A ⊥, and thereforeS n ∆ =/0. In this case, the sets of formulas∆and T S n ∆ = T /0=L !n A indeed derive the same formulas fromL n A : all of them. 234Inquisitive Action Logic On the other hand, fromα 1 ,...,α k ⊢ A ⊥we have thatα k ⊢ A ¬(α 1 ∧·∧α k−1 ), and sinceα k ∈ T S k , also¬(α 1 ∧·∧α k−1 )∈ T S k . Reasoning again as in the previous paragraph, from this and the fact that S k ∈Σ n a k (Γ)we may conclude thatΓcontains| k ¬(α 1 ∧·∧α k−1 ). So,Γcontains both| k ¬(α 1 ∧·∧α k−1 )and the negation of this formula; by deductive closure, it must contain⊥. But this is a contradiction, sinceΓis consistent by assumption. Thus,(∗)is true. Thus, T S 1 ∪·∪ T S k is a consistent subset ofL !m−1 A . By Lemma 5.4 there is a∆∈K m−1 with T S 1 ∪·∪ T S k ⊆∆. To conclude, we show that∆∈S 1 ∩·∩S k , which implies thatS 1 ∩·∩S k ̸=/0. Take anyi≤k. We know that T S i ⊆∆and we want to prove∆∈S i . Towards a contradiction, suppose that∆̸∈S i . By Lemma 5.5, we know thatS i is a finite set,S i =Θ 1 ,...,Θ ℓ for someℓand Θ 1 ,...,Θ ℓ ∈K m−1 . Forj≤ℓ,Θ j ̸=∆and therefore we can findθ j ∈L !m−1 A withθ j ∈Θ j and¬θ j ∈∆. Now letθ=θ 1 ∨·∨θ ℓ . We haveθ∈ T S i butθ̸∈∆, which is a contradiction since T S i ⊆∆. Finally, we can now put everything together and establish completeness. Proof of Theorem 5.2, left-to-right.Suppose̸⊢ A φand letn=md(φ). By Lemma 5.8, we have that T K n ̸⊢ A φ, which by Lemma 5.11 impliesM n ,K n ̸|=φ. By Lemma 5.12, there is a CGMM n that inducesM n , and so we haveM n ,K n ̸|=φ. Sinceφcan be falsified in some CGM,̸|= InqAL φ. Note that the proof yields, for anyφwhich is not provable in⊢ A , afinitecountermodel. Therefore, our proof also establishes the finite model property ofInqAL. In turn, the finite model property together with our (recursive) axiomatization yields the decidability ofInqAL. Corollary 5.13(Finite model property).If̸|= InqAL φ,φcan be refuted within a finite cg-model. Corollary 5.14(Decidability).The problem of deciding if a givenφ∈L A is valid inInqALis decidable. 6 Connection with Socially Friendly Coalition Logic In this section we relateInqALto Socially Friendly Coalition Logic (SFCL) [20], a generalization of coalition logic [26] developed by Goranko and Enqvist based on instantial neighborhood logic [4]. Modal formulas inSFCLhave the form[C](σ;π 1 ,...,π n )whereC⊆Aandσ,π 1 ,...,π n are formulas. The primitive connectives are¬and∨. To compare it withInqAL, we restrict to the individual-agent fragment ofSFCL, whereCis a singletona, which we may identify with the agenta. 11 Formulas are interpreted relative to CGMs in a standard truth-conditional fashion. The clause for modal formulas is as follows: M,w⊩[a](σ;π 1 ,...,π n )⇐⇒ ∃τ a ∈act(a,w):O a (w,τ a )⊆|σ| M andO a (w,τ a )∩|π i | M ̸=/0 fori≤n Based on the observations in §4, we can define a translation(·) ∗ from the individual-agent fragment of SFCLtoInqALin the following way:p ∗ =p;(¬φ) ∗ =¬φ ∗ ;(φ∨ψ) ∗ =φ ∗ ∨ψ ∗ ; and, finally: [a](σ;π 1 ,...,π n ) ∗ =¬(σ ∗ ⇛ a ¬π ∗ 1 ⩾ · ⩾ ¬π ∗ n ) It is easy to check that the translationσ ∗ of aSFCL-formula is always a declarative with the same truth conditions asσ. Translating in the opposite direction, fromInqALtoSFCL, is more tricky. First, since the language ofSFCLincludes only statements, we can only expect to faithfully translate declaratives, 11 The connection discussed in this section extends straighforwardly to one between fullSFCLand the natural generalization ofInqALwith 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 ofInqALtoSFCL. I. Ciardelli235 and not arbitrary formulas. Moreover, even thoughφ⇛ a ψis a declarative, the formulasφandψ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 ofInqALtoSFCLas follows:p ⋆ =p; ⊥ ⋆ = (p∧¬p)for an arbitraryp∈P;(α∧β) ⋆ =α ⋆ ∧β ⋆ ;(α→β) ⋆ =¬(α ⋆ ∧¬β ⋆ ); and, crucially, (φ⇛ a ψ) ⋆ = n i=1 ¬[a](α ⋆ i ;¬β ⋆ 1 ,...,¬β ⋆ m ) whereα 1 ,...,α n =R(φ)andβ 1 ,...,β m =R(ψ). One can prove that for any declarativeα∈L ! A , αand its translationα ∗ have the same truth conditions. The proof is identical to the one given for the translation ofInqNLinto instantial neighborhood logic (Proposition 10.2 in [12]). In sum,InqALandSFCLare 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 resolutionsR(φ)of a formulaφcan grow exponentially relative to the size ofφ, and thus, so can the length of the translation of a modal formula containingφ. It is plausible to conjecture that this blowup is unavoidable, and so, thatInqALis in general exponentially more succinct thanSFCL. It is also worth noting that there is currently no complete axiomatization ofSFCL(an axiomatization is presented in [20], but by the authors’ admission (p.c.) the completeness proof contains a mistake). It can be hoped that our Theorem 2.2 can be used to establish completeness at least for the individual-agent fragment ofSFCL. 7 Conclusions and future work We have motivated and investigatedInqAL, a logic that allows us to reason not only about what agents canforcethrough their actions, but also about what theyenableordetermine. An obvious goal for future work is to generalizeInqALfrom individual agents to coalitions. Semantically, this is straightforward. The difficulty lies in establishing a characterization theorem analogous to Theorem 2.2, which played a crucial role in our proof of completeness and decidability. A further important goal is to extendInqAL with temporal operators, yielding an inquisitive version of strategic multi-agent logics likeATL[2, 19]. In a different direction, it would be interesting to ask ifInqAL, 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. Acknowledgements.Funding from the European Research Council (ERC) under the Horizon Europe research and innovation programme (Project InqML, Grant Agreement No. 101116774) is gratefully acknowledged. Thanks to Valentin Goranko for detailed discussions on this topic, and to four anonymous reviewers for precious comments and suggestions. A Appendix: Proofs of standard results A.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 [10] and inquisitive modal logics [7, 8, 12]. In each case, we outline the proof and provide a reference where an analogous proof is spelled out. Lemma A.1(Provable normal form).For allφ∈L A ,φ⊣⊢ A \\/R(φ). Proof.This uses only the propositional component of the axiomatization. See Lemma 4.3.8 in [10]. 236Inquisitive Action Logic Lemma A.2.For allφ∈L A , if⊢ A φthen⊢ A αfor someα∈R(φ). Proof.It suffices to check that this property holds for axioms and is preserved by inference rules. When an axiom is a declarativeα, the claim is trivially true sinceR(α) =α. 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 [8]). As for the inference rules, ifφwas obtained by Conditional Necessitation thenφis declarative and the claim is trivially true. Ifφwas obtained by Modus Ponens fromψandψ→φ, then by induction hypothesis some resolutionsα∈R(ψ)andβ∈R(ψ→φ)are derivable. By definition of resolutions of an implication,βis a conjunction with one conjunct of the formα→γwhereγ∈R(φ). Sinceαandα→γare derivable,γis derivable by Modus Ponens. Lemma A.3.IfΓ⊆L ! A andΓ⊢ A φ, thenΓ⊢ A αfor someα∈R(φ) Proof.IfΓ⊢ A φ, this means that there is a finite subsetΓ 0 ⊆Γsuch that V Γ 0 →φis derivable. Let γ= V Γ 0 . SinceΓis a set of declaratives,γis a declarative, soR(γ) =γ. Then, by definition of resolutionsR(γ→φ) =γ→α|α∈R(φ). By the previous lemma, sinceγ→φis derivable, some particular resolutionγ→αis derivable. This implies thatΓ⊢ A α, and sinceα∈R(φ)we are done. Definition A.4(Resolutions for sets).Aresolution functionfor a setΦ⊆L A is a functionfassigning to eachφ∈Φa corresponding resolutionα∈R(φ). The image ofΦunder a resolution function is called aresolutionofΦ. More formally, the set of resolutions ofφis defined in the following way: R(Φ) =f[Φ]|fa resolution function forΦ. Note that ifΓ∈Φ, then for eachφ∈Φthere is some resolutionα∈R(φ)withα∈Γ. Lemma A.5.IfΦ,Ψ⊆L A andΦ̸⊢ A Ψ, thenΓ̸⊢ A Ψfor someΓ∈R(Φ). Proof.Repeated application of Lemma A.1, by standard properties of ⩾ . See Lemma 4.3.7 in [10]. A.2 Intersection Lemma (Lemma 5.8) Consider a set of declaratives∆⊆L !n A and its corresponding set ofn-bounded complete extensions, S n ∆ =Γ∈K n |∆⊆Γ. We want to show that for allφ∈L n A :∆⊢ A φ⇐⇒ T S n ∆ ⊢ A φ. The direction⇒is obvious since∆⊆ T S n ∆ . For the converse, suppose for a contradiction that for someφwe had T S n ∆ ⊢ A φbut∆̸⊢ A φ. Since T S n ∆ is a set of declaratives, by Lemma A.3 we have T S n ∆ ⊢ A αfor someα∈R(φ). Since∆̸⊢ A φ, it follows by Lemma A.1 that∆̸⊢ A α. By the axiom ¬α→α, this implies∆̸⊢ A ¬α, and therefore∆∪¬α̸⊢ A ⊥. Sinceφ∈L n A we haveα∈L !n A and thus also∆∪¬α⊆L !n A . So by Lemma 5.4 there isΓ∈K n such that∆∪¬α⊆Γ. Now sinceΓ∈S n ∆ and T S n ∆ ⊢ A αwe haveΓ⊢ A α. So we haveΓ⊢ A ¬αandΓ⊢ A α, whenceΓ⊢ A ⊥and, by deductive closure relative toL !n A ,⊥∈Γ. But this is a contradiction sinceΓ∈K n is consistent by assumption.□ A.3 Existence Lemma (Lemma 5.9) We follow closely the proof of Lemma 6.12 in [12], adapting it to our multi-agent setting and to our modal depth-bounded canonical model construction. We first establish some preliminary results. LetΓbe annCTD, withn>0. Given two setsΦ,Ψ⊆L n−1 A , we writeΦ⇛ a Γ Ψif there are finite subsetsΦ 0 ⊆ΦandΨ 0 ⊆Ψsuch that the formula V Φ 0 ⇛ a \\/Ψ 0 is inΓ. Note the following fact. Lemma A.6.IfΦ,Ψ⊆L n−1 A andΦ⊢ A Ψ, thenΦ⇛ a Γ Ψ. I. Ciardelli237 1.φ 1 ∧χ⇛ a ψ 1 (premise) 2.φ 2 ⇛ a ψ 2 ⩾ χ(premise) 3.φ 1 ∧φ 2 ⇛ a φ 1 (CN) from axiomφ 1 ∧φ 2 →φ 1 4.φ 1 ∧φ 2 ⇛ a φ 2 (CN) from axiomφ 1 ∧φ 2 →φ 2 5.φ 1 ∧φ 2 ⇛ a ψ 2 ⩾ χ(MP) from Transitivity, 4, 2 6.φ 1 ∧φ 2 ⇛ a φ 1 ∧(ψ 2 ⩾ χ)(MP) from Right Conjunction, 3, 5 7.φ 1 ∧(ψ 2 ⩾ χ)⇛ a ψ 2 ⩾ (φ 1 ∧χ)(CN) from prop. validityφ 1 ∧(ψ 2 ⩾ χ)→ψ 2 ⩾ (φ 1 ∧χ) 8.φ 1 ∧φ 2 ⇛ a ψ 2 ⩾ (φ 1 ∧χ)(MP) from Transitivity, 6, 7 9.ψ 1 ⇛ a ψ 1 ⩾ ψ 2 (CN) from axiomψ 1 →ψ 1 ⩾ ψ 2 10.ψ 2 ⇛ a ψ 1 ⩾ ψ 2 (CN) from axiomψ 2 →ψ 1 ⩾ ψ 2 11.φ 1 ∧χ⇛ a ψ 1 ⩾ ψ 2 (MP) from Transitivity, 1, 9 12.ψ 2 ⩾ (φ 1 ∧χ)⇛ a ψ 1 ⩾ ψ 2 (MP) from Left Disjunction, 10, 11 13.φ 1 ∧φ 2 ⇛ a ψ 1 ⩾ ψ 2 (MP) from Transitivity, 8, 12 Figure 2: Sketch of a proof showing(φ 1 ∧χ⇛ a ψ 1 ),(φ 2 ⇛ a ψ 2 ⩾ χ)⊢ A (φ 1 ∧φ 2 ⇛ a ψ 1 ⩾ ψ 2 ) Proof.IfΦ⊢ A Ψ, there are finite subsetsΦ 0 ⊆ΦandΨ 0 ⊆Ψsuch that⊢ A V Φ 0 →\\/Ψ 0 . By Con- ditional Necessitation, also⊢ A V Φ 0 ⇛ a \\/Ψ 0 . SinceΦ,Ψ⊆L n−1 A , the modal depth of the formula Φ 0 ⇛ a \\/Ψ 0 is at mostn, and so by deductive closure, this formula must be inΓ, witnessingΦ⇛ a Γ Ψ. Importantly, the relation⇛ a Γ also enjoys the following cut-like property. Lemma A.7.For any two setsΦ,Ψ⊆L n−1 A and formulaχ∈L n−1 A :Φ∪χ⇛ a Γ ΨandΦ⇛ a Γ Ψ∪χ impliesΦ⇛ a Γ Ψ. Proof.SupposeΦ∪χ⇛ a Γ ΨandΦ⇛ a Γ Ψ∪χ. This means that there are finite sets of formulas Φ 0 ,Φ 1 ⊆ΦandΨ 0 ,Ψ 1 ⊆Ψsuch thatΓcontains the following formulas: (χ∧ Φ 0 )⇛ a \\/Ψ 0 Φ 1 ⇛ a (χ ⩾ \\/Ψ 1 ) We prove thatΓmust contain V (Φ 0 ∪Φ 1 )⇛ a \\/(Ψ 0 ∪Ψ 1 ), thus witnessingΦ⇛ a Γ Ψ. To ease nota- tion, we spell out the details for the case in which the relevant sets are all singletonsΦ 0 =φ 0 ,Φ 1 = φ 1 ,Ψ 0 =ψ 0 ,Ψ 1 =ψ 1 , but the general case is analogous. So, we know thatΓcontains the formulas(φ 1 ∧χ⇛ a ψ 1 )and(φ 2 ⇛ a ψ 2 ⩾ χ), and we want to show that it contains(φ 1 ∧φ 2 ⇛ a ψ 1 ⩾ ψ 2 ). Since this formula is a declaratives with modal depth≤n, and sinceΓis closed under deduction relative to such formulas, it suffices to show that: (φ 1 ∧χ⇛ a ψ 1 ),(φ 2 ⇛ a ψ 2 ⩾ χ)⊢ A (φ 1 ∧φ 2 ⇛ a ψ 1 ⩾ ψ 2 ) A derivation is given in Figure 2. In the derivation, we indicate explicitly only the modal axioms and rules involved in the reasoning, omitting reference to propositional axioms. We write(MP)to indicatemodus ponensand(CN)forconditional necessitation. For simplicity, we use the formulas(φ 1 ∧χ⇛ a ψ 1 ) and(φ 2 ⇛ a ψ 2 ⩾ χ)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. Lemma A.8(Splitting lemma).LetΓbe a nCTD with n>0and takeΦ,Ψ⊆L n−1 A withΦ̸⇛ a Γ Ψ. The setL n−1 A can be partitioned into setsLandRsuch thatΦ⊆L,Ψ⊆R, andL̸⇛ a Γ R. 238Inquisitive Action Logic Proof.Fix an enumeration(χ i ) i∈N ofL n−1 A . Define a sequence of sets(L i ) i∈N and(R i ) i∈N as follows: •L 0 =Φ,R 0 =Ψ • ifL i ∪χ i ̸⇛ a Γ R i we letL i+1 :=L i ∪χ i andR i+1 =R i • ifL i ∪χ i ⇛ a Γ R i we letL i+1 :=L i andR i+1 =R i ∪χ i We show by induction onithatL i ̸⇛ a Γ R i . Forn=0 this is true by assumption. Now suppose this is true foriand consideri+1. IfL i ∪χ i ̸⇛ a Γ R i , the claim is obvious by definition ofL i+1 andR i+1 . So, supposeL i ∪χ i ⇛ a Γ R i . Since by induction hypothesisL i ̸⇛ a Γ R i , Lemma A.7 impliesL i ̸⇛ a Γ R i ∪χ i , which by definition amounts toL i+1 ̸⇛ a Γ R i+1 . Now letL= S i∈N L i andR= S i∈N R i . By construction,Φ⊆LandΨ⊆R. We haveL̸⇛ a Γ R, otherwise there would be ani∈Nsuch thatL i ⇛ a Γ R i , contrary to what we just saw. Moreover,LandR form a partition ofL n−1 A . By construction, every formula ofL n−1 A occurs in either set. Moreover, no formula cannot occur in both: to see why, suppose for a contradiction that for someχ∈L n−1 A we have χ∈L∩R; sinceχ⇛ a χis a valid declarative with modal depth≤n, and sinceΓis deductively closed with respect to such formulas, we would need to have(χ⇛ a χ)∈Γ, contradictingL⇛ a Γ R. With these preliminaries at hand, we are now ready to complete the proof of the existence lemma. Proof of Lemma 5.9.LetΓbe annCTD with¬(φ⇛ a ψ)∈Γ. This impliesn>0 (otherwiseΓwould contain only propositional formulas) and furthermoreφandψmust be inL n−1 A . SinceΓis consistent, (φ⇛ a ψ)̸∈Γ, and soφ̸⇛ a Γ ψ. Now extendφandψto setsLandRas in the previous lemma. SinceL̸⇛ a Γ R, by Lemma A.6 we haveL̸⊢ A R. By Lemma A.5 there is a set∆∈R(L)with∆̸⊢ A R. SinceL⊆L n−1 A , we have∆⊆L !n−1 A . We can now takeS=S n−1 ∆ =Γ ′ ∈K n−1 |∆⊆Γ ′ . We need to verify that (i) T S⊢ A φ, (i) T S̸⊢ A ψand (i)S∈Σ n a (Γ). • For (i), we haveφ∈L. Since∆∈R(L), for someα∈R(φ)we haveα∈∆. By Lemma A.1, ∆⊢ A φ, and thus, sinceφ∈L n−1 A , by Lemma 5.8 also T S⊢ A φ. • For (i), we haveψ∈R. Since∆̸⊢ A R, also∆̸⊢ A ψ. Sinceψ∈L n−1 A , Lemma 5.8 gives T S̸⊢ A ψ. • For (i), first note that since∆̸⊢ A R, we have∆̸⊢ A ⊥, so by Lemma 5.4,S̸=/0. Next, suppose (χ⇛ a ξ)∈Γand T S⊢ A χ. We need to show that T S⊢ A ξ. Since(χ⇛ a ξ)∈ΓandΓ∈K n we haveχ,ξ∈L n−1 A . Since T S⊢ A χandχ∈L n−1 A , Lemma 5.8 gives∆⊢ A χ. Since by construction ∆̸⊢ A R, it follows thatχ̸∈R, and sinceRandLpartition the setL n−1 A we haveχ∈L. Now we must haveξ∈Las well, for if we hadξ∈Rit would follow from(χ⇛ a ξ)∈ΓthatL⇛ a Γ R, contrary to what we know. Sinceξ∈Land∆∈R(L), for someα∈R(ξ)we haveα∈∆, so by Lemma A.1,∆⊢ A ξ. Finally, sinceξ∈L n−1 A , Lemma 5.8 implies T S⊢ A ξ, as desired.□ A.4 Range Lemma (Lemma 5.10) We follow the proof of Lemma 6.15 in [12], adapting it to our multi-agent and depth-bounded setting. Consider aΓ∈K m withm>0. We want to show the identity: [ Σ n a (Γ) =Γ ′ ∈K m−1 |∀α∈L ! A :⊞ a α∈Γimpliesα∈Γ ′ Proof.(⊆)SupposeΓ ′ ∈ S Σ n a (Γ), that is,Γ ′ ∈Sfor someS∈Σ n a (Γ). By definition ofΣ n a , sinceΓ∈K m we haveΓ ′ ∈K m−1 . Now letαbe a declarative and suppose⊞ a α∈Γ, that is,(⊤⇛ a α)∈Γ. Since S∈Σ n a (Γ)and T S⊢ A ⊤, it follows that T S⊢ A α. SinceΓ ′ ∈S, we have T S⊆Γ ′ , and so alsoΓ ′ ⊢ A α. I. Ciardelli239 Since⊞ a α∈ΓandΓ∈K m , it follows thatα∈L !m−1 A . SinceΓ ′ ⊢ A αandΓ ′ is closed under deduction relative toL !m−1 A , we haveα∈Γ ′ . (⊇)ConsiderΓ ′ ∈K m−1 and suppose for allα∈L ! A ,⊞ a α∈Γimpliesα∈Γ ′ . We must show that Γ ′ ∈Sfor someS∈Σ n a (Γ). First, we claim that /0̸⇛ a Γ ¬α|α∈Γ ′ . Towards a contradiction, suppose not: then there areα 1 ,...,α n ∈Γ ′ such that(⊤⇛ a ¬α 1 ⩾ · ⩾ ¬α n )∈Γ. Since¬α 1 ⩾ · ⩾ ¬α n ⊢ A ¬(α 1 ∧·∧α n ), by Conditional Necessitation and Transitivity we have(⊤⇛ a ¬α 1 ⩾ · ⩾ ¬α n )⊢ A (⊤⇛ a ¬(α 1 ∧·∧α n )). Since(⊤⇛ a ¬(α 1 ∧·∧α n ))∈L m A andΓis deductively closed with respect toL m A , we conclude(⊤⇛ a ¬(α 1 ∧·∧α n ))∈Γ, that is,⊞ a ¬(α 1 ∧·∧α n )∈Γ. By our assumption on Γ ′ , we must have¬(α 1 ∧·∧α n )∈Γ ′ . But this is impossible, since eachα i is inΓ ′ andΓ ′ is consistent. We have thus established the claim /0̸⇛ a Γ ¬α|α∈Γ ′ . By Lemma A.8, we can partition the languageL m−1 A into setsL,RwithL̸⇛ a Γ Rand¬α|α∈Γ ′ ⊆R. Reasoning as in the previous lemma, we can find a∆∈R(L)with∆̸⊢R, and we can show that the corresponding set ofm−1-bounded complete extensionsS m−1 ∆ is inΣ n a (Γ). We now claim thatΓ ′ ∈S m−1 ∆ . To show this, it suffices to show that∆∪Γ ′ ̸⊢ A ⊥: if this holds, it follows by Lemma 5.4 that there is aΓ ′ ∈K m−1 with∆∪Γ ′ ⊆Γ ′ . Since two bounded elements ofK m−1 cannot be properly included in one another, we must haveΓ ′ =Γ ′ , and therefore∆⊆Γ ′ , showing thatΓ ′ ∈S m−1 ∆ as desired. So, towards a contradiction, suppose∆∪Γ ′ ⊢ A ⊥. SinceΓ ′ is closed under conjunction, this means that there is a single formulaα∈Γ ′ such that∆∪α⊢ A ⊥, and so,∆⊢ A ¬α. But this is impossible, since by construction¬α∈Rand∆̸⊢R. To conclude, we have found a stateS m−1 ∆ such thatΓ ′ ∈S m−1 ∆ andS m−1 ∆ ∈Σ n a (Γ), thus showing that Γ ′ ∈ S Σ n a (Γ), as required. A.5 Support Lemma (Lemma 5.11) We must show that for allm≤n, all formulasφ∈L m A , and all non-empty statesS⊆K m we have M n ,S|=φ⇐⇒ \ S⊢ A φ The proof is by induction onφ, simultaneously for allS⊆K m . The cases for atoms and connectives are standard (see the proof of Lemma 4.3.15 in [10]). We spell out the inductive step for a modal formula φ= (ψ⇛ a χ). Note that since we are assumingφ∈L m A we havem>0 andψ,χ∈L m−1 A . Suppose T S⊢ A (ψ⇛ a χ). We must showM n ,S|= (ψ⇛ a χ). For this, take an arbitrary worldΓ∈S and a stateT∈Σ n a (Γ)withM n ,T|=ψ. We need to show thatM n ,T|=χ. By definition ofΣ n a we have T⊆K m−1 . By induction hypothesis onψ, fromM n ,T|=ψwe obtain T T⊢ A ψ. SinceΓ∈Swe have T S⊆Γ, and since T S⊢ A (ψ⇛ a χ)alsoΓ⊢(ψ⇛ a χ). Since(ψ⇛ a χ)∈L !m A andΓ∈K m , it follows that(ψ⇛ a χ)∈Γ. By definition ofΣ n a , fromT∈Σ n a (Γ),(ψ⇛ a χ)∈Γ, and T T⊢ A ψwe can conclude T T⊢ A χ. Finally, by induction hypothesis onχ, this givesM n ,T|=χ, as required. For the converse, suppose T S̸⊢ A (ψ⇛ a χ). Then there is someΓ∈Ssuch that(ψ⇛ a χ)̸∈Γ. Since (ψ⇛ a χ)∈L m A andΓ∈K m , by completeness we have¬(ψ⇛ a χ)∈Γ. By the Existence Lemma (Lemma 5.9) there is a stateT∈Σ m a (Γ)such that T T⊢ A ψand T T̸⊢ A χ. By induction hypothesis on ψandχ, this means thatM n ,T|=ψandM n ,T̸|=χ. Hence,M n ,S̸|= (ψ⇛ a χ).□ 240Inquisitive Action Logic References [1] Thomas Ågotnes, Valentin Goranko, Wojciech Jamroga & Michael Wooldridge (2015):Knowledge and ability. In Wiebe van der Hoek Hans van Ditmarsch, Joseph Halpern & Barteld Kooi, editors:Handbook of Epistemic Logic, College Publications, p. 543–589. [2] Rajeev Alur, Thomas Henzinger & Orna Kupferman (2002):Alternating-time Temporal Logic.Journal of the ACM49(5), p. 672–713, doi:10.1145/585265.585270. [3] Alexandru Baltag, Ilaria Canavotto & Sonja Smets (2021):Causal agency and responsibility: a refinement of STIT logic. In:Logic in High Definition, Springer, p. 149–176, doi:10.1007/978-3-030-53487-5_8. [4] Johan van Benthem, Nick Bezhanishvili, Sebastian Enqvist & Junhua Yu (2017):Instantial neighbourhood logic.The Review of Symbolic Logic10(1), p. 116–144, doi:10.1017/S1755020316000447. [5] Mark A. Brown (1988):On the Logic of Ability.Journal of Philosophical Logic17(1), p. 1–26, doi:10.1007/BF00249673. [6] Nils Bulling, Valentin Goranko & Wojciech Jamroga (2015):Logics for Reasoning About Strategic Abilities in Multi-player Games, p. 93–136. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-662- 48540-8_4. [7] Ivano Ciardelli (2014):Modalities in the realm of questions: axiomatizing inquisitive epistemic logic. In Rajeev Goré, Barteld Kooi & Agi Kurucz, editors:Advances in Modal Logic (AIML), College Publications, London, p. 94–113. [8] Ivano Ciardelli (2018):Dependence Statements Are Strict Conditionals. In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe & Thomas Studer, editors:Advances in Modal Logic (AIML), College Publi- cations, London, p. 123–142. [9] Ivano Ciardelli (2022):Describing Neighborhoods in Inquisitive Modal Logic. In Sophie Pinchinat, David Fernandez-Duque & Alessandra Palmigiano, editors:Advances in Modal Logic (AIML), College Publica- tions, London, p. 217–236. [10] Ivano Ciardelli (2023):Inquisitive Logic. Consequence and inference in the realm of questions. Springer, doi:10.1007/978-3-031-09706-5. [11] Ivano Ciardelli (2025):Global supervenience in inquisitive modal logic.The Review of Symbolic Logic 18(2), p. 589–615, doi:10.1017/S175502032500005X. [12] Ivano Ciardelli (2025):Inquisitive Neighborhood Logic.Journal of Logic, Language and Information34(5), p. 419–461, doi:10.1007/s10849-025-09440-0. [13] Ivano Ciardelli, Jeroen Groenendijk & Floris Roelofsen (2018):Inquisitive Semantics. Oxford University Press, doi:10.1093/oso/9780198814788.001.0001. [14] Ivano Ciardelli & Martin Otto (2021):Inquisitive Bisimulation.The Journal of Symbolic Logic86, p. 77–109, doi:10.1017/jsl.2020.77. [15] Ivano Ciardelli & Floris Roelofsen (2015):Inquisitive dynamic epistemic logic.Synthese192(6), p. 1643– 1687, doi:10.1007/s11229-014-0404-7. [16] Stéphane Demri, Valentin Goranko & Martin Lange (2016):Temporal logics in computer science: finite-state systems. 58, Cambridge University Press, doi:10.1017/CBO9781139236119. [17] Thom van Gessel (2020):Action models in inquisitive logic.Synthese197, p. 3905–3945, doi:10.1007/s11229-018-1886-5. [18] Thom van Gessel (2021):Questions in two-dimensional logic.The Review of Symbolic Logic, p. 1–30, doi:10.1017/S1755020321000186. [19] Valentin Goranko & Govert van Drimmelen (2006):Complete axiomatization and decidability of Alternating- time temporal logic.Theoretical Computer Science353(1–3), p. 93–117, doi:10.1016/j.tcs.2005.07.043. I. Ciardelli241 [20] Valentin Goranko & Sebastian Enqvist (2018):Socially friendly and group protecting coalition logics. In: Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2018), p. 372–380. [21] Valentin Goranko, Wojciech Jamroga & Paolo Turrini (2013):Strategic games and truly playable effectivity functions.Autonomous Agents and Multi-Agent Systems26(2), p. 288–314. [22] Tadeusz Litak & Albert Visser (2018):Lewis meets Brouwer: Constructive strict implication.Indagationes Mathematicae29(1), p. 36–90, doi:10.1016/j.indag.2017.10.003. [23] Emiliano Lorini, Dominique Longin & Eunate Mayor (2014):A logical analysis of responsibility attri- bution: emotions, individuals and collectives.Journal of Logic and Computation24(6), p. 1313–1339, doi:10.1093/logcom/ext072. [24] Stipe Mari ́ c & Tin Perkov (2024):Decidability of Inquisitive Modal Logic via Filtrations.Studia Logica, p. 1–19, doi:10.1007/s11225-024-10134-0. [25] Silke Meißner & Martin Otto (2022):A first-order framework for inquisitive modal logic.The Review of Symbolic Logic15(2), p. 311–333, doi:10.1017/S175502032100037X. [26] Marc Pauly (2002):A modal logic for coalitional power in games.Journal of logic and computation12(1), p. 149–166, doi:10.1093/logcom/12.1.149. [27] Vít Pun ˇ cochá ˇ r & Igor Sedlár (2021):Epistemic extensions of substructural inquisitive logics.Journal of Logic and Computation31, p. 1820–1844, doi:10.1093/logcom/exab008. [28] Vít Pun ˇ cochá ˇ r & Igor Sedlár (2021):Inquisitive propositional dynamic logic.Journal of Logic, Language and Information30(1), p. 91–116, doi:10.1007/s10849-020-09326-3. [29] Krister Segerberg, John-Jules Meyer & Marcus Kracht (2016):The Logic of Action. In Edward N. Zalta, editor:The Stanford Encyclopedia of Philosophy, winter 2016 edition, Metaphysics Research Lab, Stanford University.