Email Gateway (Aug 22 2022 at 17:00): Email Gateway (Aug 22 2022 at 17:00):From: Tobias Nipkow <nipkow@in.tum.de>
The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
Felix Brandt, Manuel Eberl, Christian Saile and Christian Stricker
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.
https://www.isa-afp.org/entries/Fishburn_Impossibility.html
Enjoy!
smime.p7s
Last updated: Apr 25 2024 at 12:23 UTC