13 February 2009, Computational Social Choice Seminar, Umberto Grandi

Abstract

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 http://www.illc.uva.nl/~ulle/seminar/, or contact Ulle Endriss (ulle at illc.uva.nl).