Social Choice Theory in HOL
This article presents formalizations in higher-order logic of two proofs of Arrow's impossibility theorem due to Geanakoplos. The Gibbard-Satterthwaite theorem is derived as a corollary. Lacunae found in the literature are discussed.
social choice theory higher-order logic gibbard-satterthwaite theorem arrow's theorem theorem proving