First-Order Coalition Logic

TL;DR

This paper introduces First-Order Coalition Logic ($ ext{FOCL}$), a highly expressive logic combining coalition and strategy logics, with a complete axiomatisation and implications for the satisfiability problem and recursive axiomatisability.

Contribution

It presents the first complete axiomatisation of any variant of Strategy Logic and demonstrates that $ ext{FOCL}$ surpasses existing coalition logics in expressiveness.

Findings

$ ext{FOCL}$ is strictly more expressive than existing coalition logics.

Provides the first sound and complete axiomatisation of a variant of $ ext{SL}$.

Reopens the question of recursive axiomatisability of $ ext{SL}$.

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}$.