First-order logic formalisation of impossibility theorems in preference aggregation

DOI10.1007/s10992-012-9240-8zbMath1285.91041MaRDI 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 logic; automated reasoning; social choice theory; preference aggregation; axiomatisability

Mathematics Subject Classification ID

91B12: Voting theory

03B35: Mechanization of proofs and logical operations

91B14: Social choice

03B80: Other applications of logic

Related Items

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

Uses Software

• OTTER
• E Theorem Prover
• Arrow Gibbard Satterthwaite

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item