Abstract
We characterize four types of agentive knowledge using a stit semantics over branching discrete-time structures. These are ex ante knowledge, ex interim knowledge, ex post knowledge, and know-how. The first three are notions that arose from game-theoretical analyses on the stages of information disclosure across the decision making process, and the fourth has gained prominence both in logics of action and in deontic logic as a means to formalize ability. In recent years, logicians in AI have argued that any comprehensive study of responsibility attribution and blameworthiness should include proper treatment of these kinds of knowledge. This paper intends to clarify previous attempts to formalize them in stit logic and to propose alternative interpretations that in our opinion are more akin to the study of responsibility in the stit tradition. The logic we present uses an extension with knowledge operators of the Xstit language, and formulas are evaluated with respect to branching discrete-time models. We also present an axiomatic system for this logic, and address its soundness and completeness.
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.
In [1] Ågotnes et al. write: “In game theory, two different terms are traditionally used to indicate lack of information: ‘incomplete’ and ‘imperfect’ information. Usually, the former refers to uncertainties about the game structure and rules, while the latter refers to uncertainties about the history, current state, etc. of the specific play of the game.”.
- 2.
Xstit was developed by Broersen in [5] on the conceptual assumption that the effects of performing an action are not instantaneous. Rather, an action that is chosen at a given moment will bring about effects only in the next.
- 3.
Observe that these definitions, coupled with the fact that histories are linearly ordered, imply that for every \(m\in T\) and \(h\in H_m\), \(\left( m^{-h} \right) ^{+h}=m\) and \(\left( m^{+h} \right) ^{-h}=m\).
- 4.
- 5.
This is related to a property that epistemic game theorists call “knowledge of one’s own action”, a feature which we will address in Sect. 3, when we compare the different interpretations of knowledge and their implications. Although it holds in this example, we do not enforce it in all BDT frames.
- 6.
In [15] (p. 1320), Remark 2.6 actually states that the authors do not intend for agents to consider all their available choices epistemically possible in the ex ante sense, but this leads precisely into having choice-dependent ex ante knowledge.
- 7.
We still want to allow for situations in which agents do not always have certainty about the actions that they choose even after choosing them. As will be seen later, this distinguishes our interpretation of ex interim knowledge from epistemic game theory’s traditional one.
- 8.
Formally, \(\mathcal {M}, \langle m,h\rangle \,\models \, [\alpha \ kstit]\varphi \) iff for every \(\langle m',h'\rangle \) such that \(\langle m, h\rangle \sim _\alpha \langle m',h'\rangle \), \(Exn_{m'}(Lbl^\alpha (\langle m,h\rangle ))\subseteq |\varphi |^{m'}\), where \(Lbl_\alpha \) is a function that maps a situation to the action type of the action token being performed at that situation, and \(Exn_{m'}\) is a partial function that maps types to their corresponding tokens at moment \(m'\).
- 9.
Horty & Pacuit’s models satisfy the following constraint: if \(\langle m, h\rangle \sim _\alpha \langle m',h'\rangle \), then \(\langle m,h_*\rangle \sim _\alpha \langle m',h'_*\rangle \) for every \(h_*\in H_m\), \(h'_*\in H_{m'}\), which, under reflexivity of \(\sim _\alpha \), corresponds syntactically to the axiom schema \(\mathcal {K}_\alpha \varphi \rightarrow \square \varphi \).
- 10.
To see how this constraint thwarts an analysis of the interaction between knowledge and action, consider our Example 1, and assume that at moment \(m_4\), for instance, we want to say that luther knows in some sense –not in an ex ante or ex interim sense, though– what benji will choose. Therefore, luther should in principle be able to somehow distinguish \(h_9\) from \(h_{12}\), and \(h_{10}\) from \(h_{11}\). However, in presence of \((\mathtt {OAC})\), this cannot be the case (see [8] (Chap. 3) for a more elaborate discussion about the undesirability of this property in epistemic stit).
- 11.
In all the treatments of game knowledge that we presently review, virtually nobody disagrees with some version of this constraint. In the case of the approaches from game theory, ATL, and Coalition Logic, the premise is very much related to the concept of ‘uniform strategies’. We will address it further when analyzing versions of know-how. It is worth mentioning that Lorini et al. remain vague about the subject. The examples they present all presuppose the condition, but they do not demand it explicitly or even refer to it. If they were to enforce it, it would bring the same technical problem as in Horty and Pacuit’s [13].
- 12.
Duijf does not demand for his models to validate \((\mathtt {OAC})\). However, as we will point out when addressing his formalization of know-how, Duijf does enforce a constraint corresponding to Horty & Pacuit’s \((\mathtt {UAAT})\).
- 13.
Comparing our version with Duijf’s, we observe that we exclude situations where agents can know ex interim that other agents will see to it that \(\varphi \) in the next moment without it being settled that \(\varphi \) will hold in the next moment, while we had seen he does not. \(K_\alpha [\alpha ]^X Y [\beta ]^X\varphi \rightarrow \square X\varphi \) is valid with respect to the class of our frames.
- 14.
Other interesting cases appear in the non-actual situations where the bombs were defused. In Example 1(a), for instance, if we take \(f_B\) to denote the proposition ‘the fail-safe mechanism of bomb B has been activated’, then \(\mathcal {M},\langle m_4, h_9 \rangle \,\models \, \lnot K_{luther/benji} (Y [ethan]^X f_B)\) and \(\mathcal {M},\langle m_4, h_9 \rangle \,\models \, X \ K_{luther/benji} \ Y \ [Ags]^X (Y \ Y [ethan]^X f_B)\) (luther and benji realize ex post that ethan secured the detonator for bomb B). Observe that, contrary to Lorini et al.’s formalization, ours does account for cases where an agent knows ex post that it brought about \(\varphi \) without knowing ex interim that it would bring about \(\varphi \): \( X \ K_\alpha \ Y \ [Ags]^X Y[\alpha ]^X \varphi \rightarrow K_\alpha [\alpha ]^X \varphi \) is not valid with respect to our frames.
- 15.
According to [8], in [9] Fantl draws the outlines of know-how by distinguishing it from two other kinds of knowledge: knowledge by acquaintance and propositional knowledge (know-that). Setting aside for the moment the concept of knowledge by acquaintance, [8] proposes that the essential difference between know-how and know-that lies in the content they take. We side by this interpretation, where procedural knowledge concerns actions, and propositional knowledge concerns propositions. Such a disambiguation identifies the concept of know-how that we study with Wang’s goal-directed know-how. This is related to the debate introduced by Ryle [19] as to whether know-how can be reduced to know-that or not, where intellectualists think it can be reduced and anti-intellectualists think it cannot.
- 16.
Duijf does not comment on such equivalence, whose deduction – in Duijf’s system – comes from the following argument. Turns out to be the case that the validity of
entails the validity of 
in Duijf’s logic. This last schema, denoted by \((Unif-H)\), is the syntactic counterpart of a condition that we call ‘uniformity of historical possibility’, and in light of it we have that
The other direction is straightforward, by axiom (T) for
. A similar deduction can be provided to ensure that Herzig & Troquard’s \(\square [\alpha \ Kstit]\Diamond [\alpha \ Kstit]\varphi \) is reducible to \(\Diamond [\alpha \ Kstit]\varphi \). - 17.
We observe that if we were to incorporate a condition of uniformity of available actions into our logic (as we do in the axiomatization), it would be equivalent to the semantic condition known as ‘uniformity of historical possibility’ \((\mathtt {Unif-H})\), which says that for every situation \(\langle m_*,h_*\rangle \), if \(\langle m_*, h_*\rangle \sim _\alpha \langle m, h\rangle \) for some \(\langle m,h\rangle \), then for every \(h_*'\in H_{m_*}\) there exists \(h'\in H_m\) such that \(\langle m_*, h_*'\rangle \sim _\alpha \langle m, h'\rangle \). Under this condition, which corresponds syntactically to the schema \(\Diamond K_\alpha \varphi \rightarrow K_\alpha \Diamond \varphi \), we would have two important consequences: our formula for ex ante knowledge would be equivalent to \(\square K_\alpha X\varphi \), and our formula for know-how would be equivalent to \(\Diamond K_\alpha [\alpha ]^X \varphi \).
- 18.
Although we focus our comparisons on the previous work within epistemic stit, it is worth discussing some of the approaches to the concept in the epistemic extensions of ATL and Coalition Logic (see [1, 11]), for the ideas behind the syntax and semantics for know-how in these logics are similar to those of stit. For instance, Naumov and Tao and Ågotnes et al. – in [17] and [1], respectively – share many intuitions with Horty and Pacuit. The notion of know-how they both formalize is characterized by the statement that an agent knows how to bring about \(\varphi \) at a given state s iff there exists a ‘strategy’ a such that in all states that are epistemically indistinguishable to s for the agent, ‘strategy’ a will lead to states at which \(\varphi \) holds. In other words, an agent knows how to do something if there exists a way for the agent to knowingly enforce \(\varphi \). [17] and [1] use different interpretations for the word ‘strategy’. While in the former the authors refer to an action label in single-step transitions, Ågotnes et al. use the term as is done in ATL, where strategies are functions that assign to each agent and state a pertinent transition. Regardless of the difference, their formalization of know-how depends on the same reasoning: an agent would know how to do \(\varphi \) iff there exists a uniform strategy such that at all epistemically indistinguishable states, the transition assigned by the strategy leads to a state at which \(\varphi \) holds. In both accounts, we face again the idea of uniformity.
entails the validity of 
in Duijf’s logic. This last schema, denoted by 
. A similar deduction can be provided to ensure that Herzig & Troquard’s References
Ågotnes, T., Goranko, V., Jamroga, W., Wooldridge, M.: Knowledge and ability. In: van Ditmarsch, H., Halpern, J., van der Hoek, W., Kooi, B. (eds.) Handbook of Epistemic Logic, pp. 543–589. College Publications (2015)
Aumann, R.J., Dreze, J.H.: Rational expectations in games. Am. Econ. Rev. 98(1), 72–86 (2008)
Belnap, N., Perloff, M., Xu, M.: Facing the Future: Agents and Choices in Our Indeterminist World. Oxford University Press, Oxford (2001)
Boudou, J., Lorini, E.: Concurrent game structures for temporal STIT logic. In: Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, pp. 381–389. International Foundation for Autonomous Agents and Multiagent Systems (2018)
Broersen, J.: A complete STIT logic for knowledge and action, and some of its applications. In: Baldoni, M., Son, T.C., van Riemsdijk, M.B., Winikoff, M. (eds.) DALT 2008. LNCS, vol. 5397, pp. 47–59. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-540-93920-7_4
Broersen, J.: Deontic epistemic STIT logic distinguishing modes of mens rea. J. Appl. Log. 9(2), 137–152 (2011)
Broersen, J., Ramírez Abarca, A.I.: Formalising oughts and practical knowledge without resorting to action types. In: Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, pp. 1877–1879. International Foundation for Autonomous Agents and Multiagent Systems (2018)
Duijf, H.: Let’s do it!: collective responsibility, joint action, and participation. Ph.D. thesis, Utrecht University (2018)
Fantl, J.: Knowing-how and knowing-that. Philos. Compass 3(3), 451–470 (2008)
Herzig, A., Troquard, N.: Knowing how to play: uniform choices in logics of agency. In: Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems, pp. 209–216. ACM (2006)
van der Hoek, W., Wooldridge, M.: Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications. Stud. Logica. 75(1), 125–157 (2003)
Horty, J.: Epistemic oughts in STIT semantics. In: Deontic Logic and Normative Systems. Proceedings of DEON 2018, pp. 157–176 (2016)
Horty, J., Pacuit, E.: Action types in STIT semantics. Rev. Symb. Log. (2017, forthcoming)
Lorini, E.: Temporal logic and its application to normative reasoning. J. Appl. Non-Class. Log. 23(4), 372–399 (2013)
Lorini, E., Longin, D., Mayor, E.: A logical analysis of responsibility attribution: emotions, individuals and collectives. J. Log. Comput. 24(6), 1313–1339 (2014)
Naumov, P., Tao, J.: Coalition power in epistemic transition systems. In: Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, pp. 723–731. International Foundation for Autonomous Agents and Multiagent Systems (2017)
Naumov, P., Tao, J.: Together we know how to achieve: an epistemic logic of know-how. arXiv preprint arXiv:1705.09349 (2017)
Payette, G.: Decidability of an Xstit logic. Stud. Logica. 102(3), 577–607 (2014)
Ryle, G.: The Concept of Mind. Routledge, Abingdon (2009)
Schwarzentruber, F.: Complexity results of STIT fragments. Stud. Logica. 100(5), 1001–1045 (2012)
Van De Putte, F., Tamminga, A., Duijf, H.: Doing without nature. In: Baltag, A., Seligman, J., Yamada, T. (eds.) LORI 2017. LNCS, vol. 10455, pp. 209–223. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-55665-8_15
Wang, Y.: A logic of knowing how. In: van der Hoek, W., Holliday, W.H., Wang, W. (eds.) LORI 2015. LNCS, vol. 9394, pp. 392–405. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48561-3_32
Xu, M.: Combinations of STIT with ought and know. J. Philos. Log. 44(6), 851–877 (2015). https://doi.org/10.1007/s10992-015-9365-7. http://dx.doi.org/10.1007/s10992-015-9365-7
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Abarca, A.I.R., Broersen, J. (2020). Stit Semantics for Epistemic Notions Based on Information Disclosure in Interactive Settings. In: Soares Barbosa, L., Baltag, A. (eds) Dynamic Logic. New Trends and Applications. DALI 2019. Lecture Notes in Computer Science(), vol 12005. Springer, Cham. https://doi.org/10.1007/978-3-030-38808-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-030-38808-9_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-38807-2
Online ISBN: 978-3-030-38808-9
eBook Packages: Computer ScienceComputer Science (R0)