First-Order Logic Formalisation of Impossibility Theorems in Preference Aggregation
Umberto Grandi, Ulle Endriss

Abstract:
In preference aggregation a set of individuals express preferences
over a set of alternatives, and these preferences have to be
aggregated into a collective preference. When preferences are
represented as orders, aggregation procedures are called social
welfare functions. Classical results in social choice theory state
that it is impossible to aggregate the preferences of a set of
individuals under different natural sets of axiomatic conditions. We
define a first-order language for social welfare functions and we give
a complete axiomatisation for this class, without having the number of
individuals or alternatives specified in the language. We are able to
express classical axiomatic requirements in our first-order language,
giving formal axioms for three classical theorems of preference
aggregation by Arrow, by Sen, and by Kirman and Sondermann. We explore
to what extent such theorems can be formally derived from our
axiomatisations, obtaining positive results for Sen's Theorem and the
Kirman-Sondermann Theorem. For the case of Arrow's Theorem, which does
not apply in the case of infinite societies, we have to resort to
fixing the number of individuals with an additional axiom. In the long
run, we hope that our approach to formalisation can serve as the basis
for a fully automated proof of classical and new theorems in social
choice theory.