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