A full formal representation of Arrow’s impossibility theorem

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.