peteg's blog - choice - social choice - 2008 11 09 MaysTheorem

May's Theorem in Isabelle

/choice/social-choice | Link

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 contradiction 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.

An interested soul has written a great overview of May's life work.