Formalizations of social choice theory in modal logic

Social choice theory is about aggregating a collective choice from given individual choices. It includes a study of strategic behavior in this context, such as declaring an insincere choice so that the outcome of aggregation becomes more preferable. Computational aspects of social choice theory include issues of decidability and complexity of e.g. computing winner of an election under a given voting rule, or regarding strategic issues, of computing a possibility to manipulate an election. To contribute to computational study of social choice, various logical formalizations are developed to reason about problems of social choice theory. This talk is a survey of some such formalizations, namely (some of) those which use modal logic.