First-Order Coalition Logic

Theorem 2 is unquestionably a named computational result, so bit (a) holds. But the proposed blocks behave as macro-agents, and multiplicity has no independent strategic role under the original \(A^n\) action semantics. Making mass operative requires a new anonymous flow-transition model and a new lifting of FOCL quantifiers, so no recognised continuous population mirror survives.

The objection that survived

With FOCL's original decisions in \(A^n\), each \(B_i\) is forced to take one action, so \(\mu\) can be compiled into the transition instance; making individual multiplicity operative requires new flow or policy semantics and abandons identity-sensitive transitions.

What the mirror covers

The proposed candidate targets only Theorem 2; no result is covered by an accepted population mirror. Theorem 3, Theorem 1, the expressivity propositions, and the axiomatisation remain untouched.

Open questions for a prover

The case FOR (proponent)

The strongest honest case is a single anchor: Theorem 2, which states that “the model checking problem for FOCL is PSPACE-complete.” This is a result proved by the authors in this work (with proof details also given in their cited extended version), not merely imported from elsewhere. It is a better anchor than Theorem 3: FOCL satisfiability is undecidable, but its undecidability comes from the existence of unbounded models and tiling, not naturally from population multiplicity.

My lead mirror is High-Multiplicity FOCL Model Checking.

The intended regime is a large replicated protocol or smart-contract ecosystem. There are \(N\) agents, but only \(\tau\) complete types, where a type records everything relevant to the transition system: protocol role, available actions, local capabilities, and any contribution the transition rule can inspect. Type \(t\) has mass \(\mu_t\in\mathbb{Q}_{\ge 0}\), with \(\sum_t\mu_t=1\). The actual population size \(N\) is not part of the instance; any sufficiently large population realizing the same rational proportions represents the same society, and \(N\gg\tau\).

This is plausible for replicated validators, automated trading agents, smart-contract users, or network participants following a small number of protocol roles. The paper itself motivates FOCL through smart-contract swaps, Stackelberg security games, and Nash-equilibrium verification, so a population of many indistinguishable protocol participants is recognizably their setting rather than an unrelated application.

Formally, an instance consists of a finite action alphabet \(A\), a finite type set partitioned into \(n\) role blocks \(B_1,\ldots,B_n\), a rational mass vector \(\mu\), a finite global state space \(S\), an initial state \(s_0\), a valuation \(V\) of atomic propositions, an exact transition representation \(\delta\), and a closed FOCL formula \(\varphi\). The transition rule takes a state and an aggregate action-flow vector \(\rho\). For a role-level action profile \(\vec a=(a_1,\ldots,a_n)\in A^n\), define \(\rho^{\vec a}\) by \(\rho^{\vec a}_{t,a}=\mu_t\) when \(t\in B_i\) and \(a=a_i\), and \(\rho^{\vec a}_{t,a}=0\) otherwise. The transition is \(s'=\delta(s,\rho^{\vec a})\). The representation of \(\delta\) may be an explicit finite table or a polynomial-time exact circuit using rational linear tests on \(\rho\).

The FOCL syntax and quantifier semantics remain unchanged. An action constant denotes a fixed role action, a variable denotes an element of \(A\), and \(\forall x\) ranges over all \(a\in A\). Thus \( ((t_1,\ldots,t_n))\psi \) holds at \(s\) exactly when the aggregate flow induced by the corresponding action tuple leads to a state \(s'\) satisfying \(\psi\). The problem asks whether \(G_\mu,s_0\models\varphi\); a solution is the correct yes/no answer, together with the usual quantified-action witness or counterexample if one is required.

I expect this problem to remain PSPACE-complete, so it is a Class B mirror: hardness transfers rather than disappearing. The PSPACE upper bound uses the same alternating recursive evaluation as Theorem 2. The current state, formula position, quantified action values, and rational aggregate flow require only polynomial space. For hardness, take any finite FOCL model-checking instance from Theorem 2, replace each original agent by a high-multiplicity type block of mass \(1/n\), and define \(\delta(s,\rho^{\vec a})\) to reproduce the original transition on \(\vec a\). The two instances satisfy exactly the same formulas by induction. The blocks may represent arbitrarily many identical agents, so this is genuinely a high-multiplicity realization rather than merely renaming the original model.

The continuous object here is the society \(\mu\), not the state space, the outcome space, or a noise distribution. Individual identities disappear because the protocol treats members of a type block symmetrically. FOCL’s arbitrary alternation over actions remains computationally meaningful: the difficulty is driven by the formula’s strategic quantifier structure, not by the number of named people.

The weakest point is that this mirror imposes uniformity within a type block. It cannot express one member of a large cohort deviating while all other members remain fixed, and it replaces an arbitrary named-agent transition rule with an anonymous aggregate transition rule. If the authors regard every agent as intrinsically individuated, this will look like a change of problem rather than continuization. The case survives only in the replicated-protocol regime, where role-level actions and aggregate effects are exactly what the application cares about. A natural follow-up would introduce a tagged infinitesimal deviator, but that is a different problem.

The mirror also generates useful further questions: whether type blocks may split their mass among several actions; whether mixed action allocations \(q_{t,a}\) lead to real-arithmetic or continuum-specific complexity; and how FOCL’s Nash and Stackelberg readings behave when a single deviator has zero mass. I would not claim that this one mirror covers Theorem 3, the axiomatisation result, or the expressivity propositions. It emphatically covers Theorem 2, and that is enough for a credible positive case.

The case AGAINST (opponent, writing after the proponent)

Theorem 2 is the only serious anchor, but its proposed mirror fails at the level of what is being continuized. FOCL is not a profile of many interchangeable agents. A CGS has \(n\) strategically distinguished coordinates, a decision in \(A^n\), and an arbitrary transition relation \(R\) that may depend on which coordinate chose which action. The formula’s variables range over action labels, and reusing a variable expresses equality of actions between named coordinates—not equality of voter types or a population policy.

The proposed construction therefore does not actually clone the agents. For each original coordinate \(i\), it creates a block \(B_i\) whose entire mass is forced to take the single action \(a_i\). This is a macro-agent with a weight attached. The multiplicity is behaviourally invisible: the formula still quantifies over one action per original coordinate, and no individual in a block can deviate independently. If the transition rule is represented explicitly, \(\mu\) can simply be compiled into the transition table. The resulting problem is weighted finite-model checking, not model checking over a continuous society.

Allowing members of a block to choose independently does not repair this while preserving FOCL. The relevant object then becomes an action-flow vector \(q_{i,a}\), not an action tuple \((a_1,\ldots,a_n)\). One must decide whether \(\forall x\) ranges over individual actions, type-level policies, flow vectors, or measurable assignments. The semantics of the formula, including its action-sharing patterns, consequently changes. Moreover, an arbitrary FOCL transition relation cannot be recovered from aggregate flow: two assignments with the same flow may differ in the identities of the agents who acted. Preserving that information makes the agents distinct types; discarding it imposes anonymity that the paper never assumes.

The strongest repair would restrict attention to anonymous replicated protocols and define a transition map \(\delta(s,q)\) on aggregate action flows. That is coherent, but it is a new anonymous or mean-field game model, not a continuous version of Theorem 2. The paper gives no canonical flow semantics, no representation for \(\delta\) on the continuum of flows, and no rule for how strategic quantifiers lift to that domain. An explicit table covers only finitely many pure profiles and reduces to the original finite problem; a circuit or piecewise-linear map introduces a new input model whose complexity is determined by choices external to FOCL.

There is also a substantive degeneration in the paper’s motivating equilibrium readings. In a nonatomic population, one individual’s deviation has zero mass and cannot change an aggregate transition. Nash and Stackelberg-style strategic influence therefore either becomes vacuous or requires a distinguished positive-mass coalition, which again changes the logic’s subject. Treating an entire type block as one decision-maker avoids that degeneration only by abandoning individual multiplicity.

Thus the two possible routes both fail as mirrors: retaining FOCL leaves the population absent, while making the population operative replaces its action semantics, transition model, and strategic objects. An anonymous flow-based logic might be worthwhile as a new research topic, but this paper does not supply a principled continuous mirror for it. The negative case is consequently strong against the claimed anchor, though not mathematically airtight against someone deliberately developing that separate mean-field extension.

The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.