| paper | A Calculus for Computing Structured Justifications for Election Outcomes |
| authors | Arthur Boixel, Ulle Endriss, Ronald de Haan |
| venue | AAAI 2022 |
| filed under | voting · theory |
| judged by | gpt-5.6-luna / xhigh (triple__luna__xhigh__c22r1) |
| judge confidence | medium |
| authors would recognise it | yes |
Theorem 4
statement extracted from the paper’s text layer
Given a finite alternative set \(X\), ranking types \(T=L(X)\), finite rational mass-profile axiom instances \(\alpha=(\mu^1,\ldots,\mu^k,R_\alpha)\) with \(R_\alpha\subseteq\Omega^k\), a rational \(\mu^\star\in\Delta(T)\), and \(X^\star\in\Omega=2^X\setminus\{\emptyset\}\), decide whether every anonymous homogeneous rule \(F_\infty:\Delta(T)\to\Omega\) satisfying all instances must satisfy \(F_\infty(\mu^\star)=X^\star\); equivalently, decide whether a rule satisfying the instances and \(F_\infty(\mu^\star)\in\Omega\setminus\{X^\star\}\) exists, and if not produce a closed tableau over the relevant mass profiles.
An anonymous homogeneous mass-profile voting rule \(F_\infty:\Delta(T)\to\Omega\), where \(T=L(X)\) and \(\mu_t\) is the fraction of voters of type \(t\). The input contains finitely many rational distributions and permitted-outcome relations; the decision concerns existence of a rule or a closed tableau, while outcomes remain discrete.
For finite axiom sets, replacing the distributions by abstract symbols yields essentially the same constraint problem, so the mass geometry may add no computational content; extending the result to axiom schemas over all of Δ(T) is also unproved.
fatal: False
The mirror covers Theorem 4 and its supporting finite-instance correctness argument, including Lemmas 1–3. It leaves the ASP implementation, proof-tree optimization, human-understandability experiments, and universal axiom schemas outside the mirror.
There is a real, though bounded, positive case. The lead anchor is Theorem 4 (Correctness), proved in this paper. It states that the tableau calculus is a sound and complete decision procedure for checking whether any voting rule satisfies a finite set of axiom instances together with a finite set of outcome statements. Lemmas 1–3, also proved here, establish termination, soundness, and completeness. The paper contains no named \( \mathrm{P} \), NP-hardness, W[1]-hardness, or approximation theorem; the SAT/ASP implementation and the cited complexity work of Boixel and De Haan are not additional anchors.
The natural mirror is an axiomatic justification problem for a large anonymous electorate. Let \(X\) be the alternatives, \(T=L(X)\) the finite set of ranking types, and
\[ \Delta(T)=\left\{\mu\in\mathbb{R}_{\ge 0}^{T}:\sum_{t\in T}\mu_t=1\right\}. \]
A type is a complete ranking \(t\in T\). A society is a distribution \(\mu\), where \(\mu_t\) is the fraction of voters of type \(t\). The outcome space remains exactly the paper’s discrete space
\[ \Omega=2^X\setminus\{\emptyset\}. \]
A continuous voting rule is a function
\[ F_\infty:\Delta(T)\rightarrow\Omega. \]
Thus the population is continuous, but winners are not fractional. The decision variable is the outcome \(F_\infty(\mu)\), or, in the tableau search, the partial assignment of outcomes to the finitely many societies mentioned by the axioms. The objective is to determine whether a target outcome is forced and, when it is, produce a structured proof.
A finite continuous axiom instance can be represented as a tuple
\[ \alpha=(\mu^1,\ldots,\mu^k,R_\alpha), \]
where the \(\mu^i\) are rational society distributions and \(R_\alpha\subseteq\Omega^k\) specifies the permitted outcome tuples. A rule satisfies \(\alpha\) exactly when
\[ \bigl(F_\infty(\mu^1),\ldots,F_\infty(\mu^k)\bigr)\in R_\alpha. \]
This is the direct mass-profile analogue of the paper’s local axiom instances. The familiar axioms have natural continuous forms:
\[ F_\infty(\delta_t)=\{\operatorname{top}(t)\} \]
for faithfulness,
\[ F_\infty(\pi\mu)=\pi(F_\infty(\mu)) \]
for neutrality under a permutation \(\pi\) of alternatives, and
\[ F_\infty(\lambda\mu+(1-\lambda)\nu) = F_\infty(\mu)\cap F_\infty(\nu) \]
whenever the two outcomes overlap, for reinforcement. Anonymity is built into the representation: named profiles with the same type distribution are identified.
The continuous problem is:
Continuous Structured-Justification Decision, \( \mathrm{CSJ}_\infty \). Given \(X\), a finite set \(E\) of continuous axiom instances, a rational society \(\mu^\star\), and a target outcome \(X^\star\in\Omega\), decide whether every continuous voting rule satisfying \(E\) must satisfy
\[ F_\infty(\mu^\star)=X^\star. \]
Equivalently, decide whether there exists no \(F_\infty\) satisfying \(E\) and
\[ F_\infty(\mu^\star)\in\Omega\setminus\{X^\star\}. \]
A yes-solution is a closed tableau rooted in
\[ \left\{\left(\mu^\star,\Omega\setminus\{X^\star\}\right)\right\}, \]
with axiom-driven expansions using instances from \(E\). A no-solution certificate is an open saturated branch, which specifies a consistent partial continuous voting rule on all relevant society distributions and can be extended arbitrarily elsewhere. This is precisely the paper’s Theorem 4 with profiles replaced by mass distributions.
The paper’s motivating example survives transparently. With \(X=\{E,K\}\), let \(t_E\) rank \(E\) above \(K\), and \(t_K\) rank \(K\) above \(E\). The three-voter profile becomes
\[ \mu^\star=\frac{2}{3}\delta_{t_E}+\frac{1}{3}\delta_{t_K}. \]
Using the continuous versions of faithfulness, anonymity, neutrality, and reinforcement, the question is whether those principles force
\[ F_\infty(\mu^\star)=\{E\}. \]
The original proof’s one-voter group and two-voter group become the societies \(\delta_{t_E}\) and \(\frac12\delta_{t_E}+\frac12\delta_{t_K}\), combined with reinforcement using weights \(1/3\) and \(2/3\). This is not a new story pasted onto the paper: it is the same proof after quotienting duplicate ballots into mass.
The regime is a large anonymous electorate with a fixed catalogue of ballot types: for example, a national election, repeated platform consultation, or institutional vote in which millions of participants fall into a relatively small number of preference classes. If \(\mu_t=n_t/n\), clearing denominators recovers a finite election with \(n_t\) clone voters of type \(t\). Conversely, an anonymous homogeneous rule on such high-multiplicity profiles induces \(F_\infty\) on rational distributions. The denominator affects encoding length, but not the number of agents represented. This gives the required high-multiplicity bridge.
I would expect the unrestricted version to fall on the hardness-transfer side, Class B, rather than being continuum-specifically hard. The population multiplicity disappears, but the combinatorics of alternatives, winner subsets, axiom branching, and tableau structure remain. The finite tableau procedure is therefore a genuine algorithmic mirror, but Theorem 4 does not imply polynomial time; its tableau may be exponential. For fixed, tightly specified axiom families and small alternative sets, tractable subcases are plausible, but that would be a new complexity result rather than something established by this paper.
The weakest point is that the mirror imposes homogeneity. The original \(F\) is formally defined over profiles with named electorates and may distinguish a three-voter profile from a \(300\)-voter profile with the same proportions. Passing to \(\mu\) identifies them. Thus this is best described as an extension to anonymous, population-scale-invariant voting rules, not a literal mirror of every rule allowed by the paper. That limitation does not undermine the example-driven case: the paper’s central motivating axioms already treat voter identity as normatively irrelevant, and the continuous model makes that intended symmetry explicit.
The main follow-up questions are whether the rational-clone correspondence is exact for every anonymous axiom corpus, whether shortest or most intelligible continuous tableaux have a distinct complexity, and whether the finite-instance theorem extends to axiom schemas quantified over all of \(\Delta(T)\). The last question is genuinely new: Theorem 4 only handles finitely many axiom instances, so a universal continuous version should not be claimed for free.
The strongest negative case is that the paper has no qualifying ChoCo anchor. Theorem 4 is called a “decision procedure,” but it is a correctness theorem for a finite axiomatic satisfiability calculus, not a complexity result about a computational social-choice problem on a society. The SAT/ASP implementation does not change that subject. The paper computes proofs that a voting rule cannot satisfy certain local constraints; it does not compute winners, interventions, robustness, or any other population-dependent object.
The proposed \( \mathrm{CSJ}_\infty \) exposes the problem. Given a finite set of continuous axiom instances, let \(P=\{\mu^1,\ldots,\mu^q\}\) be the finitely many distributions mentioned. The tableau ever observes only the finite tuple
\[ \bigl(F_\infty(\mu^1),\ldots,F_\infty(\mu^q)\bigr). \]
Replace each \(\mu^j\) by an abstract symbol \(p_j\), and replace each axiom instance by the same permitted-outcome relation on those symbols. One obtains exactly the same finite constraint problem. Denominators, clone counts, and the geometry of \(\Delta(T)\) never enter the computation. The mass distributions are labels, not computational objects.
This also defeats the motivating \(2/3\)-versus-\(1/3\) example. It is perfectly legitimate to write the three-voter profile as
\[ \mu^\star=\frac23\delta_{t_E}+\frac13\delta_{t_K}. \]
But the tableau does not calculate with that mixture. It merely receives three named points and relations between their permitted outcomes. The same proof could be stated over abstract profile symbols with one relation saying that the third profile is the relevant aggregate of the first two. That is a quotienting of the input representation, not a continuous computational mirror.
The best repair would be to impose the axioms over every \(\mu\in\Delta(T)\), rather than only at finitely many rational points. That creates a dilemma. If “continuous voting rule” means that \(F_\infty:\Delta(T)\to\Omega\) is continuous in the ordinary topological sense, then the model degenerates: \(\Delta(T)\) is connected while \(\Omega=2^X\setminus\{\emptyset\}\) is finite and discrete, so \(F_\infty\) must be constant. Faithfulness already rules this out when there are at least two alternatives.
If, more naturally, \(F_\infty\) is allowed to be discontinuous, then the finite proof no longer establishes a global theorem. Lemma 1 relies on the finite profile domain and finite set of voting rules. For finitely many local continuous instances, that argument can be repaired by quotienting rules according to their values on the finitely many mentioned distributions—but that repair gives precisely the finite abstract constraint problem above. For genuinely universal axiom schemas, an open branch cannot be extended “arbitrarily elsewhere”: its extension may violate reinforcement, neutrality, or another axiom at an unmentioned distribution. Lemma 3 therefore does not transfer without a new theory of global rules and their representation.
The high-multiplicity story is not itself implausible. A national electorate with many voters sharing a small catalogue of rankings is a sensible regime, and the proponent is right that individual prices are not a valid objection when type means a complete behavioral description. The difficulty is that this paper’s rules are allowed to depend on named electorates and are not required to be invariant under duplication. Passing from profiles to proportions therefore adds a substantive homogeneity assumption. That assumption can be reasonable, but it is not supplied by Theorem 4.
Thus Lemmas 1–3 offer no independent rescue. In the finite-instance version, termination, soundness, and completeness are generic facts about a finite relational calculus whose continuous coordinates are unused. In the global version, the finite termination and arbitrary-extension arguments no longer apply. The paper’s only plausible mirror is therefore either not genuinely about continuous populations or is a new axiomatic-continuum problem, which the ChoCo programme explicitly places outside scope.
This negative case is strongest on scope and model degeneracy, not on the claim that high-multiplicity voting is nonsensical. If axiomatic proof search itself were admitted as a ChoCo computational problem, the universal negative would be too strong; the \( \mu^\star \) reformulation is coherent. On the programme’s stated remit, however, this paper supplies no worthwhile continuous computational mirror.
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.