Deontic Action Logic

Origin. Von Wright combined action and deontic logic (1960s). Segerberg, Meyer, and others developed dynamic deontic logic (1980s-90s). Obligations about actions, not just states. "It is obligatory to do α." Foundation for normative multi-agent systems.

Models. Norms about actions. Standard deontic: O(φ) — obligatory that state φ. Action deontic: O(α) — obligatory to perform action α. Combines dynamic logic [α]φ with deontic operators. Distinguishes doing from refraining.

Formalism.

Action deontic operators:

O(α): obligatory to do α
P(α): permitted to do α
F(α): forbidden to do α

Dynamic + deontic:

[α]φ: after all α-executions, φ
O([α]φ): obligatory that doing α leads to φ
[α]O(φ): after doing α, φ becomes obligatory

Meyer's dynamic deontic logic: Violation predicate V. O(α) ≡ [ᾱ]V (not doing α leads to violation) P(α) ≡ ¬[α]V (doing α doesn't lead to violation) F(α) ≡ [α]V (doing α leads to violation)

Action negation: ᾱ: not doing α (doing something else or nothing). α ∪ ᾱ: doing anything.

Contrary-to-duty: O(α) ∧ [ᾱ]O(β): should do α, but if not, then should do β. Handles reparational obligations.

STIT connection: [i stit]φ + O(φ) in branching frameworks. Agent-relative obligations.

Symbols.

Symbol	Unicode	Name	Meaning
O	—	Obligation	Must do
P	—	Permission	May do
F	—	Forbidden	Must not do
[α]	—	After α	Dynamic modality
ᾱ	U+1FB1	Alpha with macron	Complement action: not doing α
V	—	Violation	Norm breach; the Andersonian constant
∪	U+222A	Union	Action choice
α	U+03B1	Greek alpha	Action variable
β	U+03B2	Greek beta	Second action variable
φ	U+03C6	Greek phi	Proposition variable
stit	—	Sees to it	Agency operator in the branching extension
≡	U+2261	Definitional equivalence	O(α) ≡ [ᾱ]V
¬	U+00AC	Negation	P(α) ≡ ¬[α]V
∧	U+2227	Conjunction	Contrary-to-duty pair O(α) ∧ [ᾱ]O(β)
∨	U+2228	Disjunction	What P(α ∪ β) actually yields
→	U+2192	Material conditional	Ross's paradox in action form

Metatheory. Meyer (1988) is Anderson's reduction transposed from states to actions: with V a propositional constant for violation and O(α) ≡ [ᾱ]V, F(α) ≡ [α]V, P(α) ≡ ¬[α]V, the deontic operators are not primitive, and the system is propositional dynamic logic with one distinguished atom, so its soundness, completeness and decidability are inherited from PDL, whose satisfiability problem is EXPTIME-complete (Fischer and Ladner, 1979; Pratt, 1980). Free choice permission fails, and fails computably: P(α ∪ β) unfolds to ¬([α]V ∧ [β]V), which is P(α) ∨ P(β) and not P(α) ∧ P(β). Ross's paradox reappears as O(α) → O(α ∪ β), valid because the complement of α ∪ β is contained in the complement of α, though what it now asserts is only that one of the two must be performed. Action complement is where the base logic strains: negation of atomic programs preserves decidability (Lutz and Walther, 2005), negation of arbitrary programs does not.

Applies to. Legal reasoning. Normative multi-agent systems. Robot ethics. Contract formalization. Compliance checking. Business rules. AI safety.

Limitations. The reduction makes every obligation a matter of avoiding one undifferentiated constant, so degrees of wrongdoing, which norm was breached, and how many were breached at once all collapse into V, which carries no semantics of its own beyond what a model assigns it. Contrary-to-duty structures can be written, as O(α) ∧ [ᾱ]O(β), but the primary obligation stays in force after the violation and conjoins with the secondary one, so the pragmatic oddity survives. Free choice permission is underivable. Action complement behaves well only when relativized to a fixed repertoire of actions, as Broersen (2004) argued, since the absolute complement is not a PDL program. There is no time beyond action sequencing, no agent unless a stit layer is added, and no defeasibility: adding norms never withdraws an obligation.