Social Choice Theory in HOL

被引：3

作者：

Nipkow, Tobias ^{[1
]}

机构：

[1] Tech Univ Munich, Inst Informat, Munich, Germany

来源：

JOURNAL OF AUTOMATED REASONING | 2009年 / 43卷 / 03期

关键词：

Social choice theory; Arrow's theorem; Gibbard-Satterthwaite theorem; Higher-order logic; Theorem proving; ARROWS THEOREM; WELFARE;

D O I：

10.1007/s10817-009-9147-4

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

This article presents formalizations in higher-order logic of two proofs of Arrow's impossibility theorem due to Geanakoplos. The Gibbard-Satterthwaite theorem is derived as a corollary. Lacunae found in the literature are discussed.

引用

页码：289 / 304

页数：16

共 15 条

[1] [Anonymous], 1970, Social choice and individual values
[2] A DIFFICULTY IN THE CONCEPT OF SOCIAL WELFARE
Arrow, Kenneth J.
[J]. JOURNAL OF POLITICAL ECONOMY, 1950, 58 (04) : 328 - 346
[3] GAMMIE P, 2008, ARCH FORMAL PROOFS F
[4] Three brief proofs of Arrow's impossibility theorem
Geanakoplos, J
[J]. ECONOMIC THEORY, 2005, 26 (01) : 211 - 215
[5] Geanakoplos J.D., 2001, 1123RRR COWL FDN
[6] MANIPULATION OF VOTING SCHEMES - GENERAL RESULT
GIBBARD, A
[J]. ECONOMETRICA, 1973, 41 (04) : 587 - 601
[7] Nipkow Tobias, 2002, Isabelle/ HOL: a proof assistant for higher-order logic
[8] Nisan N, 2007, ALGORITHMIC GAME THEORY, P1, DOI 10.1017/CBO9780511800481
[9] Arrow's theorem and the Gibbard-Satterthwaite theorem: a unified approach
Reny, PJ
[J]. ECONOMICS LETTERS, 2001, 70 (01) : 99 - 105
[10] ROUTLEY R, 1979, NOTRE DAME J FORM L, V20, P879

← 1 2 →