First-Order Coalition Logic

1 Introduction

Logics for strategic reasoning constitute a numerous family of formal tools devised to model, verify, and reason about the abilities and strategies of (groups of) autonomous agents in a competitive environment [Pauly, 2002; Alur et al., 2002; van der Hoek et al., 2005; Mogavero et al., 2014; Chatterjee et al., 2010]. Strategies here are 'recipes' telling agents what to do in order to achieve their goals. The competitive environment part arises from the fact that in the presence of several agents trying to achieve their own goals, the actions of one agent may influence the available strategies of another agent. Such logics have been shown to be invaluable for specification and verification within various domains: neuro-symbolic reasoning [Akintunde et al., 2020], voting protocols [Jamroga et al., 2018], autonomous submarines [Ezekiel et al., 2011], manufacturing robots [de Silva et al., 2017], and so on.

The prime representatives of logics for strategic reasoning are coalition logic (CL) [Pauly, 2002], alternating-time temporal logic (ATL), [Alur et al., 2002], and strategy logic (SL) [Mogavero et al., 2010] (and numerous variations thereof). CL extends the language of propositional logic with constructs ⟨⟨C⟩⟩φ meaning 'coalition C has a joint action such that φ holds in the next state (no matter what agents outside of the coalition do at the same time)'. ATL extends further the abilities of agents to force temporal goals expressed with the help of such modalities as 'Until' and 'Release'. Finally, SL allows for a more fine-tuned quantification over agents' abilities: while in both CL and ATL we have a fixed quantification prefix ∃∀, in SL we can have arbitrary quantification prefixes. Thus, in SL we can reason, for example, about agents sharing their strategies, and such game-theoretic notions like dominant strategies and Nash equilibria. Hence, ATL is strictly more expressive than CL, and, in turn, SL is strictly more expressive than ATL (and its more general cousin ATL∗ ).

Sound and complete axiomatisations of CL [Pauly, 2002; Goranko et al., 2013] and ATL [Goranko and van Drimmelen, 2006] are now classic results in the field. However, to the best of our knowledge, no axiomatisations of SL, nor any of its variants, have been considered in the literature so far.

In this paper, we introduce a novel variation of the nexttime fragment of SL that we call first-order coalition logic (FOCL) 1 . As its name suggests, FOCL combines the coalition reasoning capabilities of CL with the first-order features of SL. Specifically, we allow arbitrary quantification prefixes over agents' actions and also allow action labels to appear explicitly in the language. This makes FOCL to be closely related to ATL with explicit strategies [Walther et al., 2007].

We first show that FOCL is quite a special CL, being strictly more expressive than other known coalition logics. With such a remarkable expressivity comes the PSPACE-complete model checking problem and the undecidable satisfiability problem. While proving the undecidability result, we have also reopened the problem of the recursive axiomatisability of SL, which was until now assumed to be not recursively axiomatisable [Mogavero et al., 2010]. Moreover, we provide a sound and complete axiomatisation of FOCL, which is, as far as we can tell, the first axiomatisation of any variant of SL. Thus, we lay the groundwork for the axiomatisations of more expressive fragments and variants of SL.

The rest of the paper is structured as follows: Section 2 defines the syntax and semantics of FOCL, Section 3 examines its expressiveness, Section 4 presents a complete axiomatisation of FOCL, Section 5 addresses complexity, and Section 6 concludes with directions for future work.

2 Syntax and Semantics

Definition 1 (Language). A signature is a triple α = ⟨n, C, Ap⟩, where n ≥ 1 is a natural number, C is a non-empty countable set of constants, and Ap is a non-empty countable set of atomic propositions (or atoms) such that Ap ∩ C = ∅.

1 Not to be confused with quantified coalition logic [ ˚Agotnes et al., 2008], where quantification is over coalitions and which is as expressive as CL.

Fix a non-empty countable set V of variables that is disjoint from any other set in any given signature α. The language of first-order coalition logic (FOCL) is defined as

where p ∈ Ap, ti ∈ C ∪ V, x ∈ V, and all the usual abbreviations of propositional logic (such as ∨, →, ↔) and conventions for deleting parentheses hold. The existential quantifier ∃xφ is defined as ¬∀x¬φ. Formula ((t1, ..., tn)) φ is read as 'after the agents execute actions assigned to t1 · · · tn, φ is true', and ∀xφ is read as 'for all actions x, φ holds'. Given a formula φ ∈ FOCL, the size of φ, denoted by |φ|, is the number of symbols in φ.

Definition 2 (Free Variables). Given a formula φ, we define its set of free variables FV(φ) by the following cases:

1. If φ ∈ Ap, then FV(φ) = ∅;
2. If φ = ¬φ1, then FV(φ) = FV(φ1);

A formula φ such that FV(φ) = ∅ is called a closed formula, or a sentence.

Definition 3 (Kripke Frame). A Kripke frame is a tuple F = ⟨Σ, S, R⟩, where Σ is a non-empty countable alphabet, S is a non-empty set of states s.t. Σ∩S = ∅, and R ⊆ S×Σ×S is a ternary relation, dubbed transition relation. F is serial if for every s ∈ S and a ∈ Σ, there is a t ∈ S s.t. ⟨s, a, t⟩ ∈ R. F is functional whenever for all s, t, v ∈ S and for every a ∈ Σ, if ⟨s, a, t⟩ ∈ R and ⟨s, a, v⟩ ∈ R, then t = v.

Definition 4 (Concurrent Game Structure). A game frame is a tuple G = ⟨n, Ac,D, S,R⟩ with triple ⟨D, S,R⟩ being a serial and functional Kripke frame, where: n is a positive natural number and D is a set of tuples of elements of Ac of length n (elements of this set will be called decisions).

A Concurrent Game Structure (CGS) is a pair G = ⟨G, V⟩, where G is a game frame, and V : Ap → P(S) is a valuation function assigning to each atomic proposition a subset of S.

Let Prop(s) = {p ∈ Ap | s ∈ V(p)} be the set of all atomic propositions true in state s. We define the size of CGS G as |G| = n + |Ac| + |D| + |S| + |R| + ∑s∈S |Prop(s)|, where |D| = |Ac|n . We call CGS G finite, if |G| is finite.

Definition 5. Given a signature α = ⟨m, C, Ap⟩, and a CGS G = ⟨n, Ac, D, S, R, V⟩, we say that G is constructed over α iff m = n and C = Ac.

Definition 6 (Satisfaction). Let φ be a sentence and G be a CGS that are both constructed over the same signature α. The satisfaction relation G, s |= φ is inductively defined as follows:

where a1, ..., an are constants, and ψ[a/x] denotes the result of substituting every occurrence of the variable x with the constant a in ψ. We will also sometimes write ⃗a for a1 · · · an.

Definition 7 (Closure of a Formula). Given a formula φ whose set of free variables is {x1, . . . , xn}, we denote by C(φ) the closure of φ, which is the formula ∀x1 · · · ∀xnφ.

Definition 8 (Validity). Let G be a CGS constructed over a signature α, and φ a formula constructed over α. Given a state s of G, we write G, s |= φ iff G, s |= C(φ). We say that φ is valid in a CGS G (written G |= φ) iff G, s |= φ for every state s of G. Finally, we say that φ is valid (written |= φ) iff it is valid in every CGS constructed over a signature with n agents. Given a set of formulae X, we write G, s |= X if for every formula φ ∈ X, G, s |= φ. Finally, we write X |= ψ and we say that ψ is a logical consequence of X iff G |= X implies G |= ψ for every CGS G constructed over the same signature as ψ and formulae in X.

Remark 1. Note that the truth of open (i.e. not closed) formulae is reduced to the truth of the closed ones via closure (Definition 7). This approach is fairly standard in first-order logic (see, e.g., [van Dalen, 1994]). We could also define the truth of a formula w.r.t. an assignment, but this would not affect the results presented here. Our choice simplifies the formal machinery of the paper and makes it more readable.

The next proposition, that follows straightforwardly from the seriality and functionality of frames, shows that we can give an alternative and equivalent characterisation of the truth of a strategic formula in a state of a CGS.

Proposition 1. Let G = ⟨n, Ac,D, S,R, V⟩ be a CGS, s ∈ S, and φ = ((a1, ..., an)) ψ, and suppose that both G and φ are constructed over the same signature α. Then G, s |= φ iff ∀t ∈ S: ⟨s, a1, . . . , an, t⟩ ∈ R implies G, t |= ψ.

Remark 2. Due to Proposition 1, we we have that G, s |= ((⃗a)) ψ iff G, t |= ψ for the unique t such that ⟨s,⃗a, t⟩ ∈ R.

Thus, FOCL can be also viewed as an extension of multimodal logic [Blackburn et al., 2001; Hennessy and Milner, 1980] for serial and functional frames with first-order quantification over components of arrow labels (i.e. actions).

Example 1. As observed in [Belardinelli et al., 2019], strategy logics are expressive enough to capture Stackelberg equilibrium (SE). Such an equilibrium is applicable to scenarios where a leader commits to a strategy, and the follower, observing the strategy of the leader, provides her best response. SE is prominent in security games [Sinha et al., 2018], where the attacker observes the defender committing to a defensive strategy and then decides on the best way to attack (if at all).

We can express such a scenario for the case of one-step strategies by the FOCL formula ∀xd∃xa∀xe((xd, xa, xe))wina, which intuitively means that for all actions of the defender, the attacker has a counter-action guaranteeing the win for all actions of the environment.

Similarly to [Mogavero et al., 2010], with FOCL we can express the existence of deterministic Nash equilibrium (NE) for Boolean goals. If ψ1, ..., ψn are goal formulae of agents, we can assert the existence of strategy profile x1, ..., xn such that if any agent i achieves her goal ψi by deviating from x1, ..., xn, then she can also achieve her goal by sticking to the action profile. The existence of such a profile can be expressed by the following FOCL formula:

FOCL also allows for strategy sharing. Consider examples of CGSs presented in Figure 1. In structure G1 we have two states s and t, and the agents can transition between the two states if they synchronise on their actions, i.e. execute the same actions. It is easy to verify that G1, s |= ∀x∃y((x, y)) p and G1, s |= ∀x((x, x)) ¬p.

The fact that FOCL is able to capture the Stackelberg and Nash equilibria is significant, since, compared to SL and its fragments that can also capture both equilibria, the complexity of the model checking problem for FOCL is PSPACEcomplete as shown in the proof of Theorem 2 (compared to the range from 2ExpTime to non-elementary for various SL's [Mogavero et al., 2014]). Moreover, the ability to capture the equilibria can have a significant impact on the prospective applications of FOCL. In particular, it was argued [van der Meyden, 2019; Galimullin and ˚Agotnes, 2022] that CL is suitable for specification and verification of atomic swap smart contracts that allow agents to exchange their assets or private information, like passwords, on a blockchain without necessarily trusting each other. We can use FOCL to verify that acting honestly is indeed a NE for a given specification of a contract. Moreover, having the ability to express strategy sharing, we can verify that a swap is still executable in the situation, where a malicious agent that gained access to the communication channel poses as one of the honest ones by executing the same actions 2 .

3 Relation to Other Coalition Logics

In order to appreciate the richness of FOCL, we compare the logic to other CL's. In our comparison we can use two salient features of FOCL. First, the logic allows for arbitrary quantification prefixes for agents' actions. This includes using the same strategy variable for different agents to capture strategy sharing. The second special feature of FOCL is the presence of explicit action labels in its syntax.

Definition 9 (Expressivity). Let L1 and L2 be two languages, and let φ ∈ L1 and ψ ∈ L2. We call φ and ψ equivalent, if for any CGS G and state s ∈ G: G, s |= φ iff G, s |= ψ. If for all φ ∈ L1 there exists an equivalent ψ ∈ L2, then L2 is at least as expressive as L1 (L1 ⩽ L2). And L2 is strictly more expressive than L1 (L1 < L2) if L1 ⩽ L2 and L2 ̸⩽ L1.

2 This is the classic person-in-the-middle attack scenario in cryptography.

These two features of FOCL, arbitrary quantification prefixes and explicit actions, on their own are not unique in the landscape of logics for strategic reasoning. Arbitrary quantification prefixes are a hallmark feature of the whole family of strategy logics (see, e.g., [Mogavero et al., 2010; Belardinelli et al., 2019]), to which FOCL belongs. Indeed, FOCL can be considered as a variation of the next-time fragment of SL. The idea to refer to actions in the language has also been explored, with a prime example being ATL with explicit strategies (ATLES) [Walther et al., 2007]. Another example of such a logic is action logic [Borgo, 2007].

Even though both of the main features of FOCL have been explored in the literature, to our knowledge, FOCL is the first logic for strategic reasoning that combines both of them.

Coalition logic andquantified coalition logic The original coalition logic (CL) [Pauly, 2002], similarly to ATL, allows only single alternation of quantifiers in coalitional modalities. Moreover, this quantification is implicit. Thus, CL extends the language of propositional logic with constructs ⟨⟨C⟩⟩φ that mean 'there is a strategy for coalition C to achieve φ in the next step'. In quantified coalition logic (QCL) [ ˚Agotnes et al., 2008], constructs ⟨⟨C⟩⟩φ are substituted with ⟨P ⟩φ meaning 'there exists a coalition C satisfying property P such that C can achieve φ'. Since QCL is as expressive as CL (although exponentially more succinct), we will focus only on CL.

To introduce the semantics of CL, we will denote the choice of actions by coalition C ⊆ Agt with |Agt| = n as σC, and denote Agt \ C as C. Finally, σC ∪ σC ∈ D is a decision. The semantics of ⟨⟨C⟩⟩φ for a given CGS G is then defined as

The translation from formulas CL to formulas of FOCL can be done recursively using the following schema for coalitional modalities: tr(⟨⟨C⟩⟩φ) → ∃⃗x∀⃗y((⃗x, ⃗y)) tr(φ), where variables ⃗x (all different) quantify over actions of C, and ⃗y (all different) quantify over actions of Agt \ C.

At the same time, one cannot refer to particular actions in CL formulas, as well as express sharing strategies between agents. We can exploit either of these features to show that FOCL is strictly more expressive than CL. Indeed, consider a FOCL formula ∃x((x, x))¬p meaning that there is an action that both agents 1 and 2 should use to reach a ¬p-state. We can construct two CGSs that are indistinguishable by any CL formulas. At the same time, ∃x((x, x))¬p will hold in one structure and be false in another.

Consider two structures depicted in Figure 1. It is easy to see that G1, s and G2, s cannot be distinguished by any CL formula 3 . Indeed, both structures agree on the valuation of propositional variable p in corresponding states. Moreover, none of the agents, 1 and 2, can on their own force a transition from state s to state t. At the same time, the grand coalition {1, 2} can match any transition in one structure with a transition with the same effect in the other structure. Now, we can verify that G1, s |= ∃x((x, x)) ¬p and G2, s ̸|= ∃x((x, x)) ¬p. For the case of G1, s |= ∃x((x, x))¬p, it is enough to assign action a to x to have G1, s |= ((a, a))¬p. To make ∃x((x, x))¬p hold in G2, s, one needs to provide an action that once executed by both agents will force the transition to state t. It is easy to see that there is no such an action in G2, s.

3 These structures are, in fact, in the relation of alternating bisimulation [ ˚Agotnes et al., 2007], and hence satisfy the same formulas of CL and ATL. The discussion of bisimulations for all the logics we mention is, however, beyond the scope of this paper, and we leave it for future work.

Having the translation from CL to FOCL on the one hand, and the indistinguishability result on the other, we hence conclude that FOCL is strictly more expressive than CL.

Proposition 2. CL < FOCL.

Conditional strategic reasoning and socially friendly CL With the expressive power of FOCL we can go much further than the classic CL. In particular, we can express in our logic such interesting CL's like logic for conditional strategic reasoning (ConStR) [Goranko and Ju, 2022], socially friendly CL (SFCL) [Goranko and Enqvist, 2018], and group protecting CL (GPCL) [Goranko and Enqvist, 2018].

Presenting the semantics of the aforementioned logic is beyond the scope of this paper. However, we would like to point out that all of the logics can be captured by basic strategy logic (BSL) [Goranko, 2023], a variant of SL, where each agent has her own associated strategy variable. Differently from FOCL, BSL allows for all standard temporal modalities like 'neXt', 'Until' and 'Globally'. At the same time, BSL does not allow for variable sharing and does not explicitly refer to actions or strategies. Moreover, it is conjectured that BSL does not have a recursive axiomatisation, while FOCL has a finitary complete axiomatisation (see Section 4).

Translations of all coalition logics introduced in this paragraph into formulas of BSL are presented in [Goranko, 2023], where it is also claimed that BSL is strictly more expressive than all the aforementioned logics. The translation does not employ any temporal features of BSL apart from 'neXt', and thus the same translation also works for FOCL. Moreover, we can use either strategy sharing or explicit actions to argue that FOCL is strictly more expressive than the considered coalition logics. As an example, an argument for the case of SFCL is given in [Catta et al., 2025].

Proposition 3. ConStR < FOCL, SFCL < FOCL, GPCL < FOCL.

Action logic A perhaps most relevant to FOCL coalition logic in the literature is action logic (AL) [Borgo, 2007], which is a fragment of multi-agent PDL with quantificaiton (mPDLQ) [Borgo, 2005b]. AL extends the language of propositional logic with so-called modality markers [M], which are, essentially, prefixes of size |Agt| = n, each element of which can either be a quantifier Qixi with Qi ∈ {∀, ∃} or an explicit action [Borgo, 2005b; Borgo, 2005a]. An important feature here is that there are no repeating variables in modality markers. Finally, to the best of our knowledge, there is no axiomatisation of AL.

Given a modality marker [M], we denote by σ∃ a choice by all the existentially quantified agents, by σ∀ a choice by all the universally quantified agents, and by σact explicit actions in the corresponding positions in [M]. Then modality markers have the following semantics:

Intuitively, G, s |= [M]φ holds if and only if there is an assignment of actions to all existentially quantified variables in modality marker M such that no matter which actions are assigned to the universally quantified variables, once combined with the explicit actions, the outcome state satisfies φ. This is in line with the semantics of CL as we basically choose actions for a coalition (existentially quantified variables) and verify ψ in all possible outcomes given this choice.

Formulae [M]φ of AL can be translated into formulae of FOCL of the form ∃⃗x∀⃗y((t1, ..., tn))φ, where ⃗x and ⃗y with |⃗x| + |⃗y| ⩽ n are possibly empty sequences of variables for the existentially and universally quantified agents respectively, ti := xi if there is a quantifier in position i in the modality marker, and ti := ai if there is action ai in the ith posiiton in the modality marker. Also recall that AL does not allow for sharing strategies (while FOCL does), i.e. all x1, ..., xm in the modality marker are unique.

To show that FOCL is more expressive than AL, we need the following proposition. Its proof utilises the strategy sharing feature of FOCL and can be found in [Catta et al., 2025].

Proposition 4. AL is not at least as expressive as FOCL.

Having the translation from AL to FOCL on the one hand, and Lemma 4 on the other, we can conclude that FOCL is strictly more expressive than AL.

Corollary 1. AL < FOCL.

The expressivity landscape In this section we have explored the relationship between FOCL and other notable CL's from the literature. The overall expressivity landscape of the considered logics is presented in Figure 2.

4 Proof Theory

Perhaps the best-known results in the field are complete axiomatisations of CL [Pauly, 2002; Goranko et al., 2013] and ATL [Goranko and van Drimmelen, 2006] (see [Walther et al., 2006; Goranko and Shkatov, 2009] for more constructive approaches). Other completeness results include axiomatisations for logics based on CL and ATL, like already mentioned SFCL [Goranko and Enqvist, 2018], ATLES [Walther et al., 2007], as well as epistemic CL [ ˚Agotnes and Alechina, 2019], resource-bounded CL [Alechina et al., 2011] and ATL [Nguyen et al., 2018], and ATL with finitely bounded semantics [Goranko et al., 2019], to name a few.

In the context of strategy logics, we have quite an opposite picture. Since the inception of SL [Mogavero et al., 2010], its axiomatisation has been an open problem. The same can be said about any of the fragments of SL. The lack of axiomatisations of any (fragment of) SL can be traced back to the two main features of the logic: quantification over strategies and arbitrary quantification prefixes.

Indeed, arbitrary alternation of quantifiers in SL is quite different from the fixed quantification prefix of CL and ATL that allow only prefixes ∃∀ and ∀∃. Secondly, quantification over strategies 4 in SL is essentially a second-order quantification over functions. We believe that these two features combined are the root cause of the fact that no complete axiomatisations of (fragments of) SL have been proposed so far.

In FOCL we focus on arbitrary quantification prefixes. To solve this sub-problem, we consider only neXt-time modalities ((t1 · · · tn))φ and deal with the immediate outcomes of agents' choices. This allows us, in particular, to consider quantification over actions rather than strategies. Hence, quantification in FOCL is a first-order quantification, instead of the second-order quantification of SL.

In our proof, we take as inspiration the completeness proof for first-order modal logic (FOML) with constant domains [Garson, 1984]. Our construction is quite different, though, as in FOML variables appear in n-ary predicates, and in FOCL variables are placeholders for transition labels.

4.1 Axiomatisation of FOCL

Definition 10 (Axiomatisation). The axiom system for FOCL consists of the following axiom schemata and rules, where ⃗t = t1, . . . , tn for n ⩾ 1, and t and each ti are either a variable or a constant.

PC Every propositional tautology

K (((⃗t))φ∧ ((⃗t))ψ) ↔ ((⃗t)) (φ∧ψ)

E ∀xφ→φ[t/x]

B ∀x((⃗t))φ→ ((⃗t)) ∀xφ, s.t. ti ̸= x for all ti

MP From φ, φ→ψ, infer ψ

Nec From φ, infer ((⃗t))φ

Gen From φ→ψ[t/x], infer φ→ ∀xψ, if t ̸∈ φ

An axiomatic derivation π is a finite sequence of formulae φ1, . . . , φm where for each i ⩽ m: either φi is an instance of one of the axiom schemata of FOCL, or it is obtained from some preceding formulae in the sequence using rules MP, Nec, or Gen. We write ⊢ φ and say that φ is FOCL derivable (or simply derivable) iff there is a derivation π whose last element is φ. Given a set of formulae X, we write X ⊢ φ iff there is a finite subset Y of X such that ⊢ ∧ Y → φ.

4 A (memoryless) strategy for an agent i ∈ n is a function σi : S → Ac.

We will freely use the following proposition in the rest of the paper. Its proof is standard, and we omit it for brevity.

Proposition 5. The following formulae are FOCL derivable, where ⃗t = t1, . . . , tn, and each ti is either a constant or a variable:

Moreover, if φ→ψ is derivable, so is ((⃗t))φ→ ((⃗t))ψ.

Lemma 1. Each axiom schema of FOCL is valid and each rule of FOCL preserves validity.

The proof of Lemma 1 is done by the application of the definition of the semantics, and it can found in [Catta et al., 2025].

Our completeness proof is based on the canonical model construction, where states are maximal consistent sets with the ∀-property.

Definition 11 (Maximal Consistent Sets). Let Z be a set of FOCL sentences over a given signature and X ⊆ Z. We say that: (i)X is consistent iff X ̸⊢ ⊥, (ii) X is maximally consistent (MCS) iff it is consistent and there is no other consistent set of sentences Y ⊆ Z s.t. X ⊂ Y , and (iii) X has the ∀-property iff for every formula φ over the same signature as Y and variable x, there is a constant a such that φ[a/x] → ∀xφ ∈ X, where φ[a/x] is closed. We will call a set satisfying all the three requirements ∀-MCS.

Let α = ⟨n, C, Ap⟩ be a signature. We denote by α⋆ the signature ⟨n, C ∪ C ⋆ , Ap⟩ where C ⋆ is countably infinite, and C ∩ C ⋆ = ∅.

Next lemma shows that each consistent set of sentences over a given signature α can be extended to a consistent set of sentences over α⋆ having the ∀-property. Its proof follows the standard technique in FOML [Cresswell and Hughes, 1996], and can be found in [Catta et al., 2025].

Lemma 2. If X is a consistent set of sentences over a given signature α, then there is a consistent set of sentences Y over α⋆ such that X ⊆ Y , and Y has the ∀-property.

The proof of the following lemma (Lindenbaum Lemma) is standard, and we omit it for brevity.

Lemma 3. Let X be a consistent set of sentences over a given signature, then there is an MCS Y over the same signature such that X ⊆ Y .

The next two lemmas will be instrumental in the proof of the Truth Lemma, and showing that the canonical model we are to define in this proof is indeed a CGS.

Lemma 4. Let X be a consistent set of sentences over a given signature and let ⃗a be a tuple of constants, then the set Y⃗a = {ψ | ((⃗a)) ψ ∈ X} is also consistent.

Proof. If Y⃗a is empty, the result is trivially valid. Assume that φ ∈ Y⃗a and suppose towards a contradiction, that set Y⃗a is not consistent. This implies that (ψ1 ∧· · ·∧ψm) → ¬φ for some finitelty many ψ1, . . . , ψm in Y⃗a. Using Proposition 5(1) and propositional reasoning, we can then derive ((⃗a))ψ1 ∧ · · · ∧ ((⃗a))ψm → ((⃗a))¬φ. Since ((⃗a))ψi ∈ X, we conclude by MP that X ⊢ ((⃗a))¬φ. Then, by N and MP we can further derive X ⊢ ¬((⃗a)) φ, which contradicts ((⃗a)) φ ∈ X.

Lemma 5. Let X be a ∀-MCS over a given signature containing infinitely many constants. Then there exists a ∀-MCS Y over the same signature such that Z = {ψ | ((⃗a))ψ ∈ X} ⊆ Y .

Proof. If Z = ∅, the lemma trivially holds. So assume φ ∈ Z, and let E be an enumeration of all sentences of the form ∀xξ, and C an enumeration of the constants in the given signature. We define a sequence of sentences θ0, θ1, . . . where θ0 = φ, and given θn, we set θn+1 = θn ∧ (ξ[a/x] → ∀xξ), where ∀xξ is the (n + 1)-th formula in E, and a is the first constant in C such that

Let Y = Z ∪ {θn | n ∈ N}. Clearly Y has the ∀-property, and it is consistent if Z ∪ {θn} is consistent for every n ∈ N. To show this, we prove that if Z ∪ {θn} is consistent, then there always exists a constant a satisfying (⋆). The set Z ∪ {θ0} = Z is consistent by Lemma 4.

Suppose, towards a contradiction, that Z ∪ {θn} is consistent but for every constant a, the set Z ∪ {θn ∧ (ξ[a/x] → ∀xξ)} is inconsistent. Then for each constant a, there exist finitely many formulas ψa 1 , . . . , ψam in Z such that (ψa 1 ∧ · · · ∧ ψam) → (θn → ¬(ξ[a/x] → ∀xξ)) is derivable. From this, by the rules of FOCL, it follows that (((⃗a))ψa 1 ∧ · · · ∧ ((⃗a))ψam) → ((⃗a)) (θn → ¬(ξ[a/x] → ∀xξ)) is derivable. Since ψa i ∈ Z implies ((⃗a))ψa i ∈ X, we conclude that (i) ((⃗a)) (θn → ¬(ξ[a/x] → ∀xξ)) ∈ X for every constant a.

Let z be a variable that occurs neither in θn nor in ξ. Consider the sentence ∀z ((⃗a)) (θn → ¬(ξ[z/x] → ∀xξ)). From the ∀-property of X and (i), it follows that ∀z ((⃗a)) (θn → ¬(ξ[z/x] → ∀xξ)) ∈ X. By axiom B, this implies ((⃗a)) ∀z(θn → ¬(ξ[z/x] → ∀xξ)) ∈ X, and thus, by (2) of Prop. 5, we have (ii) ((⃗a)) (θn → ∀z¬(ξ[z/x] → ∀xξ)) ∈ X. Since ∃z(ξ[z/x] → ∀xξ) is derivable in FOCL, applying rule Nec gives ((⃗a)) ∃z(ξ[z/x] → ∀xξ) ∈ X. From this, together with (ii), and using Proposition 5, we conclude ((⃗a))¬θn ∈ X. By the construction of Z, this implies ¬θn ∈ Z, which contradicts the assumption that Z ∪ {θn} is consistent.

Definition 12 (Canonical Model). Given a signature α = ⟨n, C, Ap⟩, the canonical model over α is the tuple GC = ⟨n, AcC , DC , SC , RC , V C ⟩, where:

• AcC = C ∪ C ⋆ ;
• DC = AcCn ;
• SC = {X | X is a ∀-MCS over α⋆ };
• for every⃗a ∈ DC , ⟨X,⃗a, Y ⟩ ∈ RC iff for every sentence φ we have that φ ∈ Y implies ((⃗a)) φ ∈ X;
• X ∈ V C (p) iff p ∈ X for all p ∈ Ap.

The proof of the next proposition is in [Catta et al., 2025]. Proposition 6. For all states X, Y ∈ SC and for every decision ⃗a ∈ DC , it holds that ⟨X,⃗a, Y ⟩ ∈ RC iff for every sentence φ, ((⃗a)) φ ∈ X implies φ ∈ Y

Now we are ready to show that GC is indeed a CGS (proof in [Catta et al., 2025]), and then prove the Truth Lemma.

Proposition 7. The canonical model GC is a CGS.

Lemma 6 (Truth Lemma). For any state X ∈ SC and for any sentence φ, we have that GC , X |= φ iff φ ∈ X.

Proof. The proof is by induction on φ. The base case φ = p follows from the definition of V C . Boolean cases follow from the induction hypothesis (IH) and the properties of MCSs.

Case φ = ((⃗a))ψ. Let GC ,X |= φ. By the definition of semantics, this means that there is a Y such that ⟨X,⃗a, Y ⟩ ∈ RC and GC , Y |= ψ. The latter is equivalent to ψ ∈ Y by the IH, and by the definition of RC we conclude that φ ∈ X.

Let φ ∈ X. By Lemma 5, there is a maximal consistent set of sentences Y over α⋆ that has the ∀-property and such that {ψ} ∪ {θ | ((⃗a)) θ ∈ X} ⊆ Y . By Proposition 6 this means ⟨X,⃗a, Y ⟩ ∈ RC , which, in conjunction with the fact that ψ ∈ Y , is equivalent to GC ,X |= φ by the IH.

Case φ = ∀xψ. If GC ,X |= φ, then, by the IH, it holds that (i) ψ[a/x] ∈ X for every a ∈ AcC . Now, assume towards a contradiction that φ ̸∈ X. Since X is maximally consistent, we have that ¬∀xψ ∈ X. Moreover, since X has the ∀-property, there is a constant a such that ψ[a/x] → ∀xψ ∈ X. Then by (i) it follows that ∀xψ ∈ X, which contradicts ∀xψ ̸∈ X.

Suppose that φ ∈ X, which implies, by axiom E and MP, that ψ[a/x] ∈ X for every a ∈ AcC . By the IH, we conclude that GC , X |= φ[a/x] for every a ∈ AcC , which is equivalent to GC , X |= ∀xφ by the definition of semantics.

We finally prove the completeness of FOCL.

Theorem 1. For every set of formulae X and every formula φ, we have that X ⊢ φ iff X |= φ.

Proof. Let X ̸⊢ φ. This means that X ∪ {¬φ} is consistent, and, by Lemmas 2 and 3, there is a ∀-MCS Z, such that X ∪ {¬φ} ⊆ Z. As ¬φ ∈ Z, it holds that φ /∈ Z, and by the truth lemma we have that GC , Z |= X and GC , Z ̸|= φ.

5 Complexity Profile of FOCL

Now we turn to the complexity profile of FOCL, and show that the complexity of the model checking problem PSPACEcomplete and that the satisfiability problem is undecidable.

Model Checking Let G = ⟨n, Ac,D, S,R, V⟩ be a finite CGS, s ∈ S, and closed formula φ ∈ FOCL constructed over a signature of G. The local model checking problem for FOCL consists in computing whether G, s |= φ.

Theorem 2. The model checking problem for FOCL is PSPACE-complete.

Proof. To show that the model checking problem for FOCL is in PSPACE, we provide an alternating recursive Algorithm 1 5

5 For brevity, we omit Boolean cases and the whole algorithm is available in [Catta et al., 2025]

that takes as an input a finite CGS G, state of the CGS s, and a closed formula φ. The formula φ is provided in negation normal form (NNF), i.e. in equivalent rewriting, where all negations are pushed inside and appear only in front of propositional variables. To convert φ into the equivalent NNF formula, we can use propositional equivalences, interdefinability of quantifiers, and the validity ¬((⃗t))φ ↔ ((⃗t))¬φ. The size of a formula in NNF is at most linear in the size of the original formula. The correctness of the algorithm follows from the

1: procedure MC(G, s, φ) 2: case φ = ((a1, ..., an)) ψ 3: guess t ∈ S such that ⟨s, a1, ..., an, t⟩ ∈ R 4: return MC(G, t, ψ) 5: case φ = ∃xψ 6: guess a ∈ Ac 7: return MC(G, s, ψ[a/x]) 8: case φ = ∀xψ 9: universally choose a ∈ Ac 10: return MC(G, s, ψ[a/x]) 11: end procedure

definition of the semantics. Its termination follows from the fact that every recursive call is run on a subformula of smaller size. Moreover, each call of the algorithm takes at most polynomial time, and hence it is in APTIME. From the fact that APTIME = PSPACE [Chandra et al., 1981], we conclude that the model checking problem for FOCL is in PSPACE.

The hardness can be shown by the reduction from the satisfiability of quantified Boolean formulas (see [Catta et al., 2025]).

Remark 3. The model checking problem for a related SL with simple goals (SL[SG]) is P-complete [Belardinelli et al., 2019]. This is due to the fact that in SL[SG] the quantification prefix and the operators for assigning strategies to agents always go together. Hence, for example, the FOCL formula over two agents θ := ∀x∃y∀z(((z, x))φ ∧ ((z, y))ψ ∧ ((x, z))χ) cannot be expressed in SL[SG]. The higher complexity of FOCL stems from the fact that quantifiers and strategy assignments are less rigid than in SL[SG], and thus FOCL is closer to the full SL in this regard.

Satisfiability Let φ ∈ FOCL be a closed formula. The satisfiability problem for FOCL consists in determining whether there is a CGS G, s such that G, s |= φ.

Theorem 3. The satisfiability problem for FOCL is undecidable.

The undecidability can be shown by employing the construction for SL from [Mogavero et al., 2010; Mogavero et al., 2017] using the reduction from the classic tiling problem [Wang, 1961]. In their construction, the authors use only formulae of the next-time fragment of SL, and the proof can be adapted for FOCL (see [Catta et al., 2025] for details).

Remark 4. A knowledgeable reader may point out that the proof in [Mogavero et al., 2010; Mogavero et al., 2017] employed the reduction from a more complex recurring tiling problem [Harel, 1983]. The problem is known to be Σ11 - complete, and this in particular implies that the next-time fragment of SL, and hence FOCL, is not recursively axiomatisable. This is at odds with the axiomatisation of FOCL presented in this paper. However, after a closer inspection, it turned out that the Σ11 -hardness proof provided in [Mogavero et al., 2010; Mogavero et al., 2017] is incomplete (though the standard, non-recurring, tiling construction stands, and hence the (standard) undecidability). As of now, no fix to this problem has been presented, and hence the existence of a recursive axiomatisation of SL is now an open question. Note, again, that the (standard) undecidability still holds 6 .

6 Discussion

We introduced first-order coalition logic (FOCL), which combines features of both CL and SL, and, additionally, allows for explicit action labels in the syntax. With FOCL we have solved several exciting problems. First, we showed that it is strictly more expressive than other known CL's, and that its model checking problem is PSPACE-complete. We then also argued that the satisfiability problem for FOCL is undecidable, pointing out an incomplete result in the foundational SL paper [Mogavero et al., 2010] and thus reopening the question of whether SL is recursively axiomatisable. Moreover, we provided a sound and complete axiomatisation of FOCL. This is significant, since, to the best of our knowledge, it is the first axiomatisation of any strategy logic.

There is a plethora of open research questions that one can tackle building on our work. Perhaps the most immediate one is finding an axiomatisation of an extension of FOCL with LTL modalities. In such a way, we would be able to advance towards axiomatisations of such rich fragments of SL as onegoal SL [Mogavero et al., 2017] and flat conjunctive-goal SL [Acar et al., 2019]. It is also quite interesting to consider FOCL in the context of imperfect information (see [ ˚Agotnes et al., 2015] for an overview).

While dealing with the undedicability of FOCL, we mentioned the next-time fragment of SL. To the best of our knowledge, such a fragment has never been singled out and studied before. Hence, it is tempting to look into the variations of this fragment 7 , identify the axiomatisable ones, and have a proper comparison of the latter with FOCL.

As STIT logics [Horty, 2001] admit CGS semantics [Boudou and Lorini, 2018; Broersen and Herzig, 2015], another avenue of exciting further research is establishing the exact relation between FOCL and variants of STIT logics like group STIT [Herzig and Schwarzentruber, 2008; Lorini and Schwarzentruber, 2011].

6 The gap in the proof of non-axiomatisability of SL was acknowledged and corroborated by the authors of [Mogavero et al., 2010; Mogavero et al., 2017] in personal communication. The general sentiment is that SL is still not recursively axiomatisable, but to show this result, one will have to employ richer features of SL, beyond its next-time fragment.

7 There is a nuance in how we can define the next-time fragment of SL. Two obvious candidates are the fragment, where every neXt modality is immediately preceded by an assignment (similar to ATL), and the fragment, where we do not have such a condition (similar to ATL⋆ ).

Acknowledgements

The authors would like to thank Valentin Goranko for the discussion of the preliminary ideas of this paper, Fabio Mogavero for the discussion of the undecidability of SL, and the anonymous reviewers of IJCAI for their superb comments and suggestions.

This work has been partially funded by the MUR PRIN project RIPER (No. 20203FFYLK), and the PNRR MUR projects FAIR (No. PE0000013-FAIR) and INFANT (No. E23C24000390006).