A Syntactic Proof of Arrow's Theorem in a Modal Logic of Social Choice Functions

We show how to formalise Arrow’s Theorem on the impossibility of devising a method for preference aggregation that is both independent of irrelevant alternatives and Pareto efficient by using a modal logic of social choice functions. We also provide a syntactic proof of the theorem in that logic. While prior work has been successful in applying tools from logic and automated reasoning to social choice theory, this is the first human-readable formalisation of the Arrovian framework allowing for a direct derivation of the theorem. Categories and Subject Descriptors I.2.11 [Artificial Intelligence]: Distributed Artificial Intelligence—Multiagent Systems; J.4 [Social and Behavioral Sciences]: Economics General Terms Theory; Economics Keywords Social Choice Theory; Logic

• Type: Journal
• Year: 2015
• Where: ATAL
• Authors: Giovanni Ciná, Ulle Endriss
• Keywords: ATAL 2015, Intelligent Agents