Arrow's Impossibility Theorem via Kalai's Fourier Analysis

This file proves Arrow's Impossibility Theorem using Kalai's Fourier-analytic approach (Gil Kalai, "A Fourier-Theoretic Perspective on the Condorcet Paradox and Arrow's Theorem", 2002).

Setup

For 3 alternatives {a, b, c} and n voters, a social welfare function is given by an odd Boolean function f : BoolCube n → ℝ applied to each pairwise comparison of alternatives. The function being "odd" models the antisymmetry of pairwise preference: if society prefers a to b, it must not also prefer b to a.

Main result

arrow_theorem: Any odd, ±1-valued, unanimous, acyclic social welfare function must be a dictator.

Proof sketch (Kalai)

1. For voters with i.i.d. uniform orderings of {a,b,c}, the Condorcet cycle probability is Pr[cycle] = (1 + 3·∑_S f̂(S)²·(-1/3)^|S|) / 4.
2. For odd f, only odd Fourier levels contribute.
3. Since (-1/3)^k ≥ -1/3 for all odd k, we have Pr[cycle] ≥ 0.
4. Pr[cycle] = 0 forces all Fourier weight onto level 1.
5. A ±1-valued degree-1 function satisfying unanimity must be a dictator.

References

• Gil Kalai, A Fourier-Theoretic Perspective on the Condorcet Paradox and Arrow's Theorem, Advances in Applied Mathematics, 2002.
• Ryan O'Donnell, Analysis of Boolean Functions, Chapter 2.

Social choice definitions

def ArrowTheorem.unanimity {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) : Prop

Unanimity: if all voters prefer a to b, society prefers a to b. In our encoding, f(all-false) = 1 means "a preferred to b" when every voter marks false (i.e., prefers the first alternative).

Equations

• ArrowTheorem.unanimity f = ((f fun (x : Fin n) => false) = 1)

def ArrowTheorem.isDictator {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) : Prop

f is a dictatorship: there exists some voter i whose preference always determines society's preference.

Equations

• ArrowTheorem.isDictator f = ∃ (i : Fin n), f = BooleanAnalysis.dictator i

The voter ordering model

We model each voter as choosing one of the 6 transitive strict orderings of {a, b, c}, indexed by Fin 6. For each ordering we record the voter's preference in three pairwise comparisons:

• abPref: comparison of a vs. b (false = prefer a, true = prefer b)
• bcPref: comparison of b vs. c (false = prefer b, true = prefer c)
• caPref: comparison of c vs. a (false = prefer c, true = prefer a)

The sign convention: boolToSign false = 1 ("pro first") and boolToSign true = -1 ("pro second").

The six orderings and their signs (s_ab, s_bc, s_ca): | Index | Ordering | s_ab | s_bc | s_ca | |-------|----------|------|------|------| | 0 | a>b>c | 1 | 1 | -1 | | 1 | a>c>b | 1 | -1 | -1 | | 2 | b>a>c | -1 | 1 | -1 | | 3 | b>c>a | -1 | 1 | 1 | | 4 | c>a>b | 1 | -1 | 1 | | 5 | c>b>a | -1 | -1 | 1 |

def ArrowTheorem.abPref : Fin 6 → Bool

Preference of ordering k in the a-vs-b comparison (false = prefer a).

Equations

• ArrowTheorem.abPref ⟨0, isLt⟩ = false
• ArrowTheorem.abPref ⟨1, isLt⟩ = false
• ArrowTheorem.abPref ⟨2, isLt⟩ = true
• ArrowTheorem.abPref ⟨3, isLt⟩ = true
• ArrowTheorem.abPref ⟨4, isLt⟩ = false
• ArrowTheorem.abPref ⟨5, isLt⟩ = true

def ArrowTheorem.bcPref : Fin 6 → Bool

Preference of ordering k in the b-vs-c comparison (false = prefer b).

Equations

• ArrowTheorem.bcPref ⟨0, isLt⟩ = false
• ArrowTheorem.bcPref ⟨1, isLt⟩ = true
• ArrowTheorem.bcPref ⟨2, isLt⟩ = false
• ArrowTheorem.bcPref ⟨3, isLt⟩ = false
• ArrowTheorem.bcPref ⟨4, isLt⟩ = true
• ArrowTheorem.bcPref ⟨5, isLt⟩ = true

def ArrowTheorem.caPref : Fin 6 → Bool

Preference of ordering k in the c-vs-a comparison (false = prefer c).

Equations

• ArrowTheorem.caPref ⟨0, isLt⟩ = true
• ArrowTheorem.caPref ⟨1, isLt⟩ = true
• ArrowTheorem.caPref ⟨2, isLt⟩ = true
• ArrowTheorem.caPref ⟨3, isLt⟩ = false
• ArrowTheorem.caPref ⟨4, isLt⟩ = false
• ArrowTheorem.caPref ⟨5, isLt⟩ = false

Key correlation lemma

For a single voter uniformly drawn from the 6 orderings, the sum of products of pairwise preference signs has a specific value. This is the core computation behind the Fourier formula for cycle probability.

theorem ArrowTheorem.sum_abPref_bcPref : ∑ k : Fin 6, BooleanAnalysis.boolToSign (abPref k) * BooleanAnalysis.boolToSign (bcPref k) = -2

The sum of s_ab · s_bc over all 6 orderings equals -2. (Expectation E[s_ab · s_bc] = -1/3.)

theorem ArrowTheorem.sum_bcPref_caPref : ∑ k : Fin 6, BooleanAnalysis.boolToSign (bcPref k) * BooleanAnalysis.boolToSign (caPref k) = -2

Similarly, E[s_bc · s_ca] = -1/3.

theorem ArrowTheorem.sum_abPref_caPref : ∑ k : Fin 6, BooleanAnalysis.boolToSign (abPref k) * BooleanAnalysis.boolToSign (caPref k) = -2

Similarly, E[s_ab · s_ca] = -1/3.

Acyclicity and profiles

@[reducible, inline]

abbrev ArrowTheorem.Profile (n : ℕ) : Type

A profile assigns each of the n voters one of the 6 orderings.

Equations

• ArrowTheorem.Profile n = (Fin n → Fin 6)

def ArrowTheorem.abVotes {n : ℕ} (p : Profile n) : BooleanAnalysis.BoolCube n

Given a profile, the a-vs-b preference vector of all n voters.

Equations

• ArrowTheorem.abVotes p i = ArrowTheorem.abPref (p i)

def ArrowTheorem.bcVotes {n : ℕ} (p : Profile n) : BooleanAnalysis.BoolCube n

Given a profile, the b-vs-c preference vector.

Equations

• ArrowTheorem.bcVotes p i = ArrowTheorem.bcPref (p i)

def ArrowTheorem.caVotes {n : ℕ} (p : Profile n) : BooleanAnalysis.BoolCube n

Given a profile, the c-vs-a preference vector.

Equations

• ArrowTheorem.caVotes p i = ArrowTheorem.caPref (p i)

def ArrowTheorem.acyclic {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) : Prop

A social welfare function f is acyclic if no profile of transitive voter orderings produces a Condorcet cycle in society's preferences.

A Condorcet cycle occurs when f(ab) = f(bc) = f(ca) = 1 (society prefers a to b, b to c, and c to a — a cycle a>b>c>a) or f(ab) = f(bc) = f(ca) = -1 (the reverse cycle).

Equations

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

The Fourier formula for cycle probability

The heart of Kalai's proof: for n voters with i.i.d. uniform orderings, the expected product f(ab)·f(bc)·f(ca) factors through a correlation of -1/3 per voter per pair of comparisons.

We compute: E_p[f(ab_p) · f(bc_p)] = ∑_S f̂(S)² · (-1/3)^|S|

This is because:

• Voters are independent, so the expectation factors as a product over voters.
• Per voter, E[s_ab · s_bc] = -1/3.
• The only terms surviving in the Fourier expansion are those where both S components at each voter i are present or both absent (otherwise the marginal E[s_ab] = 0 kills the term).

noncomputable def ArrowTheorem.corrFunc {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) : ℝ

The pairwise correlation function: ∑_S f̂(S)² · (-1/3)^|S|. For odd f, only odd-level terms are nonzero.

Equations

• ArrowTheorem.corrFunc f = ∑ S : Finset (Fin n), BooleanAnalysis.fourierCoeff f S ^ 2 * (-1 / 3) ^ S.card

theorem ArrowTheorem.corrFunc_ge_neg_third {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) (hodd : BooleanAnalysis.isOddFunc f) (hpm : BooleanAnalysis.isPmOne f) : corrFunc f ≥ -1 / 3

For any odd ±1-valued function, the correlation function is ≥ -1/3.

Proof: (-1/3)^k ≥ -1/3 for all odd k (since |(-1/3)^k| = (1/3)^k ≤ 1/3 for k ≥ 1). The even-level coefficients vanish by oddness. Hence ∑_S f̂(S)²·(-1/3)^|S| ≥ ∑_S f̂(S)²·(-1/3) = (-1/3)·∑_S f̂(S)² = -1/3.

theorem ArrowTheorem.corrFunc_eq_neg_third_of_weight_one {n : ℕ} {f : BooleanAnalysis.BooleanFunc n} (hodd : BooleanAnalysis.isOddFunc f) (hpm : BooleanAnalysis.isPmOne f) (hcorr : corrFunc f = -1 / 3) (S : Finset (Fin n)) : S.card ≠ 1 → BooleanAnalysis.fourierCoeff f S = 0

If the correlation function equals -1/3, then f̂(S) = 0 for all S with |S| ≥ 3 (i.e., all Fourier weight is on levels 0 and 1).

Since f is odd, f̂(∅) = f̂(S for even |S|) = 0. So in fact all Fourier weight is on level 1.

The main Fourier cycle formula (key lemma from Kalai)

For voters with i.i.d. uniform orderings, the expected product E[f(ab) · f(bc)] factors as a sum of Fourier coefficients weighted by (-1/3)^|S|. The acyclicity assumption forces this to equal -1/3, which by the lower bound forces W_1 = 1.

theorem ArrowTheorem.expected_product_eq_corrFunc {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) : (1 / 6) ^ n * ∑ p : Profile n, f (abVotes p) * f (bcVotes p) = corrFunc f

The expected value of f(ab-votes) · f(bc-votes) over all uniform profiles equals the correlation function ∑_S f̂(S)² · (-1/3)^|S|.

Proof sketch: Since voters are independent, E[f(x^ab) · f(x^bc)] = ∑_{S,T} f̂(S) f̂(T) ∏_i E[s^ab_i^{1[i∈S]} · s^bc_i^{1[i∈T]}] The per-voter factor is nonzero only when the voter is in both S and T or neither (single indicators give E[s_ab] = 0). This forces S = T, and the per-voter factor for i ∈ S is E[s_ab · s_bc] = -1/3. Hence E[f(ab)·f(bc)] = ∑_S f̂(S)² · (-1/3)^|S|.

Acyclicity implies degree-1 Fourier structure

theorem ArrowTheorem.acyclic_implies_corrFunc {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) (hodd : BooleanAnalysis.isOddFunc f) (hpm : BooleanAnalysis.isPmOne f) (hacyc : acyclic f) : corrFunc f = -1 / 3

Acyclicity of f implies that the Fourier correlation function equals -1/3.

Key steps:

1. Acyclicity means no profile gives a cycle, so the cycle probability = 0.
2. Cycle probability = (1 + 3·corrFunc f) / 4 = 0 implies corrFunc f = -1/3.

Degree-1 implies dictator

theorem ArrowTheorem.degree_one_implies_dictator {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) (hodd : BooleanAnalysis.isOddFunc f) (hpm : BooleanAnalysis.isPmOne f) (huniv : unanimity f) (hdeg1 : ∀ (S : Finset (Fin n)), S.card ≠ 1 → BooleanAnalysis.fourierCoeff f S = 0) : isDictator f

A ±1-valued odd unanimous function with all Fourier weight on level 1 is a dictator.

Proof: f = ∑i a_i · χ{i} with ∑_i a_i² = 1 (Parseval).

• Unanimity: f(false,...,false) = ∑_i a_i = 1.
• For each j: f(only-j-true) = 1 - 2·a_j ∈ {-1,1}, so a_j ∈ {0,1}.
• From a_j ∈ {0,1} and ∑ a_j² = ∑ a_j = 1: exactly one a_{j₀} = 1.
• Hence f = χ_{{j₀}} = dictator j₀.

Arrow's Impossibility Theorem

theorem ArrowTheorem.arrow_theorem {n : ℕ} (f : BooleanAnalysis.BooleanFunc n) (hodd : BooleanAnalysis.isOddFunc f) (hpm : BooleanAnalysis.isPmOne f) (huniv : unanimity f) (hacyc : acyclic f) : isDictator f

Arrow's Impossibility Theorem (via Kalai's Fourier proof):

Any social welfare function f that is:

• odd (antisymmetric: f(¬x) = -f(x))
• ±1-valued (gives definite preferences)
• unanimous (unanimously preferred alternatives are socially preferred)
• acyclic (no Condorcet cycles arise)

must be a dictatorship (there is one voter whose preference always wins).

The proof uses Fourier analysis on Boolean functions:

1. Acyclicity forces the Fourier cycle probability to be 0.
2. This forces all Fourier weight onto level 1 (degree-1 functions).
3. A degree-1 ±1-valued unanimous function must be a dictator.