{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:17:00Z","timestamp":1760203020199},"reference-count":38,"publisher":"Oxford University Press (OUP)","issue":"4","license":[{"start":{"date-parts":[[2021,1,25]],"date-time":"2021-01-25T00:00:00Z","timestamp":1611532800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,6,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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\u2013Satterthwaite 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.<\/jats:p>","DOI":"10.1093\/logcom\/exab001","type":"journal-article","created":{"date-parts":[[2021,1,5]],"date-time":"2021-01-05T20:08:56Z","timestamp":1609877336000},"page":"1055-1078","source":"Crossref","is-referenced-by-count":2,"title":["Reasoning about strategic voting in modal logic quickly becomes undecidable"],"prefix":"10.1093","volume":"31","author":[{"given":"Erik","family":"Parmann","sequence":"first","affiliation":[{"name":"BKK AS, N-5020 Bergen, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"\u00c5gotnes","sequence":"additional","affiliation":[{"name":"Institute of Logic and Intelligence, Southwest University, 400715, Chongqing, China and Department of Information Science and Media Studies, University of Bergen, N-5020 Bergen, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2021,1,25]]},"reference":[{"key":"2022011119145376300_ref1","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1007\/s11225-016-9657-0","article-title":"The undecidability of quantified announcements","volume":"104","author":"\u00c5gotnes","year":"2016","journal-title":"Studia Logica"},{"key":"2022011119145376300_ref2","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1016\/j.jal.2008.12.002","article-title":"Group announcement logic","volume":"8","author":"\u00c5gotnes","year":"2010","journal-title":"Journal of Applied Logic"},{"key":"2022011119145376300_ref3","first-page":"543","article-title":"Knowledge and ability","volume-title":"Handbook of Epistemic Logic","author":"\u00c5gotnes","year":"2015"},{"key":"2022011119145376300_ref4","first-page":"1","article-title":"Towards a logic of social welfare","volume-title":"Proceedings of The 7th Conference on Logic and the Foundations of Game and Decision Theory (LOFT)","author":"\u00c5gotnes","year":"2006"},{"key":"2022011119145376300_ref5","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/s10458-009-9115-8","article-title":"On the logic of preference and judgment aggregation","volume":"22","author":"\u00c5gotnes","year":"2011","journal-title":"Autonomous Agents and Multi-Agent Systems"},{"key":"2022011119145376300_ref6","first-page":"673","article-title":"Coalitions and announcements","volume-title":"Proceedings of the Seventh International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2008)","author":"\u00c5gotnes","year":"2008"},{"volume-title":"Social Choice and Individual Values","year":"1951","author":"Arrow","key":"2022011119145376300_ref7"},{"volume-title":"Handbook of Social Choice and Welfare","year":"2002","author":"Arrow","key":"2022011119145376300_ref8"},{"key":"2022011119145376300_ref9","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1017\/S1755020308080210","article-title":"\u2018Knowable\u2019 as \u2018known after an announcement\u2019","volume":"1","author":"Balbiani","year":"2008","journal-title":"The Review of Symbolic Logic"},{"key":"2022011119145376300_ref10","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1007\/s003550100151","article-title":"An introduction to strategy-proof social choice functions","volume":"18","author":"Barbera","year":"2001","journal-title":"Social Choice and Welfare"},{"key":"2022011119145376300_ref11","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1111\/j.1755-2567.1988.tb00717.x","article-title":"Seeing to it that: a canonical form for agentives","volume":"54","author":"Belnap","year":"1988","journal-title":"Theoria"},{"key":"2022011119145376300_ref12","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"Blackburn","year":"2001"},{"key":"2022011119145376300_ref13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3125642","article-title":"Proving the incompatibility of efficiency and strategyproofness via SMT solving","volume":"65","author":"Brandl","year":"2018","journal-title":"Journal of the ACM"},{"key":"2022011119145376300_ref14","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.4959","article-title":"Finding strategyproof social choice functions via SAT solving","volume":"55","author":"Brandt","year":"2016","journal-title":"Journal of Artificial Intelligence Research"},{"key":"2022011119145376300_ref15","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1016\/j.mathsocsci.2016.09.003","article-title":"Optimal bounds for the no-show paradox via SAT solving","volume":"90","author":"Brandt","year":"2017","journal-title":"Mathematical Social Sciences"},{"key":"2022011119145376300_ref16","doi-asserted-by":"crossref","first-page":"963","DOI":"10.1007\/s10458-016-9328-6","article-title":"Proving classical theorems of social choice theory in modal logic","volume":"30","author":"Cin\u00e1","year":"2016","journal-title":"Autonomous Agents and Multi-Agent Systems"},{"key":"2022011119145376300_ref17","first-page":"333","article-title":"Logic and social choice theory","volume":"2","author":"Endriss","year":"2012","journal-title":"Logic and Philosophy Today"},{"key":"2022011119145376300_ref18","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning About Knowledge","author":"Fagin","year":"1995"},{"key":"2022011119145376300_ref19","first-page":"23","article-title":"Undecidability for arbitrary public announcement logic","author":"French","year":"2008","journal-title":"Advances in Modal Logic 7"},{"volume-title":"Many-Dimensional Modal Logics: Theory and Applications","year":"2003","author":"Gabbay","key":"2022011119145376300_ref20"},{"key":"2022011119145376300_ref21","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1613\/jair.3126","article-title":"Automated search for impossibility theorems in social choice theory: ranking sets of objects","volume":"40","author":"Geist","year":"2011","journal-title":"Journal of Artificial Intelligence Research"},{"key":"2022011119145376300_ref22","first-page":"249","article-title":"Computer-aided methods for social choice theory","author":"Geist","year":"2017","journal-title":"Trends in Computational Social Choice"},{"key":"2022011119145376300_ref23","doi-asserted-by":"crossref","first-page":"587","DOI":"10.2307\/1914083","article-title":"Manipulation of voting schemes: a general result","volume":"41","author":"Gibbard","year":"1973","journal-title":"Econometrica"},{"key":"2022011119145376300_ref24","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1007\/s10992-012-9240-8","article-title":"First-order logic formalisation of impossibility theorems in preference aggregation","volume":"42","author":"Grandi","year":"2013","journal-title":"Journal of Philosophical Logic"},{"key":"2022011119145376300_ref25","first-page":"133","article-title":"Properties of logics of individual and group agency","volume-title":"Advances in Modal Logic 7, Papers from the Seventh Conference on \u201cAdvances in Modal Logic\u201d held in Nancy, France, 9\u201312 September 2008","author":"Herzig","year":"2008"},{"key":"2022011119145376300_ref26","doi-asserted-by":"crossref","first-page":"311","DOI":"10.2307\/2273191","article-title":"The equational theory of $C{A}_3$ is undecidable","volume":"45","author":"Maddux","year":"1980","journal-title":"The Journal of Symbolic Logic"},{"key":"2022011119145376300_ref27","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-5694-3","volume-title":"Multi-dimensional Modal Logic","author":"Marx","year":"1997"},{"key":"2022011119145376300_ref28","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/s10817-009-9147-4","article-title":"Social choice theory in hol","volume":"43","author":"Nipkow","year":"2009","journal-title":"Journal of Automated Reasoning"},{"volume-title":"Expressing Properties of Social Choice Functions Using Modal Logic","year":"2011","author":"Parmann","key":"2022011119145376300_ref29"},{"key":"2022011119145376300_ref30","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/s11229-007-9200-y","article-title":"On the role of language in social choice theory","volume":"163","author":"Pauly","year":"2008","journal-title":"Synthese"},{"key":"2022011119145376300_ref31","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s00355-010-0479-0","article-title":"Generalizing the Gibbard\u2013Satterthwaite theorem: partial preferences, the degree of manipulation, and multi-valuedness","volume":"37","author":"Reffgen","year":"2011","journal-title":"Social Choice and Welfare"},{"key":"2022011119145376300_ref32","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/S0165-1765(00)00332-3","article-title":"Arrow\u2019s theorem and the Gibbard\u2013Satterthwaite theorem: a unified approach","volume":"70","author":"Reny","year":"2001","journal-title":"Economics Letters"},{"key":"2022011119145376300_ref33","doi-asserted-by":"crossref","first-page":"695","DOI":"10.1007\/s11225-018-9815-7","article-title":"Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter","volume":"107","author":"Rybakov","year":"2019","journal-title":"Studia Logica"},{"key":"2022011119145376300_ref34","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/0022-0531(75)90050-2","article-title":"Strategy-proofness and Arrow\u2019s conditions: existence and correspondence theorems for voting procedures and social welfare functions","volume":"10","author":"Satterthwaite","year":"1975","journal-title":"Journal of Economic Theory"},{"key":"2022011119145376300_ref35","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/j.jmateco.2014.09.007","article-title":"The proof of the Gibbard\u2013Satterthwaite theorem revisited","volume":"55","author":"Svensson","year":"2014","journal-title":"Journal of Mathematical Economics"},{"key":"2022011119145376300_ref36","doi-asserted-by":"crossref","first-page":"1041","DOI":"10.1016\/j.artint.2009.02.005","article-title":"Computer-aided proofs of Arrow\u2019s and other impossibility theorems","volume":"173","author":"Tang","year":"2009","journal-title":"Artificial Intelligence"},{"key":"2022011119145376300_ref37","first-page":"237","article-title":"A logic of propositional control for truthful implementations","volume-title":"Proceedings of the 12th Conference on Theoretical Aspects of Rationality and Knowledge, TARK \u201909","author":"Troquard","year":"2009"},{"key":"2022011119145376300_ref38","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/s10992-011-9189-z","article-title":"Reasoning about social choice functions","volume":"40","author":"Troquard","year":"2011","journal-title":"Journal of Philosophical Logic"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/31\/4\/1055\/42098935\/exab001.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/31\/4\/1055\/42098935\/exab001.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,21]],"date-time":"2024-08-21T22:30:03Z","timestamp":1724279403000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/31\/4\/1055\/6105782"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,25]]},"references-count":38,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2021,1,25]]},"published-print":{"date-parts":[[2021,6,4]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exab001","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2021,6]]},"published":{"date-parts":[[2021,1,25]]}}}