First-Order Coalition Logic

We introduce First-Order Coalition Logic ($\mathsf{F}\mathsf{O}\mathsf{C}\mathsf{L}$), which combines key intuitions behind Coalition Logic ($\mathsf{C}\mathsf{L}$) and Strategy Logic ($\mathsf{S}\mathsf{L}$). Specifically, $\mathsf{F}\mathsf{O}\mathsf{C}\mathsf{L}$ allows for arbitrary quantification over actions of agents. $\mathsf{F}\mathsf{O}\mathsf{C}\mathsf{L}$ is interesting for several reasons. First, we show that $\mathsf{F}\mathsf{O}\mathsf{C}\mathsf{L}$ is strictly more expressive than existing coalition logics. Second, we provide a sound and complete axiomatisation of $\mathsf{F}\mathsf{O}\mathsf{C}\mathsf{L}$, which, to the best of our knowledge, is the first axiomatisation of any variant of $\mathsf{S}\mathsf{L}$ in the literature. Finally, while discussing the satisfiability problem for $\mathsf{F}\mathsf{O}\mathsf{C}\mathsf{L}$, we reopen the question of the recursive axiomatisability of $\mathsf{S}\mathsf{L}$.