STIT Logic

Origin. Belnap and Perloff developed STIT ("seeing to it that") logic (1988, 1992). Logic of agency and action. Agent "sees to it" that φ: agent's choice guarantees φ. Branching time framework. Foundation for deontic logic of action.

Models. Agents making choices in branching time. Time: tree structure with moments and histories. Choice: partition of histories at a moment. [i stit]φ: agent i's choice guarantees φ regardless of others' choices and nature. Captures "deliberate action."

Formalism.

Branching time structure:

Tree of moments with ≤ ordering
Histories: maximal chains through tree
H_m: histories passing through moment m

Choice function: Choice^m_i: partition of H_m for agent i at m. Agent i's choice at m: which cell of partition.

STIT operators:

[i stit]φ: agent i sees to it that φ True at m/h iff φ true at m for all h' in agent i's choice containing h, and φ not settled true at m (non-trivial choice).
[i dstit]φ (deliberative stit): i's choice guarantees φ, but some alternative choice doesn't.
[i cstit]φ (Chellas stit): φ true throughout i's choice cell (may be trivial).

Independence of agents: Product of choices: what happens determined by all agents' choices together. Independence of agents: every combination of choices (one cell per agent) has a non-empty intersection — no agent's choice can constrain another's.

Interaction with time: Sett: φ (settled true): φ on all histories through m. Was: φ, Will: φ — past and future operators.

Symbols.

Symbol	Unicode	Name	Meaning
[i stit]	—	Sees to it	Agent i guarantees
[i dstit]	—	Deliberative	Non-trivial guarantee
[i cstit]	—	Chellas	Choice guarantees
Sett	—	Settled	True on all histories
m/h	—	Index	Moment-history pair
Choice	—	Choice function	Agent's options
[i astit]	—	Achievement stit	Guarantee witnessed at an earlier moment
H_m	—	History set	Histories passing through moment m
Was, Will	—	Tense operators	Past and future along a history
φ	U+03C6	Greek phi	Formula variable
ψ	U+03C8	Greek psi	Second formula variable
≤	U+2264	Tree ordering	Earlier-than on moments
¬	U+00AC	Negation	Negative condition of dstit
∧	U+2227	Conjunction	dstit as cstit φ ∧ ¬Sett φ
∨	U+2228	Disjunction	Counterexample to monotonicity of dstit
→	U+2192	Material conditional	Sett φ → [i cstit]φ
∩	U+2229	Intersection	Independence of agents
∅	U+2205	Empty set	Independence: no combination of cells is empty

Metatheory. Settledness is an S5 modality over the histories through a moment and the Chellas stit an S5 modality over the agent's choice cell, which is one of the blocks partitioning them, so Sett φ → [i cstit]φ. The deliberative stit is definable as [i cstit]φ ∧ ¬Sett φ, and that negative conjunct makes it non-normal: necessitation fails, and monotonicity with it, since φ can be unsettled where φ ∨ ψ is settled — agglomeration survives, because Sett distributes over conjunction. Independence of agents is a first-order frame condition, that any selection of one cell per agent has non-empty intersection, and without it the product of simultaneous choices is not well defined. Xu (1994) proved the multi-agent deliberative stit logic decidable, and the axiomatizations are collected in Belnap, Perloff and Xu, Facing the Future (2001). Herzig and Schwarzentruber (2008) showed that admitting a stit operator for every coalition costs decidability. Horty (2001) defines ought-to-do by dominance among available actions and argues on that basis that it does not reduce to ought-to-be.

Applies to. Philosophy of action. Legal responsibility. Multi-agent systems. Deontic logic (ought implies can). Free will analysis. Robot ethics. Autonomous systems.

Limitations. Independence of agents is imposed at the level of frames, so any situation in which one agent's options depend on what another simultaneously does simply falls outside the models — which excludes much of what makes joint action hard. Choices are instantaneous and their outcomes are read at the same moment, so there is no representation of duration, of process, or of causal contribution as against mere guaranteeing: [i cstit]φ holds for every settled φ, so on the Chellas reading each agent sees to every necessary truth. Achievement stit requires a strictly earlier witnessing moment, which forces a no-busy-choice postulate on the tree. Dominance ought-to-do needs a value ordering on histories that the framework takes as given, and yields no obligation when no action is optimal. Group agency is undecidable once arbitrary coalitions receive operators, and outcomes are all-or-nothing, with no probability over what nature does.