The seventh rung · what a group can force

Strategic Arithmetic

Every rung so far is about a single agent. This one is about groups. A coalition can ensure an outcome when it has a joint strategy that forces it no matter what the other agents do. That one idea — ability against an adversary — turns a pile of independent agents into something you can reason about as a system: who can guarantee safety, who can reach a goal, and who can't do it without help. It's also the rung that makes obligation honest, because you can only be obligated to ensure what you can actually force.

IThe algebra

The setting is a concurrent game structure: a set of states; a set of agents; for each agent at each state, the moves available to it; and a transition that takes a state plus one move from every agent at once to a successor. Nobody moves alone — every step is the joint product of all the agents' choices, which is what makes it a game rather than a single-agent machine.

Everything is built from one operation, the controllable predecessor: the states from which a coalition C can force the next state into a target set — ∃ moves for C, ∀ moves for the rest, the successor lands in the set. That single quantifier alternation (C chooses, then the adversary chooses, and C must still win) is the whole idea of ability.

From the controllable predecessor, the temporal abilities follow as fixpoints — the same machinery the temporal rung uses, now played against an adversary. Maintenance, ⟨⟨C⟩⟩□φ ("C can keep φ true forever"), is the greatest fixpoint: the largest set of φ-states from which C can always force the next state to stay in the set. Reachability, ⟨⟨C⟩⟩◊φ ("C can drive the system to φ"), is the least fixpoint: φ-states, plus every state from which C can force its way one step closer, until nothing new is added.

IIThe laws

Eight for coalitional ability, three for the bridges to the rest of the ladder. The highlighted cross-check shows coalition power growing with size — the grand coalition reaches everything a lone agent can, and usually more.

IIIThe laws, checked

Each law against random concurrent game structures in your browser — same engine that ships in box-and-box.

IVType sketch

// a concurrent game: states, agents, moves per agent per state, joint transition
interface Game {
  states: State[]; agents: Agent[];
  moves: (a: Agent, s: State) => MoveId[];
  delta: (s: State, joint: Record<Agent,MoveId>) => State;   // one move from EVERY agent
}

function effectivity(g: Game, C: Agent[], s: State, φ: Formula): boolean; // [C]◯φ
function canKeep(g: Game, C: Agent[], φ: Formula, s: State): boolean;     // ⟨⟨C⟩⟩□φ — gfp
function canEnsure(g: Game, C: Agent[], φ: Formula, s: State): boolean;   // ⟨⟨C⟩⟩◊φ — lfp

// the bridges
function oblige(g, C, φ, s): "discharge"|"escalate";            // ought-implies-can
function executable(g, C, φ, s, commonKnowledge: boolean): boolean; // ability ∧ CK

VWorked example

A controller and an environment share the game above. The controller can keep the system safe on its own, but the goal is only reachable when the environment cooperates — so an obligation on the controller alone to reach the goal cannot be discharged and must escalate to recruit the environment. Runs live.

VIStanding on

The effectivity operator [C]φ — what a coalition can guarantee against the worst case — is Pauly's coalition logic (2002). Lifting it over time with maintenance and reachability is Alur, Henzinger & Kupferman's Alternating-time Temporal Logic (2002), and the fixpoint computations are the controllable-predecessor algorithms from game-based controller synthesis. The bridges are where it earns its place in the ladder: a one-agent game is just the temporal rung (reachability with no adversary); ought-implies-can sends impossible obligations back up to the deontic rung; and joint execution needs the common knowledge of the epistemic rung. As elsewhere, the logic is established; the contribution is the executable, property-tested synthesis and the connections across the stack.