Lean declarations

def SocialChoice.Voting.IsWeaklyDecisiveFor EconCSLib @ cef01c7, EconCSLib.SocialChoice.Voting.Decisive

def IsWeaklyDecisiveFor [Fintype N] [Fintype A]
    (F : SWF N A) (C : Set N) (a b : A) : Prop :=
  ∀ P : Profile N A,
    (∀ i ∈ C, Prefers P i a b) ∧ (∀ i ∉ C, Prefers P i b a) →
      strict (F P) a b

theorem SocialChoice.Voting.isWeaklyDecisiveFor_of_isDecisiveFor EconCSLib @ cef01c7, EconCSLib.SocialChoice.Voting.Decisive

theorem isWeaklyDecisiveFor_of_isDecisiveFor [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

Modules: EconCSLib.SocialChoice.Voting.Decisive

Weakly Decisive Coalition

A coalition $C \subseteq N$ is weakly decisive for the ordered pair $(a, b)$ under a social welfare function $F$ ([[social_choice.voting.swf]]) if unanimous $a \succ b$ inside $C$, combined with unanimous $b \succ a$ outside $C$, forces society to rank $a \succ b$: $$ \forall P,\ \bigl(\forall i \in C,\ a \succ_{P_i} b\bigr) \wedge \bigl(\forall i \notin C,\ b \succ_{P_i} a\bigr) \Rightarrow a \succ_{F(P)} b. $$

In Lean: SocialChoice.Voting.IsWeaklyDecisiveFor F C a b.

Weak decisiveness is implied by decisiveness ([[social_choice.voting.is_decisive_for]]) — a witness profile satisfying the stronger constraint of total opposition is in particular a witness for plain decisiveness: SocialChoice.Voting.isWeaklyDecisiveFor_of_isDecisiveFor.

The opposite-direction-strengthening — turning weak decisiveness into full decisiveness — is the substantive content of the field expansion lemma [[social_choice.voting.decisive_spread]]. The split into "weak" vs full decisiveness lets the Arrow proof use only the simpler hypothesis when building witnesses.

References

[MSZ 21.14ff] Maschler, Solan, and Zamir, Game Theory. Weak decisiveness in the field-expansion argument.

Used by

Field Expansion — Decisive on One Pair Implies Decisive Everywhere

Weakly Decisive Coalition

References

Used by

Also in