Social Choice Theory in HOL

被引:3
|
作者
Nipkow, Tobias [1 ]
机构
[1] Tech Univ Munich, Inst Informat, Munich, Germany
关键词
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
相关论文
共 50 条
  • [31] Application of Social Choice Theory to Modify the Value Measure of Health Systems
    Fu, Yelin
    Sui, Yubing
    Luo, Hao
    Han, Biao
    SOCIAL INDICATORS RESEARCH, 2020, 148 (03) : 1005 - 1019
  • [32] Online Marketing Research Based on Social Choice Theory and Cloud Computing
    Li, Li
    Niu, Ben-yu
    Tang, Xiao-jia
    2015 IEEE/ACM 8TH INTERNATIONAL CONFERENCE ON UTILITY AND CLOUD COMPUTING (UCC), 2015, : 391 - 396
  • [33] A Consistent Foundation for Isabelle/HOL
    Kuncar, Ondrej
    Popescu, Andrei
    JOURNAL OF AUTOMATED REASONING, 2019, 62 (04) : 531 - 555
  • [34] A Consistent Foundation for Isabelle/HOL
    Ondřej Kunčar
    Andrei Popescu
    Journal of Automated Reasoning, 2019, 62 : 531 - 555
  • [35] A new approach to rights in social choice theory which incorporates utilitarianism
    Richard Barrett
    Anne Petron-Brunel
    Maurice Salles
    Social Choice and Welfare, 2004, 22 : 17 - 28
  • [36] Reasoning About Social Choice Functions
    Troquard, Nicolas
    van der Hoek, Wiebe
    Wooldridge, Michael
    JOURNAL OF PHILOSOPHICAL LOGIC, 2011, 40 (04) : 473 - 498
  • [37] Social choice and the logic of simple games
    Daniels, Tijmen R.
    JOURNAL OF LOGIC AND COMPUTATION, 2011, 21 (06) : 883 - 906
  • [38] Uniformly bounded information and social choice
    Campbell, Donald E.
    Kelly, Jerry S.
    JOURNAL OF MATHEMATICAL ECONOMICS, 2009, 45 (7-8) : 415 - 421
  • [39] On the Formalization of the Heat Conduction Problem in HOL
    Deniz, Elif
    Rashid, Adnan
    Hasan, Osman
    Tahar, Sofiene
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2022, 2022, 13467 : 21 - 37
  • [40] An interview with Paul Samuelson: welfare economics, “old” and “new”, and social choice theory
    Kotaro Suzumura
    Social Choice and Welfare, 2005, 25 : 327 - 356