STIT logic

Short description: Family of modal logics for agency and choice

STIT logic (from seeing to it that) is a family of modal and branching-time logics for reasoning about agency and choice. A typical STIT operator has the form [i stit:φ], usually read as "agent i sees to it that φ", and is interpreted in models where agents choose between alternative possible futures.[1][2]

STIT logics are used in action theory, deontic logic, epistemic logic, and the theory of intelligent agents to formalise notions such as "could have done otherwise", responsibility, joint action, and strategic ability in an indeterministic world.[3][4]

## Contents

* 1 Etymology
* 2 History
* 3 Branching-time semantics
* 4 Chellas and deliberative STIT operators
* 5 Group agency and joint action
* 6 Deontic and normative STIT
* 7 Temporal and epistemic extensions
* 8 Relationships to other logics
* 9 Applications
* 9.1 Philosophy
* 9.2 Computer science and artificial intelligence
* 10 See also
* 11 References
* 12 Further reading
* 13 External links

## Etymology

The acronym STIT comes from the English phrase "seeing to it that", introduced in influential work by Nuel Belnap and Michael Perloff on the logical analysis of agentive expressions.[5] In this tradition, "to see to it that φ" is treated as a primitive agency operator, rather than being reduced to ordinary modal necessity.

## History

Modern STIT logic arose in the 1980s in the context of branching-time semantics and formal theories of agency. Belnap and Perloff's article "Seeing to it that: A canonical form for agentives" introduced the idea of treating expressions of the form "agent i sees to it that φ" as a primitive modal operator, and analysed such sentences using a branching tree of moments and histories.[5] This approach was further developed in a series of papers on indeterminism and agency and provided the conceptual core for later STIT formalisms.[1][6]

In the 1990s the basic formal systems of STIT logic were worked out. Horty and Belnap's influential paper on the deliberative STIT operator distinguished between a "Chellas" STIT that merely records the result of an agent's present choice and a "deliberative" STIT that requires the agent's choice to make a difference, and connected STIT with issues of action, omission, ability and obligation.[7] Around the same time, Ming Xu proved completeness and decidability results for basic STIT systems, including a single-agent logic with Kripke-style semantics and axiomatizations for multi-agent deliberative STIT, thereby establishing STIT as a well-behaved normal modal framework.[8][9]

This early work was systematised in Belnap, Perloff and Xu's monograph Facing the Future: Agents and Choices in Our Indeterminist World, which presents a general branching-time semantics for individual and group STIT operators, discusses independence-of-agents conditions and articulates the metaphysical picture of an indeterministic "tree" of moments.[1][6] At roughly the same time, Horty's book Agency and Deontic Logic developed deontic STIT logics in which obligations are tied to agents' available choices rather than to static states of affairs, and used the resulting systems to analyse "ought implies can", contrary-to-duty obligations and deontic paradoxes.[4][10] These works helped to position STIT at the intersection of action theory, temporal logic and deontic logic.

From the late 1990s and 2000s onward, STIT logics were combined with epistemic, temporal and strategic modalities. Broersen introduced complete STIT logics for knowledge and action and deontic-epistemic STIT systems that distinguish different modes of mens rea, with applications to responsibility and the specification of multi-agent systems.[11][12] Work on group and coalitional agency investigated axiomatisations and complexity results for group STIT logics,[13] and related STIT-based analyses of agency to coalition logic and alternating-time temporal logic (ATL) by exhibiting formal embeddings between the frameworks.[14][15][16]

Explicit temporal operators were added to STIT in so-called temporal STIT logics. Lorini proposed a temporal STIT with "next" and "until" operators along histories and showed how it can be applied to normative reasoning about ongoing behaviour and commitments.[17] Ciuni and Lorini compared different semantics for temporal STIT, clarifying the relationships between branching-time, game-based and epistemic approaches,[18] while Boudou and Lorini gave a semantics for temporal STIT based on concurrent game structures, thus strengthening links with standard models of multi-agent interaction used for ATL and strategy logic.[19] In parallel, complexity-theoretic work by Balbiani, Herzig and Troquard and by Schwarzentruber and co-authors investigated the satisfiability and model-checking problems for various STIT fragments, showing for instance that many expressive group STIT logics are undecidable or of high computational complexity.[20][21]

In the 2010s, STIT ideas were combined with justification logic, imagination operators and refined deontic notions. Justification STIT logics, developed by Olkhovikov and others, merge explicit justifications with STIT-style agency so that producing a proof can itself be treated as an action that brings about knowledge, and they come with completeness and decidability results.[22] Olkhovikov and Wansing introduced STIT imagination logics, together with axiomatic systems and tableau calculi, to model acts of voluntary imagining and their role in doxastic control.[23][24] Other authors have proposed STIT-based logics of responsibility, blameworthiness and intentionality for use in philosophical and AI settings.[25][26][27] Xu's survey article "Combinations of STIT with Ought and Know" (2015) reviews many of these developments and emphasises the interplay between deontic and epistemic STIT logics.[28]

Current research on STIT focuses on proof theory, automated reasoning and richer expressive resources. Lyon and van Berkel, building on earlier work on labelled calculi for STIT, have developed cut-free sequent systems and proof-search algorithms that yield syntactic decision procedures for a range of deontic and non-deontic multi-agent STIT logics and support applications such as duty checking and compliance checking in autonomous systems.[29] Sawasaki has proposed first-order cstit-based STIT logics that can distinguish de re and de dicto readings of agency statements and has proved strong completeness results for Hilbert systems over finite models, moving the STIT programme beyond the purely propositional level.[30] Further work investigates interpreted-system and computationally grounded semantics for STIT and its extensions in order to model the behaviour of autonomous agents in multi-agent settings, and proposes STIT-based semantics for epistemic notions based on patterns of information disclosure in interactive systems.[31][32]

## Branching-time semantics

STIT logics are usually interpreted over branching-time models. A standard STIT frame consists of:[1][2]

* a non-empty set of moments T, partially ordered by < so that (T,<) forms a tree (every pair of moments with a common predecessor has a greatest lower bound);
* a set of histories, each history being a maximal linearly ordered subset of T;
* a non-empty set of agents Ag;
* for each agent i∈Ag and moment m, a choice function choiceim that partitions the set of histories passing through m into choice cells.

The idea is that a moment represents a time at which choices are made, and histories represent complete possible future courses of events. At each moment, each agent's choice corresponds to selecting one of the available cells of histories determined by their choice function.

Formulas are evaluated at pairs (m,h) of a moment and a history through that moment (sometimes written m/h). A valuation assigns truth-values to atomic propositions at such indices; Boolean connectives are interpreted pointwise as in Kripke-style modal logic.[1]

## Chellas and deliberative STIT operators

Several STIT operators have been distinguished in the literature. A common approach uses two closely related operators, often called Chellas STIT and deliberative STIT.[1][9]

Let Hm be the set of histories passing through a moment m, and write Hm ⟦φ⟧m={h∈Hm∣M,m/h⊨φ} for the set of histories at m where φ holds.

* The Chellas STIT operator, often written [i cstit:φ], is given by

M,m/h⊨[i cstit:φ]iffchoiceim(h)⊆⟦φ⟧m.
Intuitively, agent i sees to it that φ if φ holds at all histories compatible with their present choice.

* The deliberative STIT operator, [i dstit:φ], adds a "non-triviality" or "negative" condition:

M,m/h⊨[i dstit:φ] iff M,m/h⊨[i cstit:φ] and φ is not already historically necessary at m (i.e. fails at some history through m).[9]

To express the latter, a historic necessity operator ◻H is often defined by

M,m/h⊨◻Hφifffor all h′∈Hm,M,m/h′⊨φ.

On this basis, Chellas and deliberative STIT become interdefinable by:

[i dstit:φ]↔([i cstit:φ]∧¬◻Hφ),
[i cstit:φ]↔([i dstit:φ]∨◻Hφ).[1]

Ming Xu proved completeness results and axiomatizations for basic dstit logics with single and multiple agents, establishing STIT as a well-behaved modal system.[9][2]

## Group agency and joint action

STIT models naturally support notions of group and collective agency. Given a set of agents G⊆Ag, a group STIT operator [G stit:φ] can be defined so that it is true exactly when the collective choices of all agents in G guarantee φ.[1] Different notions of joint agency (for instance, where all group members are essential vs. inessential participants) can be distinguished by constraints on the choice functions for groups and individuals.[1][33]

Group STIT operators have been combined with temporal and epistemic operators to study collective responsibilities, joint intentions, and coordination in multi-agent systems.[11]

## Deontic and normative STIT

STIT logic has been combined with deontic logic to model obligations and permissions that concern an agent's actions rather than mere states of affairs. John F. Horty developed a deontic STIT framework in which obligations to act are evaluated against an indeterministic branching-time background, allowing for a distinction between "ought-to-do" and "ought-to-be" and addressing classic deontic paradoxes.[4][10] See Agentive logic § John Horty's ought-to-do logic.

Subsequent work has explored deontic STIT logics for formalising contrary-to-duty obligations, prioritised norms, and policies in computational normative systems, and for connecting STIT-based notions of agency with input/output logic and other frameworks for normative reasoning.[34][35]

## Temporal and epistemic extensions

Although the original STIT systems used an implicit branching-time background, later work has combined STIT with explicit temporal operators, resulting in temporal STIT logics. These add connectives for "next", "always", or "until" along histories, allowing reasoning about what agents can ensure over time.[2][36]

Epistemic and doxastic STIT logics enrich the framework with operators for knowledge and belief, enabling analysis of "knowingly doing", informational responsibility, and strategic ignorance.[11] Justification STIT logics merge STIT with justification logic, modelling proofs or justifications as actions that result in knowledge.[35]

## Relationships to other logics

STIT logic is closely related to, but distinct from, several other modal frameworks:

* Like branching-time temporal logic, it uses tree-like models with histories, but STIT operators focus on agents' choices rather than temporal quantification alone.[2][37]
* Compared to dynamic logic, which treats actions as program-like relations between states, STIT treats actions implicitly via partitions of histories determined by agents' choices; some authors have studied embeddings and combinations of these perspectives.[1][38]
* Coalition logic and alternating-time temporal logic (ATL) analyse what groups of agents can achieve by choosing strategies; STIT's group operators are closely related and there are formal embeddings in both directions.[39][40][41]

## Applications

### Philosophy

In philosophy of action and metaphysics, STIT logics model free will, alternative possibilities, and moral responsibility in indeterministic settings. The framework has been used to articulate conditions under which agents "could have done otherwise", and to analyse the compatibility of free agency with branching-time metaphysics.[1][6]

In ethics and deontic logic, deontic STIT connects obligations with agents' available choices and abilities, providing tools to reason about "ought implies can", contrary-to-duty obligations, and practical dilemmas.[4][10] John Horty's ought-to-do logic, created for modelling agentive duties, was developed based on STIT operators.

### Computer science and artificial intelligence

In computer science and artificial intelligence, STIT-based logics contribute to the specification and verification of multi-agent systems, autonomous agents, and normative systems. Temporal-epistemic STIT logics have been proposed as specification languages for agents with knowledge, goals, and actions, and have been related to more mainstream modal logics used in model checking.[11][42]

STIT ideas have also been combined with justification and proof-theoretic formalisms to represent reasoning as an activity that produces knowledge, and to study interactions between agency and proof in formal systems.[35]

## See also

* Action theory
* Agentive logic
* Deontic logic
* Dynamic logic (modal logic)
* Epistemic logic
* Branching time
* Coalition logic
* Alternating-time temporal logic
* Dynamic epistemic logic

## References

1. ↑ 1.00 1.01 1.02 1.03 1.04 1.05 1.06 1.07 1.08 1.09 1.10 Belnap, Nuel; Perloff, Michael; Xu, Ming (2001). Facing the Future: Agents and Choices in Our Indeterminist World. Oxford: Oxford University Press. doi:10.1093/oso/9780195138788.001.0001. ISBN 978-0-19-513878-8.
2. ↑ 2.0 2.1 2.2 2.3 2.4 Goranko, Valentin (2015). "Temporal Logic". in Zalta, Edward N.. The Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/entries/logic-temporal/.
3. ↑ Segerberg, Krister (1992). "Getting started: Beginnings in the logic of action". Studia Logica 51 (3–4): 347–378. doi:10.1007/BF01028968.
4. ↑ 4.0 4.1 4.2 4.3 Horty, John F. (2001). Agency and Deontic Logic. Oxford: Oxford University Press.
5. ↑ 5.0 5.1 Belnap, Nuel; Perloff, Michael (1988). "Seeing to it that: A canonical form for agentives". Theoria 54 (3): 175–199. doi:10.1111/j.1755-2567.1988.tb00700.x.
6. ↑ 6.0 6.1 6.2 Müller, Thomas (2014). "Introduction: The many branches of Belnap's logic". in Thomas Müller. Nuel Belnap on Indeterminism and Free Action. Outstanding Contributions to Logic. 2. Cham: Springer. pp. 1–34. doi:10.1007/978-3-319-01754-9_1. ISBN 978-3-319-01753-2.
7. ↑ Horty, John F.; Belnap, Nuel (1995). "The deliberative stit: A study of action, omission, ability, and obligation". Journal of Philosophical Logic 24 (6): 583–644. doi:10.1007/BF01306968.
8. ↑ Xu, Ming (1995). "On the basic logic of STIT with a single agent". Journal of Symbolic Logic 60 (2): 459–483. doi:10.2307/2275620.
9. ↑ 9.0 9.1 9.2 9.3 Xu, Ming (1998). "Axioms for deliberative STIT". Journal of Philosophical Logic 27 (5): 505–552. doi:10.1023/A:1004288801405.
10. ↑ 10.0 10.1 10.2 McNamara, Paul (2004). "Review of John F. Horty, Agency and Deontic Logic". Notre Dame Philosophical Reviews. https://ndpr.nd.edu/reviews/agency-and-deontic-logic/.
11. ↑ 11.0 11.1 11.2 11.3 Broersen, Jan M. (2009). "A complete STIT logic for knowledge and action, and some of its applications". in Matteo Baldoni. Declarative Agent Languages and Technologies VI. Lecture Notes in Computer Science. 5422. Springer. pp. 47–59. doi:10.1007/978-3-642-03839-8_3.
12. ↑ Broersen, Jan M. (2011). "Deontic epistemic stit logic distinguishing modes of mens rea". Journal of Applied Logic 9 (2): 137–152. doi:10.1016/j.jal.2010.06.002.
13. ↑ Balbiani, Philippe; Herzig, Andreas; Troquard, Nicolas (2008). "Alternative axiomatics and complexity of deliberative STIT theories". Journal of Philosophical Logic 37 (4): 387–406. doi:10.1007/s10992-007-9078-7.
14. ↑ Pauly, Marc (2001). "Logic for social software". Journal of Applied Non-Classical Logics 11 (1–2): 135–165.
15. ↑ Alur, Rajeev; Henzinger, Thomas A.; Kupferman, Orna (2002). "Alternating-time temporal logic". Journal of the ACM 49 (5): 672–713. doi:10.1145/585265.585270.
16. ↑ Broersen, Jan M. (2006). "Embedding Alternating-time Temporal Logic in strategic STIT logic of agency". Journal of Logic and Computation 16 (5): 559–578. doi:10.1093/logcom/exl006.
17. ↑ Lorini, Emiliano (2013). "Temporal STIT logic and its application to normative reasoning". Journal of Applied Non-Classical Logics 23 (4): 372–399. doi:10.1080/11663081.2013.861302.
18. ↑ Ciuni, Roberto; Lorini, Emiliano (2018). "Comparing semantics for temporal STIT logic". Logique et Analyse (N.S.) 61 (243): 299–339.
19. ↑ Boudou, Joseph; Lorini, Emiliano (2018). "Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2018)". pp. 381–389.
20. ↑ Schwarzentruber, François (2012). "Complexity results of STIT fragments". Studia Logica 100 (5): 1001–1045. doi:10.1007/s11225-012-9445-4.
21. ↑ Schwarzentruber, François; Semmling, Caroline (2014). "Proceedings of the 21st European Conference on Artificial Intelligence (ECAI 2014)". pp. 1093–1094.
22. ↑ Olkhovikov, Grigory K. (2019). "The basics of justification STIT logic". Studia Logica 107 (4): 713–742. doi:10.1007/s11225-017-9779-z.
23. ↑ Olkhovikov, Grigory K.; Wansing, Heinrich (2018). "An axiomatic system and a tableau calculus for STIT imagination logic". Journal of Philosophical Logic 47 (2): 259–279. doi:10.1007/s10992-017-9426-1.
24. ↑ Olkhovikov, Grigory K.; Wansing, Heinrich (2019). "Simplified tableaux for STIT imagination logic". Journal of Philosophical Logic 48 (6): 981–1001. doi:10.1007/s10992-019-09503-1.
25. ↑ Baltag, Alexandru; Canavotto, Ilaria; Smets, Sonja (2020). "Causal agency and responsibility: A refinement of STIT logic". in Alessandro Giordani. Logic in High Definition: Trends in Logical Semantics. Springer. pp. 149–176.
26. ↑ Abarca, Aldo Iván Ramírez; Broersen, Jan M. (2021). "Proceedings of the Eighteenth Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2021)". 335. pp. 281–294.
27. ↑ Abarca, Aldo Iván Ramírez; Broersen, Jan M. (2022). "Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2022)". pp. 1717–1719.
28. ↑ Xu, Ming (2015). "Combinations of STIT with Ought and Know". Journal of Philosophical Logic 44 (6): 851–877. doi:10.1007/s10992-015-9365-7.
29. ↑ Lyon, Tim S.; van Berkel, Kees (2024). "Proof theory and decision procedures for deontic STIT logics". Journal of Artificial Intelligence Research 81: 837–876. doi:10.1613/jair.1.15710.
30. ↑ Sawasaki, Takahiro (2025). "Bringing De Re and De Dicto into STIT Logic". Journal of Philosophical Logic. doi:10.1007/s10992-025-09822-6.
31. ↑ Herzig, Andreas; Lorini, Emiliano; Perrotin, Eric (2022). "Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI 2022)". pp. 2648–2654. doi:10.24963/ijcai.2022/367.
32. ↑ Abarca, Aldo Iván Ramírez; Broersen, Jan M. (2021). "Stit semantics for epistemic notions based on information disclosure in interactive settings". Journal of Logical and Algebraic Methods in Programming 123. doi:10.1016/j.jlamp.2021.100708.
33. ↑ Zanardo, Alberto (2013). "Indistinguishability, choices, and logics of agency". Studia Logica 101 (2): 287–310. doi:10.1007/s11225-013-9530-3.
34. ↑ Gabbay, Dov; Horty, John F.; Parent, Xavier; van der Torre, Leendert; others (2013). Handbook of Deontic Logic and Normative Systems. London: College Publications.
35. ↑ 35.0 35.1 35.2 Olkhovikov, Grigory K. (2019). "The basics of justification STIT logic". Studia Logica 107 (4): 713–742. doi:10.1007/s11225-017-9779-z.
36. ↑ Lorini, Emiliano (2013). "Temporal STIT logic and its application to normative reasoning". Journal of Applied Non-Classical Logics 23 (4): 372–399. doi:10.1080/11663081.2013.861302.
37. ↑ Spolaore, Giuliano (2025). "Branching Time". in Zalta, Edward N.. The Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/entries/branching-time/.
38. ↑ Broersen, Jan M. (2009). "Combinations of STIT and actions". in Hinrichs. Essays in Logic and Practical Reasoning. Springer.
39. ↑ Pauly, Marc (2001). "Logic for social software". Journal of Applied Non-Classical Logics 11 (1–2): 135–165.
40. ↑ Alur, Rajeev; Henzinger, Thomas A.; Kupferman, Orna (2002). "Alternating-time temporal logic". Journal of the ACM 49 (5): 672–713. doi:10.1145/585265.585270.
41. ↑ Broersen, Jan M. (2006). "Embedding Alternating-time Temporal Logic in strategic STIT logic of agency". Journal of Logic and Computation 16 (5): 559–578. doi:10.1093/logcom/exl006.
42. ↑ Thomason, Richmond H. (2018). "Logic and Artificial Intelligence". in Zalta, Edward N.. The Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/entries/logic-ai/.

## Further reading

* Belnap, Nuel; Perloff, Michael; Xu, Ming (2001). Facing the Future: Agents and Choices in Our Indeterminist World. Oxford: Oxford University Press.
* Belnap, Nuel; Perloff, Michael (1988). "Seeing to it that: A canonical form for agentives". Theoria 54 (3): 175–199. doi:10.1111/j.1755-2567.1988.tb00717.x.
* Xu, Ming (1998). "Axioms for deliberative STIT". Journal of Philosophical Logic 27 (5): 505–552. doi:10.1023/A:1004274131669.
* Horty, John F. (2001). Agency and Deontic Logic. Oxford: Oxford University Press.
* Broersen, Jan M. (2009). "A complete STIT logic for knowledge and action, and some of its applications". in Matteo Baldoni. Declarative Agent Languages and Technologies VI. Lecture Notes in Computer Science. 5422. Springer. pp. 47–59.
* Olkhovikov, Grigory K. (2019). "The basics of justification STIT logic". Studia Logica 107 (4): 713–742. doi:10.1007/s11225-017-9779-z.
* Segerberg, Krister; Meyer, John-Jules C.; Kracht, Marcus (2016). "The Logic of Action". in Zalta, Edward N.. The Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/entries/logic-action/.

## External links

* Segerberg, Krister. "The Logic of Action". in Zalta, Edward N.. Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/entries/logic-action/.
* McNamara, Paul. "Deontic Logic". in Zalta, Edward N.. Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/entries/logic-deontic/.
* Hendricks, Vincent F.. "Epistemic Logic". in Zalta, Edward N.. Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/entries/logic-epistemic/.

* v
* t
* e

Non-classical logic

Modal|

* Alethic
* Axiologic
* Deontic
* Doxastic
* Epistemic
* Temporal
* Normal
* Regular
* Classical

Intuitionistic|

* Intuitionistic logic
* Constructive analysis
* Heyting arithmetic
* Intuitionistic type theory
* Constructive set theory

Fuzzy|

* Degree of truth
* Fuzzy rule
* Fuzzy set
* Fuzzy finite element
* Fuzzy set operations

Substructural|

* Structural rule
* Relevance logic
* Linear logic

Paraconsistent|

* Dialetheism

Description|

* Ontology
* Ontology language

Many-valued|

* Three-valued
* Four-valued
* Łukasiewicz

Digital logic|

* Three-state logic
* Tri-state buffer
* Four-valued
* Verilog
* IEEE 1164
* VHDL

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/STIT logic. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Philosophy:STIT_logic&oldid=4230661"
*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template