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.

Day 1: Arrow's Theorem and decisive coalitions

August 15, 2022

W. Holliday and E. Pacuit, Arrow's Decisive Coalitions

Day 2: Voting methods and voting paradoxes

August 16, 2022

W. Holliday and E. Pacuit Axioms for Defeat in Democratic Elections, Section 6 and Appendix B

pref_voting.readthedocs.io

Day 3: Using SAT to find impossibility theorems I

August 17, 2022

Day 4: Using SAT to find impossibility theorems II

August 18, 2022

Day 5: Social Choice Theory in the Lean theorem prover

August 19, 2022