The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency

Title:	The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
Authors:	Felix Brandt, Manuel Eberl, Christian Saile and Christian Stricker
Submission date:	2018-03-22
Abstract:	This formalisation contains the proof that there is no anonymous Social Choice Function for at least three agents and alternatives that fulfils both Pareto-Efficiency and Fishburn-Strategyproofness. It was derived from a proof of Brandt et al., which relies on an unverified translation of a fixed finite instance of the original problem to SAT. This Isabelle proof contains a machine-checked version of both the statement for exactly three agents and alternatives and the lifting to the general case.
BibTeX:	@article{Fishburn_Impossibility-AFP, author = {Felix Brandt and Manuel Eberl and Christian Saile and Christian Stricker}, title = {The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency}, journal = {Archive of Formal Proofs}, month = mar, year = 2018, note = {\url{http://isa-afp.org/entries/Fishburn_Impossibility.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Randomised_Social_Choice
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.