# Dyadic obligations: proofs and countermodels via hypersequents

arXiv: https://arxiv.org/abs/2406.09088 · HTML: https://mlsanity.com/paper/2406.09088/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Jun 2024.

## Built on by (most cited first, 1 of 1)

- [Defeasible Conditional Obligation in a Two-tiered Preference-based Semantics (Extended Version)](https://mlsanity.com/paper/2604.26977/) (2026)

## Abstract (arXiv)

The basic system E of dyadic deontic logic proposed by AAqvist 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.