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

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.

  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{},
            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.