The Incompatibility of SD-Efficiency and SD-Strategy-Proofness

Title:	The Incompatibility of SD-Efficiency and SD-Strategy-Proofness
Author:	Manuel Eberl
Submission date:	2016-05-04
Abstract:	This formalisation contains the proof that there is no anonymous and neutral Social Decision Scheme for at least four voters and alternatives that fulfils both SD-Efficiency and SD-Strategy- Proofness. The proof is a fully structured and quasi-human-redable one. It was derived from the (unstructured) SMT proof of the case for exactly four voters and alternatives by Brandl et al. Their proof relies on an unverified translation of the original problem to SMT, and the proof that lifts the argument for exactly four voters and alternatives to the general case is also not machine-checked. In this Isabelle proof, on the other hand, all of these steps are fully proven and machine-checked. This is particularly important seeing as a previously published informal proof of a weaker statement contained a mistake in precisely this lifting step.
BibTeX:	@article{SDS_Impossibility-AFP, author = {Manuel Eberl}, title = {The Incompatibility of SD-Efficiency and SD-Strategy-Proofness}, journal = {Archive of Formal Proofs}, month = may, year = 2016, note = {\url{http://isa-afp.org/entries/SDS_Impossibility.html}, 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.