Skip to main content
SpringerLink
Log in

Stit Logics, Games, Knowledge, and Freedom

  • Chapter
  • First Online:
Johan van Benthem on Logic and Information Dynamics

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 5))

Abstract

This chapter has two main goals: highlighting the connections between Stit logics and game theory and comparing Stit logics with Matrix Game Logic, a Dynamic Logic introduced by van Benthem in order to model some interesting epistemic notions from game theory. Achieving the first goal will prove the flexibility of Stit logics and their applicability in the logical foundations of game theory, and will lay the groundwork for accomplishing the second. A comparison between Stit logics and Matrix Game Logic is already offered in recent work by van Benthem and Pacuit. Here, we push the comparison further by embedding Matrix Game Logic into a fragment of group Stit logic, and using the embedding to derive some properties of Matrix Game Logic—in particular, undecidability and the lack of finite axiomatizability. In addition, the embedding sheds light on some open issues about the so-called “freedom operator” of Matrix Game Logic.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Belnap and Perloff [4] and von Kutschera [27] are usually regarded as the two papers that, independently, lay the foundations of STIT.

  2. 2.

    See, however, the important earlier work by Kooi and Tamminga [25], Tamminga [29], and Turrini [5].

  3. 3.

    Others have also tried to developed unified perspectives encompassing STIT and dynamic logics. See for instance Herzig and Lorini [20], which presents a dynamic logic of agency in the tradition of Propositional Dynamic Logics. In this framework, a basic stit operator can be defined as an existential quantifier over the actions of a given agent.

  4. 4.

    This particular operator was first isolated, and given this name, by Horty and Belnap [22]; the name reflects the fact that the operator captures, in the different framework of stit semantics, ideas introduced much earlier by Chellas [15]. A comparison between Chellas’s early work on agency and the later STIT can be found in Chellas [16], and also in Horty and Belnap [22].

  5. 5.

    STIT is traditionally interpreted on branching-time structures (see [3] and [24]) where moments are linearly ordered toward the past but are not linearly ordered toward the future. In such structures, choices are sets of histories, and histories are in turn sets of moments which are (1) maximal with respect to inclusion and (2) linearly ordered toward the future. However, the most widespread stit operators do not express any temporal dimension, and thus the indeterministic framework can be replaced by Kripke frames where no temporal order is imposed. Such frames are used by Balbiani, Herzig, and Troquard et al. [1], and by Herzig and Schwarzentruber [21]; and we follow them in the present chapter.

  6. 6.

    In case this condition seems too strong, it is helpful to think of one of the agents as “nature,” which removes any remaining indeterminacy once all the more ordinary agents have made their choices; this tactic was mentioned in [24, p. 91].

  7. 7.

    D1 just encodes a special case of the game-theoretical principle of additivity, which characterizes the construction of all groups in group STIT; see condition R4 in Sect. 23.5.

  8. 8.

    Actually, the correspondence between games and consequentialist CKF\(^+\)’s (see below for a definition) can also be established without imposing condition R3; see, for example, van Benthem and Pacuit [11] and Tamminga [29]. However, the condition makes the proof of such a correspondence much more straightforward and general. In addition the proofs which do not use R3 essentially rely on consideration about language, while the correspondence result which uses R3, established by Turrini in [5], relies only on the structures in question.

  9. 9.

    See Balbiani, Herzig, and Troquard et al. [1] for discussion. This axiomatization is due to Xu [31], where, however, the Chellas stit was replaced by the deliberative stit, and completeness is proved relative to trees endowed with choices and agents.

  10. 10.

    Thus, for instance, the validity of IA implies the validity of \(\Diamond [i]\phi \wedge \Diamond [j]\phi \ \rightarrow \Diamond ([i]\phi \wedge [j]\phi )\)—see [1, p. 391].

  11. 11.

    TC also plays a role in replacing IA with the new axiom in [1]: the two-agent version of IA (\(\Diamond [i]\phi \wedge \Diamond [j]\phi \ \rightarrow \Diamond ([i]\phi \wedge [j]\phi )\)) is derivable by TC, S5 and MA by Modus Ponens and Necessitation of \(\Box \), while the \(k\)-agent version can be proved by induction on the \(k-1\) case and \(\Diamond \phi \ \rightarrow \ \langle k\rangle \bigwedge _{1\le i < k}\langle i\rangle \phi \), for \(k > 1\) ([1, pp. 392–393]).

  12. 12.

    Balbiani et al. [1] also introduces a third (and more compact) axiomatic system for \(\mathsf {CSTIT}\), consisting of S5 for \([i]\) agency operators, the definition \(\Box \phi \leftrightarrow [1][2]\phi \) and the formula \(\langle i\rangle \langle j\rangle \phi \rightarrow \langle k\rangle \bigwedge _{m \in \overline{k}}\langle m\rangle \phi \). S5 for \(\Box \), MA, the axiom \(\Diamond \phi \ \rightarrow \ \langle i\rangle \bigwedge _{j \in \overline{i}}\langle j\rangle \phi \)—and hence IA—are provable from these new axioms by Modus Ponens and Necessitation. See [1, pp. 394 and 397].

  13. 13.

    These results were first established by Xu [30]; see also Balbiani et al. [1].

  14. 14.

    Balbiani et al. [1, p. 395] prove that the logic of two-agent Chellas stit is nothing but S5\(^{2}\).

  15. 15.

    See Hirsch et al. [23].

  16. 16.

    A noticeable exception is the combinations of STIT and actions explored by Xu [32].

  17. 17.

    If we follow Belnap’s reading, deliberative stit may prove more suitable than the Chellas stit, since the former does not allow for trivial truths to be seen to by any agent; the Chellas stit allows for this and does not seem to fit equally well the idea of a causal contribution to a change in the world.

  18. 18.

    Such a component proves relevant also if we wish to represent the sequential aspect of choice-making in extended game forms, since a sequence of choice-making acts presuppose a temporal dimension.

  19. 19.

    To be more precise, the temporal component of BT + AC structures are trees. Along the years, other temporal components of indeterministic time for choices and agents have been introduced; see, for instance, the \(\mathsf {XSTIT}\) frames due to Broersen [12], the bundled choice trees of Ciuni and Zanardo [19], and the Temporal Kripke STIT models of Lorini [28].

  20. 20.

    Display of a temporal order is necessary to define the so-called ‘stit operators for non-instantaneous agency’, that is operators that express a temporal hiatus between choice and result. Examples of such operators are the fused \(\mathsf {xstit}\) in Broersen [12], and the operators introduced in Ciuni and Mastop [18] and Ciuni and Zanardo [19]. A hiatus between choices and results can be also expressed by combining autonomous operators for agency and for temporal distinctions. Broersen follows this line in [13] and [14], as does Lorini [28]. A very complex stit operator is the original “achievement stit” due to Belnap and Perloff [4] which captures the cross-temporal dimension of agency by expressing the notion that a result holds at \(m\) due to a previous choice of \(i\); variants of the achievement stit are proposed by Zanardo [33] and Ciuni [17].

  21. 21.

    One should not forget that game-theoretical ideas were very important in STIT since its very beginning. This is clear from [3, pp. 283, 343–344], where the matrix representation of games is mentioned and independence of agents is explained with it, and where a comparison between extended game forms and BT + AC is briefly drawn.

  22. 22.

    Since we do not deal with the sequential aspect of choice-making here, we prefer to use the term ‘action’ rather than ‘strategy’.

  23. 23.

    This result, established as Theorem 1 in [5], is actually stated there for full groups of agents (“coalitions” in the standard game-theoretical terminology) and their anti-groups. Notice that the result in [5] naturally extends to CKF\(^+\)’s without preference relation and strategic game forms, which obtain from games by dropping the preference relation.

  24. 24.

    Thus, from every game \(\fancyscript{G}\) we can construct the corresponding CCKF\(^+\) \({\fancyscript{C^{G}}} = \langle W^{\fancyscript{G}}, Ags^{\fancyscript{G}}, \{\sim ^{C{\fancyscript{G}}}_{i} \mid i \in Ags\}, \{\succeq ^{C{\fancyscript{G}}}_{i} \mid i \in Ags\}\rangle \), where \(w\sim ^{C{\fancyscript{G}}}_{i}w'\) iff \(w' \in [w']_{i}\) for \([w]^{}_i \in Ch^{\fancyscript{G}}\).

  25. 25.

    \(o(a_i)\) is a weakly dominant action iff \(o(a_{i}, a_{\overline{i}}) \succeq _{i} o(a^{\prime }_{i}, a_{\overline{i}})\) for all \(a^{\prime }_{i} \in A_i\) and all \(a_{\overline{i}}\in A_{\overline{i}}\).

  26. 26.

    See, for example, Kooi and Tamminga [25], Turrini [5], and Tamminga [29].

  27. 27.

    \(o(a_i)\) is a best action of \(i\) iff \(o(a_i, a_{\overline{i}}) \succeq _{i} o(a^{\prime }_i, a_{\overline{i}})\) for all \(a^{\prime }_{i}\in A_i\).

  28. 28.

    This also explains why the function \(Ch(i)\) is defined as a partition (see end of Sect. 23.2).

  29. 29.

    This is no proof that STIT can deal with correlation as intended by [11], but is a general sign of the adaptability of STIT relative to the issue of independence.

  30. 30.

    Also, notice that the “utilitarian STIT frames” introduced by [24] are grounded on branching-time structures. In such frames, the value attached to a history is not only agent-independent, but also moment-independent, that is it does not vary with time. This reminds the definition of preferences and priorities in standard rational-choice theory.

  31. 31.

    In its original version, MGL sees action profiles themselves as states. Thus, \(W\) and \(o\) are not included in the original definition of a MGF. Here we consider situations where there is no action-profile gap, which can be in turn seen as situations where the function \(o\) is total and no restriction is imposed on the construction of action profiles. In this case, MGF’s can be defined as in the text.

  32. 32.

    The translation \(\tau \) above is already defined in and [8] and [11]. However, it does not define a mutual embedding there, since the full MGL is considered, and as we shall see, \(\mathsf {CSTIT}\) is a proper fragment of it.

  33. 33.

    It may seem that introducing linguistic atoms \(b_{1}\), \(b_2, b_3, \dots \) to express the notion of a best action is a kind of trick. However, the move makes sense if the goal is not providing an analysis of the notion, but simply to give us linguistic means to express the fact that such an action is being performed.

  34. 34.

    Theorem 6 in [6] is easily adapted to finite CCKF\(^+\)’s.

  35. 35.

    Group STIT was already present at the beginning of STIT; see Belnap [3] and Horty [24]. Both Belnap and Horty assume additivity; see [3, Definition 10–3], and [24, Definition 2.10]. Neither Belnap nor Horty assume condition R3\('\) below—that the joint agency of all the agents may determine a unique outcome—although, as mentioned earlier, Horty [24, p. 91] considers models that satisfy this condition. Basically, the conditions we present here build on those presented in Horty [24] by adding the standard game-theoretical condition of coalitional monotonicity. The latter can be actually derived by R2\('\), but we present it here as a basic condition in order to conform with the standard presentation of group STIT.

  36. 36.

    The principle is also called “Rectangularity” in Turrini [5].

  37. 37.

    The standard condition in game theory is actually superadditivity, which allows for the choice of \(I\) to be a subset of the choices of \(I\)’s members; the condition is actually a consequence of coalition monotonicity. However, we prefer to include R4 in order to comply with the standard choice in group STIT, and also because it makes the construction of groups conceptually easier.

  38. 38.

    Again, see Hirsch et al. [23] for these results concerning \(S5^{n}\).

  39. 39.

    Here we mean MGL as defined in this chapter, not the full logic defined in van Benthem [8], which also includes an operator for preferences.

  40. 40.

    See our observation above on the conditions for undecidability and failure of finite axiomatizability in group \(\mathsf {CSTIT}\). Of course, decidability and finite axiomatizability are restored if we confine to MGL with only two agents, so that \(Ags = \{1, 2\}\). In that case, \(\overline{1} = 2\) and \(\overline{2} = 1\). The anti-groups thus collapse into different agents, and MGL with two agents actually collapse into EMGL with two agents—which is indeed decidable and finitely axiomatizable, since EMGL is, no matter the cardinality of \(Ags\). Thus, the case with two agents does not hold much interest.

References

  1. Balbiani P, Herzig A, Troquard N (2008) Alternative axiomatics and complexity of deliberative STIT theories. J Philos Logic 37(4):387–406

    Google Scholar 

  2. Baltag A, Moss LS, Solecki S (1998) The logic of public announcements, common knowledge and private suspicions. In: Proceedings TARK, Morgan Kaufmann Publishers, Los Altos, pp 43–56. (updated versions through 2004)

    Google Scholar 

  3. Belnap N, Michael P, Ming X (2001) Facing the future: agents and choices in our indeterminist world. Oxford University Press, Oxford

    Google Scholar 

  4. Belnap N, Perloff M (1988) Seeing to it that: a canonical form for agentives. Theoria 54:175–199

    Google Scholar 

  5. van Benthem J (2007) Rational dynamics and epistemic logic in games. Int Game Theory Rev 9(1):13–45

    Google Scholar 

  6. van Benthem J (2011) Logical dynamics of information and interaction. Cambridge University Press, Cambridge

    Google Scholar 

  7. van Benthem J (forthcoming) Logic in games. The MIT Press, Cambridge (MA)

    Google Scholar 

  8. van Benthem J, Pacuit E (forthcoming) Connecting logics for choice and change. In: M\(\ddot{\rm u}\)ller Thomas (ed) Volume in honour of Nuel Belnap. Springer, Berlin (outstanding logicians series)

    Google Scholar 

  9. Broersen J (2011) A deontic epistemic stit logic distinguishing modes of Mens Rea. J Appl Logic 9(2):137–152

    Google Scholar 

  10. Broersen J (2011) Modeling attempt and action failure in probabilistic stit logic. In: Proceedings of twenty-second international joint conference on artificial intelligence (IJCAI 2011), pp 792–797

    Google Scholar 

  11. Broersen J (2011) Probabilistic stit logic. In: Proceedings 11th european conference on symbolic and quantitative approaches to reasoning with uncertainty (ECSQARU 2011). Lecture notes in artificial intelligence, vol 6717. Springer, Berlin, pp 521–531

    Google Scholar 

  12. Broersen J, Herzig A, Troquard N (2006) Embedding ATL in strategic STIT logic of agency. J Comput 16(5):559–578

    Google Scholar 

  13. Broersen J, Herzig A, Troquard N (2006) From coalition logic to STIT. Electron Notes Theoret Comput Sci 157:23–35

    Google Scholar 

  14. Chellas B (1969) The logical form of imperatives. PhD thesis, Philosophy Department, Stanford University

    Google Scholar 

  15. Chellas B (1992) Time and modality in the logic of agency. Studia Logica 51:485–517

    Google Scholar 

  16. Ciuni R (2010) From achievement stit to metric possible choices, logica 2009 yearbook. College Publications, London, pp 33–46

    Google Scholar 

  17. Ciuni R, Mastop R (2009) Attributing distributed responsibility in stit logic. In: Xiandong H, Horty J, Pacuit E (eds) Logic rationality, interaction (lecture notes in computer science, vol 5834. Springer, Berlin, pp 66–75

    Google Scholar 

  18. Ciuni R, Zanardo A (2010) Completeness of a branching-time logic with possible choices. Studia Logica 96(3):393–420

    Google Scholar 

  19. Herzig A, Lorini E (2010) A dynamic logic of agency I: STIT, abilities and powers. J Logic Lang Inform19(1):89–121

    Google Scholar 

  20. Herzig A, Schwarzentruber F (2008) Properties of logics for individual and group agency. In: Areces C, Goldblatt R (eds) Advances in modal logic, vol VII. College Publications, London, pp 133–149

    Google Scholar 

  21. Hirsch R, Hodkinson I, Kurucz A (2002) On modal logics between K\(\times \)K\(\times \)K and S5\(\times \)S5\(\times \)S5. J Symbol Logic 67(1):221–234

    Google Scholar 

  22. Horty J (1996) Agency and obligation. Synthese 108(2):269–307

    Google Scholar 

  23. Horty J (2001) Agency and deontic logic. Oxford University Press, Oxford

    Google Scholar 

  24. Horty J, Belnap N (1995) The deliberative stit: a study of action, omission, and obligation. J Philos Logic 24(6):583–644

    Google Scholar 

  25. Kooi B, Tamminga A (2008) Moral conflicts between groups of agents. J Philos Logic 37:1–21

    Google Scholar 

  26. von Kutschera F (1986) Bewirken. Erkenntnis 24(3):253–281

    Google Scholar 

  27. Lorini E (2013) Temporal STIT logic and its application to normative reasoning. J Appl Non-Class Logics 23(4):372–399

    Google Scholar 

  28. Tamminga A (2013) Deontic logic for strategic games. Erkenntnis 78(1):183–200

    Google Scholar 

  29. Turrini P (2012) Agreements as norms. In: Ågotnes T, Broersen J, Elgesem D (eds) DEON 2012, LNAI 7393. Springer, Berlin, pp 31–45

    Google Scholar 

  30. Xu M (1994) Decidability of deliberative stit theories with multiple agents. In: Gabbay D, Ohlbach H (eds) Proceedings of the first international conference in temporal logic. Springer, Berlin, pp 332–348

    Google Scholar 

  31. Xu M (1998) Axioms for deliberative stit. J Philos Logic 27:505–552

    Google Scholar 

  32. Xu M (2010) Combinations of STIT and actions. J Logic Lang Inform 19(4):485–503

    Google Scholar 

  33. Zanardo A (2013) Indistinguishability, choices and logics of agency. Studia Logica 101(6): 1215–1236

    Google Scholar 

Download references

Acknowledgments

This work was carried out while Roberto Ciuni was a Humboldt Postdoctoral Fellow working on the project ‘A Tempo-Modal Logic for Responsibility Attribution in Many-Step Actions’ (2011–2013). We wish to thank Alexandru Baltag and Yan Zhang for very helpful comments on earlier versions of this work.

Author information

Authors and Affiliations

  1. Department of Philosophy II, Ruhr University Bochum, Universitätsstraße 150, 44780, Bochum, Germany

    Roberto Ciuni

  2. Philosophy Department, University of Maryland, College Park, MD, 20742, USA

    John Horty

Authors
  1. Roberto Ciuni
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Horty
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Roberto Ciuni .

Editor information

Editors and Affiliations

  1. University of Amsterdam Inst Logic,Language & Computation, Amsterdam, The Netherlands

    Alexandru Baltag

  2. Amsterdam, The Netherlands

    Sonja Smets

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Ciuni, R., Horty, J. (2014). Stit Logics, Games, Knowledge, and Freedom. In: Baltag, A., Smets, S. (eds) Johan van Benthem on Logic and Information Dynamics. Outstanding Contributions to Logic, vol 5. Springer, Cham. https://doi.org/10.1007/978-3-319-06025-5_23

Download citation

Publish with us

Policies and ethics

Search

Navigation