First-order logic formalisation of impossibility theorems in preference aggregation (Q373021)

The authors present a formalisation of several results from social choice theory in classical first-order logic. They concentrate on three theorems, proved by Arrow, Sen, and Kirman and Sondermann, respectively. They start presenting a first-order language and a theory for social welfare functions, they formalise Arrow's conditions, like Independence of Irrelevant Alternatives and the Universal Domain condition, as first-order statements and extend the language to cover the model of individual rights proposed by Sen. A thorough study of the formalisation of the Universal Domain condition is carried out throughout the paper, to cover the case of weak orders and of general sets of alternatives. The proof of Sen's theorem enables the authors to state an easy correspondence between the original statement and the inconsistency of the first-order logic axioms formalising Sen's conditions. For the case of Arrow's theorem they solve the issue of an infinite number of alternatives by proving a lemma which reduces the impossibility to the case of three alternatives. Arrow's statement is therefore equivalent to the unsatisfiability of their axioms in finite models. They also prove that, if the number of individuals is fixed in their language, then there is a formal derivation of Arrow's theorem from their axioms. For the most general case of a possibly infinite number of individuals they prove that a statement inconsistent with the assumption of an infinite society can be formally derived from Arrow's conditions, formalising in this way the Kirman-Sondermann theorem. In the long run, the authors hope that their approach to formalisation can serve as the basis for a fully automated proof of classical and new theorems in social choice theory.