Beyond Ability: The Four-Fold Spectrum of Power and the Logic of Full Inability

TL;DR

This paper introduces a four-fold spectrum of coalition power, including full inability, and develops a logical framework to analyze these strategic states with algebraic, order-theoretic, and proof-theoretic tools.

Contribution

It defines and formalizes a symmetric four-region classification of coalition power, extending Coalition Logic with a primitive for Full Inability and analyzing its properties.

Findings

The four power regions form an order-convex structure in the powerset lattice.

Axiomatization of the logic CLFI with soundness and completeness results.

The extension maintains the same expressive power and complexity as standard Coalition Logic.

Abstract

Coalition Logic studies what coalitions can enforce. Recent work treats inability as simple non-ability: $\neg\Eff{C}\varphi$. This conflates two distinct configurations -- a coalition unable to force $\varphi$ may still force $\neg\varphi$, retaining adversarial control rather than genuine inability. We introduce \textbf{Full Inability} ($\FI$): the symmetric condition in which a coalition can enforce neither a proposition nor its negation. Combining coalitional effectivity with propositional negation yields a four-fold spectrum: \textbf{Full Control} ($\FC$), \textbf{Positive Determination} ($\PD$), \textbf{Adverse Determination} ($\AD$), and \textbf{Full Inability} ($\FI$). These categories partition a coalition's strategic status exhaustively and exclusively. We establish their algebraic and order-theoretic structure. Under $\alpha$-duality, propositional negation and coalition complementation generate a Klein four-group symmetry. In playable models, the four power regions are order-convex in the powerset lattice, yielding interval-stable verification of inability. We axiomatize $\CLFI$, a definitional extension treating Full Inability as a primitive modality. Via elimination translation, we prove soundness, completeness, and conservativity over Coalition Logic. The extension preserves expressive power and complexity ($\PSPACE$-complete), but provides direct proof-theoretic access to symmetric inability, strategic dependence, propositional dummyhood, and containment verification.