A logic for default deontic reasoning

TL;DR

This paper introduces a proof-theoretic framework for deontic reasoning based on default logic, enabling agents to handle conflicting norms and dynamic environments with local soundness checks.

Contribution

It presents a novel controlled sequent calculus for deontic logic that supports reasoning under incomplete information and normative conflicts, with proven soundness and completeness.

Findings

Controlled sequent calculus satisfies admissibility of contraction.

The framework enables local soundness checks for normative reasoning.

It provides a flexible basis for resolving deontic conflicts.

Abstract

In many real-life settings, agents must navigate dynamic environments while reasoning under incomplete information and acting on a corpus of unstable, context-dependent, and often conflicting norms. We introduce a general, non-modal, proof-theoretic framework for deontic reasoning grounded in default logic. Its central feature is the notion of controlled sequent - a sequent annotated with sets of formulas (control sets) that prescribe what should or should not be entailed by the formulas in the antecedent. When combined with distinct extra-logical rules representing defaults and norms, these control sets record the conditions and constraints governing their applicability, thereby enabling local soundness checks for derived sequents. We prove that controlled sequent calculi satisfies admissibility of contraction and non-analytic cuts, and we establish their strong completeness with respect to credulous consequence in default theories and normative systems. Finally, we illustrate in depth how controlled sequent calculi provide a flexible and expressive basis for resolving deontic conflicts and capturing dynamic deontic notions via appropriate extra-logical rules.