D - Deontic Normal Modal Logic

D, also known as the Logic of Obligation, is an extension of K, with a serial access relation.

---

Semantics

D semantics behave just like K semantics.

Seriality

D adds a serial restriction on the access relation for models.

Seriality

In every model, for each world \(w\), there is some world \(w'\) such that \(\langle\ w,w'\ \rangle\) is in the access relation.

Tableaux

D tableaux are constructed just like K system tableaux.

Nodes

Nodes for bivalent modal tableaux come in two types:

• A sentence-world pair like \(A, w\), indicating that \(A\) is true at \(w\).

• An access node like \(w_1Rw_2\), indicating that the pair \(\langle\ w_1, w_2\ \rangle\) is in the access relation \(R\).

Trunk

To build the trunk for an argument, add a node with each premise, with world \(w_0\), followed by a node with the negation of the conclusion with world \(w_0\).

To build the trunk for the argument A₁ ... A_n ∴ B write:

A₁, w₀

⋮

A_n, w₀

¬B, w₀

Closure

⊗KContradiction Closure

A, w₀

⋮

¬A, w₀

⊗

⊗¬=KSelf Identity Closure

⋮

a ≠ a, w₀

⊗

⊗¬E!KNon Existence Closure

⋮

¬E!a, w₀

⊗

Rules

D contains all the K rules plus an additional Serial rule.

The Serial rule applies to a an open branch b when there is a world w that appears on b, but there is no world w' such that w accesses w'.

Access Rules

RserSerial

A, w₀

⋮

w₀Rw₁

Operator Rules

¬ Rules

¬¬KDouble Negation

¬¬A, w₀

⋮

A, w₀

∧ Rules

∧KConjunction

A ∧ B, w₀

⋮

A, w₀

B, w₀

¬∧KConjunction Negated

¬(A ∧ B), w₀

⋮

¬A, w₀

¬B, w₀

∨ Rules

∨KDisjunction

A ∨ B, w₀

⋮

A, w₀

B, w₀

¬∨KDisjunction Negated

¬(A ∨ B), w₀

⋮

¬A, w₀

¬B, w₀

⊃ Rules

⊃KMaterial Conditional

A ⊃ B, w₀

⋮

¬A, w₀

B, w₀

¬⊃KMaterial Conditional Negated

¬(A ⊃ B), w₀

⋮

A, w₀

¬B, w₀

≡ Rules

≡KMaterial Biconditional

A ≡ B, w₀

⋮

¬A, w₀

¬B, w₀

B, w₀

A, w₀

¬≡KMaterial Biconditional Negated

¬(A ≡ B), w₀

⋮

A, w₀

¬B, w₀

¬A, w₀

B, w₀

Modal Operator Rules

◇ Rules

◇KPossibility

◇A, w₀

⋮

A, w₁

w₀Rw₁

¬◇KPossibility Negated

¬◇A, w₀

⋮

◻¬A, w₀

◻ Rules

◻KNecessity

◻A, w₀

w₀Rw₁

⋮

A, w₁

¬◻KNecessity Negated

¬◻A, w₀

⋮

◇¬A, w₀

Predicate Rules

= Rules

=KIdentity Indiscernability

Fa, w₀

a = b, w₀

⋮

Fb, w₀

Quantifier Rules

∃ Rules

∃KExistential

∃xFx, w₀

⋮

Fa, w₀

¬∃KExistential Negated

¬∃xFx, w₀

⋮

∀x¬Fx, w₀

∀ Rules

∀KUniversal

∀xFx, w₀

⋮

Fa, w₀

¬∀KUniversal Negated

¬∀xFx, w₀

⋮

∃x¬Fx, w₀

Compatibility Rules

⚬ Rules

⚬KAssertion

⚬A, w₀

⋮

A, w₀

¬⚬KAssertion Negated

¬⚬A, w₀

⋮

¬A, w₀

→ Rules

→KConditional

A → B, w₀

⋮

¬A, w₀

B, w₀

¬→KConditional Negated

¬(A → B), w₀

⋮

A, w₀

¬B, w₀

↔ Rules

↔KBiconditional

A ↔ B, w₀

⋮

¬A, w₀

¬B, w₀

B, w₀

A, w₀

¬↔KBiconditional Negated

¬(A ↔ B), w₀

⋮

A, w₀

¬B, w₀

¬A, w₀

B, w₀

Notes

References

Further Reading

• Stanford Encyclopedia on Deontic Logic

class Rules

closure: tuple[type[ClosingRule], ...] = (<class 'pytableaux.logics.k.Rules.ContradictionClosure'>, <class 'pytableaux.logics.k.Rules.SelfIdentityClosure'>, <class 'pytableaux.logics.k.Rules.NonExistenceClosure'>)

class Serial(tableau, /, **opts)

Rser

A, w₀

⋮

w₀Rw₁

The Serial rule applies to a an open branch b when there is a world w that appears on b, but there is no world w' such that w accesses w'.

The exception to this is when the Serial rule was the last rule to apply to the branch. This prevents infinite repetition of the Serial rule for open branches that are otherwise finished. For this reason, the Serial rule is ordered last in the rules, so that all other rules are checked before it.

For a node n on an open branch b on which appears a world w for which there is no world w' on b such that w accesses w', add a node to b with w as world1, and w1 as world2, where w1 does not yet appear on b.

Parameters:

tableau (Tableau) --

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({<class 'pytableaux.proof.helpers.MaxWorlds'>: Config(operators=qsetf({<Operator: Possibility>, <Operator: Necessity>})), <class 'pytableaux.proof.helpers.UnserialWorlds'>: None, <class 'pytableaux.proof.helpers.AdzHelper'>: None})

Helper classes mapped to their settings.

ignore_ticked = False

ticking: bool = False

Whether this is a ticking rule.

marklegend = [(Marking.tableau, ('access', 'serial'))]

example_nodes()

branching: int = 0

The number of additional branches created.

defaults = mappingproxy({'is_rank_optim': True, 'nolock': False})

legend: tuple[tuple[str, Any], ...] = ((Marking.tableau, ('access', 'serial')),)

The rule class legend.

name: str = 'Serial'

The rule class name.

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

groups: tuple[tuple[type[Rule], ...], ...] = ((<class 'pytableaux.logics.k.Rules.IdentityIndiscernability'>, <class 'pytableaux.logics.k.Rules.Assertion'>, <class 'pytableaux.logics.k.Rules.AssertionNegated'>, <class 'pytableaux.logics.k.Rules.Conjunction'>, <class 'pytableaux.logics.k.Rules.DisjunctionNegated'>, <class 'pytableaux.logics.k.Rules.MaterialConditionalNegated'>, <class 'pytableaux.logics.k.Rules.ConditionalNegated'>, <class 'pytableaux.logics.k.Rules.DoubleNegation'>, <class 'pytableaux.logics.k.Rules.PossibilityNegated'>, <class 'pytableaux.logics.k.Rules.NecessityNegated'>, <class 'pytableaux.logics.k.Rules.ExistentialNegated'>, <class 'pytableaux.logics.k.Rules.UniversalNegated'>), (<class 'pytableaux.logics.k.Rules.Necessity'>, <class 'pytableaux.logics.k.Rules.Possibility'>), (<class 'pytableaux.logics.k.Rules.ConjunctionNegated'>, <class 'pytableaux.logics.k.Rules.Disjunction'>, <class 'pytableaux.logics.k.Rules.MaterialConditional'>, <class 'pytableaux.logics.k.Rules.MaterialBiconditional'>, <class 'pytableaux.logics.k.Rules.MaterialBiconditionalNegated'>, <class 'pytableaux.logics.k.Rules.Conditional'>, <class 'pytableaux.logics.k.Rules.Biconditional'>, <class 'pytableaux.logics.k.Rules.BiconditionalNegated'>), (<class 'pytableaux.logics.k.Rules.Existential'>, <class 'pytableaux.logics.k.Rules.Universal'>), (<class 'pytableaux.logics.d.Rules.Serial'>,))