Automated Search for Impossibility Theorems in Social Choice Theory: Ranking Sets of Objects
Christian Geist, Ulle Endriss
Abstract:
We present a method for using standard techniques from satisfiability
checking to automatically verify and discover theorems in an area of
economic theory known as ranking sets of objects. The key question in
this area, which has important applications in social choice theory
and decision making under uncertainty, is how to extend an agent's
preferences over a number of objects to a preference relation over
nonempty sets of such objects. Certain combinations of seemingly
natural principles for this kind of preference extension can result in
logical inconsistencies, which has led to a number of important
impossibility theorems. We first prove a general result that shows
that for a wide range of such principles, characterised by their
syntactic form when expressed in a many-sorted first-order logic, any
impossibility exhibited at a fixed (small) domain size will
necessarily extend to the general case. We then show how to formulate
candidates for impossibility theorems at a fixed domain size in
propositional logic, which in turn enables us to automatically search
for (general) impossibility theorems using a SAT solver. When applied
to a space of 20 principles for preference extension familiar from the
literature, this method yields a total of 84 impossibility theorems,
including both known and nontrivial new results.