  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 agents 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.
