The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency

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

March 22, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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