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. Each combination of choices (one per agent) picks exactly one history.

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

Metatheory. STIT logic decidable for finite agents. Complete axiomatizations exist. Expressively rich: captures ability, responsibility. Independence condition crucial. Combinations with deontic operators studied. Complexity varies by fragment.

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

Limitations. Branching time ontology controversial. Independence assumption strong. Continuous action not modeled. Probabilistic outcomes need extensions. Complex semantics. Limited tool support.