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.