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.

翻译：个体理性选择的一个基本原则是森的γ公理，也称为扩展一致性，它规定从两个备选菜单中分别选出的任何备选方案，也必须从这两个菜单的并集中选出。扩展一致性同样适用于社会选择框架。在投票理论中，该公理指出：从两个候选人集合中分别选出的任何候选人，也必须从这两个集合的并集中选出。该公理的一个重要特例是二元扩展一致性，它规定：从一个初始候选人集合中选出的候选人，若在与新候选人的一对一较量中仍被选出，则当该新候选人加入初始集合时，该候选人依然应当被选中——这排除了“搅局者”效应。本文研究了扩展一致性的这种弱化形式与决断性弱化形式之间的张力。决断性要求在任何选举中仅选出一名候选人。众所周知，决断性与社会选择的基本公平条件（即匿名性和中立性）不相容。本文证明，即使与匿名性和中立性相容的显著弱化的决断性，也与二元扩展一致性不相容。证明过程使用了SAT求解技术，其中SAT编码的正确性通过Lean定理证明器进行了形式化验证；同时，我们还提出了一种策略，将针对特定类型投票方法（即多数决投票法和成对比较投票法）获得的不可能性定理，推广至任意投票方法的不可能性定理。该证明策略因可能适用于社会选择领域中的其他不可能性定理而具有独立的研究价值。