Formalization and Verification of Proportional Representation Voting Systems using Isabelle/HOL: A Study of D'Hondt and Sainte-Laguë Methods

This master thesis delves into the multifaceted realm of Social Choice Theory, aspiring to not only deepen but also broaden our understanding of collective decision-making in the face of diverse and conflicting individual preferences. At the core of this exploration is the critical examination of the formalization, verification, and customization of voting systems—foundational mechanisms that significantly impact pivotal decision-making scenarios, including elections and resource allocation. Leveraging the advanced capabilities of Isabelle/HOL, a sophisticated platform for formal mathematical reasoning, this project meticulously investigates the intricacies of the D'Hondt and Sainte-Laguë voting systems. Social Choice Theory, the theoretical backdrop of this study, encompasses more than mere preference aggregation—it accentuates the complex interplay of rationality and fairness criteria essential for fostering democratic governance. Within this theoretical framework, voting systems assume various forms, including plurality, ranked preference, and proportional representation systems, each guided by distinct rules that collectively shape the integrity of the decision-making process. Emphasizing the unique features of Isabelle/HOL, particularly its application of Higher-Order Logic, this study constructs rigorous mathematical models that ensure precision and consistency in the analysis of these intricate systems. This endeavor represents a pioneering effort to synthesize the principles of Social Choice Theory with the formalization capabilities of Isabelle/HOL. The application of this logical framework to D'Hondt and Sainte-Laguë voting systems serves as a crucial bridge, shedding light on the underlying mechanisms of democratic governance. Beyond theoretical exploration, the study undertakes a practical mission—to provide a robust foundation for electoral reform and decision-making processes. This involves aligning theoretical insights with the formidable formalization and verification tools offered by Isabelle/HOL, thereby contributing to the advancement of informed and equitable democratic practices. Central to this research are the properties of anonymity and monotonicity, which are systematically examined within the context of voting systems. Anonymity ensures that individual preferences remain confidential, safeguarding the democratic process against undue influence, while monotonicity scrutinizes the consistency of outcomes when preferences are altered. By probing these properties, the study not only deepens our theoretical understanding but also presents practical implications for the design and implementation of voting systems, adding a layer of insight crucial for the improvement of democratic decision-making.