d4-conf-atal-2007-0083

The strongest positive case I see is the model-checking result. Theorem 2, proved in this paper, says that model checking JAL is \(\Delta^p_2\)-hard when an aggregation rule is represented by a polynomially bounded Turing machine that takes a judgment profile as input and returns a judgment set. It also says the problem is NP-hard even when the query has the form \(\Diamond\psi\), where \(\psi\) contains no further \(\Box\) or \(\Diamond\) operators. The result is a hardness bound, not a completeness claim.

Lead mirror — Role-mass JAL model checking. Fix a finite agenda \(A\), an underlying logic \(L\), and constituency roles \(R=\{1,\ldots,n\}\) with positive rational population shares \(q_r\) summing to one. Let \(J(A,L)\) be the complete, consistent judgment sets. A type is a pair \((r,J)\): a role and a complete judgment set. A society is a rational distribution \(\mu\) over these types, with total mass \(q_r\) in each role. Its support size is \(\tau\), and its masses are given in binary.

For a role \(r\), let \(D_r(\mu)\) be the judgment set with greatest mass within that role, with a fixed tie-breaking rule. A continuous aggregation rule \(\mathcal F\) maps each such society to a complete, consistent collective judgment set. In the JAL interpretation, \(h_p\) means the current agenda item is \(p\), \(\sigma\) means \(p\in\mathcal F(\mu)\), and the atom \(r\) means \(p\in D_r(\mu)\). The modal operator \(\Box\) quantifies over all rational societies with the same agenda, roles, and role shares.

An instance gives \(A,L,q\), a finite-support society \(\mu_0\), an item \(p\), a formula \(\phi\), and a polynomial-time representation of \(\mathcal F\). The question is whether \(\mathcal F,\mu_0,p\models\phi\). Its answer is yes or no; there is no optimization objective. The relevant input parameters include \(n\), the agenda and formula sizes, the rule representation, \(\tau\), and the bit length of the masses.

This has a plausible high-multiplicity setting: large constituencies deliberating over a policy agenda, where each resident has a complete, rational judgment set and the constituency’s public position is its most common complete view. The roles and their policies are part of an agent’s type, so members who differ on either are distinct types. The regime is many residents but comparatively few roles and observed types. For any discrete rule \(f\), define \(\mathcal F_f(\mu)=f(D_1(\mu),\ldots,D_n(\mu))\). Every ordinary judgment profile is represented by a society placing all of role \(r\)’s mass on its profile judgment. Conversely, every society induces a legal profile through its \(D_r\)’s. Thus the modal states visible to the logic are exactly the original profiles, and the model-checking question retains the paper’s semantics on those states. This gives a route for Theorem 2’s hardness to carry over, with polynomial overhead in evaluating the \(D_r\)’s.

I would expect this mirror to be hardness that transfers (Class B), since the hard profile-model-checking problem embeds in it. The mirror covers Theorem 2’s computational result only; it does not claim to continuize the paper’s axiomatization, Arrow’s theorem, or all judgment aggregation. Further questions include whether the \(\Delta^p_2\) bound can be matched for this encoding, and whether hardness persists for anonymous, role-free aggregation rules whose decisions depend directly on population shares.

The soft spot is that the original paper’s \(i\) denotes an individual agent, whereas this mirror treats it as a constituency’s most common coherent view. The population masses determine that view, but the logic and rule then see the selected judgment set rather than every detail of the mass distribution. A referee might regard this as a natural two-level judgment aggregation problem, or might find it too indirect a continuous version of the authors’ original model. The hardness transfer is exact once that constituency interpretation is accepted.