First-Order Coalition Logic
Davide Catta, Rustam Galimullin, Aniello Murano
TL;DR
This paper introduces $FOCL$, a first-order coalition logic that merges coalition reasoning with first-order quantification over actions and explicit action labels, positioning it as strictly more expressive than existing coalition logics. It provides a sound and complete axiomatisation for $FOCL$, marking the first such result for a variant of strategy logic, and establishes that $FOCL$ enjoys PSPACE-model checking while its satisfiability is undecidable, thereby reopening questions about recursive axiomatisability of $SL$. The authors situate $FOCL$ within the expressivity landscape of coalition logics, show translations from $CL$ and $AL$, and demonstrate the ability to capture equilibria and strategy sharing, with implications for verification and security/contractual applications. The work lays groundwork for further extensions (e.g., with LTL modalities) and invites exploration of imperfect information and connections to STIT logics, highlighting both theoretical and practical significance in strategic reasoning domains.
Abstract
We introduce First-Order Coalition Logic ($\mathsf{FOCL}$), which combines key intuitions behind Coalition Logic ($\mathsf{CL}$) and Strategy Logic ($\mathsf{SL}$). Specifically, $\mathsf{FOCL}$ allows for arbitrary quantification over actions of agents. $\mathsf{FOCL}$ is interesting for several reasons. First, we show that $\mathsf{FOCL}$ is strictly more expressive than existing coalition logics. Second, we provide a sound and complete axiomatisation of $\mathsf{FOCL}$, which, to the best of our knowledge, is the first axiomatisation of any variant of $\mathsf{SL}$ in the literature. Finally, while discussing the satisfiability problem for $\mathsf{FOCL}$, we reopen the question of the recursive axiomatisability of $\mathsf{SL}$.