EconCSLib.SocialChoice.Voting.Arrow #

Arrow's Impossibility Theorem: there is no social welfare function satisfying unanimity, IIA, and non-dictatorship when |A| ≥ 3.

Main results #

arrow_impossibility — Arrow's theorem [MSZ 21.10]

This file is the public theorem entrypoint over the shared SWF / bundled-preference API. Its implementation delegates to the internal complete proof module.

Implementation note #

The public theorem below delegates to the complete decisive-coalitions proof over the shared social-choice API.

References #

[MSZ] Chapter 21, Theorem 21.10
Arrow, K.J. (1951). Social Choice and Individual Values.

source

theorem SocialChoice.Voting.arrow_impossibility {N : Type u_1} {A : Type u_2} [Fintype A] [Fintype N] [Nonempty N] (hA : Fintype.card A ≥ 3) (F : SWF N A) (hU : F.Unanimity) (hIIA : F.IIA) :

F.Dictatorial

Arrow's Impossibility Theorem [MSZ 21.10]:

If there are at least 3 alternatives, every social welfare function satisfying unanimity and IIA is dictatorial. The implementation uses the decisive-coalitions proof over the shared bundled-preference interface.