Formalizing Arrow's theorem

DOI10.1007/S12046-009-0005-1MaRDI QIDQ1040010zbMATH OpenOpenAlexWikidataFDO

Authors 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 theoryArrow's theoremformalization of mathematicsMizarGibbard-Satterthwaite theoremproof errors

Mathematics Subject Classification ID

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

Recommendations

• First-order logic formalisation of Arrow's theorem
• Computer-aided proofs of Arrow's and other impossibility theorems
• Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
• First-order logic formalisation of impossibility theorems in preference aggregation
• Automated reasoning in social choice theory: some remarks

Cites work

• scientific article; zbMATH DE number 2182815 (Why is no real title available?)
• scientific article; zbMATH DE number 1863394 (Why is no real title available?)
• scientific article; zbMATH DE number 1863397 (Why is no real title available?)
• A compendium of continuous lattices in MIZAR
• Arrow's theorem and the Gibbard-Satterthwaite theorem: A unified approach
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Repairing proofs of Arrow's general impossibility theorem and enlarging the scope of the theorem
• Sets in Coq, Coq in Sets
• Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
• Three brief proofs of Arrow's impossibility theorem
• Towards Self-verification of HOL Light

Cited in

(18)

• Polygonal numbers
• Euler's partition theorem
• Flexary operations
• The ForMaRE project -- formal mathematical reasoning in economics
• Lyndon words formalized in Isabelle/HOL
• Verifying randomised social choice
• Foreword
• The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema
• Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
• Routh's, Menelaus' and generalized Ceva's theorems
• First-order logic formalisation of impossibility theorems in preference aggregation
• Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
• Formalization and execution of linear algebra: from theorems to algorithms
• First-order logic formalisation of Arrow's theorem
• Computer-aided proofs of Arrow's and other impossibility theorems
• An introduction to mechanized reasoning
• scientific article; zbMATH DE number 4029217 (Why is no real title available?)
• Using Theorema in the Formalization of Theoretical Economics

Describes a project that uses

Uses Software

• Coq
• Mizar
• Nuprl
• Arrow Gibbard Satterthwaite

This page was built for publication: Formalizing Arrow's theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1040010)