Formalizing Arrow’s theorem

被引：0

作者：

Freek Wiedijk

机构：

[1] Radboud University Nijmegen,Institute for Computing and Information Sciences

来源：

Sadhana | 2009年 / 34卷

关键词：

formalization of mathematics; Mizar; social choice theory; Arrow’s theorem; Gibbard-Satterthwaite theorem; proof errors;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

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.

引用

页码：193 / 220

页数：27

共 50 条

[1] Formalizing Arrow's theorem
Wiedijk, Freek
SADHANA-ACADEMY PROCEEDINGS IN ENGINEERING SCIENCES, 2009, 34 (01): : 193 - 220
[2] FUZZY ARROW'S THEOREM
Mordeson, John N.
Clark, Terry D.
NEW MATHEMATICS AND NATURAL COMPUTATION, 2009, 5 (02) : 371 - 383
[3] Arrow's Impossibility Theorem
Wiedijk, Freek
FORMALIZED MATHEMATICS, 2007, 15 (04): : 171 - 174
[4] Arrow’s impossibility theorem
Renuka Ravindran
Resonance, 2005, 10 (11) : 18 - 26
[5] Arrow's theorem as a corollary
Nehring, K
ECONOMICS LETTERS, 2003, 80 (03) : 379 - 382
[6] Arrow's Impossibility Theorem
Ravindran, Renuka
RESONANCE-JOURNAL OF SCIENCE EDUCATION, 2005, 10 (11): : 18 - 26
[7] Formalizing the separability condition in Bell's theorem
Fogel, Brandon
STUDIES IN HISTORY AND PHILOSOPHY OF MODERN PHYSICS, 2007, 38 (04): : 920 - 937
[8] Formalizing Moessner's theorem and generalizations in NUPRL
Bickford, Mark
Kozen, Dexter
Silva, Alexandra
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2022, 124
[9] Formalizing Pick's Theorem in Isabelle/HOL
Binder, Sage
Kosaian, Katherine
INTELLIGENT COMPUTER MATHEMATICS, CICM 2024, 2024, 14690 : 109 - 126
[10] Arrow's Theorem and Turing computability
Mihara, HR
ECONOMIC THEORY, 1997, 10 (02) : 257 - 276

← 1 2 3 4 5 →