First-order logic formalisation of impossibility theorems in preference aggregation

DOI10.1007/s10992-012-9240-8zbMath1285.91041OpenAlexW2117864711MaRDI QIDQ373021

Ulle Endriss, Umberto Grandi

Publication date: 21 October 2013

Published in: Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10992-012-9240-8

zbMATH Keywords

first-order logicautomated reasoningsocial choice theorypreference aggregationaxiomatisability

Mathematics Subject Classification ID

Voting theory (91B12) Mechanization of proofs and logical operations (03B35) Social choice (91B14) Other applications of logic (03B80)

Related Items

Voting theory in the Lean theorem prover, Representing voting rules in Łukasiewicz’s three-valued logic, Arrow's decisive coalitions, Natural deduction for modal logic of judgment aggregation, Dependence and Independence in Social Choice: Arrow’s Theorem

Uses Software

• OTTER
• E Theorem Prover
• Arrow Gibbard Satterthwaite

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Impossibility results for infinite-electorate abstract aggregation rules
• Reasoning about social choice functions
• Computer-aided proofs of Arrow's and other impossibility theorems
• On the role of language in social choice theory
• Three brief proofs of Arrow's impossibility theorem
• Arrow's theorem, countably many agents, and more visible invisible dictators
• Handbook of social choice and welfare. Vol. 1.
• Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
• Automated Search for Impossibility Theorems in Social Choice Theory: Ranking Sets of Objects
• The Existence of Social Welfare Functions
• Aggregating Partially Ordered Preferences
• Automated Reasoning