The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency

Felix Brandt 🌐, Manuel Eberl 🌐, Christian Saile 🌐 and Christian Stricker 🌐

March 22, 2018


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.


BSD License


Session Fishburn_Impossibility