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.
翻译:个人理性选择的根本原则是Sen的 $\ gamma$ axiom, 也称为扩展的一致性, 指出从两个菜单中从每个菜单中选择的任何替代选择都必须从菜单的组合中选择, 扩大一致性也可以在社会选择的设置中形成。 在投票理论中, 任何从两个候选人领域选择的候选人都必须从候选人的组合中选择。 轴中的一个重要特殊情况是二进制扩展一致性, 也就是说, 任何候选人从候选人的初始领域中选择, 并在与新候选人的头对头的匹配中选择, 都必须在新候选人加入字段时选择任何替代选择, 从而排除破坏效应。 在本文中, 我们研究扩张一致性和坚定性减弱之间的紧张关系。 在任何选举中, 要求从两个候选人的组合中选择单一候选人。 众所周知, 绝对性与社会选择的基本公平性条件不一致, 即匿名性和中立性。 我们在这里证明, 任何独立性的坚定性( 与匿名性和中立性一致的) 也与二进制扩展一致性一致, 从而排除破坏性效果效果效果效果效果效果。 我们研究的是, 将主要选举战略的证明, 以普通选举方法的正确性方法 。