EconCSLib.SocialChoice.Voting.Decisive

Decisive coalitions and the decisive-coalitions proof of Arrow's impossibility theorem over strict voting profiles.

This file records the public decisive-coalition vocabulary for the strict ranked-ballot voting domain. The proof route is the standard one:

1. unanimity implies the grand coalition is decisive;
2. weak decisiveness for one ordered pair spreads to decisiveness for all pairs;
3. any decisive coalition of size at least two has a strictly smaller nonempty decisive subcoalition;
4. a minimal decisive coalition is a singleton;
5. the singleton voter is a dictator.

def SocialChoice.Voting.IsDecisiveFor {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (F : SWF N A) (C : Set N) (a b : A) : Prop

A coalition is decisive for a over b if unanimous strict support inside the coalition forces the social strict preference a ≻ b.

Equations

• SocialChoice.Voting.IsDecisiveFor F C a b = ∀ (P : SocialChoice.Voting.Profile N A), (∀ i ∈ C, SocialChoice.Voting.Prefers P i a b) → strict (F P).rel a b

def SocialChoice.Voting.IsDecisive {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (F : SWF N A) (C : Set N) : Prop

A coalition is decisive if it is decisive for every ordered pair of alternatives.

Equations

• SocialChoice.Voting.IsDecisive F C = ∀ (a b : A), SocialChoice.Voting.IsDecisiveFor F C a b

def SocialChoice.Voting.SWF.IsDictator {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (F : SWF N A) (i : N) : Prop

An individual is a dictator exactly when their singleton coalition is decisive.

Equations

• F.IsDictator i = SocialChoice.Voting.IsDecisive F {i}

theorem SocialChoice.Voting.unanimity_univ_isDecisive {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] {F : SWF N A} (h : F.Unanimity) : IsDecisive F Set.univ

theorem SocialChoice.Voting.singleton_unanimity_isDictator {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Subsingleton N] {F : SWF N A} (h : F.Unanimity) (i : N) : F.IsDictator i

theorem SocialChoice.Voting.singleton_unanimity_dictatorial {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Subsingleton N] [Nonempty N] {F : SWF N A} (h : F.Unanimity) : F.Dictatorial

def SocialChoice.Voting.IsWeaklyDecisiveFor {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (F : SWF N A) (C : Set N) (a b : A) : Prop

Weak decisiveness tests a coalition against a complement unanimously supporting the opposite strict ranking.

Equations

• One or more equations did not get rendered due to their size.

theorem SocialChoice.Voting.isWeaklyDecisiveFor_of_isDecisiveFor {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] {F : SWF N A} {C : Set N} {a b : A} (h : IsDecisiveFor F C a b) : IsWeaklyDecisiveFor F C a b

theorem SocialChoice.Voting.iia_strict {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] {F : SWF N A} (hF : F.IIA) {P Q : Profile N A} {a b : A} (hab : ∀ (i : N), Prefers P i a b ↔ Prefers Q i a b) (hba : ∀ (i : N), Prefers P i b a ↔ Prefers Q i b a) : strict (F P).rel a b ↔ strict (F Q).rel a b

Strict ballot surgery for the decisive-coalitions proof

theorem SocialChoice.Voting.decisive_spread {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] {F : SWF N A} (hU : F.Unanimity) (hIIA : F.IIA) {C : Set N} {x y z : A} (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) (hC : C.Nonempty) (h : IsWeaklyDecisiveFor F C x y) : IsDecisive F C

def SocialChoice.Voting.exists_nonempty_decisive_of_size {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (F : SWF N A) (n : ℕ) : Prop

Equations

• SocialChoice.Voting.exists_nonempty_decisive_of_size F n = ∃ (C : Set N), C.Nonempty ∧ SocialChoice.Voting.IsDecisive F C ∧ C.ncard = n

theorem SocialChoice.Voting.exists_minimal_decisive_coalition {N : Type u_1} {A : Type u_2} [Fintype N] [Nonempty N] [Fintype A] {F : SWF N A} (hU : F.Unanimity) : ∃ (n : ℕ), Minimal (exists_nonempty_decisive_of_size F) n

theorem SocialChoice.Voting.decisive_contraction {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] {F : SWF N A} (h0 : ∃ (x : A) (y : A) (z : A), x ≠ y ∧ x ≠ z ∧ y ≠ z) {C : Set N} (hCdec : IsDecisive F C) (hCcard : 2 ≤ C.ncard) (hU : F.Unanimity) (hIIA : F.IIA) : ∃ (S : Set N), S.Nonempty ∧ S < C ∧ IsDecisive F S

theorem SocialChoice.Voting.decisive_minimal {N : Type u_1} {A : Type u_2} [Fintype N] [Nonempty N] [Fintype A] (h0 : ∃ (x : A) (y : A) (z : A), x ≠ y ∧ x ≠ z ∧ y ≠ z) {F : SWF N A} (hU : F.Unanimity) (hIIA : F.IIA) : Minimal (exists_nonempty_decisive_of_size F) 1

theorem SocialChoice.Voting.arrow_of_unanimity_iia {N : Type u_1} {A : Type u_2} [Fintype N] [Nonempty N] [Fintype A] (h0 : ∃ (x : A) (y : A) (z : A), x ≠ y ∧ x ≠ z ∧ y ≠ z) {F : SWF N A} (h1 : F.Unanimity) (h2 : F.IIA) : F.Dictatorial

Arrow's decisive-coalitions theorem for strict finite voting profiles: unanimity and IIA imply dictatorship.