Institute for Logic, Language and Computation

13 February 2009, Computational Social Choice Seminar, Umberto Grandi

Speaker: Umberto Grandi
Title: Automated Reasoning in Social Choice Theory: Arrow's Theorem
Date: Friday 13 February 2009
Time: 16:00
Location: P-3.27, Euclides Building, Plantage Muidergracht 24, Amsterdam


Arrow's Theorem is a famous impossibility result in social choice theory, stating that under certain natural conditions it is not possible to aggregate the preferences of a finite set of individuals. Several proofs and generalisations of the theorem are known, but many of them have been criticized in the literature for, arguably, relying on somewhat cumbersome proofs. We argue in favour of the use of automated reasoning techniques in this field to explore new results in an easier way, avoiding errors due to the level of detail in these proofs. In this talk we present a first-order axiomatization of the problem of aggregating preferences represented as linear orders. We discuss different formulations of Arrow's Theorem in this framework, and the issue of an infinite number of individuals. We present a language where the number of individuals is fixed, and we show that Arrow's Theorem can (in principle) be implemented (and proved correct) using an automated theorem prover. We then discuss different approaches to the use of languages that do not specify the number of individuals.

For more information, see, or contact Ulle Endriss ().

The websites of the UvA make use of cookiesThis site uses cookies More informationMore info Hide this message XHide X