STIT logic

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\ {\mathsf {stit}}:\varphi ]$, usually read as "agent $i$ sees to it that $\varphi$", and is interpreted in models where agents choose between alternative possible futures.

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.

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. In this tradition, "to see to it that $\varphi$" 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. This approach was further developed in a series of papers on indeterminism and agency and provided the conceptual core for later STIT formalisms.

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. 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.

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. 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. 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. Work on group and coalitional agency investigated axiomatisations and complexity results for group STIT logics, and related STIT-based analyses of agency to coalition logic and alternating-time temporal logic (ATL) by exhibiting formal embeddings between the frameworks.

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. Ciuni and Lorini compared different semantics for temporal STIT, clarifying the relationships between branching-time, game-based and epistemic approaches, 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. 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.

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. 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. Other authors have proposed STIT-based logics of responsibility, blameworthiness and intentionality for use in philosophical and AI settings. 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.

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. 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. 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.

Branching-time semantics

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

• 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\in Ag$ and moment $m$, a choice function ${\mathsf {choice}}_{i}^{m}$ 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.

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.

Let $H_{m}$ be the set of histories passing through a moment $m$, and write $H_{m}$ ${\text{⟦}}\varphi {\text{⟧}}_{m}=\{h\in H_{m}\mid M,m/h\models \varphi \}$ for the set of histories at $m$ where $\varphi$ holds.

• The Chellas STIT operator, often written $[i\ {\mathsf {cstit}}:\varphi ]$, is given by

$M,m/h\models [i\ {\mathsf {cstit}}:\varphi ]\quad {\text{iff}}\quad {\mathsf {choice}}_{i}^{m}(h)\subseteq {\text{⟦}}\varphi {\text{⟧}}_{m}.$

Intuitively, agent $i$ sees to it that $\varphi$ if $\varphi$ holds at all histories compatible with their present choice.

• The deliberative STIT operator, $[i\ {\mathsf {dstit}}:\varphi ]$, adds a "non-triviality" or "negative" condition:

$M,m/h\models [i\ {\mathsf {dstit}}:\varphi ]$ iff $M,m/h\models [i\ {\mathsf {cstit}}:\varphi ]$ and $\varphi$ is not already historically necessary at $m$ (i.e. fails at some history through $m$).

To express the latter, a historic necessity operator $\Box _{H}$ is often defined by

$M,m/h\models \Box _{H}\varphi \quad {\text{iff}}\quad {\text{for all }}h'\in H_{m},\,M,m/h'\models \varphi .$

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

$[i\ {\mathsf {dstit}}:\varphi ]\leftrightarrow {\bigl (}[i\ {\mathsf {cstit}}:\varphi ]\land \neg \Box _{H}\varphi {\bigr )},$

$[i\ {\mathsf {cstit}}:\varphi ]\leftrightarrow {\bigl (}[i\ {\mathsf {dstit}}:\varphi ]\lor \Box _{H}\varphi {\bigr )}.$

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

Group agency and joint action

STIT models naturally support notions of group and collective agency. Given a set of agents $G\subseteq Ag$, a group STIT operator $[G\ {\mathsf {stit}}:\varphi ]$ can be defined so that it is true exactly when the collective choices of all agents in $G$ guarantee $\varphi$. 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.

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

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. 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.

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.

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

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.
• 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.
• 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.

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.

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. 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.

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.

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

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.
• Xu, Ming (1998). "Axioms for deliberative STIT". Journal of Philosophical Logic. 27 (5): 505–552.
• 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; Tran Cao Son; M. Birna van Riemsdijk; Michael Winikoff (eds.). Declarative Agent Languages and Technologies VI. Lecture Notes in Computer Science. Vol. 5422. Springer. pp. 47–59.
• Olkhovikov, Grigory K. (2019). "The basics of justification STIT logic". Studia Logica. 107 (4): 713–742.
• Segerberg, Krister; Meyer, John-Jules C.; Kracht, Marcus (2016). "The Logic of Action". In Zalta, Edward N. (ed.). The Stanford Encyclopedia of Philosophy.

External links

• Segerberg, Krister. "The Logic of Action". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
• McNamara, Paul. "Deontic Logic". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
• Hendricks, Vincent F. "Epistemic Logic". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.