#### 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