Impossibility theorems involving weakenings of expansion consistency and resoluteness in voting
A fundamental principle of individual rational choice is Sen's $\gamma$ axiom, also known as expansion consistency, stating that any alternative chosen from each of two menus must be chosen from the union of the menus. Expansion consistency can also be formulated in the setting of social choice. In voting theory, it states that any candidate chosen from two fields of candidates must be chosen from the combined field of candidates. An important special case of the axiom is binary expansion consistency, which states that any candidate chosen from an initial field of candidates and chosen in a head-to-head match with a new candidate must also be chosen when the new candidate is added to the field, thereby ruling out spoiler effects. In this paper, we study the tension between this weakening of expansion consistency and weakenings of resoluteness, an axiom demanding the choice of a single candidate in any election. As is well known, resoluteness is inconsistent with basic fairness conditions on social choice, namely anonymity and neutrality. Here we prove that even significant weakenings of resoluteness, which are consistent with anonymity and neutrality, are inconsistent with binary expansion consistency. The proofs make use of SAT solving, with the correctness of a SAT encoding formally verified in the Lean Theorem Prover, as well as a strategy for generalizing impossibility theorems obtained for special types of voting methods (namely majoritarian and pairwise voting methods) to impossibility theorems for arbitrary voting methods. This proof strategy may be of independent interest for its potential applicability to other impossibility theorems in social choice.
Code (2)
Tasks
FairnessSimilar Papers 제목 키워드 기반
Aggregating Credences into Beliefs: Agenda Conditions for Impossibility Results
Binarizing belief aggregation addresses how to rationally aggregate individual probabilistic beliefs into collective binary beliefs. Similar to the development of judgment aggregation theory, formulating axiomatic requir…
BinarizationNegationAutomated Search for Impossibility Theorems in Social Choice Theory: Ranking Sets of Objects
We present a method for using standard techniques from satisfiability checking to automatically verify and discover theorems in an area of economic theory known as ranking sets of objects. The key question in this area, …
Decision MakingDecision Making Under UncertaintyImpossibility and Uncertainty Theorems in AI Value Alignment (or why your AGI should not have a utility function)
Utility functions or their equivalents (value functions, objective functions, loss functions, reward functions, preference orderings) are a central tool in most current machine learning systems. These mechanisms for defi…
BIG-bench Machine LearningEscaping Arrow's Theorem: The Advantage-Standard Model
There is an extensive literature in social choice theory studying the consequences of weakening the assumptions of Arrow's Impossibility Theorem. Much of this literature suggests that there is no escape from Arrow-style …
modelImpossibility Results in AI: A Survey
An impossibility theorem demonstrates that a particular problem or set of problems cannot be solved as described in the claim. Such theorems put limits on what is possible to do concerning artificial intelligence, especi…
Decision MakingEthicsSurvey