Abstract
It is often convenient to view a computational procedure, or a program, as a relation on a set of states, where a state can be thought of as a function that assigns a value to every possible variable and a truth value to all propositions. This idea was proposed by Pratt [19] and extends the work of of Floyd [4] and Hoare [6]. Harel, Kozen and Tiuryn [5] provide a very thorough discussion of computational procedures from this point of view. In [12], Rohit Parikh suggests that a similar framework can be developed for studying social procedures, such as fair division algorithms or voting protocols.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
When the ratio is closer to 1, a unit gain for Bob costs a smaller loss for Ann.
- 3.
A strategy profile in an extensive game is a subgame perfect equilibrium if no agent has a reason to deviate from the profile and this is true for all subgames. Consult [8] for details.
- 4.
That is, an extensive game (i.e., a game tree) without the preferences over the outcomes.
- 5.
Note that Pauly does not restrict to definable sets here. Thus he is provided an extensional semantics rather than an intensional semantics. Issues related to this, such as whether or not certain properties are expressible in a logical language (say first-order logic), is left for future work. We agree with Pauly that, although this raises some interesting questions, it will only complicate the current discussion.
- 6.
Note that Pe is an atomic relation symbol. Alternatively, we may first define a relation \((\sigma,\alpha,\beta)\succ (\sigma',\alpha',\beta')\) iff either \(\sum\nolimits_i \sigma_i\alpha_i>\sum\nolimits_i\sigma_i'\alpha_i\) and \(\sum\nolimits_i(1-\sigma_i)\beta_i\ge \sum\nolimits_i(1-\sigma'_i)\beta_i\) or \(\sum\nolimits_i \sigma_i\alpha_i\ge\sum\nolimits_i\sigma_i'\alpha_i\) and \(\sum\nolimits_i(1-\sigma_i)\beta_i> \sum\nolimits_i(1-\sigma'_i)\beta_i\). Then the we can define the predicate Pe as follows: \(Pe(\sigma,\alpha,\beta):=\forall s ((\sigma,\alpha,\beta)\succ (s,\alpha,\beta))\). However, this formula is not in the language we described above as a quantifier is involved.
- 7.
In this cake-cutting algorithm, the first agent cuts a slice of the cake he considers fair. This piece is then inspected by each of the remaining agents in turn. Each agent can decide either leave the piece as is or diminish the piece and return the extra portion to the main part of the cake. The last person to diminish the piece receives that piece of the cake (or if no-one diminishes the piece, the cutter receives the piece). See [2] for details.
- 8.
This assumes that there are valuations which are, as a matter of fact, the agents’ actual valuations. However, it may very well be that the players themselves cannot point to a valuation which they consider their “true” valuation. After all, valuations are simply a way to represent the players’ preferences or utilities over the set of goods. See (Parikh R., and Pacit E. Safe Votes, Sincere Votes, and Strategizing. Unpublished Manuscript, 2005.) for a relevant discussion in the context of voting. Nonetheless, for this paper we assume that each player is associated with a unique “true valuation”.
- 9.
Here we need only consider Nash equilibrium and not subgame perfect equilibrium as there is only one point in AW when the agents make a choice.
- 10.
Note that this does not mean moving to imperfect information games. Although this may be an interesting direction for future research, all that is needed here is a formal model of the agents information about the other agents’ preferences.
References
Alur R., Henzinger T., and Kupferman O. Alternating-time temporal logic, JACM, 495: 672–713, 2002.
Brams S. J., and Taylor A. D. Fair Division: From Cake-Cutting to Dispute Resolution. Cambridge University Press, Cambridge, 1996.
Brams S. J., and Taylor A. D. The Win–Win Solution. W. W. Norton and Company, New York, NY, 1999.
Floyd R. W. Assigning meanings to programs, Proc. Symp. Appl. Math., 19: 19–31, 1967.
Harel D., Kozen D., and Tiuryn J. Dynamic Logic. MIT Press, Cambridge, MA, 2000.
Hoare C. A. R. An axiomatic basis for computer programming, Commun. ACM, 12: 576–583, 1969.
Nielson H. R., and Nielson F. Semantics with Applications. Wiley, Chichester, 1992.
Osborne M., and Rubinstein A. A Course in Game Theory. The MIT Press, Cambridge, 1994.
Pacuit E., Parikh R., and Salame S. Some recent results on adjusted winner. In U. Endriss and J. Lange, editors, Proceedings of Computational Social Choice. ILLC Technical, Amsterdam, The Netherlands, 2006.
Pacuit E., and Parikh R. Introduction to Formal Epistemology. Coursenotes for ESSLLI 2007. Available at staff.science.uva.nl/epacuit/formep esslli.html
Parikh R. The logic of games and its applications. In M. Karpinski and J. van Leeuwen, editors, Topics in the Theory of Computation, (vol. 24 of Annals of Discrete Mathematics), Elsevier, Amsterdam, 1985.
Parikh R. Language as social software (abstract). In International Congress on Logic, Methodology and Philosophy of Science, page 415. 1995.
Parikh R. Knowledge and structure in social algorithms (extended abstract). Presented at Stony Brook Conference on Game Theory, 2007.
Pauly M. A modal logic for coalitional power in games, J. Log. Comput., 121: 149–166, 2002.
Pauly M. Programming and verifying subgame perfect mechanisms, J. Log. Comput., 153: 295–316, 2005.
Pauly M., and Parikh R. Game logic – An overview, Stud. Log., 752: 165–182, 2003.
Pratt V. R. Semantical considerations on Floyd-Hoare logic. In Proceedings of. 17th Symposium on Foundation of Computer Science. IEEE, pages 109–121, 1976
van Otterloo S. A Strategic Analysis of Multi-Agent Protocols. PhD thesis, University of Liverpool, 2005.
Wooldridge M., Agotnes T., Dunne P., and van der Hoek, W. Logic for automated mechanism design — A progress report. In Twenty-Second Conference on Artificial Intelligence (AAAI-07), 2007.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Pacuit, E. (2011). Towards a Logical Analysis of Adjusted Winner . In: van Benthem, J., Gupta, A., Parikh, R. (eds) Proof, Computation and Agency. Synthese Library, vol 352. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-0080-2_13
Download citation
DOI: https://doi.org/10.1007/978-94-007-0080-2_13
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-007-0079-6
Online ISBN: 978-94-007-0080-2
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)