All definitions, propositions, lemmas and theorems for multi-winner voting with argumentative ballots are formalised and mechanically checked in Lean 4.
Abstract
We introduce multi-winner voting with argumentative ballots (MVArg) and investigate theoretical properties. As our conceptual contribution, we generalise approval ballots to argumentative ballots, thereby allowing voters to express defeasible preferences over candidates. We accordingly generalise voter cohesion and justified representation axioms JR, PJR and EJR. As our theoretical contribution, we establish several key results. First, MVArg is strictly more expressive than multi-winner voting with approval ballots (MV). Second, our notions of cohesion and justified representation are conservative generalisations of their counterparts in MV. Third, the MVArg counterpart of JR can always be satisfied, whereas the counterparts of PJR and EJR cannot always be. Fourth, although verifying whether a winner set satisfies the MVArg counterpart of JR is already coNP-hard, such a winner set can be constructed in polynomial time. All definitions, propositions, auxiliary lemmas and theorems have been formalised and mechanically checked in Lean 4.
Problem
Approval-based multi-winner voting limits how voters express preferences and does not capture relational attack/defence information between candidates. Standard justified representation axioms (JR, PJR, EJR) are defined only for approval ballots.
Approach
The authors introduce multi-winner voting with argumentative ballots (MVArg), generalising approval ballots to abstract argumentation frameworks whose grounded extensions induce individual and collective approvals. They generalise voter cohesion and the JR, PJR, EJR axioms to argumentative counterparts (ArgJR, ArgPJR, ArgEJR, ArgEJR-Spot). All definitions, propositions, auxiliary lemmas, and theorems are formalised and certified in Lean 4.
Figure 1: The first row from left to right : a blank ballot; v_{1} ’s ballot approving c_{1} and c_{5} ; v_{2} ’s ballot approving c_{1},c_{2} and c_{4} ; and v_{3} ’s ballot approving c_{1},c_{2},c_{3} and c_{6} . The second row from left to right : \{v_{1},v_{2}\} ’s collective approval of c_{1} and c_{4} ; \{v_{1},v_{3}\} ’s collective approval of c_{1} ; \{v_{2},v_{3}\} ’s collective approval
Results
MVArg is strictly more expressive than approval-based voting and the new axioms conservatively generalise their counterparts, preserving the EJR⊆PJR⊆JR hierarchy. An ArgJR winner set always exists and is polynomial-time constructible, while ArgPJR and ArgEJR winner sets need not exist; verifying ArgJR membership is coNP-hard.
