Social Choice Theory in HOL: Arrow and Gibbard-Satterthwaite
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.
pdf
Springer online
BibTeX:
@article{Nipkow-Arrow,author={Tobias Nipkow},
title={{Social Choice Theory in HOL: Arrow and Gibbard-Satterthwaite}},
journal={J. Automated Reasoning},volume=43,pages={289--304},year=2009}
Isabelle theories in the
Archive of Formal Proofs