Action Logic (Deontic)

Origin. Segerberg (1980s), Belnap and Perloff (1988). Agency in deontic logic. stit (sees to it that). Actions as logical objects. Foundation for agent responsibility.

Models. Branching time with agents. Choice functions. Agent ensures outcome across choices. Deliberative vs causal agency.

Formalism.

stit operator: [i stit: φ]: agent i sees to it that φ. i's choice guarantees φ.

Branching time: Tree structure. Moments and histories. Choices partition histories at moments.

Achievement stit: [i astit: φ]: i acts so φ, alternative had ¬φ. Counterfactual contrast.

Deliberative stit: [i dstit: φ]: i ensures φ, could have done otherwise. Free will assumption.

Ought-to-do: O[i stit: φ]: i ought to see to φ. Deontic on actions.

Ability: Can(i, φ): some choice of i guarantees φ. ◇[i stit: φ]

Group agency: [G stit: φ]: group G jointly ensures φ. Coalition choices.

Independence: Agent choices independent. Product of individual choices.

STIT semantics: w, m/h ⊨ [i stit: φ] iff ∀h' ∈ Choice_i(m): w, m/h' ⊨ φ Agent's choice cell satisfies φ.

Symbols.

Symbol	Unicode	Name	Meaning
stit	—	Sees to it	Agency
Choice_i	—	Choices	Agent's options
m/h	—	Moment/history	Index
O	—	Ought	Obligation
astit	—	Achievement stit	Counterfactual contrast with a prior choice
dstit	—	Deliberative stit	cstit plus the negative condition ¬□φ
cstit	—	Chellas stit	Choice cell box, an S5 modality
G	—	Group	Coalition of agents
□	U+25A1	Box	Historical necessity: all histories through a moment
◇	U+25C7	Diamond	Historical possibility; ability as ◇[i stit: φ]
⊨	U+22A8	Satisfaction	Truth at an index m/h
∀	U+2200	Universal quantifier	Over histories in Choice_i(m)
∈	U+2208	Membership	h' ∈ Choice_i(m)
¬	U+00AC	Negation	Negative condition of dstit; refraining
∧	U+2227	Conjunction	dstit as cstit φ ∧ ¬□φ

Metatheory. Historical necessity □ and the Chellas stit are both S5 modalities, the first quantifying over all histories through a moment and the second over the histories in the agent's choice cell at that moment, so cstit is the box of a partition refining □ and [i cstit: φ] follows from □φ. The deliberative stit adds the negative condition, [i dstit: φ] := [i cstit: φ] ∧ ¬□φ, and that makes it non-normal: necessitation fails, since no agent deliberately sees to what is settled anyway, and monotonicity fails with it, because φ can be unsettled where φ ∨ ψ is not. Agglomeration survives. Frames satisfy independence of agents — any selection of one choice cell per agent has nonempty intersection — which is what makes simultaneous individual choices jointly realizable. Xu (1994) proved the multi-agent deliberative stit logic decidable; Herzig and Schwarzentruber (2008) showed that admitting a stit operator for every coalition makes satisfiability undecidable. Horty (2001) grounds ought-to-do in a dominance ordering on actions rather than in ought-to-be.

Applies to. Legal responsibility. Moral philosophy. Agent theory. Robot ethics. Causation.

Limitations. Independence of agents is built into the frames, so cases in which one agent's options are constrained by what another simultaneously chooses cannot be modelled at all. Choices are instantaneous and their effects are read off at the same moment, so there is no account of the duration of an action, of the process by which an outcome comes about, or of causal contribution as against mere guaranteeing — [i cstit: φ] holds for every settled φ, so on that reading each agent sees to every necessary truth. Dominance ought-to-do requires a value ordering on histories that the logic takes as given, and yields no obligation when no action is optimal. Group agency is undecidable once operators for arbitrary coalitions are admitted, and refraining has to be built by iterating stit rather than taken as primitive.