The beginnings of a proof of Arrow's Theorem in Isabelle.
Tue, Dec 12, 2006./choice/social-choice | LinkOn the side I've been chugging through Amartya Sen's classic Collective Choice and Social Welfare (1970), trying to convince Isabelle of some of the classic results in what is ultimately a theory of voting. As Richard Routley observes in his Repairing Proofs of Arrow's General Impossibility Theorem and Enlarging the Scope of the Theorem (Notre Dame Journal of Formal Logic, Volume XX, Number 4, October 1979):
The importance of a logically adequate proof is in no way diminished because, as it fortunately turns out, the theorem is correct under the intended (if often inadequately formulated) conditions. But that makes it easy to say that it is trivial to fuss over quantificational details of the standard proofs (proof failure comes ultimately in every case from quantificational errors, omission of necessary quantifiers or mistaken orderings of quantifiers, both major sources of invalidity in logic and mathematics) for every economist knows what is meant by the theorem, that it is essentially correct and its proof intuitively clear, and that a rigorous proof can be produced. The claim is false, as will emerge, even of the economic textbook writers. The textbooks have failed to produce what it is essential to have, especially in the case of a theorem with such far-reaching consequences (even if it is after all only an exercise in second-order quantificational logic), namely a correct and rigorous proof. The history of mathematics is replete with cases where what everyone was thought to know proved false, or where what was intuitively clear turned out to be mistaken or correct only under restrictive conditions.
In other words, perfect for formalisation in Isabelle.
At this point I have formalised the definitions given by Sen (and others) and shown Arrow's General Possibility Theorem (commonly known as Arrow's Impossibility Theorem) and the positive result about Social Decision Functions (SDFs). It's a huge space and there's plenty more to do.