Gibbard–Satterthwaite theorem

16 fully proved

Strict preference orders

AbbreviationStrict preference orders for the Gibbard–Satterthwaite theorem#✓fully proved

A strict total order on a type \(\alpha\) is a binary relation \(<\) on \(\alpha\) that is irreflexive (\(a < a\) holds for no \(a\)), transitive (\(a < b\) and \(b < c\) imply \(a < c\)) and total on distinct elements (\(a \ne b\) implies \(a < b\) or \(b < a\)). In the Gibbard–Satterthwaite development it models a voter's strict preference over alternatives.

abbrev StrictTotalOrder (α : Type*) :=
  MathlibExt.Order.StrictTotalOrder α

Uses 1 · Used by 9

Statement usesStrict total order

Used byProfiles differing only at one voter · Gibbard–Satterthwaite theorem, finiteness form · Irreflexivity of strict preference · Top-ranked alternative · Relation of a strict preference order · Building a strict preference order in the Gibbard–Satterthwaite setting · Preference profiles for the Gibbard–Satterthwaite theorem · Strict preferences in the Gibbard–Satterthwaite setting are total · Transitivity of strict preferences in the Gibbard–Satterthwaite setting

Strict Total Order

AbbreviationBuilding a strict preference order in the Gibbard–Satterthwaite setting#✓fully proved

A binary relation \(<\) on a type \(\alpha\) that is irreflexive (\(a < a\) holds for no \(a\)), transitive (\(a < b\) and \(b < c\) imply \(a < c\)) and total on distinct elements (\(a \ne b\) implies \(a < b\) or \(b < a\)) defines a strict total order on \(\alpha\) whose relation is \(<\).

abbrev mk {α : Type*} (lt : α → α → Prop)
    (irrefl : ∀ a, ¬lt a a)
    (trans : ∀ {a b c}, lt a b → lt b c → lt a c)
    (total : ∀ {a b}, a ≠ b → lt a b ∨ lt b a) :
    StrictTotalOrder α :=
  MathlibExt.Order.StrictTotalOrder.mk lt irrefl trans total

Uses 2

Statement usesStrict preference orders for the Gibbard–Satterthwaite theorem · Strict total order

AbbreviationRelation of a strict preference order#✓fully proved

The relation of a strict total order \(T\) on a type \(\alpha\) is its underlying binary relation \(\lt _T\) on \(\alpha\), which is irreflexive, transitive, and relates any two distinct elements in one direction or the other.

abbrev lt {α : Type*} (self : StrictTotalOrder α) : α → α → Prop :=
  MathlibExt.Order.StrictTotalOrder.lt self

Uses 2 · Used by 6

Statement usesStrict preference orders for the Gibbard–Satterthwaite theorem · Strict total order

Used byGibbard–Satterthwaite theorem, finiteness form · Irreflexivity of strict preference · Strategy-proof social choice function · Top-ranked alternative · Strict preferences in the Gibbard–Satterthwaite setting are total · Transitivity of strict preferences in the Gibbard–Satterthwaite setting

AbbreviationIrreflexivity of strict preference#✓fully proved

Let \(T\) be a strict total order on a type \(\alpha\), with relation \(\lt _T\). Then \(a \lt _T a\) fails for every \(a \in \alpha\).

abbrev irrefl {α : Type*} (self : StrictTotalOrder α) (a : α) : ¬self.lt a a :=
  MathlibExt.Order.StrictTotalOrder.irrefl self a

Uses 3 · Used by 1

Statement usesStrict preference orders for the Gibbard–Satterthwaite theorem · Relation of a strict preference order · Strict total order

Used byGibbard–Satterthwaite theorem, finiteness form

AbbreviationTransitivity of strict preferences in the Gibbard–Satterthwaite setting#✓fully proved

Let \(<\) be the relation of a strict total order on a type \(\alpha\). If \(a, b, c \in \alpha\) satisfy \(a < b\) and \(b < c\), then \(a < c\).

abbrev trans {α : Type*} (self : StrictTotalOrder α) {a b c : α}
    (h1 : self.lt a b) (h2 : self.lt b c) : self.lt a c :=
  MathlibExt.Order.StrictTotalOrder.trans self h1 h2

Uses 3 · Used by 1

Statement usesStrict preference orders for the Gibbard–Satterthwaite theorem · Relation of a strict preference order · Strict total order

Used byGibbard–Satterthwaite theorem, finiteness form

AbbreviationStrict preferences in the Gibbard–Satterthwaite setting are total#✓fully proved

Let \(<\) be the relation of a strict total order on a type \(\alpha\). If \(a, b \in \alpha\) and \(a \ne b\), then \(a < b\) or \(b < a\).

abbrev total {α : Type*} (self : StrictTotalOrder α) {a b : α} (h : a ≠ b) :
    self.lt a b ∨ self.lt b a :=
  MathlibExt.Order.StrictTotalOrder.total self h

Uses 3 · Used by 1

Statement usesStrict preference orders for the Gibbard–Satterthwaite theorem · Relation of a strict preference order · Strict total order

Used byGibbard–Satterthwaite theorem, finiteness form

Social choice functions and the Gibbard–Satterthwaite theorem

AbbreviationPreference profiles for the Gibbard–Satterthwaite theorem#✓fully proved

For a type \(A\) of alternatives and a type \(V\) of voters, a profile is a function assigning to each voter \(i \in V\) a strict total order \(\lt _i\) on \(A\), the strict preference of voter \(i\).

abbrev Profile (Alt Voter : Type*) := Voter → StrictTotalOrder Alt

Uses 1 · Used by 6

Statement usesStrict preference orders for the Gibbard–Satterthwaite theorem

Used byProfiles differing only at one voter · Gibbard–Satterthwaite theorem, finiteness form · Dictator of a social choice function · Onto social choice function · Strategy-proof social choice function · Social choice functions

AbbreviationSocial choice functions#✓fully proved

For a type \(A\) of alternatives and a type \(V\) of voters, a resolute social choice function is a function \(F\) sending each profile \(p\) (an assignment of a strict total order on \(A\) to each voter in \(V\)) to a single chosen alternative \(F(p) \in A\).

abbrev SocialChoiceFunction (Alt Voter : Type*) := Profile Alt Voter → Alt

Uses 1 · Used by 6

Statement usesPreference profiles for the Gibbard–Satterthwaite theorem

Used byGibbard–Satterthwaite theorem · Gibbard–Satterthwaite theorem, finiteness form · Dictator of a social choice function · Dictatorial social choice function · Onto social choice function · Strategy-proof social choice function

DefinitionTop-ranked alternative#✓fully proved

For a strict total order \(o\) on the alternatives, write \(x \succ_o y\) when \(x\) is related to \(y\) by \(o\) (\(o\) ranks \(x\) above \(y\)). An alternative \(t\) is top-ranked by \(o\) when \(t \succ_o b\) for every alternative \(b \ne t\).

def IsTopRanked {Alt : Type*} (o : StrictTotalOrder Alt) (top : Alt) : Prop :=
  ∀ b, b ≠ top → o.lt top b

Uses 2 · Used by 2

Statement usesStrict preference orders for the Gibbard–Satterthwaite theorem · Relation of a strict preference order

Used byGibbard–Satterthwaite theorem, finiteness form · Dictator of a social choice function

DefinitionOnto social choice function#✓fully proved

A resolute social choice function \(F\) is onto when every alternative \(a\) is chosen at some profile, that is, \(F(p) = a\) for some profile \(p\).

def IsOnto {Alt Voter : Type*} (F : SocialChoiceFunction Alt Voter) : Prop :=
  ∀ a, ∃ p : Profile Alt Voter, F p = a

Uses 2 · Used by 2

Statement usesPreference profiles for the Gibbard–Satterthwaite theorem · Social choice functions

Used byGibbard–Satterthwaite theorem · Gibbard–Satterthwaite theorem, finiteness form

DefinitionProfiles differing only at one voter#✓fully proved

Let \(p_1\) and \(p_2\) be profiles, each assigning a strict total order on the alternatives to every voter, and let \(i\) be a voter. Then \(p_2\) differs from \(p_1\) at most at voter \(i\) when \(p_1(j) = p_2(j)\) for every voter \(j \ne i\).

def DiffAtMostAt {Alt Voter : Type*} (p₁ p₂ : Profile Alt Voter) (i : Voter) : Prop :=
  ∀ j, j ≠ i → p₁ j = p₂ j

Uses 2 · Used by 2

Statement usesPreference profiles for the Gibbard–Satterthwaite theorem · Strict preference orders for the Gibbard–Satterthwaite theorem

Used byGibbard–Satterthwaite theorem, finiteness form · Strategy-proof social choice function

DefinitionStrategy-proof social choice function#✓fully proved

For a strict total order \(P\), write \(x \succ_P y\) when \(x\) is related to \(y\) by \(P\) (\(P\) ranks \(x\) above \(y\)). A resolute social choice function \(F\) is strategy-proof when, for all profiles \(p_1\), \(p_2\) and every voter \(i\) such that \(p_1(j) = p_2(j)\) for all voters \(j \ne i\), it is not the case that \(F(p_2) \succ_{p_1(i)} F(p_1)\): no voter gains by misreporting alone, judged by the true order \(p_1(i)\).

def IsStrategyProof {Alt Voter : Type*} (F : SocialChoiceFunction Alt Voter) : Prop :=
  ∀ (p₁ : Profile Alt Voter) (i : Voter) (p₂ : Profile Alt Voter),
    DiffAtMostAt p₁ p₂ i → ¬ (p₁ i).lt (F p₂) (F p₁)

Uses 4 · Used by 2

Statement usesProfiles differing only at one voter · Preference profiles for the Gibbard–Satterthwaite theorem · Social choice functions · Relation of a strict preference order

Used byGibbard–Satterthwaite theorem · Gibbard–Satterthwaite theorem, finiteness form

DefinitionDictator of a social choice function#✓fully proved

For a resolute social choice function \(F\), a voter \(d\) is a dictator when, for every profile \(p\), the chosen alternative \(F(p)\) is top-ranked in the preference order \(p(d)\) of voter \(d\).

def IsDictator {Alt Voter : Type*} (F : SocialChoiceFunction Alt Voter) (d : Voter) : Prop :=
  ∀ p : Profile Alt Voter, IsTopRanked (p d) (F p)

Uses 3 · Used by 2

Statement usesTop-ranked alternative · Preference profiles for the Gibbard–Satterthwaite theorem · Social choice functions

Used byGibbard–Satterthwaite theorem, finiteness form · Dictatorial social choice function

DefinitionDictatorial social choice function#✓fully proved

A resolute social choice function \(F\) is dictatorial when some voter is a dictator for \(F\): there is a voter \(d\) such that, for every profile \(p\), the chosen alternative \(F(p)\) is top-ranked in the preference order \(p(d)\) of voter \(d\).

def IsDictatorial {Alt Voter : Type*} (F : SocialChoiceFunction Alt Voter) : Prop :=
  ∃ d : Voter, IsDictator F d

Uses 2 · Used by 2

Statement usesDictator of a social choice function · Social choice functions

Used byGibbard–Satterthwaite theorem · Gibbard–Satterthwaite theorem, finiteness form

TheoremGibbard–Satterthwaite theorem, finiteness form#✓fully proved

Let the set of alternatives be finite and the set of voters be finite and nonempty, and suppose there are at least three distinct alternatives. Then every resolute social choice function on profiles of strict preference orders that is onto and strategy-proof is dictatorial.

theorem gibbard_satterthwaite_general
    {Alt Voter : Type*} [Finite Alt] [Finite Voter] [Nonempty Voter]
    (hAlt : ∃ a b c : Alt, a ≠ b ∧ a ≠ c ∧ b ≠ c)
    (F : SocialChoiceFunction Alt Voter)
    (hOnto : IsOnto F) (hSP : IsStrategyProof F) :
    IsDictatorial F

Sources

• A. Gibbard, Econometrica 41 (1973), 587-601, DOI 10.2307/1914083; M. A. Satterthwaite, J. Econom. Theory 10 (1975), 187-217, DOI 10.1016/0022-0531(75)90050-2.

Uses 21 · Used by 1

Statement usesDictatorial social choice function · Onto social choice function · Strategy-proof social choice function · Social choice functions

Proof usesDictator of a social welfare function · Dictatorial social welfare function · Independence of irrelevant alternatives · Pareto condition · Preference profile (Arrow's theorem) · Preference relation of a strict total order (Arrow's theorem) · Arrow's impossibility theorem for strict preferences, general form · Profiles differing only at one voter · Dictator of a social choice function · Top-ranked alternative · Preference profiles for the Gibbard–Satterthwaite theorem · Strict preference orders for the Gibbard–Satterthwaite theorem · Irreflexivity of strict preference · Relation of a strict preference order · Strict preferences in the Gibbard–Satterthwaite setting are total · Transitivity of strict preferences in the Gibbard–Satterthwaite setting · Strict total order

Used byGibbard–Satterthwaite theorem

TheoremGibbard–Satterthwaite theorem#✓fully proved

Let the set of alternatives be finite and the set of voters be finite and nonempty, and suppose there are at least three distinct alternatives. Then every resolute social choice function on profiles of strict preference orders that is onto and strategy-proof is dictatorial.

theorem gibbard_satterthwaite
    {Alt Voter : Type*} [Fintype Alt] [DecidableEq Alt]
    [Fintype Voter] [DecidableEq Voter] [Nonempty Voter]
    (hAlt : ∃ a b c : Alt, a ≠ b ∧ a ≠ c ∧ b ≠ c)
    (F : SocialChoiceFunction Alt Voter)
    (hOnto : IsOnto F) (hSP : IsStrategyProof F) :
    IsDictatorial F

Sources

• A. Gibbard, Econometrica 41 (1973), 587-601, DOI 10.2307/1914083; M. A. Satterthwaite, J. Econom. Theory 10 (1975), 187-217, DOI 10.1016/0022-0531(75)90050-2.

Uses 5

Statement usesDictatorial social choice function · Onto social choice function · Strategy-proof social choice function · Social choice functions

Proof usesGibbard–Satterthwaite theorem, finiteness form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.