Arrow and Gibbard-Satterthwaite

Title:	Arrow and Gibbard-Satterthwaite
Author:	Tobias Nipkow
Submission date:	2008-09-01
Abstract:	This article formalizes two proofs of Arrow's impossibility theorem due to Geanakoplos and derives the Gibbard-Satterthwaite theorem as a corollary. One formalization is based on utility functions, the other one on strict partial orders. An article about these proofs is found here.
Status: [ok]	This is the development version of this entry generated for Isabelle-09-Feb-2010. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any.

Older releases: