Arrow's theorem

With three or more alternatives, a rule on profiles of values that is ordinally invariant, outputs weak orderings, respects weak Pareto and is independent of irrelevant alternatives has a dictator, an individual whose strict rankings are the strict overall rankings. Ordinal invariance makes the values carry no more than each individual's ranking, which recovers Arrow's setting. The proof is by field expansion and group contraction: the whole population is decisive, an almost decisive group is decisive for every pair, and a decisive group with two or more members has a decisive proper subgroup.

Main statements

• SocialChoice.exists_isDictator: a rule meeting Arrow's conditions has a dictator.
• SocialChoice.arrow: no rule meets all of Arrow's conditions.

References

• [Arr50]
• [Sen70]

Arrow's theorem

def SocialChoice.Decisive {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] (a : Rule ι α K) (G : Finset ι) : Prop

A group G is decisive when the rule ranks x strictly above y whenever every individual in G does.

Equations

• SocialChoice.Decisive a G = ∀ (v : SocialChoice.Profile ι α K) (x y : α), (∀ i ∈ G, v y i < v x i) → AsymmRel (a v) x y

def SocialChoice.DecisiveOn {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] (a : Rule ι α K) (G : Finset ι) (x y : α) : Prop

A group G is decisive for the pair x, y when the rule ranks x strictly above y whenever every individual in G does.

Equations

• SocialChoice.DecisiveOn a G x y = ∀ (v : SocialChoice.Profile ι α K), (∀ i ∈ G, v y i < v x i) → AsymmRel (a v) x y

def SocialChoice.AlmostDecisiveOn {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] (a : Rule ι α K) (G : Finset ι) (x y : α) : Prop

A group G is almost decisive for the pair x, y when it prevails if every individual outside G ranks y strictly above x.

Equations

• SocialChoice.AlmostDecisiveOn a G x y = ∀ (v : SocialChoice.Profile ι α K), (∀ i ∈ G, v y i < v x i) → (∀ i ∉ G, v x i < v y i) → AsymmRel (a v) x y

theorem SocialChoice.DecisiveOn.almost {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} {G : Finset ι} {x y : α} (h : DecisiveOn a G x y) : AlmostDecisiveOn a G x y

theorem SocialChoice.decisive_of_decisiveOn {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} {G : Finset ι} (hne : G.Nonempty) (h : ∀ (x y : α), x ≠ y → DecisiveOn a G x y) : Decisive a G

theorem SocialChoice.iff_of_pattern {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] (hO : Invariant ordinal a) (hI : Independent a) {v w : Profile ι α K} {x y : α} (h : ∀ (i : ι), (v x i < v y i ↔ w x i < w y i) ∧ (v y i < v x i ↔ w y i < w x i)) : a v x y ↔ a w x y

Under ordinal invariance and independence, the verdict on a pair depends only on how each individual orders the pair.

theorem SocialChoice.decisiveOn_of_almost {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] (hW : WeakOrderValued a) (hP : WeakPareto a) (hI : Independent a) {G : Finset ι} {x y : α} (hxy : x ≠ y) (h : AlmostDecisiveOn a G x y) {z : α} (hzy : z ≠ y) : DecisiveOn a G x z

In the first half of field expansion, a group almost decisive for x, y is decisive for x, z.

theorem SocialChoice.decisiveOn_of_almost' {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] (hW : WeakOrderValued a) (hP : WeakPareto a) (hI : Independent a) {G : Finset ι} {x y : α} (hxy : x ≠ y) (h : AlmostDecisiveOn a G x y) {z : α} (hzx : z ≠ x) : DecisiveOn a G z y

In the second half of field expansion, a group almost decisive for x, y is decisive for z, y.

theorem SocialChoice.decisiveOn_of_almost_of_ne {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] [Fintype α] (hW : WeakOrderValued a) (hP : WeakPareto a) (hI : Independent a) (h₃ : 3 ≤ Fintype.card α) {G : Finset ι} {x y : α} (hxy : x ≠ y) (h : AlmostDecisiveOn a G x y) {u w : α} (huw : u ≠ w) : DecisiveOn a G u w

By field expansion, with three or more alternatives a group almost decisive for one pair is decisive for every pair.

theorem SocialChoice.exists_decisive_ssubset {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] [Fintype α] (hO : Invariant ordinal a) (hW : WeakOrderValued a) (hP : WeakPareto a) (hI : Independent a) (h₃ : 3 ≤ Fintype.card α) {G : Finset ι} (hG : Decisive a G) (h₂ : 2 ≤ G.card) : ∃ G' ⊂ G, Decisive a G'

By group contraction, a decisive group with two or more individuals has a decisive proper subgroup.

theorem SocialChoice.exists_isDictator {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] [Fintype α] [Fintype ι] (hO : Invariant ordinal a) (hW : WeakOrderValued a) (hP : WeakPareto a) (hI : Independent a) (h₃ : 3 ≤ Fintype.card α) : ∃ (i : ι), IsDictator a i

Arrow's theorem says that with three or more alternatives a rule that is ordinally invariant, outputs weak orderings, respects weak Pareto and is independent has a dictator.

theorem SocialChoice.arrow {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] [Field K] [IsStrictOrderedRing K] [Fintype α] [Fintype ι] (h₃ : 3 ≤ Fintype.card α) (a : Rule ι α K) : ¬(Invariant ordinal a ∧ WeakOrderValued a ∧ WeakPareto a ∧ Independent a ∧ NonDictatorial a)

Arrow's theorem is an impossibility, since no rule meets all of Arrow's conditions.