Lean declarations

abbrev SocialChoice.Voting.VotingRule EconCSLib @ cef01c7, EconCSLib.SocialChoice.Voting.Basic
A set-valued voting rule on fixed finite voter and candidate types.
```
abbrev VotingRule (N A : Type*) [Fintype N] [Fintype A] :=
  Profile N A → Finset A
```
def SocialChoice.Voting.IsTotal EconCSLib @ cef01c7, EconCSLib.SocialChoice.Voting.Basic
A voting rule is total if it always returns at least one winner.
```
def IsTotal [Fintype N] [Fintype A] (f : VotingRule N A) : Prop :=
  ∀ P : Profile N A, (f P).Nonempty
```
def SocialChoice.Voting.Resolute EconCSLib @ cef01c7, EconCSLib.SocialChoice.Voting.Basic
A voting rule is resolute if it always returns exactly one winner.
```
def Resolute [Fintype N] [Fintype A] (f : VotingRule N A) : Prop :=
  ∀ P : Profile N A, Finset.card (f P) = 1
```

Modules: EconCSLib.SocialChoice.Voting.Basic

Social Choice Function

A social choice function aggregates a preference profile into the alternatives that win. In this formalization it is the set-valued voting rule $$ f : \mathrm{PrefProfile}(N, A) \to \mathcal{P}(A) $$ returning, for every profile, the (possibly tied) winner set $f(P)$.

In Lean this is SocialChoice.Voting.VotingRule N A, the abbreviation Profile N A → Finset A. Two refinements isolate the single-winner case:

IsTotal f — every profile has at least one winner, $f(P) \ne \varnothing$.
Resolute f — every profile has exactly one winner, $\#f(P) = 1$. A resolute rule is the set-valued encoding of the classical single-valued SCF $G : \mathrm{PrefProfile}(N,A) \to A$ via $f(P) = \{G(P)\}$.

Compared with a social welfare function ([[social_choice.voting.swf]]) the voting rule returns only the chosen winners rather than a full ranking. The standard axioms — unanimity ([[social_choice.voting.unanimity]]), monotonicity ([[social_choice.voting.monotonic_scf]]), strategy-proofness ([[social_choice.voting.strategyproof]]), and (non-)dictatorship ([[social_choice.voting.dictatorial_scf]]) — are all stated on the winner set $f(P)$, with strategy-proofness and dictatorship specializing to the resolute case.

References

[MSZ 21.21] Maschler, Solan, and Zamir, Game Theory. Social choice function.

Social Choice Function

References

Used by

Also in