| paper | Voting by Axioms |
| authors | — |
| venue | AAMAS 2023 |
| filed under | frontier · tools-data |
| judged by | gpt-5.6-terra / high (triple__gpt-5.6-terra__high__ctx2r8-rejudge1) |
| judge confidence | high |
| authors would recognise it | yes |
Theorem 6
statement extracted from the paper’s text layer
Given alternatives \(C\), a rational society \(\mu\in\Delta(L(C))\), and a nontrivial finite propositional axiom formula \(\Phi\) over atoms \(p_{\nu,c}\) for explicitly named rational societies \(\nu\), decide whether every continuous voting rule \(F:\Delta(L(C))\to\mathcal{P}^{+}(C)\) satisfying \(\Phi\) assigns the same outcome to \(\mu\).
Society types are complete rankings \(t\in L(C)\), with masses \(\mu_t\); the universally quantified admissible decision object is a continuous voting rule \(F:\Delta(L(C))\to\mathcal{P}^{+}(C)\), and the objective is to decide whether \(\Phi\) uniquely fixes \(F(\mu)\).
The flat propositional encoding constrains only finitely many named societies, so the simplex's aggregate geometry does not affect the inherited coNP-completeness result.
fatal: False
The mirror directly covers Theorem 6 and the associated task of deciding whether an axiom corpus forces an outcome; it leaves the paper's axiomatic characterisation results alone.
I think this paper has a defensible, but deliberately narrow, continuous mirror. Its strongest anchor is Theorem 6, proved in this paper: ExistsForced is coNP-complete in the combined size of the propositional \(L\)-encodings of the supplied axioms. This is the result I would lead with; I would not pad the case with the paper’s axiomatic characterisation results, which are less clearly computational continuizations.
Call the continuous problem Continuous ExistsForced (the lead problem). Let \(C\) be the alternatives and let \(T=L(C)\) be the finite set of complete preference rankings. An instance contains a rational society
\[
\mu\in\Delta(T),
\]
together with a finite propositional axiom encoding \(\Phi\). Its atomic propositions have the form \(p_{\nu,c}\), where \(\nu\in\Delta(T)\) is a rational society explicitly named in the input and \(c\in C\). Their intended meaning is: “\(c\) belongs to the collective outcome for society \(\nu\).”
A continuous voting rule is a function
\[
F:\Delta(T)\rightarrow {\cal P}^+(C).
\]
It satisfies \(p_{\nu,c}\) exactly when \(c\in F(\nu)\), and it satisfies \(\Phi\) under the ordinary propositional semantics. We call \(\Phi\) nontrivial if some such \(F\) satisfies it. The question is whether all continuous voting rules satisfying \(\Phi\) give exactly the same nonempty outcome on \(\mu\). A solution is Yes/No; in the Yes case, the unique forced outcome is the associated decision.
This is not a mass-transfer LP, because the paper’s computational object is not manipulation but necessity: does the axiom corpus leave any latitude at this society? The societal mass vector is the instance, the output is the collective choice, and the universally quantified “decision variable” is the admissible continuous rule \(F\). Equivalently, the non-forcing witness consists of two admissible rules that disagree at \(\mu\).
The high-multiplicity regime is plausible in a setting quite different from the authors’ stated small, high-stakes committee application: a large public consultation, member-owned platform, union, professional association, or city-wide participatory decision process choosing among a small set of policy alternatives. The institution observes an aggregate distribution of complete rankings, and maintains a ranked corpus of publicly defensible decision principles. Here “\(23\%\) rank policy \(a\) above \(b\) above \(c\)” is the natural input, not a list of named people. With, say, four to seven alternatives, there may be hundreds of thousands of participants but only a small active subset of the at-most-\(m!\) ranking types. The normative corpus is institutional, rather than a feature that each individual agent must carry, so aggregating agents with the same ranking loses no information the decision uses.
The familiar axioms translate naturally. For example, continuous Condorcet says that if
\[
\sum_{t:\,a\succ_t b}\mu_t>1/2
\]
for every \(b\neq a\), then \(F(\mu)=\{a\}\). Continuous Pareto says that if all mass ranks \(a\) above \(b\), then \(b\notin F(\mu)\). These are genuinely conditions on a society distribution, rather than on a finite voter list. A practical language should express such conditions as compact arithmetic schemas, but the problem above mirrors the paper’s own explicit \(L\)-encoding regime: a finite formula can name the finitely many societal profiles it needs to constrain.
I expect Continuous ExistsForced to be Class B: hardness transfers. The transfer is especially clean for the paper’s own proof of Theorem 6. That proof establishes hardness on a subfamily with one voter, using the distinct one-voter rankings \(R_1,\ldots,R_{m!}\) as named profiles. Map each \(R_i\) to the point-mass society \(\delta_{t_i}\), and replace every atom \(p_{R_i,c}\) by \(p_{\delta_{t_i},c}\). Satisfaction of the constructed formula is unchanged. Any truth assignment on those finitely named societies extends to a continuous voting rule by assigning an arbitrary nonempty outcome at every other society. Thus the SAT reduction survives verbatim in the continuous model. Conversely, the usual two-model witness establishes membership in coNP, because only the finitely named atomic propositions need be recorded; unconstrained societies can again be completed arbitrarily. So this is not merely an analogy: in the extensional encoding used by Theorem 6, the continuous version is coNP-complete as well.
The interesting new questions are therefore not whether arbitrary propositional axiom corpora become easy—they should not—but whether compact, socially meaningful continuous axiom languages change the landscape. In particular:
I think the authors would recognise this as their problem’s continuous analogue for Theorem 6: it keeps their forcing semantics, their arbitrary axiom encodings, and their question of whether axioms uniquely determine an outcome, while replacing an electorate profile by an anonymous distribution over complete voter types. It does not claim that every practical deployment of “voting by axioms” should be large-scale, nor that the paper’s whole agenda is naturally high-multiplicity.
The weakest point is also clear. The inherited coNP-hardness lives at point-mass societies, so it demonstrates a valid continuous problem and a genuine Class-B boundary, but it does not yet exploit the analytic or optimization benefits that motivate continuization elsewhere. Moreover, the paper itself explicitly presents its method as best suited to small groups. The case survives because the theorem is about a general forcing formalism, not specifically about intimate committees, and because large-population institutional decisions with aggregate preferences are a credible second regime. But the strongest positive claim is modest: this paper has one solid continuous computational mirror, with hardness preserved; obtaining a richer tractable continuous theory requires moving beyond its flat propositional encoding.
The only computational anchor is Theorem 6, and its proposed lift exposes a real weakness: it is a syntactic relabelling, not a population-level relaxation. The theorem’s reduction uses one-voter profiles solely as names for propositional variables. Replacing each by a Dirac society replaces those names by different names. An admissible “continuous rule” is otherwise completely arbitrary on the simplex, so neither nearby mass vectors nor the distribution’s aggregate structure constrain anything. Fractions enter only as labels of finitely many atoms. That is not the kind of high-multiplicity object from which column generation, convexity, robustness, or even a meaningful notion of approximation could emerge.
The stronger continuous formulation would replace the flat atoms by quantified arithmetic axiom schemas over \(\mu\): Condorcet regions, Pareto faces, reinforcement under mixture, and so on. But that is no longer Theorem 6’s problem. It requires a new representation language and, crucially, a substantive choice of regularity and semantics for rules over the simplex. The paper’s coNP result says essentially nothing about that setting: its proof depends precisely on permitting unrelated constraints at finitely many isolated profiles. A complexity theory for such schemas could be worthwhile, but it would be a new programme on computational reasoning with continuous axioms, rather than a continuization of the paper’s named result.
That is the strongest negative case available: reject the proponent’s flat-encoding “continuous” problem as an uninformative domain relabelling, and insist that a meaningful version must be rebuilt rather than inherited from Theorem 6.
But it does not defeat the anchor in the universal sense required here. A large public consultation or membership vote genuinely can be represented by a distribution over ranking types; identity is irrelevant, and Pareto and Condorcet have natural mass-based meanings. Once one permits the stronger arithmetic-schema version, there is plainly a sensible continuous computational question about whether an institutional axiom corpus forces an outcome at \(\mu\). The paper’s small-committee motivation weakens its fit, but does not eliminate that separate high-multiplicity regime.
So the honest negative verdict is weak. The proponent’s particular coNP-completeness claim should not be mistaken for evidence of a rich continuization, but it supplies a defensible anchor, and a better continuous reformulation survives the objections.
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.