Formalizing Arrow's theorem

DOI10.1007/s12046-009-0005-1zbMath1176.91039OpenAlexW2143444807WikidataQ56168713 ScholiaQ56168713MaRDI QIDQ1040010

Freek Wiedijk

Publication date: 23 November 2009

Published in: Sādhanā (Search for Journal in Brave)

Full work available at URL: https://www.ias.ac.in/describe/article/sadh/034/01/0193-0220

zbMATH Keywords

social choice theoryGibbard-Satterthwaite theoremArrow's theoremformalization of mathematicsMizarproof errors

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Computational methods for problems pertaining to game theory, economics, and finance (91-08) Social choice (91B14)

Related Items

Lyndon words formalized in Isabelle/HOL ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ Social choice theory in HOL. Arrow and Gibbard-Satterthwaite ⋮ Foreword ⋮ Polygonal numbers ⋮ Flexary operations ⋮ Euler's partition theorem ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ An introduction to mechanized reasoning ⋮ Using Theorema in the Formalization of Theoretical Economics ⋮ Routh’s, Menelaus’ and Generalized Ceva’s Theorems

Uses Software

• Coq
• Mizar
• Nuprl
• Arrow Gibbard Satterthwaite

Cites Work

• Repairing proofs of Arrow's general impossibility theorem and enlarging the scope of the theorem
• Arrow's theorem and the Gibbard-Satterthwaite theorem: A unified approach
• Three brief proofs of Arrow's impossibility theorem
• A compendium of continuous lattices in MIZAR
• Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
• Towards Self-verification of HOL Light
• Formal certification of a compiler back-end or
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item