Reasoning about Social Choice Functions
Nicolas Troquard, Wiebe van der Hoek, Michael Wooldridge

TL;DR
This paper introduces a logic for reasoning about social choice functions, enabling formal analysis of their properties, including strategy-proofness, with proven expressiveness and decidability.
Contribution
It presents a novel logic that characterizes all social choice functions and supports reasoning about their strategic and preference-related properties.
Findings
Logic is expressively complete for social choice functions
The logic is decidable and has a complete axiomatization
Application demonstrated in verifying strategy-proofness
Abstract
We introduce a logic specifically designed to support reasoning about social choice functions. The logic includes operators to capture strategic ability, and operators to capture agent preferences. We establish a correspondence between formulae in the logic and properties of social choice functions, and show that the logic is expressively complete with respect to social choice functions, i.e., that every social choice function can be characterised as a formula of the logic. We prove that the logic is decidable, and give a complete axiomatization. To demonstrate the value of the logic, we show in particular how it can be applied to the problem of determining whether a social choice function is strategy-proof.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
