Skip to main content
SpringerLink
Log in

Formalizing Arrow’s theorem

  • Published:
Sadhana Aims and scope Submit manuscript

Abstract

A small project in which I encoded a proof of Arrow’s theorem—probably the most famous results in the economics field of social choice theory—in the computer using the Mizar system is presented here. The details of this specific project, as well as the process of formalization (encoding proofs in the computer) in general are discussed.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  • Arrow K 1950 A Difficulty in the Concept of Social Welfare. Journal of Political Economy 58(4): 328–346

    Article  Google Scholar 

  • Asperti A, Coen CS, Tassi E, Zacchiroli S 2007 Crafting a Proof Assistant. In T Altenkirch, C McBride, eds., Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18–21, 2006, Revised Selected Papers, volume 4502 of Lecture Notes in Computer Science, pages 18–32. Springer

  • Bancerek G, Rudnicki P 2003 A Compendium of Continuous Lattices in Mizar. Journal of Automated Reasoning 29(3–4): 189–224

    MathSciNet  Google Scholar 

  • Barras B 1999 Auto-validation d’un système de preuves avec familles inductives. Thèse de doctorat, Université Paris 7

  • Barras B, Werner B 1997 Coq in Coq. 〈http://pauillac.inria.fr/~barras/coqincoq.ps.gz〉

  • Blazy S, Dargaye Z, Leroy X 2006 Formal Verification of a C Compiler Front-end. In FM 2006: Int. Symp. on Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 460–475. Springer

  • Fox A 2003 Formal Specification and Verification of ARM6. In D A Basin, B Wolff, eds., Theorem Proving in Higher Order Logics, 16th International Conference TPHOLs 2003, Rome, Italy, September 8–12, 2003, Proceedings, volume 2758 of Lecture Notes in Computer Science, pages 25–40. Springer

  • Geanakoplos J 2001 Three Brief Proofs of Arrow’s Impossibility Theorem. Technical Report 1123RRR, Cowles Foundation

  • Gonthier G 2006 A computer-checked proof of the Four Colour Theorem. 〈http://research.microsoft.com/~gonthier/4colproof.pdf〉

  • Harrison J HOL Done Right 1995 〈http://www.cl.cam.ac.uk/users/jrh/papers/holright.ps.gz〉

  • Harrison J 2008 Towards self-verification of HOL Light. In U Furbach, N Shankar, eds., Proceedings of the Third International Joint Conference IJCAR 2006, volume 4130 of Lecture Notes in Computer Science, pages 177–191, Seattle, WA: Springer

    Google Scholar 

  • Harrison J 2008 Formalizing an Analytic Proof of the Prime Number Theorem (extended abstract). In R Boulton, J Hurd, K Slind, eds., Tools and Techniques for Verification of System Infrastructure, pages 17–22, London: The Royal Society

    Google Scholar 

  • Leroy X 2006 Formal Certification of a Compiler Back-end, or: Programming a Compiler with a Proof Assistant. In POPL’06, Charleston, South Carolina, USA

  • Naumov P, Stehr M-O, Meseguer J 2001 The HOL/NuPRL Proof Translator: A Practical Approach to Formal Interoperability. In R J Boulton, P B Jackson, eds., The 14th International Conference on Theorem Proving in Higher Order Logics, volume 2152 of LNCS, pages 329–345. Springer-Verlag

  • Nipkow T 2008 A Bit of Social Choice Theory in HOL: Arrow and Gibbard-Satterthwaite. In R Boulton, J Hurd, K Slind, eds., Tools and Techniques for Verification of System Infrastructure, page 9, London: The Royal Society

    Google Scholar 

  • Obua S, Skalberg S 2006 Importing HOL into Isabelle/HOL. In U Furbach, N Shankar, eds., IJCAR, volume 4130 of Lecture Notes in Computer Science, pages 298–302. Springer

  • Papadimitriou C 2008 CS294-1 Algorithmic Aspects of Game Theory, Lecture 2: January 23. 〈http://www.cs.berkeley.edu/~kunal/cs294-1-lec2.ps〉

  • Reny P 2000 Arrow’s Theorem and the Gibbard-Satterthwaite Theorem: A Unified Approach

  • Routley R 1979 Repairing Proofs of Arrow’s General Impossibility Theorem and Enlarging the Scope of the Theorem. Notre Dame Journal of Formal Logic, XX(4)

  • Taylor A D 2005 Social Choice and the Mathematics of Manipulation. Outlooks. Cambridge University Press

  • Varian H R 1992 Microeconomic Analysis. W W Norton, 3rd edition

  • Wiedijk F 2004 Formal Proof Sketches. In S Berardi, M Coppo, F Damiani, eds., Types for Proofs and Programs: Third International Workshop, TYPES 2003, Torino, Italy, April 30–May 4, Revised Selected Papers, volume 3085 of LNCS, pages 378–393

  • Wiedijk F 2007 Writing a Mizar article in nine easy steps. 〈http://www.cs.ru.nl/~freek/mizar/mizman.pdf〉

  • Wiedijk F 2007 Arrow’s Impossibility Theorem. Formalized Mathematics 15(4): 171–174

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Computing and Information Sciences, Radboud University Nijmegen, Toernooiveld 1, 6525 ED, Nijmegen, The Netherlands

    Freek Wiedijk

Authors
  1. Freek Wiedijk
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Freek Wiedijk.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Wiedijk, F. Formalizing Arrow’s theorem. Sadhana 34, 193–220 (2009). https://doi.org/10.1007/s12046-009-0005-1

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s12046-009-0005-1

Keywords

Search

Navigation