First-Order Logic Formalisation of Arrow's Theorem

被引:6
|
作者
Grandi, Umberto [1 ]
Endriss, Ulle [1 ]
机构
[1] Univ Amsterdam, Inst Log Language & Computat, NL-1012 WX Amsterdam, Netherlands
来源
LOGIC, RATIONALITY, AND INTERACTION, PROCEEDINGS | 2009年 / 5834卷
关键词
IMPOSSIBILITY THEOREM;
D O I
10.1007/978-3-642-04893-7_11
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Arrow's Theorem is a central result in social choice theory. It states that, tinder certain natural conditions, it is impossible to aggregate the preferences of a finite set of individuals into a social preference ordering. We formalise this result in the language of first-order logic, thereby reducing Arrow's Theorem to a statement saying that a given set of first-order formulas does not possess a finite model. In the long run, we hope that this formalisation can serve as the basis for a fully automated proof of Arrow's Theorem and similar results in social choice theory. We prove that this is possible in principled at least for a fixed number of individuals, and we report on initial experiments with automated reasoning tools.
引用
收藏
页码:133 / 146
页数:14
相关论文
共 3 条
  • [1] Arrow’s theorem in judgment aggregation
    Franz Dietrich
    Christian List
    Social Choice and Welfare, 2007, 29 : 19 - 33
  • [2] Revisiting the role of value judgments in Arrow's impossibility theorem
    Nieto, Nestor Lovera
    EUROPEAN JOURNAL OF THE HISTORY OF ECONOMIC THOUGHT, 2024, 31 (06): : 976 - 997
  • [3] Design decisions: concordance of designers and effects of the Arrow's theorem on the collective preference ranking
    Franceschini, Fiorenzo
    Maisano, Domenico
    RESEARCH IN ENGINEERING DESIGN, 2019, 30 (03) : 425 - 434