Tobias Nipkow has written an article about mechanising some recent proofs of Arrow's Theorem and Gibbard-Satterthwaite in Isabelle, and has kindly cited my clumsy attempts at similar things. In an attempt at differentiation I have polished up my proofs from Sen's magnum opus and added one of May's Theorem. As one might expect from a positive result in social choice theory there are endless reworkings of the original conditions in the literature since 1952, and I am not entirely sure what the state of the art is.
The proof itself is fairly straightfoward, although Sen makes an
uncharacteristic slip by unnecessarily arguing by contradition in his
proof of my anonymous_neutral_indifference. When I'm next
bored and idle I'll see if that makes any difference in the bigger
scheme of things.
The hope is to get all of this into the Archive of Formal Proofs and obtain some feedback on the nastier parts of the mechanisation.
Once more:
- arrows_theorem.pdf
- An Isabelle-generated document of the development.
darcs get http://peteg.org/isabelle/arrows_theorem/- A darcs repository for the development.
An interested soul has written a great overview of May's life work.
