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
BibTeX:
@techreport{Nipkow-Arrow,author={Tobias Nipkow},
title={Social Choice Theory in HOL: Arrow and Gibbard-Satterthwaite},
institution={Technische Universit\"at M\"unchen},year=2008,
note="Submitted for publication"}
Isabelle theories in the
Archive of Formal Proofs