EconCSLib.SocialChoice.Voting.VotingRules

Concrete voting-rule vocabulary over strict finite profiles.

The main rules in this file are set-valued: ties are represented by multiple winners in the returned Finset.

Main definitions

• rank, position — ordinal position of an alternative in a ballot
• margin, MajorityPrefers, CondorcetWinner
• scoringRule, plurality, borda, veto
• copeland

Main result

• condorcet_paradox_possible — a concrete 3-voter, 3-alternative profile with no Condorcet winner

Rank and position

noncomputable def SocialChoice.Voting.rank {A : Type u_2} [Fintype A] (r : LinearOrder A) (a : A) : ℕ

rank r a is the number of alternatives strictly above a in ballot r.

Equations

• SocialChoice.Voting.rank r a = {b : A | SocialChoice.Voting.BallotPrefers r b a}.card

noncomputable def SocialChoice.Voting.position {A : Type u_2} [Fintype A] (r : LinearOrder A) (a : A) : ℕ

The 1-based position of a in ballot r.

Equations

• SocialChoice.Voting.position r a = SocialChoice.Voting.rank r a + 1

theorem SocialChoice.Voting.position_eq_rank_succ {A : Type u_2} [Fintype A] (r : LinearOrder A) (a : A) : position r a = rank r a + 1

theorem SocialChoice.Voting.rank_lt_card {A : Type u_2} [Fintype A] (r : LinearOrder A) (a : A) : rank r a < Fintype.card A

theorem SocialChoice.Voting.position_le_card {A : Type u_2} [Fintype A] (r : LinearOrder A) (a : A) : position r a ≤ Fintype.card A

theorem SocialChoice.Voting.rank_lt_of_lt {A : Type u_2} [Fintype A] (r : LinearOrder A) {a b : A} (hab : BallotPrefers r a b) : rank r a < rank r b

theorem SocialChoice.Voting.rank_lt_iff {A : Type u_2} [Fintype A] (r : LinearOrder A) {a b : A} : rank r a < rank r b ↔ BallotPrefers r a b

theorem SocialChoice.Voting.rank_injective {A : Type u_2} [Fintype A] (r : LinearOrder A) : Function.Injective (rank r)

Pairwise majority and margins

noncomputable def SocialChoice.Voting.votersPreferring {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (a b : A) : Finset N

Voters who strictly prefer a to b.

Equations

• SocialChoice.Voting.votersPreferring P a b = {i : N | SocialChoice.Voting.Prefers P i a b}

noncomputable def SocialChoice.Voting.margin {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (a b : A) : ℤ

Pairwise majority margin: voters preferring a to b minus voters preferring b to a.

Equations

• SocialChoice.Voting.margin P a b = Int.ofNat (SocialChoice.Voting.votersPreferring P a b).card - Int.ofNat (SocialChoice.Voting.votersPreferring P b a).card

def SocialChoice.Voting.margin_pos {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (a b : A) : Prop

Positive pairwise majority margin.

Equations

• SocialChoice.Voting.margin_pos P a b = (0 < SocialChoice.Voting.margin P a b)

theorem SocialChoice.Voting.margin_self {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (a : A) : margin P a a = 0

theorem SocialChoice.Voting.margin_skew {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (a b : A) : margin P a b = -margin P b a

def SocialChoice.Voting.MajorityPrefers {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (a b : A) : Prop

Pairwise majority comparison.

Equations

• SocialChoice.Voting.MajorityPrefers P a b = SocialChoice.Voting.margin_pos P a b

def SocialChoice.Voting.CondorcetWinner {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (a : A) : Prop

a is a Condorcet winner if it beats every other alternative by strict pairwise majority.

Equations

• SocialChoice.Voting.CondorcetWinner P a = ∀ (b : A), b ≠ a → SocialChoice.Voting.MajorityPrefers P a b

def SocialChoice.Voting.HasCondorcetWinner {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) : Prop

A profile has at least one Condorcet winner.

Equations

• SocialChoice.Voting.HasCondorcetWinner P = ∃ (a : A), SocialChoice.Voting.CondorcetWinner P a

def SocialChoice.Voting.CondorcetConsistency {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) : Prop

A rule is Condorcet-consistent if every Condorcet winner is the unique winner.

Equations

• SocialChoice.Voting.CondorcetConsistency f = ∀ (P : SocialChoice.Voting.Profile N A) (a : A), SocialChoice.Voting.CondorcetWinner P a → f P = {a}

Scoring rules

noncomputable def SocialChoice.Voting.scoreCandidate {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (score : ℕ → ℤ) (a : A) : ℤ

Total score for a candidate under a positional score vector.

Equations

• SocialChoice.Voting.scoreCandidate P score a = ∑ i : N, score (SocialChoice.Voting.rank (P.pref i) a)

noncomputable def SocialChoice.Voting.scoringWinners {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (score : ℕ → ℤ) : Finset A

Winners with maximal score.

Equations

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

noncomputable def SocialChoice.Voting.scoringRule {N : Type u_1} {A : Type u_2} (score : ℕ → ℕ → ℤ) [Fintype N] [Fintype A] : VotingRule N A

Generic positional scoring rule. The first argument is the number of alternatives, and the second is the zero-based rank.

Equations

• SocialChoice.Voting.scoringRule score P = SocialChoice.Voting.scoringWinners P fun (r : ℕ) => score (Fintype.card A) r

theorem SocialChoice.Voting.scoringWinners_nonempty {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Nonempty A] (P : Profile N A) (score : ℕ → ℤ) : (scoringWinners P score).Nonempty

theorem SocialChoice.Voting.scoringRule_isTotal {N : Type u_1} {A : Type u_2} (score : ℕ → ℕ → ℤ) [Fintype N] [Fintype A] [Nonempty A] : IsTotal (scoringRule score)

def SocialChoice.Voting.pluralityScore (_m r : ℕ) : ℤ

Plurality score vector.

Equations

• SocialChoice.Voting.pluralityScore _m r = if r = 0 then 1 else 0

def SocialChoice.Voting.bordaScore (m r : ℕ) : ℤ

Borda score vector, with top rank receiving m - 1 points.

Equations

• SocialChoice.Voting.bordaScore m r = Int.ofNat (m - 1 - r)

def SocialChoice.Voting.vetoScore (m r : ℕ) : ℤ

Veto score vector: every non-last rank receives one point.

Equations

• SocialChoice.Voting.vetoScore m r = if r + 1 = m then 0 else 1

noncomputable def SocialChoice.Voting.plurality {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] : VotingRule N A

Plurality rule.

Equations

• SocialChoice.Voting.plurality = SocialChoice.Voting.scoringRule SocialChoice.Voting.pluralityScore

noncomputable def SocialChoice.Voting.borda {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] : VotingRule N A

Borda rule.

Equations

• SocialChoice.Voting.borda = SocialChoice.Voting.scoringRule SocialChoice.Voting.bordaScore

noncomputable def SocialChoice.Voting.veto {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] : VotingRule N A

Veto rule.

Equations

• SocialChoice.Voting.veto = SocialChoice.Voting.scoringRule SocialChoice.Voting.vetoScore

theorem SocialChoice.Voting.plurality_isTotal {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Nonempty A] : IsTotal plurality

theorem SocialChoice.Voting.borda_isTotal {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Nonempty A] : IsTotal borda

theorem SocialChoice.Voting.veto_isTotal {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Nonempty A] : IsTotal veto

Copeland rule

noncomputable def SocialChoice.Voting.copelandScore {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (a : A) : ℤ

Copeland score: pairwise majority wins minus pairwise majority losses.

Equations

• SocialChoice.Voting.copelandScore P a = Int.ofNat {b : A | SocialChoice.Voting.MajorityPrefers P a b}.card - Int.ofNat {b : A | SocialChoice.Voting.MajorityPrefers P b a}.card

noncomputable def SocialChoice.Voting.copeland {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] : VotingRule N A

Copeland winners.

Equations

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

theorem SocialChoice.Voting.copeland_isTotal {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Nonempty A] : IsTotal copeland

Condorcet paradox

theorem SocialChoice.Voting.condorcet_paradox_possible : ∃ (P : Profile (Fin 3) (Fin 3)), ¬HasCondorcetWinner P

Condorcet paradox: with 3 voters and 3 alternatives, pairwise majority can cycle, so a Condorcet winner need not exist.