Eine formalisierte Version desselben Beweises findet sich bei Tobias Nipkow: Social Choice Theory in HOL. Arrow and Gibbard-Satterthwaite. In: Journal of Automated Reasoning. 43, Nr. 3, 2009, S. 289–304, doi:10.1007/s10817-009-9147-4.
Robert Wilson: Social choice theory without the Pareto Principle. In: Journal of Economic Theory. 5, Nr. 3, 1972, S. 478–486, doi:10.1016/0022-0531(72)90051-8.
jstor.org
Julian H. Blau: The Existence of Social Welfare Functions. In: Econometrica. 25, Nr. 2, 1957, S. 302–313 (JSTOR:1910256).