EconCSLib.SocialChoice.Voting.GibbardSatterthwaite

The Gibbard-Satterthwaite theorem and its standard finite-profile proof route.

The public statements use the voting layer's set-valued VotingRule interface plus a Resolute hypothesis. The proof is intentionally deferred while the voting architecture is being rebuilt.

Theorem statements

• muller_satterthwaite — monotonic + unanimous + resolute implies dictatorial
• strategyproof_monotonic — resolute strategy-proof implies monotonic
• gibbard_satterthwaite — resolute strategy-proof + unanimous implies dictatorial

References

• [MSZ] Chapter 21, Theorems 21.27, 21.35, 21.39
• Gibbard (1973), Satterthwaite (1975)

Profile-surgery lemmas

theorem SocialChoice.Voting.monotonic_zProfile {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) (hM : Monotonicity f) (P Q : Profile N A) (R : Set A) [(a : A) → Decidable (a ∈ R)] {a : A} (haR : a ∈ R) (ha : a ∈ f P) : a ∈ f (zProfile P Q R)

If a monotonic resolute voting rule selects a at P, then a remains selected after the MSZ splice Z(P,Q;R), provided a ∈ R.

This is the set-valued strict-profile form of [MSZ 21.31].

theorem SocialChoice.Voting.unanimous_strict_pref_not_chosen {N : Type u_1} {A : Type u_2} [Fintype N] [Nonempty N] [Fintype A] (f : VotingRule N A) (hU : Unanimity f) (_hM : Monotonicity f) (P : Profile N A) {a b : A} (hab : ∀ (i : N), Prefers P i a b) : b ∉ f P

If every voter strictly prefers a to b, then a unanimous monotonic resolute voting rule cannot choose b. This is the set-valued strict-profile form of [MSZ 21.32].

theorem SocialChoice.Voting.zProfile_choice_mem {N : Type u_1} {A : Type u_2} [Fintype N] [Nonempty N] [Fintype A] (f : VotingRule N A) (hU : Unanimity f) (_hM : Monotonicity f) (P Q : Profile N A) (R : Set A) [(a : A) → Decidable (a ∈ R)] (hR : R.Nonempty) {a : A} (ha : a ∈ f (zProfile P Q R)) : a ∈ R

Under unanimity and monotonicity, every winner of zProfile P Q R belongs to R whenever R is nonempty. This is the set-valued strict-profile form of [MSZ 21.33].

Intermediate theorems

theorem SocialChoice.Voting.muller_satterthwaite {N : Type u_1} {A : Type u_2} [Fintype N] [Nonempty N] [Fintype A] [Nonempty A] (hA : Fintype.card A ≥ 3) (f : VotingRule N A) (hf_total : IsTotal f) (hf_res : Resolute f) (hU : Unanimity f) (hM : Monotonicity f) : Dictatorial f

Muller-Satterthwaite Theorem: if there are at least three alternatives, every resolute, unanimous, and monotonic voting rule on a finite nonempty voter set is dictatorial. [MSZ 21.27]

theorem SocialChoice.Voting.strategyproof_monotonic {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) (hf_res : Resolute f) (hSP : ResoluteStrategyproofness f hf_res) : Monotonicity f

Strategy-proofness implies monotonicity for finite voter sets. [MSZ 21.35]

Gibbard-Satterthwaite theorem

theorem SocialChoice.Voting.gibbard_satterthwaite {N : Type u_1} {A : Type u_2} [Fintype N] [Nonempty N] [Fintype A] [Nonempty A] (hA : Fintype.card A ≥ 3) (f : VotingRule N A) (hf_total : IsTotal f) (hf_res : Resolute f) (hU : Unanimity f) (hSP : ResoluteStrategyproofness f hf_res) : Dictatorial f

Gibbard-Satterthwaite Theorem: if there are at least three alternatives, every resolute, nonmanipulable, and unanimous voting rule on a finite nonempty voter set is dictatorial. [MSZ 21.39, Gibbard 1973, Satterthwaite 1975]