Preorder'

A total preorder over candidates α, representing an individual's preference ranking.

structure Preorder' (α : Type) : Type

A total preorder: reflexive, transitive, and total.

• le : α → α → Prop
• refl (a : α) : a ≽[self] a
• trans (a b c : α) : (b ≽[self] a) → (c ≽[self] b) → c ≽[self] a
• total (a b : α) : (b ≽[self] a) ∨ a ≽[self] b

def Preorder'.lt {α : Type} (p : Preorder' α) (a b : α) : Prop

Strict preference: a is strictly preferred to b iff a ≤ b but not b ≤ a.

Equations

• (b ≻[p] a) = ((b ≽[p] a) ∧ ¬a ≽[p] b)

def «term_≻[_]_» : Lean.TrailingParserDescr

Equations

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

def «term_≽[_]_» : Lean.TrailingParserDescr

Equations

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

def «term_≻[_]_≻_» : Lean.TrailingParserDescr

Equations

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

def «term_≽[_]_≻_» : Lean.TrailingParserDescr

Equations

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

theorem Preorder'.lt_asymm {α : Type} {p : Preorder' α} {a b : α} : (b ≻[p] a) → ¬a ≻[p] b

theorem Preorder'.not_lt {α : Type} {p : Preorder' α} {a b : α} : (¬b ≻[p] a) ↔ a ≽[p] b

theorem Preorder'.lt_trans {α : Type} {p : Preorder' α} {a b c : α} (h1 : b ≻[p] a) (h2 : c ≻[p] b) : c ≻[p] a

theorem Preorder'.lt_of_lt_of_le {α : Type} {p : Preorder' α} {a b c : α} (hab : b ≻[p] a) (hbc : c ≽[p] b) : c ≻[p] a

inductive Cmp {α : Type} (p : Preorder' α) (a b : α) : Type

The three possible outcomes when comparing two elements under a total preorder.

• Indiff {α : Type} {p : Preorder' α} {a b : α} (h₁ : b ≽[p] a) (h₂ : a ≽[p] b) : Cmp p a b
• LT {α : Type} {p : Preorder' α} {a b : α} (h : b ≽[p] a) (hn : ¬a ≽[p] b) : Cmp p a b
• GT {α : Type} {p : Preorder' α} {a b : α} (hn : ¬b ≽[p] a) (h : a ≽[p] b) : Cmp p a b

noncomputable def Preorder'.cmp {α : Type} (p : Preorder' α) (a b : α) : Cmp p a b

Equations

• p.cmp a b = if hab : b ≽[p] a then if hba : a ≽[p] b then Cmp.Indiff hab hba else Cmp.LT hab hba else Cmp.GT hab ⋯

Social Welfare Function

Core definitions for Arrow's theorem: profiles, SWFs, and the three key properties.

def Profile (α : Type) (N : ℕ) : Type

A preference profile assigns each voter i ∈ Fin N their preference ordering.

Equations

• Profile α N = (Fin N → Preorder' α)

def SWF (α : Type) (N : ℕ) : Type

A Social Welfare Function aggregates individual preferences into a social ordering.

Equations

• SWF α N = (Profile α N → Preorder' α)

def Dictates {α : Type} {N : ℕ} (R : SWF α N) (k : Fin N) (a b : α) : Prop

Voter k is a dictator for the pair (a, b) if whenever k prefers a over b, society also prefers a over b.

Equations

• Dictates R k a b = ∀ (p : Profile α N), (a ≻[p k] b) → a ≻[R p] b

def AgreeOn {α : Type} {N : ℕ} (p q : Profile α N) (a b : α) : Prop

Two profiles agree on (a, b) if every voter ranks a vs b the same way in both.

Equations

• AgreeOn p q a b = ∀ (i : Fin N), ((a ≽[p i] b) ↔ a ≽[q i] b) ∧ ((b ≽[p i] a) ↔ b ≽[q i] a)

def Unanimity {α : Type} {N : ℕ} (R : SWF α N) : Prop

Unanimity (Pareto): If all voters prefer a over b, so does society.

Equations

• Unanimity R = ∀ (p : Profile α N) (a b : α), (∀ (i : Fin N), a ≻[p i] b) → a ≻[R p] b

def AIIA {α : Type} {N : ℕ} (R : SWF α N) : Prop

Independence of Irrelevant Alternatives: The social ranking of a vs b depends only on individual rankings of a vs b.

Equations

• AIIA R = ∀ (p q : Profile α N) (a b : α), AgreeOn p q a b → ((a ≽[R p] b) ↔ a ≽[R q] b) ∧ ((b ≽[R p] a) ↔ b ≽[R q] a)

def NonDictatorship {α : Type} {N : ℕ} (R : SWF α N) : Prop

Non-Dictatorship: No single voter dictates the outcome for all pairs.

Equations

• NonDictatorship R = ¬∃ (i : Fin N), ∀ (a b : α), a ≠ b → Dictates R i a b

Preference Construction

We construct concrete preference orderings to build test profiles for the proof. Given three alternatives, prefer a₀ a₁ a₂ tie ranks them with optional ties.

inductive Tie : Type

Where ties occur in a 3-element preference ranking

• Not : Tie
• Top : Tie
• Bot : Tie

def prefer_ifs {α : Type} (x y a₀ _a₁ a₂ : α) (tie : Tie) : Prop

Equations

• prefer_ifs x y a₀ _a₁ a₂ Tie.Not = if x = a₂ then True else if y = a₀ then True else if x = a₀ then y = a₀ else if y = a₂ then x = a₂ else True
• prefer_ifs x y a₀ _a₁ a₂ Tie.Top = if y = a₂ then x = a₂ else if x = a₂ then True else True
• prefer_ifs x y a₀ _a₁ a₂ Tie.Bot = if x = a₀ then y = a₀ else if y = a₀ then True else True

def prefer {α : Type} (a₀ _a₁ a₂ : α) (tie : Tie) (h02 : a₀ ≠ a₂) : Preorder' α

Construct a preference ordering with optional ties:

• Tie.Not: a₀ > a₁ > a₂ (strict ranking)
• Tie.Top: a₀ ~ a₁ > a₂ (top two tied)
• Tie.Bot: a₀ > a₁ ~ a₂ (bottom two tied)

Equations

• prefer a₀ _a₁ a₂ tie h02 = { le := fun (x y : α) => prefer_ifs x y a₀ _a₁ a₂ tie, refl := ⋯, trans := ⋯, total := ⋯ }

Pivotal Voter

The key construction: we find the "pivotal voter" who flips society's preference. Starting from a profile where everyone prefers b ≻ a, we flip voters one by one to prefer a ≻ b. By unanimity, society eventually flips too. The first voter whose flip changes society's preference is the pivotal voter.

def canonicalSwap {α : Type} {N : ℕ} (a b : α) (hab : a ≠ b) : Fin (N + 1) → Profile α N

A family of profiles indexed by k ∈ Fin (N+1): voters 0..k-1 prefer b ≻ a, voters k..N-1 prefer a ≻ b.

Equations

• canonicalSwap a b hab k i = if ↑i < ↑k then prefer b b a Tie.Not ⋯ else prefer a b b Tie.Not hab

def flipping {α : Type} {N : ℕ} (R : SWF α N) (a b : α) (hab : a ≠ b) (k : Fin N) : Prop

flipping R a b hab k holds iff society prefers b ≻ a when voters 0..k prefer b ≻ a.

Equations

• flipping R a b hab k = ¬a ≻[R (canonicalSwap a b hab k.succ)] b

theorem flip_exists {α : Type} {N : ℕ} [NeZero N] (R : SWF α N) (a b : α) (hab : a ≠ b) (hu : Unanimity R) : ∃ (k : Fin N), flipping R a b hab k

By unanimity, a flip must occur: when all voters prefer b ≻ a, so does society.

noncomputable def pivoter {α : Type} {N : ℕ} [NeZero N] {R : SWF α N} (a b : α) (hab : a ≠ b) (hu : Unanimity R) : Fin N

The pivotal voter for (a, b): the minimum k where society flips from a ≻ b to b ≻ a.

Equations

• pivoter a b hab hu = Fin.find (flipping R a b hab) ⋯

theorem no_flip {α : Type} {N : ℕ} [NeZero N] {R : SWF α N} (a b : α) {hab : a ≠ b} (i : Fin N) {hu : Unanimity R} : i < pivoter a b hab hu → a ≻[R (canonicalSwap a b hab i.succ)] b

Before the pivotal voter, society still prefers a ≻ b.

theorem flipped {α : Type} {N : ℕ} [NeZero N] {R : SWF α N} (a b : α) {hab : a ≠ b} {hu : Unanimity R} : b ≽[R (canonicalSwap a b hab (pivoter a b hab hu).succ)] a

At the pivotal voter, society flips to b ≻ a.

theorem nab_dictate_bc {α : Type} {N : ℕ} [NeZero N] {R : SWF α N} (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hu : Unanimity R) (hAIIA : AIIA R) : Dictates R (pivoter a b hab hu) b c

The pivotal voter for (a, b) dictates the pair (b, c).

theorem nab_le_nbc {α : Type} {N : ℕ} [NeZero N] {R : SWF α N} (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hu : Unanimity R) (hAIIA : AIIA R) : pivoter a b hab hu ≤ pivoter b c hbc hu

The pivotal voter for (a, b) comes no later than the one for (b, c).

theorem ncb_le_nab {α : Type} {N : ℕ} [NeZero N] {R : SWF α N} (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hu : Unanimity R) (hAIIA : AIIA R) : pivoter c b ⋯ hu ≤ pivoter a b hab hu

The pivotal voter for (c, b) comes no later than the one for (a, b).

theorem ncb_le_nbc {α : Type} {N : ℕ} [NeZero N] {R : SWF α N} (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hu : Unanimity R) (hAIIA : AIIA R) : pivoter c b ⋯ hu ≤ pivoter b c hbc hu

Combining the above: pivoter (c, b) ≤ pivoter (b, c).

theorem nab_eq_nbc_ncb {α : Type} {N : ℕ} [NeZero N] {R : SWF α N} (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hu : Unanimity R) (hAIIA : AIIA R) : pivoter b c hbc hu = pivoter c b ⋯ hu ∧ pivoter c b ⋯ hu = pivoter a b hab hu

All pivotal voters for pairs in {a, b, c} are the same: pivoter (b, c) = pivoter (c, b) = pivoter (a, b).

theorem nab_dictate_xy {α : Type} {N : ℕ} [NeZero N] {R : SWF α N} (a b c x y : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hxy : x ≠ y) (hu : Unanimity R) (hAIIA : AIIA R) : Dictates R (pivoter a b hab hu) x y

The pivotal voter for any pair (a, b) dictates every pair (x, y).

theorem Impossibility {α : Type} {N : ℕ} [NeZero N] [Fintype α] (ha : Fintype.card α ≥ 3) : ¬∃ (R : SWF α N), Unanimity R ∧ AIIA R ∧ NonDictatorship R

Arrow's Impossibility Theorem: No SWF with ≥3 alternatives and ≥1 voters can satisfy Unanimity, IIA, and Non-Dictatorship simultaneously.