Arrow's impossibility theorem

AbbreviationStrict preference orders for Arrow's theorem#✓fully proved

A strict total order on a type \(\alpha\) consists of a 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\)). Here it models a strict preference over alternatives.

abbrev StrictTotalOrder := MathlibExt.Order.StrictTotalOrder
Uses 1 · Used by 8
Statement usesStrict total order
Used byArrow's impossibility theorem for strict preferences, general form · Irreflexivity of strict preference (Arrow's theorem) · Preference relation of a strict total order (Arrow's theorem) · Strict total order from a relation (Arrow's theorem) · Preference profile (Arrow's theorem) · Social welfare function · Strict preference orders for Arrow's theorem are total · Strict preference orders for Arrow's theorem are transitive

AbbreviationStrict total order from a relation (Arrow's theorem)#✓fully proved

A 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\).

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 Arrow's theorem · Strict total order

AbbreviationPreference relation of a strict total order (Arrow's theorem)#✓fully proved

For a strict total order \(T\) on a type \(\alpha\), this is its underlying binary relation \(\lt _T\) on \(\alpha\).

abbrev lt {α : Type*} (self : StrictTotalOrder α) : α → α → Prop :=
  MathlibExt.Order.StrictTotalOrder.lt self
Uses 2 · Used by 8
Statement usesStrict preference orders for Arrow's theorem · Strict total order
Used byArrow's impossibility theorem for strict preferences, general form · Irreflexivity of strict preference (Arrow's theorem) · Dictator of a social welfare function · Independence of irrelevant alternatives · Pareto condition · Strict preference orders for Arrow's theorem are total · Strict preference orders for Arrow's theorem are transitive · Gibbard–Satterthwaite theorem, finiteness form

AbbreviationIrreflexivity of strict preference (Arrow's theorem)#✓fully proved

Let \(T\) be a strict total order on a type \(\alpha\), and write \(a \lt _T b\) for its relation. Then for every \(a \in \alpha\), \(a \lt _T a\) does not hold.

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 Arrow's theorem · Preference relation of a strict total order (Arrow's theorem) · Strict total order
Used byArrow's impossibility theorem for strict preferences, general form

AbbreviationStrict preference orders for Arrow's theorem are transitive#✓fully proved

If \(<\) is a strict total order on a type \(\alpha\) and \(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 Arrow's theorem · Preference relation of a strict total order (Arrow's theorem) · Strict total order
Used byArrow's impossibility theorem for strict preferences, general form

AbbreviationStrict preference orders for Arrow's theorem are total#✓fully proved

If \(<\) is a strict total order on a type \(\alpha\) and \(a, b \in \alpha\) are distinct, 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 Arrow's theorem · Preference relation of a strict total order (Arrow's theorem) · Strict total order
Used byArrow's impossibility theorem for strict preferences, general form

AbbreviationPreference profile (Arrow's theorem)#✓fully proved

A profile assigns to each voter a strict total order on the alternatives.

abbrev Profile (Alt Voter : Type*) := Voter → StrictTotalOrder Alt
Uses 1 · Used by 6
Statement usesStrict preference orders for Arrow's theorem
Used byArrow's impossibility theorem for strict preferences, general form · Dictator of a social welfare function · Independence of irrelevant alternatives · Pareto condition · Social welfare function · Gibbard–Satterthwaite theorem, finiteness form

AbbreviationSocial welfare function#✓fully proved

A social welfare function maps each unrestricted profile to a social strict total order.

abbrev SocialWelfareFunction (Alt Voter : Type*) := Profile Alt Voter → StrictTotalOrder Alt
Uses 2 · Used by 6
Statement usesPreference profile (Arrow's theorem) · Strict preference orders for Arrow's theorem
Used byArrow's impossibility theorem for strict preferences · Arrow's impossibility theorem for strict preferences, general form · Dictator of a social welfare function · Dictatorial social welfare function · Independence of irrelevant alternatives · Pareto condition

DefinitionPareto condition#✓fully proved

A social welfare function \(F\) satisfies the Pareto condition if for every profile \(p\) and all alternatives \(a, b\), whenever every voter strictly prefers \(a\) to \(b\) in \(p\), the social order \(F(p)\) also strictly prefers \(a\) to \(b\).

def IsPareto {Alt Voter : Type*} (F : SocialWelfareFunction Alt Voter) : Prop :=
  ∀ (p : Profile Alt Voter) (a b : Alt), (∀ i, (p i).lt a b) → (F p).lt a b
Uses 3 · Used by 3
Statement usesPreference profile (Arrow's theorem) · Social welfare function · Preference relation of a strict total order (Arrow's theorem)
Used byArrow's impossibility theorem for strict preferences · Arrow's impossibility theorem for strict preferences, general form · Gibbard–Satterthwaite theorem, finiteness form

DefinitionIndependence of irrelevant alternatives#✓fully proved

A social welfare function \(F\) satisfies independence of irrelevant alternatives if for all profiles \(p_1, p_2\) and all alternatives \(a, b\) the following holds: if every voter strictly prefers \(a\) to \(b\) in \(p_1\) exactly when that voter strictly prefers \(a\) to \(b\) in \(p_2\), then \(F(p_1)\) strictly prefers \(a\) to \(b\) exactly when \(F(p_2)\) does.

def IsIIA {Alt Voter : Type*} (F : SocialWelfareFunction Alt Voter) : Prop :=
  ∀ (p₁ p₂ : Profile Alt Voter) (a b : Alt),
    (∀ i, (p₁ i).lt a b ↔ (p₂ i).lt a b) → ((F p₁).lt a b ↔ (F p₂).lt a b)
Uses 3 · Used by 3
Statement usesPreference profile (Arrow's theorem) · Social welfare function · Preference relation of a strict total order (Arrow's theorem)
Used byArrow's impossibility theorem for strict preferences · Arrow's impossibility theorem for strict preferences, general form · Gibbard–Satterthwaite theorem, finiteness form

DefinitionDictator of a social welfare function#✓fully proved

A voter \(d\) is a dictator for a social welfare function \(F\) if for every profile \(p\) and all alternatives \(a, b\), whenever \(d\) strictly prefers \(a\) to \(b\) in \(p\), the social order \(F(p)\) also strictly prefers \(a\) to \(b\).

def IsDictator {Alt Voter : Type*} (F : SocialWelfareFunction Alt Voter) (d : Voter) : Prop :=
  ∀ (p : Profile Alt Voter) (a b : Alt), (p d).lt a b → (F p).lt a b
Uses 3 · Used by 3
Statement usesPreference profile (Arrow's theorem) · Social welfare function · Preference relation of a strict total order (Arrow's theorem)
Used byArrow's impossibility theorem for strict preferences, general form · Dictatorial social welfare function · Gibbard–Satterthwaite theorem, finiteness form

DefinitionDictatorial social welfare function#✓fully proved

A social welfare function \(F\) is dictatorial if some voter \(d\) is a dictator for \(F\): for every profile \(p\) and all alternatives \(a, b\), whenever \(d\) strictly prefers \(a\) to \(b\) in \(p\), the social order \(F(p)\) also strictly prefers \(a\) to \(b\).

def IsDictatorial {Alt Voter : Type*} (F : SocialWelfareFunction Alt Voter) : Prop :=
  ∃ d : Voter, IsDictator F d
Uses 2 · Used by 3
Statement usesDictator of a social welfare function · Social welfare function
Used byArrow's impossibility theorem for strict preferences · Arrow's impossibility theorem for strict preferences, general form · Gibbard–Satterthwaite theorem, finiteness form

TheoremArrow's impossibility theorem for strict preferences, general form#✓fully proved

Suppose there are finitely many alternatives, at least three of them, and finitely many voters, at least one. Then every social welfare function, which assigns a strict total order of the alternatives to each profile of strict total orders (one per voter), that satisfies the Pareto condition and independence of irrelevant alternatives is dictatorial.

Here finiteness is assumed only as a property. The companion statement of Arrow's impossibility theorem also fixes an explicit enumeration of the alternatives and of the voters and a decision procedure for equality on each; this extra data does not change the mathematical content.

theorem arrow_impossibility_general
    {Alt Voter : Type*} [Finite Alt] [Finite Voter] [Nonempty Voter]
    (hAlt : ∃ a b c : Alt, a ≠ b ∧ a ≠ c ∧ b ≠ c)
    (F : SocialWelfareFunction Alt Voter)
    (hPareto : IsPareto F) (hIIA : IsIIA F) :
    IsDictatorial F
Uses 12 · Used by 2
Statement usesDictatorial social welfare function · Independence of irrelevant alternatives · Pareto condition · Social welfare function
Proof usesDictator of a social welfare function · Preference profile (Arrow's theorem) · Strict preference orders for Arrow's theorem · Irreflexivity of strict preference (Arrow's theorem) · Preference relation of a strict total order (Arrow's theorem) · Strict preference orders for Arrow's theorem are total · Strict preference orders for Arrow's theorem are transitive · Strict total order
Used byArrow's impossibility theorem for strict preferences · Gibbard–Satterthwaite theorem, finiteness form

TheoremArrow's impossibility theorem for strict preferences#✓fully proved

Suppose there are finitely many alternatives, at least three of them, and finitely many voters, at least one. Then every social welfare function, which assigns a strict total order of the alternatives to each profile of strict total orders (one per voter), that satisfies the Pareto condition and independence of irrelevant alternatives is dictatorial.

theorem arrow_impossibility
    {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 : SocialWelfareFunction Alt Voter)
    (hPareto : IsPareto F) (hIIA : IsIIA F) :
    IsDictatorial F
Sources
  • K. J. Arrow, Social Choice and Individual Values, Wiley (1951; 2nd ed. 1963).
Uses 5
Statement usesDictatorial social welfare function · Independence of irrelevant alternatives · Pareto condition · Social welfare function
Proof usesArrow's impossibility theorem for strict preferences, general form

TheoremArrow's impossibility theorem for weak preferences#✓fully proved

Let \(A\) be a type of alternatives containing three distinct elements, and let \(E\) be a finite nonempty set of voters. A profile \(P\) assigns to every voter \(v\) a relation \(P_v\) on \(A\); it is admissible if, for every \(v \in E\), \(P_v\) is a total preorder (reflexive, transitive, and \(P_v(x, y)\) or \(P_v(y, x)\) for all \(x, y \in A\)). For a relation \(R\) on \(A\), say \(R\) strictly ranks \(a\) above \(b\) if \(R(a, b)\) holds and \(R(b, a)\) does not. Then there is no map \(F\), sending each profile \(P\) to a relation \(F(P)\) on \(A\), with all of the following properties. (Unrestricted domain) \(F(P)\) is a total preorder for every admissible \(P\). (Pareto) For every admissible \(P\) and all \(a, b \in A\), if \(P_v\) strictly ranks \(a\) above \(b\) for every \(v \in E\), then \(F(P)\) strictly ranks \(a\) above \(b\). (Independence of irrelevant alternatives) For all admissible \(P, Q\) and \(a, b \in A\), if \(P_v(a, b) \iff Q_v(a, b)\) and \(P_v(b, a) \iff Q_v(b, a)\) for every \(v \in E\), then \(F(P)(a, b) \iff F(Q)(a, b)\) and \(F(P)(b, a) \iff F(Q)(b, a)\). (Non-dictatorship) For every \(d \in E\) there are an admissible \(P\) and \(a, b \in A\) such that \(P_d\) strictly ranks \(a\) above \(b\) but \(F(P)\) does not.

MetaMathlibExt.arrowImpossibility · 20 lines 
theorem arrowImpossibility : ∀ {Alt Voter : Type}
    (electorate : Finset Voter)
    (F : (Voter → Alt → Alt → Prop) → (Alt → Alt → Prop))
    (hexists : ∃ a b c : Alt, a ≠ b ∧ a ≠ c ∧ b ≠ c)
    (hNonempty : ∃ d, d ∈ electorate)
    (hUniv : ∀ P : Voter → Alt → Alt → Prop,
      (∀ v ∈ electorate, IsPreorder Alt (P v) ∧ ∀ x y : Alt, P v x y ∨ P v y x) →
      IsPreorder Alt (F P) ∧ ∀ x y : Alt, F P x y ∨ F P y x)
    (hPareto : ∀ (P : Voter → Alt → Alt → Prop) (a b : Alt),
      (∀ v ∈ electorate, IsPreorder Alt (P v) ∧ ∀ x y : Alt, P v x y ∨ P v y x) →
      (∀ v ∈ electorate, P v a b ∧ ¬ P v b a) → F P a b ∧ ¬ F P b a)
    (hIIA : ∀ (P Q : Voter → Alt → Alt → Prop) (a b : Alt),
      (∀ v ∈ electorate, IsPreorder Alt (P v) ∧ ∀ x y : Alt, P v x y ∨ P v y x) →
      (∀ v ∈ electorate, IsPreorder Alt (Q v) ∧ ∀ x y : Alt, Q v x y ∨ Q v y x) →
      (∀ v ∈ electorate, (P v a b ↔ Q v a b) ∧ (P v b a ↔ Q v b a)) →
      (F P a b ↔ F Q a b) ∧ (F P b a ↔ F Q b a))
    (hNoDict : ∀ d ∈ electorate, ∃ (P : Voter → Alt → Alt → Prop) (a b : Alt),
      (∀ v ∈ electorate, IsPreorder Alt (P v) ∧ ∀ x y : Alt, P v x y ∨ P v y x) ∧
      (P d a b ∧ ¬ P d b a) ∧ ¬ (F P a b ∧ ¬ F P b a)),
    False
Sources
  • https://en.wikipedia.org/wiki/Arrow%27s_impossibility_theorem.
15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.