First-Order Logic Formalisation of Arrow's Theorem
Umberto Grandi, Ulle Endriss
Abstract:
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.