10 June 2011, Computational Social Choice Seminar, Erik Parmann
We will look at the possibility of expressing properties of social choice functions in a modal logic, and we will look at a specific modal logic created to do this. This logic is simple, while still strong enough to express the properties involved in the Gibbard-Satterthwaite theorem. Then we observe that a very simple fragment of this language has tight connections to the logic of products of S5 frames, a logic with undesirable computational properties. We will then discuss to what extent this is a negative result for the overall goal of finding an expressive logic for this domain with nice computational properties.