Logics for Social Choice Theory
Instructor: Eric Pacuit (website)
ESSLLI 2022 • National University of Ireland Galway
Monday, August 15th - Friday, August 19th
11:00am - 12:30pm • AC202
Many different logical systems have been developed that can formalize results in social choice theory. In recent years, much of the research on logic and social choice has focused on computer-aided methods such as SAT solving and interactive theorem proving. This course will be a broad overview of recent work on logic and social choice theory. The course will start by introducing key results in social choice theory (e.g., May's Theorem, Arrow's Theorem, the Gibbard-Satterthwaite Theorem) and the different logical systems that have been developed to formalize these results. The second part of the course will show how SAT solvers have been used to discover new results in the study of voting methods. Finally, the last part of the course will be a brief introduction to the Lean interactive proof assistant and how to use Lean to formalize results in social choice theory.
W. Holliday and E. Pacuit, Arrow's Decisive Coalitions
W. Holliday and E. Pacuit Axioms for Defeat in Democratic Elections, Section 6 and Appendix B
C. Geist and D. Peters, Computer Aided Methods for Social Choice pref_voting.readthedocs.io