Formal methods and the theory of social choice

Abstract

Social Choice Theory (SCT, see [2] for an introduction) studies social aggregation problems, i.e., the problem of aggregating individual choices, preferences, opinions, judgments, etc. into a group choice, preference, opinion or judgment. Examples of such aggregation problems include the following: aggregating the political opinions of a country's population in order to choose a president or parliament, assigning college students to dormitories based on their preferences, dividing an inheritance among a number of people, and matching romance-seeking web users at an internet dating site. On the one hand, SCT analyzes existing aggregation mechanisms, e.g. the voting procedures of different countries or different matching algorithms. On the other hand, SCT explores different normative properties such as anonymity or neutrality, and the logical dependencies among them. The central results in SCT fall into the second category, the most well-known being Arrow's impossibility theorem [1] and the Gibbard-Satterthwaite theorem [3,8]. © 2008 Springer-Verlag Berlin Heidelberg.