### Abstract

This work contains a formalisation of basic Randomised Social Choice, including Stochastic Dominance and Social Decision Schemes (SDSs) along with some of their most important properties (Anonymity, Neutrality, ex-post- and SD-Efficiency, SD-Strategy-Proofness) and two particular SDSs – Random Dictatorship and Random Serial Dictatorship (with proofs of the properties that they satisfy). Many important properties of these concepts are also proven – such as the two equivalent characterisations of Stochastic Dominance and the fact that SD-efficiency of a lottery only depends on the support. The entry also provides convenient commands to define Preference Profiles, prove their well-formedness, and automatically derive restrictions that sufficiently nice SDSs need to satisfy on the defined profiles. Currently, the formalisation focuses on weak preferences and Stochastic Dominance, but it should be easy to extend it to other domains – such as strict preferences – or other lottery extensions – such as Bilinear Dominance or Pairwise Comparison.

### License

BSD License

### Topics

- Mathematics/Games and economics

### Session Randomised_Social_Choice

- Order_Predicates
- Preference_Profiles
- Elections
- Lotteries
- Utility_Functions
- Stochastic_Dominance
- SD_Efficiency
- Social_Decision_Schemes
- SDS_Lowering
- Random_Dictatorship
- Random_Serial_Dictatorship
- Randomised_Social_Choice
- Preference_Profile_Cmd
- QSOpt_Exact
- SDS_Automation

### Depends on

- List Index

### Used by

- The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections
- The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
- The Incompatibility of SD-Efficiency and SD-Strategy-Proofness

## Cite

×

Randomised_Social_Choice-AFP

    @article{Randomised_Social_Choice-AFP,
      author  = {Manuel Eberl},
      title   = {Randomised Social Choice Theory},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Randomised_Social_Choice.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- May 5, 2016 : Isabelle2016