# A full formal representation of Arrow’s impossibility theorem

## TL;DR

This paper provides a fully formal logical proof of Arrow’s impossibility theorem, emphasizing rigorous derivation and broader applicability.

## Contribution

It introduces a formal logic-based proof method for Arrow’s theorem, expanding the scope of preference relations considered.

## Key findings

- A formal proof of Arrow’s theorem is constructed using a proof calculus in formal logic.
- The approach reveals the global structure of the social welfare function in the theorem.
- The method allows for a broader range of preference relations than standard economic models.

## Abstract

Revised proofs of Kenneth Arrow’s impossibility theorem, one of the most influential theorems in economics, political science, and philosophy, have been presented in prose form, incorporating novel ideas such as decisive sets and pivotal voters. This study develops another approach to proving the theorem. Using a proof calculus in formal logic, we construct a proof with a full mathematical representation. While previous proofs emphasize intuitive accessibility, this one focuses on meticulous derivation and reveals the global structure of the social welfare function central to the theorem. The primary aim is to contribute methodologically to research on the theorem by demonstrating the effectiveness of systematically applying techniques from formal logic to its proof. Additionally, it accommodates a broader range of preference relations than those typically considered rational in standard economic models, allowing for the integration of diverse human behavior patterns into a single theoretical framework. The interdisciplinary relevance of the theorem is also discussed, including its relation to epistemology and philosophy.