Abstract
We propose a refinement of STIT logic to make it suitable to model causal agency and responsibility in basic multi-agent scenarios in which agents can interfere with one another. We do this by supplementing STIT semantics, first, with action types and, second, with a relation of opposing between action types. We exploit these novel elements to represent a test for potential causation, based on an intuitive notion of expected result of an action, and two tests for actual causation from the legal literature, i.e., the but-for and the NESS tests. We then introduce three new STIT operators modeling corresponding notions of causal responsibility, which we call potential, strong, and plain responsibility, and use them to provide a fine-grained analysis of a number of case studies involving both individual agents and groups.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The selection of the relevant context is similar to the process of choosing the variables constituting a causal model (see, e.g., [16]). As it is not always straightforward to decide which variables should be included in a causal model (and which values they should take), in the same way it is not always straightforward to decide which agents and actions should be included in the relevant context. In modeling case studies in Sect. 4 we will presuppose that the relevant context has been identified, without attempting to pinpoint the criteria leading to this identification—but see [15] for more on this issue.
- 2.
The need to introduce action types in STIT logic is already emphasized in [31] and, more recently, in [3]; the same need is expressed by [20] in relation to the problem of modeling uniform strategies in STIT. In the last decade, several authors, including [11, 21, 24, 32, 34, 40, 41], have taken up this challenge. Our semantics is inspired by these proposals and, in particular, by [21]. From a more philosophical perspective, a detailed analysis of ontology of action against the backdrop of STIT theory can be found, e.g., in [35].
- 3.
As we will make precise below, joint action types are combinations of individual action types, and their execution coincides with the simultaneous execution of all individual types constituting them. Joint action types are thus the most elementary kind of group actions: they require neither a cohesive group nor coordinated actions.
- 4.
The question naturally arises whether there is a limit to the specification of types: can we admit all of, e.g., Alice’s shooting, Alice’s shooting David, Alice’s shooting David with a rifle, Alice’s shooting David with a rifle while stepping back, and so on, as action types? We assume a minimal view on these matters: the only thing we require is that action types, unlike action tokens, are repeatable, i.e., they can be executed in different places and/or times. Given that this requirement is satisfied, the choice to refer to a more or to a less specific type depends on which details of the considered situation we take to be relevant. Of course assuming this minimal view may raise the worry that it gives the modeler too much flexibility, and that some general criteria to be followed in the modeling practice should be laid down. We leave a more in-depth discussion of this issue to another venue. Thanks to an anonymous referee for raising this point.
- 5.
- 6.
It is by performing simple tests of this kind that we expect, for instance, that the man’s walking towards the exit results in him being out of the building, that the kid’s throwing a rock against the window results in the window’s being broken, that Alice’s poisoning David’s water results in David’s death, and so on.
- 7.
Note that hindering is weaker than blocking: in our view, it is possible that two actions, one opposing the other, are executed at the same time without the opposed action being blocked. So, in Example 3(a), Alice’s pushing the trolley and Beth’s pushing in the opposite direction can be executed at the same time without Beth necessarily being stopped.
- 8.
Although the types in these (and later) examples are quite specific, note that they are still types: a situation in which Alice pushes a trolley and Beth pushes it in the opposite direction is a type of situation that can occur at different times and in different places (cf. fn. 4 on this.)
- 9.
See [25] for a recent overview and discussion.
- 10.
The acronym “NESS” stands for “necessary element of a sufficient set”. The NESS test is closely related, in philosophy, to Mackie’s INUS account [27, 28] (“INUS” stands for “insufficient but necessary part of an unnecessary but sufficient condition”) and, in the law, to Hart’s and Honoré’s “causally relevant factor” account [18]. This test is implicit in Belnap’s notion of strict joint agency [1] and has recently been given a game-theoretic formulation and used to analyze responsibility in voting contexts in [5,6,7].
- 11.
Note that we do not rule out the possibility that \( \mathbf {Exe_{\mathbf {IA}}}(m) \ne \mathbf {IA}\), in accordance with the intuition that the execution of an action typically requires the presence of specific preconditions.
- 12.
For simplicity, we use expressions like \( a_i \), \( \alpha (i) \), \( \alpha _I \), \( \alpha \) ambiguously as individual, joint, global actions in the semantics and as terms for individual, joint, global actions in the syntax.
- 13.
The problem of modeling continuous actions in STIT theory is considered in details by Müller [29]. Suggestions to account for continuous actions in a STIT framework supplied with action types are advanced in [34]. Due to space limitations, we cannot provide a detailed comparison between these latter proposals and our own. Suffice it to say that in our framework the use of action types is combined with a formalization of the notion of expected result (see Sect. 3.1), which is something that is left to future work in [34]. Also, as we will see in Sect. 3.3, our language is powerful enough to describe a situation in which an agent is doing something expected to result in \( \varphi \), where \( \varphi \) is not settled, which is the main desideratum set by Müller in [29].
- 14.
- 15.
It is not difficult to prove that there is a double embedding between \( \mathcal {DLA} \) and the fragment of \( \mathcal {ALO}\) defined by the axioms and rules in groups 1-4. The details are omitted for reasons of space.
- 16.
With respect to the game-theoretic representation provided in [5], our representation has the advantage of explicitly taking into account the dynamics of actions. This allows us to distinguish the states where a sufficient/necessary condition obtains (viz. where an action is initiated) from the states at which the results obtain (see also [36]).
- 17.
Note that \( \vdash _{\mathcal {ALO}} BF(\alpha _I,\varphi ) \vee NESS(\alpha _I,\varphi ) \rightarrow X\varphi \wedge \lnot \square X\varphi \) follows immediately from definitions D4 and D5. Hence \( [I\,sxstit]\varphi \) and \( [I\,cxstit]\varphi \) are stronger than \( [I\,pxstit]\varphi \). Example 4 and its variant can be used to see that the two operators are in fact strictly stronger than \( [I\,pxstit]\varphi \) and independent of one another.
- 18.
In this respect, the distinction between potential and actual cause is close to the distinction between legal and factual causation characterizing analyses of causation in criminal law [19]. While a factual cause of a fact \( \varphi \) is what we called an actual cause of \( \varphi \) (factual causation is established by applying either the but-for or the NESS test), a legal cause of \( \varphi \) is, roughly, something that, in the specific circumstances, played a substantial role in bringing about \( \varphi \). The question of what counts as “substantial” is open-ended, but, as our notion of potential cause, it aims to prune away the factors that are not relevant to the legal inquiry.
References
Belnap, N., & Perloff, M. (1993). In the realm of agents. Annals of Mathematics and Artificial Intelligence, 9(1), 25–48.
Belnap, N., Perloff, M., & Xu, M. (2001). Facing the future: Agents and choices in our indeterministic world. Oxford: Oxford University Press.
van Benthem, J., & Pacuit, E. (2014). Connecting logics of choice and change. In T. Müller (Ed), Nuel Belnap on indeterminism and free action (pp. 291–314). Cham: Springer International Publishing.
Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal logic. Cambridge Tracts in Theoretical Computer Science. Cambridge: Cambridge University Press.
Braham, M., & van Hees, M. (2009). Degrees of causation. Erkenntnis, 71(3), 323–344.
Braham, M., & van Hees, M. (2011). Responsibility voids. The Philosophical Quarterly, 61(242), 6–15.
Braham, M., & van Hees, M. (2018). Voids or fragmentation: Moral responsibility for collective outcomes. The Economic Journal, 128(612), F95–F113.
Broersen, J. M. (2009). A complete STIT logic for knowledge and action, and some of its applications. In M. Baldoni, T. C. Son, B. M. van Riemsdijk, & M. Winikoff (Eds.), Declarative agent languages and technologies VI (pp. 47–59). Berlin: Springer.
Broersen, J. M. (2011). Deontic epistemic stit logic distinguishing modes of mens rea. Journal of Applied Logic, 9(2), 137–152.
Broersen, J. M. (2011). Making a start with the stit logic analysis of intentional action. Journal of Philosophical Logic, 40(4), 499–530.
Broersen, J. M. (2014). On the reconciliation of logics of agency and logics of event types. Outstanding Contributions to Logic, 1(Krister Segerberg on Logic of Actions), 41–59.
Broersen, J. M., Herzig, A., & Troquard, N. (2006). From coalition logic to STIT. Electronic Notes in Theoretical Computer Science, 157(4), 23–35.
Ciuni, R., & Horty, J. F. (2014). Stit logics, games, knowledge, and freedom. Outstanding Contributions to Logic, 5(Johan van Benthem on Logic and Information Dynamics), 631–656.
Ciuni, R., & Mastop, R. (2009). Attributing distributed responsibility in stit logic. In X. He, J.F. Horty, & E. Pacuit (Eds.), Logic, rationality, and interaction (pp. 66–75). Berlin: Springer.
Halpern, J. Y., & Hitchcock, C. (2010). Actual causation and the art of modeling. In Causality, probability, and heuristics: A tribute to Judea Pearl, chapter 23 (pp. 383–406). London: College Publications.
Halpern, J. Y., & Pearl, J. (2005) Causes and explanations: A structural-model approach. Part II: Explanations. The British Journal for the Philosophy of Science, 56(4),889–911.
Harel, D., Kozen, D., & Tiuryn, J. (2000). Dynamic logic. MA: MIT Press.
Hart, H. L. A., & Honoré, T. (1959). Causation in the law. Oxford: Oxford University Press.
Herring, J. (2012). Criminal law: Text, cases, and material. Oxford: Oxford University Press.
Herzig, A., & Troquard, N. (2006) Knowing how to play: Uniform choices in logics of agency. In Proceedings of the 5th International Joint Conference on Autonomous Agents and Multi-agent Systems (AAMAS-06) (pp. 209–216). The Association for Computing Machinery Press.
Herzig, A., & Lorini, E. (2010). A Dynamic logic of agency I: STIT, capabilities and powers. Journal of Logic, Language and Information, 19(1), 89–121.
Horty, J. F. (2001). Agency and deontic logic.. Oxford: Oxford University Press.
Horty, J. F., & Belnap, N. (1995). The deliberative stit: A study of action, omission, ability, and obligation. Journal of Philosophical Logic, 24(6), 583–644.
Horty, J. F., & Pacuit, E. (2017). Action types in stit semantics. The Review of Symbolic Logic, 10(4), 617–637.
Lagnado, D. A., & Gerstenberg, T. (2017). Causation in legal and moral reasoning. In M. R. Waldmann (Ed.) The Oxford handbook of causal reasoning, chapter 29 (pp. 565–601). Oxford: Oxford University Press.
Lorini, E., Longin, D., & Mayor, E. (2013). A logical analysis of responsibility attribution: Emotions, individuals and collectives. Journal of Logic and Computation, 24(6), 1313–1339.
Mackie, J. L. (1965). Causes and conditions. American Philosophical Quarterly, 2(4), 245–264.
Mackie, J. L. (1974). The cement of the universe: A study of causation. Oxford: Oxford University Press.
Müller, T. (2005). On the formal structure of continuous action. In R. Schmidt, I. Pratt-Hartmann, M. Reynolds, & H. Wansing (Eds.) Advances in modal logic, volume 5 (pp. 191–209). London: King’s College Publications.
Prior, A. (1967). Past, present, and future. Oxford: Oxford University Press.
Segerberg, K. (1992). Getting started: Beginnings in the logic of action. Studia Logica, 51(3), 347–378.
Segerberg, K. (2002). Outline of a logic of action. In F. Wolter, H. Wansing, M. de Rijke, & M. Zakharyaschev (Eds.) Advances in modal logic (vol. 3, pp. 365–387). Singapore: World Scientific.
Thomason, R. H. (1970). Indeterminist time and truth-value gaps. Theoria, 36(3), 264–281.
Troquard, N., & Vieu, L. (2006). Towards a logic of agency and actions with duration. In European Conference on Artificial Intelligence 2006 (ECAI’06) (p. 775–776). IOS Press.
Trypuz, R. (2007). Formal ontology of action: A unifying approach. Ph.D. thesis, University of Trento.
von Wright, G. H. (1971). Explanation and understanding. London: Cornell University Press.
Woodward, J. (2003). Making things happen: A theory of causal explanation. Oxford: Oxford University Press.
Wright, R. W. (1988). Causation, responsibility, risk, probability, naked statistics, and proof: Pruning the bramble bush by clarifying the concepts. Iowa Law Review, 73, 1001–1077.
Wright, R. W. (2013). The NESS account of natural causation: A response to criticism. In M. Stepanians & K. Benedikt (Eds.), Critical essays on “causation and responsibility”, chapter 14 (pp. 13–66). Berlin: De Gruyter.
Xu, M. (2010). Combinations of stit and actions. Journal of Logic, Language and Information, 19(4), 485–503.
Xu, M. (2012). Actions as events. Journal of Philosophical Logic, 41(4), 765–809.
Acknowledgements
We thank the participants of the audience of the following seminars and conferences at which this paper was presented: KNAW Colloquium Reasoning in Social Contexts (Amsterdam, 2018), Trends in Logic XVIII (Milan, 2018), final PIOTR project workshop (Bayreuth, 2018), Philosophy Seminar (Utrecht, 2019), LIRa seminar (Amsterdam, 2019), CLMPST 2019 (Prague), and Logic Seminar (University of Maryland, 2019). We would also like to thank Nathan Wood and an anonymous referee for their valuable comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendix: Soundness and Completeness of \( \mathcal {ALO}\)
Appendix: Soundness and Completeness of \( \mathcal {ALO}\)
The proof that the axiom system \( \mathcal {ALO}\) is sound with respect to the class of all models for \( \mathcal {L}_{\mathcal {ALO}} \) is routine, and is thus omitted. The proof of completeness consists of two main steps: (1) we identify a class of Kripke models with respect to which \( \mathcal {ALO}\) is sound and complete; (2) we show that any formula satisfiable in a model of the identified class is also satisfiable in a model for \( \mathcal {L}_{\mathcal {ALO}} \).
Step 1 Kripke semantics for \( \mathcal {ALO}\)
Definition 6
(Kripke model for \( \mathcal {L}_{\mathcal {ALO}} \)) A Kripke model for \( \mathcal {L}_{\mathcal {ALO}} \) is a tuple \( \mathcal {M}= \left\langle {W,Ag, \mathbf {T},R_{\square },R_{X},D,O, \pi }\right\rangle \) where \( W\ne \varnothing \) is a set of possible worlds, \( Ag\) and \( \mathbf {T} \) are fixed finite sets of agents and action types, \( R_{\square } \subseteq W\times W\) is an equivalence relation on W, \( R_{X} \subseteq W \times W\) is a serial and functional relation on W, \( D: \mathbf {IA}\rightarrow \wp (W) \) intuitively assigns to every individual action the set of worlds where it is performed, \( O: \mathbf {Act}\rightarrow \wp (\mathbf {Act}) \) intuitively assigns to every action the set of actions opposing it, and \( \pi : Prop \rightarrow \wp (W) \) is a standard valuation. The functions D and \( O\) are required to satisfy the following conditions, where, for any \( I \subseteq Ag \) and \( \alpha \in \mathbf {GA}\), \( D(\alpha _I)= \bigcap _{i\in I}D(\alpha (i)) \) (and so, for any \( \alpha \in \mathbf {GA}\), \( D(\alpha )= \bigcap _{i\in Ag}D(\alpha (i)) \)).
Definition 7
(Kripke semantics) Where \( \varphi \) is a formula of \( \mathcal {L}_{\mathcal {ALO}} \), \( \mathcal {M}\) a Kripke model for \( \mathcal {L}_{\mathcal {ALO}} \), and w a world in \( \mathcal {M}\), the relation \( \mathcal {M},w\models \varphi \) of truth of \( \varphi \) at w is recursively defined by the the following conditions, where the constant \( \perp \), the propositional variables, and the Boolean connectives have the usual interpretation:
Theorem 2
The axiom system \( \mathcal {ALO}\) is sound and strongly complete with respect to the class of all Kripke models for \( \mathcal {L}_{\mathcal {ALO}} \).
The proof of soundness is routine. The proof of completeness proceeds along standard lines and exploits the possibility of building a canonical model for any given \( \mathcal {ALO}\)-consistent set of formulas. Where w is any maximal \( \mathcal {ALO}\)-consistent set (henceforth: mcs), let:
-
\( w/\square = \{ \varphi \,|\, \square \varphi \in w\}\) and \( w/X= \{ \varphi \,|\, X\varphi \in w\}\)
-
\( pos_{\triangleright }(w) = \{ \alpha _I \triangleright \beta _J \,|\, \alpha _I \triangleright \beta _J \in w \}\) and \( neg_{\triangleright }(w) = \{ \lnot ( \alpha _I \triangleright \beta _J) \,|\, \lnot ( \alpha _I \triangleright \beta _J) \in w \}\)
Lemma 1
(Lindenbaum Lemma) Every consistent set can be extended to a mcs.
Proof
Standard.
Definition 8
(Canonical model) Let \( w_0 \) be a fixed mcs. The canonical model \( \mathcal {M}\) around \( w_0 \) for \(\mathcal {ALO}\) is a tuple \( \mathcal {M}= \left\langle {W,Ag,\mathbf {T},R_{\square },R_{X},D, O, \pi }\right\rangle \), where \( W = \{w \,|\, pos_{\triangleright }(w_0)\cup \, neg_{\triangleright }(w_0) \subseteq w \}\) for w ranging over mcs, \( w R_{\square } v\) iff \( w/\square \subseteq v \), \( w R_{X} v\) iff \( w/X\subseteq v \), \( w\in D(a_i) \) iff \( do(a_i) \in w \), \( \alpha _I \in O(\beta _J) \) iff \( \alpha _I \triangleright \beta _J \in w_0\), and \( w\in \pi (p_i) \) iff \( p_i \in w \).
The proofs of the following lemmas proceed as usual and are left to the reader.
Lemma 2
For all \( w\in W \) and formula \( \varphi \) of \(\mathcal {L}_{\mathcal {ALO}} \), \( \mathcal {M},w\models \varphi \) iff \( \varphi \in w \).
Lemma 3
\( \mathcal {M}\) is a Kripke model for \( \mathcal {L}_{\mathcal {ALO}} \).
Since, by the Lindenbaum Lemma, any \( \mathcal {ALO}\)-consistent set of formulas can be extended to a mcs, Lemmas 2 and 3 imply that any \( \mathcal {ALO}\)-consistent set of formulas is satisfiable in a Kripke model for \( \mathcal {L}_{\mathcal {ALO}} \), and hence that \( \mathcal {ALO}\) is strongly complete with respect to the class of all Kripke models for \( \mathcal {L}_{\mathcal {ALO}} \).
Step 2 From Kripke models for \( \mathcal {L}_{\mathcal {ALO}} \) to models for \( \mathcal {L}_{\mathcal {ALO}} \)
Assume that \( \varphi _0 \) is \( \mathcal {ALO}\)-consistent. Then, by Theorem 2, there are a Kripke model \( \mathcal {M}\) and a world \( w_0\in \mathcal {M}\) such that \( \mathcal {M},w_0\models \varphi _0 \). We show that \( \mathcal {M}\) can be transformed into a model for \( \mathcal {L}_{\mathcal {ALO}} \) in which \( \varphi _0 \) is satisfiable. By adapting the techniques used in [21], we proceed in steps by unraveling \( \mathcal {M}\).
Step 2.1 Initial unraveling
Definition 9
(Unraveling of \( \mathcal {M}\)) Let \( \mathcal {M}'=\left\langle { W',Ag, \mathbf {T}, R'_{\square },R'_{X},D',O, \pi ' }\right\rangle \) be s.t.
-
\( W' \) is the set of all sequences \( \overrightarrow{w_{n}}= (w_1, w_2, \dots , w_n) \) s.t. \( w_1 R_{\square } w_0\) and \( w_i R_{X} w_{i+1}\), for all \(1 \le i < n \)
-
\( \overrightarrow{w_{n}} R'_{\square } \overrightarrow{v_{m}} \) iff (i) \( n = m \), (ii) \( w_{i} R_{\square } v_{i} \) for all \( 1\le i \le n \), and (iii) \( w_{i} \in D(a_i)\) iff \( v_{i} \in D(a_i)\) for all \( 1\le i < n \) and \( a_i \in \mathbf {IA}\)
-
\( \overrightarrow{w_{n}} R'_{X} \overrightarrow{v_{m}} \) iff \( \overrightarrow{v_{m}} = (\overrightarrow{w_{n}}, v_m) \) where \( w_n R_{X} v_m \)
-
\(\overrightarrow{w_{n}} \in D'(a_i) \) iff \( w_n \in D(a_i) \)
-
\(\overrightarrow{w_{n}} \in \pi '(p) \) iff \( w_n \in \pi (p) \)
Proposition 3
If \( \overrightarrow{w_n} \in W' \) and \( w_n R_{\square } v \), then there is \( \overrightarrow{v_n}\in W' \) s.t. \( v_n = v \) and \( \overrightarrow{w_n} R_{\square } \overrightarrow{v_n} \).
Proof
Immediate from Definition 9, since \( \mathcal {M}\) satisfies condition D3.
The following proposition follows straightforwardly from Definition 9.
Proposition 4
\( \mathcal {M}' \) is a Kripke model for \( \mathcal {L}_{\mathcal {ALO}} \).
Theorem 3
Let \( f: W' \rightarrow W \) be the mapping defined by setting: for all \( \overrightarrow{w_n} \in W' \), \( f(\overrightarrow{w_n}) = w_n \). Then, for all \( \overrightarrow{w_n}\in W' \), \( \mathcal {M}', \overrightarrow{w_n} \models \varphi \) iff \( \mathcal {M}, f( \overrightarrow{w_n}) \models \varphi \).
Proof
It suffices to show that the map \( f: W' \rightarrow W \) such that \( f(\overrightarrow{w_{n}}) = w_n\), for all \( \overrightarrow{w_n} \in W'\) defines a bounded morphism from \( \mathcal {M}' \) to \( \mathcal {M}\) (see [4]). Specifically, letting \( R_{\otimes } \) be either \( R_{\square } \) or \( R_{X} \), we need to check that
-
(1)
if \( \overrightarrow{w_n} R'_{\otimes } \overrightarrow{v_m} \), then \( f(\overrightarrow{w_n} ) R_{\otimes } f( \overrightarrow{v_m}) \)
-
(2)
if \( f(\overrightarrow{w_n} ) R_{\otimes } v_m \), then there is \( \overrightarrow{u_k} \in W' \) s.t. \( f(\overrightarrow{u_k}) = v_m \) and \( \overrightarrow{w_n} R'_{\otimes } \overrightarrow{u_k} \)
-
(3)
\( \overrightarrow{w_n} \in D'(a_i) \) iff \( f(\overrightarrow{w_n}) \in D(a_i) \)
-
(4)
\( \overrightarrow{w_n} \in \pi '(p) \) iff \( f(\overrightarrow{w_n}) \in \pi (p) \)
The proof follows immediately from Definition 9 in all cases, except in case (2) when \( \otimes \) is \( \square \). But this case coincides with Proposition 3.
Corollary 1
\(\mathcal {M}', \overrightarrow{w_0} \models \varphi _0 \)
Step 2.2 Divide histories in \(\mathcal {M}' \) that remain undivided
Definition 10
Let \( ND(\varphi _0) \) be the maximum degree of nested \( X\) operators in \( \varphi _0 \) and \( \mathcal {M}''= \left\langle {W',Ag, \mathbf {T}, R''_{\square },R'_{X},D',O, \pi ' }\right\rangle \), where
\( \overrightarrow{w_n} R''_{\square } \overrightarrow{v_m} \text { iff } {\left\{ \begin{array}{ll} \overrightarrow{w_n} R'_{\square } \overrightarrow{v_m} &{} \text {if } n \le ND(\varphi _0) \\ \overrightarrow{w_n} = \overrightarrow{v_m} &{} \text {if } ND(\varphi _0) < n \\ \end{array}\right. } \)
It is immediate to check that \( \mathcal {M}'' \) is still a Kripke model for \( \mathcal {L}_{\mathcal {ALO}} \). The following proposition follows straightforwardly from Theorem 3 and from the fact that sequences equivalent in \( \mathcal {M}' \) are separated only at an \( R'_{X} \)-depth that is higher than the maximum degree of nesting of \( X\) operators in \( \varphi _0 \).
Proposition 5
\( \mathcal {M}'',\overrightarrow{w_0}\models \varphi _0 \).
For any sequence \( \sigma \), let \( last(\sigma )\) be the last element of \( \sigma \).
Definition 11
(History in \( \mathcal {M}'' \)) A history in \(\mathcal {M}'' \) is a function \( h: \mathbb {N} \rightarrow W' \) such that (i) \( h(1) R''_{\square } \overrightarrow{w_0} \) and (ii) \( h(n+1) = (h(n), v) \) where \( last(h(n))R_{X} v\). The set of all histories in \( \mathcal {M}'' \) is denoted with Hist.
The following proposition follows from Definitions 10 and 11.
Proposition 6
For every \( \overrightarrow{w_n} \in W''\) there is a unique history h s.t. \( h(n) = \overrightarrow{w_n} \).
We will denote with \( h_{\overrightarrow{w_n}} \) the unique history associated with \( \overrightarrow{w_n} \).
Step 2.3 Transform \( \mathcal {M}'' \) in a model for \( \mathcal {L}_{\mathcal {ALO}} \)
We start by defining a DBT structure based on \( \mathcal {M}'' \). For any \( \overrightarrow{w_n} \in W'\), let \( [ \overrightarrow{w_n}] \) be the equivalence class of \( \overrightarrow{w_n} \) under \( R''_{\square } \).
Definition 12
(DBT structure based on \( \mathcal {M}'' \)) Define \(\mathcal {T}= \left\langle Mom,<\right\rangle \) so that
-
\( Mom = \{ [\overrightarrow{w_n}] \,|\, n\in \mathbb {N} \text { and } \overrightarrow{w_n} \in W' \} \)
-
\( [\overrightarrow{w_n}] < [\overrightarrow{v_m}] \) iff \( n < m \) and all prefixes of length n of sequences in \( [\overrightarrow{v_m}] \) are in \( [\overrightarrow{w_n}] \)
It is not difficult to check that \( \mathcal {T} \) is a DBT structure. For any \( \overrightarrow{w_n}\in W' \), let \( \mathbf {X}(\overrightarrow{w_{n}}) \) be the unique successor of \( \overrightarrow{w_n} \) along \( R'_{X} \).
Definition 13
(History in \( \left\langle Mom,<\right\rangle \)) A history \( h^* \) in \( \mathcal {T} \) is a function \( h^*: \mathbb {N} \rightarrow Mom \) s.t. (i) \( h^*(1) = [\overrightarrow{w_0}] \) and (ii) \( h^*(n+1) = [\mathbf {X}(\overrightarrow{w_{n}}) ]\) for some \( \overrightarrow{w_n} \in h^*(n)\). The set of all histories in \( \left\langle Mom,<\right\rangle \) is denoted with \( Hist^* \).
It is immediate to see that the following pair of functions define a one-to-one correspondence between the set of histories in \( \mathcal {M}'' \) and the set of histories in \( \mathcal {T} \):
-
\( \gamma : Hist \rightarrow Hist^* \) is s.t. \( \gamma _h(n)= [h(n)] \) for all \( n \in \mathbb {N}\)
-
\( \beta : Hist^* \rightarrow Hist \) is s.t. \( \beta _{h^*}(n) \in h^*(n) \) for all \( n \in \mathbb {N}\)
Given a moment \([\overrightarrow{w_n}] \in Mom\) and a history \( h^* \in Hist^*\), \( h^* \) passes through m iff there is \( n\in \mathbb {N} \) s.t. \( h^*(n)=[ \overrightarrow{w_n}] \). The set \( S([\overrightarrow{w_n}]) \) of successors of \( [\overrightarrow{w_n}] \) is the set of equivalence classes \( [\overrightarrow{v_{n+1}}] \in Mom\) s.t. \( [\overrightarrow{w_n}] \) contains the prefixes of length n of all sequences in \( [\overrightarrow{v_{n+1}}] \). A transition is any pair \( \tau = ([\overrightarrow{w_n}], [\overrightarrow{v_{n+1}}]) \) s.t. \( [\overrightarrow{v_{n+1}}] \in S([\overrightarrow{w_n}])\).
Definition 14
(Model for \( \mathcal {L}_{\mathcal {ALO}} \) based on \( \mathcal {M}'' \)) Let \( M= \left\langle {\mathcal {T}, Ag,\mathbf{T} , Act, \mathbf {O},V}\right\rangle \) be s.t. \( \mathcal {T} \) is as in Definition 12, \( Ag\) and \( \mathbf{T} \) are as in \( \mathcal {M}'' \), \( \mathbf {O}= O\), and the functions \( Act : Tr \rightarrow \mathbf {GA}\) and \(V: Prop \rightarrow \wp (Ind)\) are defined as follows:
-
\( Act(([\overrightarrow{w_n}], [\overrightarrow{v_{n+1}}])) = \alpha \) iff \( \overrightarrow{v_{n}} \in D''(\alpha )\)
-
\( [\overrightarrow{w_n}]/h^*\in V(p_i) \) iff \( \beta _{h^*}(n) \in \pi ''(p_i) \)
Observe that the functions Act is well defined. Specifically:
-
1.
If \( [\overrightarrow{v_{n+1}}] = [\overrightarrow{u_{n+1}}] \), then \( Act([\overrightarrow{w_n}], [\overrightarrow{v_{n+1}}])= Act([\overrightarrow{w_n}], [\overrightarrow{u_{n+1}}])\). In fact, if \( \overrightarrow{v_{n+1}}R_{\square }'' \overrightarrow{u_{n+1}} \), then, by the definition of \( R_{\square }'' \), \( \overrightarrow{v_n}\in D''(\alpha ) \) iff \( \overrightarrow{u_n}\in D''(\alpha ) \).
-
2.
For any transition \( \tau = ([\overrightarrow{w_n}], [\overrightarrow{v_{n+1}}]) \), there is \( \alpha \in \mathbf {GA}\) s.t. \( v_n \in D''(\alpha ) \). This is an immediate consequence of condition D1.
-
3.
For any transition \( \tau = ([\overrightarrow{w_n}], [\overrightarrow{v_{n+1}}]) \), there is a unique \( \alpha \in \mathbf {GA}\) s.t. \( v_n \in D''(\alpha ) \). This is an immediate consequence of condition D2.
The proof of the following proposition is routine.
Proposition 7
\( M\) is a model for \( \mathcal {L}_{\mathcal {ALO}} \).
Given Proposition 5, the following proposition ensures that \( \varphi _0 \) is satisfiable in \( M\).
Proposition 8
For all formulas \( \varphi \) of \( \mathcal {L}_{\mathcal {ALO}} \) and world \( \overrightarrow{w_n} \) in \( \mathcal {M}'' \), \( \mathcal {M}'', \overrightarrow{w_n} \models \varphi \) iff \( M, [\overrightarrow{w_n}]\ \gamma _{h_{\overrightarrow{w_n}}} \models \varphi \).
Proof
The proof is by induction on the complexity of \( \varphi \). We only prove the cases (1) \( \varphi = X\psi \) and (2) \( \varphi = do(a_i)\). The case in which \( \varphi =\alpha _I \triangleright \beta _J \) is straightforward because the semantics of \( \alpha _I \triangleright \beta _J \) does not depend on the index at which the formula is evaluated and because \( \mathbf {O}= O''\).
Since \( \mathcal {M}'', \overrightarrow{w_0} \models \varphi _0 \), Proposition 8 implies that \( M, [\overrightarrow{w_0}]/ \gamma _{h_{\overrightarrow{w_0}}} \models \varphi _0 \). Hence, any proposition satisfiable in a Kripke model for \( \mathcal {L}_{\mathcal {ALO}} \) is satisfiable in a model for \( \mathcal {L}_{\mathcal {ALO}} \). Given Theorem 2, this ensures that any \( \mathcal {ALO}\)-consistent sentence is satisfiable in a model for \( \mathcal {L}_{\mathcal {ALO}} \). Thus, \( \mathcal {ALO}\) is weakly complete with respect to the class of all models for \( \mathcal {L}_{\mathcal {ALO}} \).
Rights and permissions
Copyright information
© 2021 The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Baltag, A., Canavotto, I., Smets, S. (2021). Causal Agency and Responsibility: A Refinement of STIT Logic. In: Giordani, A., Malinowski, J. (eds) Logic in High Definition. Trends in Logic, vol 56. Springer, Cham. https://doi.org/10.1007/978-3-030-53487-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-53487-5_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-53486-8
Online ISBN: 978-3-030-53487-5
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)