Formal Methods for Social Choice Theory

社会选择理论提供了一个数学框架，将个人的偏好结合起来，使集体社会福利最大化。一些最著名的结果来自被称为投票理论的社会选择理论的分支，即阿罗的不可能性定理和吉巴德-萨特思韦特定理。它们都描述了一个系统的一些简单的、理想的特性，比如不存在独裁者（一个可以单方面决定结果的选民），并证明如果所有其他理想的特性都成立，就一定存在独裁者。这种形式的论证对于数学家来说是一个熟悉的景象，特别是那些从事形式逻辑的数学家。你从一些合理的、一致的公理开始，探索其结果。在彻底探索之后，调整一两个公理，然后再次探索。这就是双曲几何被发现的过程，它从传统的欧几里得几何中诞生，通过调整一个公理。从历史上看，社会选择理论并没有这么严格，其论证虽然是数学化的，但却很不正式。人们对计算机科学与社会选择理论的交叉越来越感兴趣。考虑到该领域在推理什么对一个人、一个群体或更大的社会是最好的方面的应用，这当然是我们想要正确处理的事情，尤其是在人工智能爆炸迫在眉睫的情况下。虽然这个交叉领域的最新发展主要是关于算法的计算方面，以及考虑到计算特性（通常被称为计算社会选择理论）而开发新的聚合机制，但我们将研究形式逻辑在该领域的应用。我们将在Isabelle/HOL交互证明系统中开发一个动态逻辑，并使用它来形式化地证明各种机制的性质。社会选择理论中与形式化方法相关的大部分努力都是关于半非正式的（非正式的意思是没有在证明系统中实施和验证）特定领域逻辑的发展，例如博弈论、联盟形成和资源谈判的逻辑。我们认为，使用通用逻辑（如扩展动态逻辑）来证明机制的输入输出属性，并能够提取由该逻辑验证的正确程序，将是非常有益的。这个逻辑应该可以被用户扩展，以包含新的公理，同时让他们能够访问在没有额外公理的情况下证明的证明体，而Isabelle的区域设置是实现这一目标的方便机制。最后，虽然社会选择理论通常关注的是确定性的环境和机制(例如；拍卖，投票，资源分配)，我们也将扩展这种逻辑，使其具有表达能力，能够形式化概率机制和系统的属性，希望这可以作为社会选择理论及其相关领域未来正式发展的基础。

Social choice theory provides a mathematical framework for combining the preferences of individuals in such a way as to maximise collective social welfare. Some of the most famous results come from the branch of social choice theory known as voting theory, namely Arrow's impossibility theorem and the Gibbard-Satterthwaite theorem. They both describe some simple, desirable properties of a system such as there being no dictator (a voter who can unilaterally decide the outcome), and prove that there must be a dictator if all other desirable properties hold.This form of argument is a familiar sight to mathematicians, particularly those who practice formal logic. You begin with some sensible, consistent axioms and explore the consequences. After exploring thoroughly, tweak an axiom or two and explore again. This is essentially how hyperbolic geometry was discovered, born from traditional Euclidean geometry by tweaking one axiom. Social choice theory has historically not been so rigorous and the arguments, while mathematical, were nevertheless informal.There is an increasing interest in the intersection of computer science and social choice thoery. Considering the field's application to reasoning about what is best for a person, group, or larger society, it is certainly something we want to get right, particularly with the looming AI explosion. While the majority of recent developments in this intersection have been about the computational aspects of algorithms and developing new aggregation mechanisms with computational properties in mind (often referred to as Computational Social Choice Theory), we will be investigating the application of formal logic to the field.We will develop a dynamic logic in the Isabelle/HOL interactive proof system and use it to formally prove properties of various mechanisms. Much of the effort related to formal methods in social chocie theory has been about semi-informal (informal in the sense of not implemented and verified in a proof system) developments of domain-specific logics, such as logics for game theory, coalition formation, and resource negotiations. We believe it would be highly beneficial to use a generic logic such as an extended dynamic logic for proving input-output properties of mechanisms, and being able to extract correct programs verified by this logic. This logic should be extendable by users to include new axioms while leaving them with access to the body of proofs proven without the additional axioms, and Isabelle's locales are a convenient mechanism for achieving this.Finally, while social choice theory typically concerns itself with deterministic environments and mechanisms (eg. auctions, voting, resource allocations), we will also extend this logic to equip it with the expressive power to be able to formalise properties of probabilistic mechanisms and systems, with the hope that this can serve as a basis for future formal developments of social choice theory and its related fields.