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{https://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.