Table of Contents

1. 1. Preferences
2. 2. Social Welfare Functions
3. 3. Proof Overview
4. 4. Constructing Concrete Preferences
5. 5. The Canonical Swap
6. 6. The Pivotal Voter
7. 7. From Pivotal Voter to Dictator
8. 8. Arrow's Impossibility Theorem
9. Index

1. Preferences🔗

In any social choice setting, each person holds a ranking of the available alternatives. We model this as a total preorder: a binary relation that is reflexive (everyone is at least as good as themselves), transitive (rankings chain consistently), and total (any two alternatives are always comparable in at least one direction).

Note that le a b and le b a can both hold simultaneously — this captures indifference between a and b. Strict preference, where one option is unambiguously ranked above the other, is defined separately:

So p.lt a b holds when a is weakly below b but b is not weakly below a.

The proof uses two notation shorthands throughout:

Notice the reversal: a ≻[p] b expands to Preorder'.lt p b a. Since lt x y means "x is below y", to say "a is above b" we write lt b a. The notation hides this reversal so the mathematical reading stays natural: a ≻[p] b means "under preference p, alternative a is strictly preferred to b."

Several useful properties of lt are proved as lemmas: asymmetry (lt_asymm), transitivity (lt_trans), and a mixed version (lt_of_lt_of_le) that upgrades a strict preference followed by a weak preference into a strict one.

2. Social Welfare Functions🔗

With N voters each holding a preference ordering over alternatives α, a preference profile records everyone's ranking simultaneously:

A Social Welfare Function (SWF) is a procedure that takes a preference profile and produces a single social preference ordering — a way of aggregating individual opinions into a collective verdict:

3. Proof Overview🔗

Arrow's theorem says these three conditions are mutually incompatible when there are at least three alternatives and at least one voter. The proof proceeds by contradiction: assume all three conditions hold, then construct an explicit dictator — violating Non-Dictatorship.

The central idea is the pivotal voter. Fix two distinct alternatives a and b, and imagine flipping voters one by one from preferring a ≻ b to preferring b ≻ a.

         k=0          k=1          k=2          k=N
  a≻b  [0,1,...,N-1]  [1,...,N-1]  [2,...,N-1]   ∅
  b≻a  ∅              {0}          {0,1}          [0,...,N-1]

When k = 0, everyone prefers a ≻ b, so by Unanimity, society prefers a ≻ b. When k = N, everyone prefers b ≻ a, so by Unanimity, society prefers b ≻ a. Somewhere along the way, the social preference must flip. The pivotal voter is the first voter whose switch causes this flip.

The clever part: using IIA, one can show that this pivotal voter must dictate every pair of alternatives — not just (a, b). This contradicts Non-Dictatorship.

4. Constructing Concrete Preferences🔗

The proof needs to reason about specific profiles with known rankings. To do this, it uses a helper function prefer that builds a Preorder' from an explicit ordering of three alternatives.

First, a type for the three tie patterns:

Then prefer produces a Preorder' where a₀ is the top-ranked alternative and a₂ is the bottom-ranked one, with tie controlling indifference:

The proof only requires a₀ ≠ a₂ (the top and bottom are distinct); the middle element can even be a duplicate of a₀ or a₂, which the proof exploits — for example, prefer b b a .Not h effectively creates a ranking where b ≻ a with b duplicated.

5. The Canonical Swap🔗

The central construction is a parametric family of profiles indexed by k ∈ Fin (N+1). In profile canonicalSwap a b hab k, voters 0, …, k-1 all prefer b ≻ a while voters k, …, N-1 all prefer a ≻ b:

At index k = 0, every voter prefers a ≻ b and society must follow by Unanimity. At index k = N, every voter prefers b ≻ a and society must follow by Unanimity.

flipping records the event that society's preference has switched: when the first k+1 voters have been flipped to prefer b ≻ a, society no longer strictly prefers a ≻ b:

The lemma flip_exists uses Unanimity to show that flipping must occur for some k.

6. The Pivotal Voter🔗

The pivotal voter for the pair (a, b) is defined as the minimum voter index at which flipping first occurs:

Being the minimum, it satisfies two precise boundary conditions.

Before the pivot — for any voter i strictly earlier than the pivotal voter — society still prefers a ≻ b when voters 0, …, i have been flipped:

At the pivot itself, society has (at least weakly) switched to b ≽ a:

Note that flipped gives a weak preference b ≽ a, not a strict one. This is because pivoter is the first k where ¬(a ≻ b), which by not_lt is equivalent to b ≽ a, but doesn't immediately imply b ≻ a.

Together, voter pivoter is precisely the tipping point: include one fewer voter and society still prefers a; include the pivotal voter and society switches to weakly preferring b.

7. From Pivotal Voter to Dictator🔗

8. Arrow's Impossibility Theorem🔗

Assembling all the pieces: if an SWF satisfies Unanimity and IIA, its pivotal voter for any pair dictates every other pair — making them a full dictator and contradicting Non-Dictatorship.

The proof:

1. Assume for contradiction that such an R exists with hu : Unanimity R, hIIA : IIA R, and hNonDictator : NonDictatorship R.

2. Since |α| ≥ 3, extract three distinct alternatives a, b, c using Fintype.two_lt_card_iff.

3. Let n = pivoter a b hab hu.

4. By nab_dictate_xy, voter n dictates every distinct pair (x, y).

5. This gives an explicit dictator, contradicting hNonDictator. ∎

Index🔗