The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency

Felix Brandt, Manuel Eberl, Christian Saile and Christian Stricker

22 March 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

Depends On


Related Entries