Reasoning about strategic voting in modal logic quickly becomes undecidable

Abstract In this paper, we show that modal logics for reasoning about social choice quickly become undecidable. In particular, we study modal logics that can be used to reason about situations involving both actual and claimed preferences in the context of a social choice function and argue that reasoning on this level often occurs in social choice. We formally define a particular logic, interpreted in such situations, that can express the properties involved in the Gibbard–Satterthwaite theorem. We then, however, demonstrate that any modal logic interpreted in such situations having a certain natural expressive power, in particular a modality quantifying over all possible claimed preferences, becomes undecidable when there are enough agents in the system. We also discuss a decidable special case and provide a complete axiomatization of fragment of the language.