- Proving Classical Theorems of Social Choice Theory in Modal Logic
- Autonomous Agents and Multi-Agent Systems
- Volume | Issue number
- 30 | 5
- Pages (from-to)
- Document type
- Interfacultary Research Institutes
Faculty of Science (FNWI)
- Institute for Logic, Language and Computation (ILLC)
A number of seminal results in the field of social choice theory demonstrate the difficulties of aggregating the preferences of several individual agents for the purpose of making a decision together. We show how to formalise three of the most important impossibility results of this kind—Arrow’s Theorem, Sen’s Theorem, and the Muller–Satterthwaite Theorem—by using a modal logic of social choice functions. We also provide syntactic proofs of these theorems in the same logic. While prior work has been successful in applying tools from logic and automated reasoning to social choice theory, this is the first human-readable formalisation of the Arrovian framework allowing for a direct derivation of the main impossibility theorems of social choice theory. This is useful for gaining a deeper understanding of the foundations of collective decision making, both in human society and in groups of autonomous software agents.
- go to publisher's site
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.