Arrow's theorem

This file proves a version of Arrow's theorem [arrow1950] for 3-candidate elections, see dictator_of_condorcet_and_unanimous. We follow O'Donnell [odonnell2014], Sec. 2.5, which follows Kalai's approach [kalai2002] via Fourier analysis of Boolean valued functions.

Implementation notes

The proof in [odonnell2014] makes key use of notions from probability such as joint probability distributions on the discrete cube. We prefer to avoid this in this formalization, so we unpack most of the probability language in the proof. This is mainly facilitated by introducing an auxiliary linear operator, see _Tnae3.

References

• [K. Arrow, A difficulty in the concept of social welfare][arrow1950]
• [G. Kalai, A Fourier-theoretic perspective on the Condorcet paradox and Arrow's theorem][kalai2002]
• [R. O'Donnell, Analysis of Boolean functions][odonnell2014]

@[reducible, inline]

abbrev LeanPool.LeanBooleanfun.BooleanFun.BV.Votes (n : ℕ) : Type

Encodes votes of n voters in a 2-candidate election.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.BV.Votes n = (Fin n → Fin 2)

def LeanPool.LeanBooleanfun.BooleanFun.BV.majority {n : ℕ} : BooleanFunc n

±1-valued majority function

Equations

• LeanPool.LeanBooleanfun.BooleanFun.BV.majority x = if ∑ j : Fin n, ↑(x j) > n / 2 then 1 else -1

instance LeanPool.LeanBooleanfun.BooleanFun.BV.instBooleanValuedMajority {n : ℕ} : BooleanValued majority

The majority function is Boolean valued.

@[reducible, inline]

abbrev LeanPool.LeanBooleanfun.BooleanFun.BV.dictator {n : ℕ} (i : Fin n) : BooleanFunc n

A dictator is a Walsh character of a singleton set.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.BV.dictator i = LeanPool.LeanBooleanfun.BooleanFun.walshCharacter {i}

@[reducible, inline]

abbrev LeanPool.LeanBooleanfun.BooleanFun.BV.NAE3 {α : Type u_1} (x y z : α) : Prop

Not-all-equal predicate on three values.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.BV.NAE3 x y z = ¬(x = y ∧ y = z)

def LeanPool.LeanBooleanfun.BooleanFun.BV.VoteConsistent {n : ℕ} (x y z : Votes n) : Prop

Voter preferences in an election among 3 candidates A, B, C are represented by three vote ensembles x y z representing votes in the three 2-candidate elections among the candidates: x contains the votes for the election A vs. B, y for B vs. C and z for C vs. A. Three vote ensembles x y z are consistent if they encode a ranking of the three candidates A, B, C for each voter. This is expressed by the not-all-equal predicate. See [odonnell2014], Sec. 2.5.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.BV.VoteConsistent x y z = ∀ (i : Fin n), LeanPool.LeanBooleanfun.BooleanFun.BV.NAE3 (x i) (y i) (z i)

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.VoteConsistent.comm_right {n : ℕ} {x y z : Votes n} : VoteConsistent x y z = VoteConsistent x z y

Commute arguments of VoteConsistent predicate

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.VoteConsistent.comm_rcyc {n : ℕ} {x y z : Votes n} : VoteConsistent x y z = VoteConsistent y z x

Commute arguments of VoteConsistent predicate

def LeanPool.LeanBooleanfun.BooleanFun.BV.IsCondorcet {n : ℕ} (f : BooleanFunc n) : Prop

A voting rule is Condorcet, if in every 3-candidate election conducted using it there is a Condercet winner.

Equations

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

def LeanPool.LeanBooleanfun.BooleanFun.BV.HasDictator {n : ℕ} (f : BooleanFunc n) : Prop

A voting rule admits a dictator if it is equal to dictator i for some i.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.BV.HasDictator f = ∃ (i : Fin n), f = LeanPool.LeanBooleanfun.BooleanFun.BV.dictator i

def LeanPool.LeanBooleanfun.BooleanFun.BV.IsUnanimous {n : ℕ} (f : BooleanFunc n) : Prop

A voting rule is unanimous if it selects candidate i if everyone votes for i.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.BV.IsUnanimous f = (f 0 = 1 ∧ f 1 = -1)

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.zero_not_unanimous {n : ℕ} (f : BooleanFunc n) (hn : n = 0) : ¬IsUnanimous f

The (unique) voting rule for zero voters is not unanimous.

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.oneOn_NAE3_eq {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] {x y z : Fin n → Fin 2} : oneOn (NAE3 (f x) (f y) (f z)) = 3 / 4 - 1 / 4 * f x * f y - 1 / 4 * f y * f z - 1 / 4 * f x * f z

Explicit Walsh-Fourier expansion of the not-all-equal predicate on a 3-tuple composed with a Boolean valued function. A crucial step in the proof of Arrow's theorem.

noncomputable def LeanPool.LeanBooleanfun.BooleanFun.BV.probabilityCondorcetWinner {n : ℕ} (f : BooleanFunc n) : ℝ

The probability of a Condorcet winner equals the proportion out of the 6ⁿ possible voter preferences (x, y, z) so that (f(x), f(y), f(z)) is a consistent preference tuple. The impartial culture assumption is encoded by giving each tuple (x, y, z) the same weight.

Equations

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

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.probabilityCondorcetWinner_eq_one {n : ℕ} {f : BooleanFunc n} (hc : IsCondorcet f) : probabilityCondorcetWinner f = 1

If a voting rule is Condorcet, then the probability of a Condorcet winner equals 1.

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.probabilityCondorcetWinner_eq {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] : probabilityCondorcetWinner f = 3 / 4 * (1 - noiseStability (-1 / 3) f)

The probability of having a Condorcet winner can be expressed in terms of the noise operator. See [odonnell2014], Theorem 2.56.

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.dictator_of_condorcet_and_unanimous {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] (h : IsUnanimous f) : IsCondorcet f → HasDictator f

Arrow's theorem as formulated in [odonnell2014], Sec. 2.5 : Every unanimous voting rule that always admits a Condorcet winner is a dictatorship.