Automated Search for Impossibility Theorems in Choice Theory: Ranking Sets of Objects Christian Geist Abstract: In the subarea of (social) choice theory commonly referred to as ranking sets of objects the question arises whether, given preferences over some domain, there is a preference relation on the power set of this domain that is compatible with certain axioms. The Kannai-Peleg Theorem (Journal of Economic Theory, 1984) gives a negative answer to this question for the case of six or more elements in the domain in combination with the two (very intuitive) axioms called dominance and independence. It is the main (and earliest) impossibility theorem in this particular area. Our initial goal was to find a suitable formulation of the Kannai-Peleg Theorem in logic that would facilitate an automatic verification of the result. It turned out, however, that developing a first-order formulation of this problem and feeding it to a first-order theorem prover was not very effective. Therefore, we successfully tried an inductive proof consisting of a manual in- ductive step together with a formalization of the base case in propositional logic (in order to use a SAT solver). This particular way of using automated theorem proving in social choice theory is due to Tang and Lin (Artificial Intelligence Journal, 2009), who have in this way proved major impossibility results, like Arrow’s Theorem, the Muller-Satterthwaite Theorem, and Sen’s Theorem. We extended their technique to be able to treat the Kannai-Peleg Theorem and were able to verify it with a verification time of less than ten seconds. With our initial objective met, we then developed a further extension of the method in order to discover new impossibility results. Using tools from model theory, a universal form of the previous inductive step (now applicable to a large class of axioms) allows for a fully automated theorem search, which has produced 84 impossibility theorems on a space of 20 axioms from the literature. Many of these results are variations of known impossibilities, but also a few new results were obtained. Interestingly, one of the impossibility theorems found by our program had even wrongly been published as a possibility result earlier (Economic Theory, 2000, 2003). Finally, we give some manual proofs of the new results to underline the fruitfulness of this computer-aided method of searching for impossibility results in the field of ranking sets of objects.