Computer-aided proofs of Arrow's and other impossibility theorems

Arrow's impossibility theorem is one of the landmark results in social choice theory. Over the years since the theorem was proved in 1950, quite a few alternative proofs have been put forward. In this paper, we propose yet another alternative proof of the theorem. The basic idea is to use induc...

Full description

Saved in:
Bibliographic Details
Published in:Artificial intelligence 2009-07, Vol.173 (11), p.1041-1053
Main Authors: Tang, Pingzhong, Lin, Fangzhen
Format: Article
Language:English
Subjects:
Applied sciences
Arrow's theorem
Artificial intelligence
Computer science
control theory
systems
Computer-aided theorem proving
Decision theory. Utility theory
Exact sciences and technology
Knowledge representation
Logic and foundations
Mathematical logic, foundations, set theory
Mathematics
Muller–Satterthwaite theorem
Operational research and scientific management
Operational research. Management science
Proof theory and constructive mathematics
Sciences and techniques of general use
Sen's theorem
Social choice theory
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Arrow's impossibility theorem is one of the landmark results in social choice theory. Over the years since the theorem was proved in 1950, quite a few alternative proofs have been put forward. In this paper, we propose yet another alternative proof of the theorem. The basic idea is to use induction to reduce the theorem to the base case with 3 alternatives and 2 agents and then use computers to verify the base case. This turns out to be an effective approach for proving other impossibility theorems such as Muller–Satterthwaite and Sen's theorems as well. Motivated by the insights of the proof, we discover a new theorem with the help of computer programs. We believe this new proof opens an exciting prospect of using computers to discover similar impossibility or even possibility results.
ISSN:0004-3702
1872-7921
DOI:10.1016/j.artint.2009.02.005