First-Order Logic Formalisation of Arrow's Theorem

10 years 9 months ago
First-Order Logic Formalisation of Arrow's Theorem
Arrow’s Theorem is a central result in social choice theory. It states that, under certain natural conditions, it is impossible to aggregate the preferences of a finite set of individuals into a social preference ordering. We formalise this result in the language of first-order logic, thereby reducing Arrow’s Theorem to a statement saying that a given set of first-order formulas does not possess a finite model. In the long run, we hope that this formalisation can serve as the basis for a fully automated proof of Arrow’s Theorem and similar results in social choice theory. We prove that this is possible in principle, at least for a fixed number of individuals, and we report on initial experiments with automated reasoning tools.
Umberto Grandi, Ulle Endriss
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where LORI
Authors Umberto Grandi, Ulle Endriss
Comments (0)