Collective Choice and Social Welfare

The code in this repository is formalizes and proves the results from Amartya Sen's book "Collective Choice and Social Welfare" (expanded 2017 edition). The book alternates between un-starred and starred chapters, with the un-starred chapters (e.g. Chapter 1) discussing some topic informally while the starred chapters (e.g. Chapter 1*) go over the formal aspects of the discussion: definitions, theorems, proofs...


  • Chapter 1* --- order relations: definitions and properties;
  • Chapter 2* --- collective choice as indexed collections of order relations;
  • Chapter 3* --- Arrow's impossibility theorem;
  • ...