Dyadic obligations: proofs and countermodels via hypersequents

TL;DR

This paper develops a hypersequent calculus for the dyadic deontic logic system E, enabling effective proof search, decision procedures, and polynomial-sized countermodels, thus advancing proof-theoretic analysis of normative logics.

Contribution

It introduces a cut-free hypersequent calculus for system E, providing a decision procedure and polynomial-size countermodels, enhancing proof-theoretic methods for dyadic deontic logic.

Findings

Validity in E is Co-NP.

Countermodels have polynomial size.

The calculus supports effective proof search and countermodel computation.

Abstract

The basic system E of dyadic deontic logic proposed by {\AA}qvist offers a simple solution to contrary-to-duty paradoxes and allows to represent norms with exceptions. We investigate E from a proof-theoretical viewpoint. We propose a hypersequent calculus with good properties, the most important of which is cut-elimination, and the consequent subformula property. The calculus is refined to obtain a decision procedure for E and an effective countermodel computation in case of failure of proof search. Using the refined calculus, we prove that validity in E is Co-NP and countermodels have polynomial size.