Social Choice Theory in HOL: Arrow and Gibbard-Satterthwaite

Tobias Nipkow

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


@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