Reasoning about Social Choice Functions

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 ev-ery 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.