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.
Slides
W. Holliday and E. Pacuit, Arrow's Decisive Coalitions
Slides
W. Holliday and E. Pacuit Axioms for Defeat in Democratic Elections, Section 6 and Appendix B