Formal Methods for Social Choice Theory

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.