Abstract
In preference aggregation a set of individuals express preferences over a set of alternatives, and these preferences have to be aggregated into a collective preference. When preferences are represented as orders, aggregation procedures are called social welfare functions. Classical results in social choice theory state that it is impossible to aggregate the preferences of a set of individuals under different natural sets of axiomatic conditions. We define a first-order language for social welfare functions and we give a complete axiomatisation for this class, without having the number of individuals or alternatives specified in the language. We are able to express classical axiomatic requirements in our first-order language, giving formal axioms for three classical theorems of preference aggregation by Arrow, by Sen, and by Kirman and Sondermann. We explore to what extent such theorems can be formally derived from our axiomatisations, obtaining positive results for Sen’s Theorem and the Kirman-Sondermann Theorem. For the case of Arrow’s Theorem, which does not apply in the case of infinite societies, we have to resort to fixing the number of individuals with an additional axiom. In the long run, we hope that our approach to formalisation can serve as the basis for a fully automated proof of classical and new theorems in social choice theory.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ågotnes, T., van der Hoek, W., & Wooldridge, M. (2009). On the logic of preference and judgment aggregation. Autonomous Agents and Multi-Agents Systems, 22(1), 4–30.
Arrow, K. J. (1963). Social choice and individual values, 2nd edition. John Wiley & Sons.
Arrow, K. J., Sen, A. K., & Suzumura, K. (Eds.) (2002). Handbook of social choice and welfare. North-Holland.
Black, D. (1948). On the rationale of group decision-making. The Journal of Political Economy, 56(1), 23–34.
Blau, J. H. (1957). The existence of social welfare functions. Econometrica, 25(2), 302–313.
Blau, J. H. (1971). Arrow’s Theorem with weak independence. Economica, 38(152), 413–420.
Burdman Feferman, A., & Feferman, S. (2004). Alfred Tarski: Life and logic. Cambridge University Press.
Davey, B. A., & Priestley, H. A. (1990). Introduction to lattices and orders. Cambridge University Press.
Ebbinghaus, H. D., & Flum, J. (1999). Finite model theory. Springer.
Enderton, H. B. (1972). A mathematical introduction to logic. Academic Press.
Endriss, U. (2011). Logic and social choice theory. In A. Gupta & J. van Benthem (Eds.), Logic and philosophy today (Vol. 2, pp. 333–377). College Publications.
Fishburn, P. C. (1970). Arrow’s impossibility theorem: Concise proof and infinite voters. Journal of Economic Theory, 2(1), 103–106.
Gaertner, W. (2001). Domain conditions in social choice theory. Cambridge University Press.
Gaertner, W. (2006). A primer in social choice theory. Oxford University Press.
Geanakoplos, J. (2005). Three brief proofs of Arrow’s impossibility theorem. Economic Theory, 26(1), 211–215.
Geist, C., & Endriss, U. (2011). Automated search for impossibility theorems in social choice theory: Ranking sets of objects. Journal of Artificial Intelligence Research, 40, 143–174.
Herzberg, F., & Eckert, D. (2012). Impossibility results for infinite-electorate abstract aggregation rules. Journal of Philosophical Logic, 41, 273–286.
Kirman, A., & Sondermann, D. (1972). Arrow’s Theorem, many agents, and invisible dictators. Journal of Economic Theory, 5(2), 267–277.
Lin, F. (2007). Finitely-verifiable classes of sentences. Presented at the 8th international symposium on logical formalizations of commonsense reasoning, Stanford.
McCune, W. (2003). ANL/MCS-TM-263 OTTER 3.3 reference manual. Technical memo, Argonne National Laboratory, Argonne.
Nipkow, T. (2009). Social choice theory in HOL: Arrow and Gibbard-Satterthwaite. Journal of Automated Reasoning, 43(3), 289–304.
Pauly, M. (2008). On the role of language in social choice theory. Synthese, 163(2), 227–243.
Pini, M. S., Rossi, F., Venable, K. B., & Walsh, T. (2009). Aggregating partially ordered preferences. Journal of Logic and Computation, 19, 475–502.
Schulz, S. (2004). System description: E 0.81. In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR-2004).
Sen, A. K. (1970). The impossibility of a Paretian liberal. The Journal of Political Economics, 78(1), 152–157.
Tang, P. (2010). Computer-aided theorem discovery: A new adventure and its application to economic theory. Ph.D. Thesis, Hong Kong University of Science and Technology.
Tang, P., & Lin, F. (2009). Computer-aided proofs of Arrow’s and other impossibility theorems. Artificial Intelligence, 173(11), 1041–1053.
Taylor, A. D. (2005). Social choice and the mathematics of manipulation. Cambridge University Press.
Troquard, N., van der Hoek, W., & Wooldridge, M. (2011). Reasoning about social choice functions. Journal of Philosophical Logic, 40, 473–498.
Väänänen, J. (2007). Dependence logic. Cambridge University Press.
Wiedijk, F. (2007) Arrow’s impossibility theorem. Formalized Mathematics, 15(4), 171–174.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 2.0 International License (https://creativecommons.org/licenses/by/2.0), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
About this article
Cite this article
Grandi, U., Endriss, U. First-Order Logic Formalisation of Impossibility Theorems in Preference Aggregation. J Philos Logic 42, 595–618 (2013). https://doi.org/10.1007/s10992-012-9240-8
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-012-9240-8