Email Gateway (Aug 22 2022 at 13:18): Email Gateway (Aug 22 2022 at 13:18):From: Lawrence Paulson <lp15@cam.ac.uk>
Manuel’s second AFP contribution is now online. This is a direct application of his Randomised Social Choice development.
Larry Paulson
The Incompatibility of SD-Efficiency and SD-Strategy-Proofness
Manuel Eberl
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.
http://www.isa-afp.org/entries/SDS_Impossibility.shtml
Last updated: Nov 21 2024 at 12:39 UTC