Arrow's Impossibility Theorem Freek Wiedijk — 2007 Formalized Mathematics A formalization of the first proof from [6].