A Formal Proof of the Incompatibility of SD-Efficiency and SD-Strategy-Proofness

by Manuel Eberl

Bachelor's thesis at the Technical University of Munich (2016)




In the design of voting rules, there are three intuitively desirable properties that one might reasonably expect such a rule to fulfil: A voting rule should treat every voter and any alternative on the ballot equally; The result should satisfy the voters as far as possible, i.e. there should be no other result that is obviously better for everyone; No voter should be able to obtain an advantage by lying about her preferences.

These intuitively desirable properties have formal counterparts by the name of Anonymity and Neutrality, Efficiency, and Strategy-Proofness, respectively. It is well-known that the last two are in some way in conflict to one another – fulfilling both of them is often not possible or imposes great restrictions.

This work focuses on the setting of randomised voting with weak preferences (i.e. voters may submit preferences with ties), particularly on previous work by Brandl et al., who used computerised search and SMT solvers to prove a conjecture by Aziz et al. that no anonymous and neutral randomised voting rule (known as Social Decision Scheme) can fulfil the notions of both SD-Efficiency and SD-Strategy-Proofness. My work consists of a fully mechanised formal proof of this result using the interactive theorem prover Isabelle and, based upon this, a human-readable pen-and-paper proof.

Download PDF (977 KiB)


 author = {Eberl, Manuel},
 title = {A Formal Proof of the Incompatibility of \mathit{SD}-Efficiency and \mathit{SD}-Strategy-Proofness},
 year = {2016},
 month = {7},
 school = {Technical University of Munich},
 type = {Bachelor's thesis},
 note = {\url{https://www21.in.tum.de/~eberlm/pdfs/sds.pdf}}

Download BibTeX (329 Bytes)