Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Dyadic obligations: proofs and countermodels via hypersequents

Agata Ciabattoni, Nicola Oliveti, Xavier Parent

TL;DR

The paper develops a Gentzen-style hypersequent calculus for Åqvist's dyadic deontic logic $E$, enabling cut-elimination, a relaxed subformula property, and constructive proof-search tools. It refines the calculus to ${HE}^+$ to support automated proof search and countermodel construction, and proves that $E$-validity lies in $co\text{-}NP$ with polynomial-size countermodels. It also clarifies the connection between $E$ and modal logic $S5$ and provides a framework for explaining CTD paradoxes via maximality reasoning.

Abstract

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

Dyadic obligations: proofs and countermodels via hypersequents

TL;DR

The paper develops a Gentzen-style hypersequent calculus for Åqvist's dyadic deontic logic , enabling cut-elimination, a relaxed subformula property, and constructive proof-search tools. It refines the calculus to to support automated proof search and countermodel construction, and proves that -validity lies in with polynomial-size countermodels. It also clarifies the connection between and modal logic and provides a framework for explaining CTD paradoxes via maximality reasoning.

Abstract

The basic system E of dyadic deontic logic proposed by Å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.
Paper Structure (3 sections, 1 theorem, 2 equations, 1 figure)

This paper contains 3 sections, 1 theorem, 2 equations, 1 figure.

Table of Contents

  1. Introduction
  2. System E
  3. A cut-free hypersequent calculus for ${\bf E}$

Key Result

theorem 1.1

E is sound and complete w.r.t. the class of all preference models.

Theorems & Definitions (5)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • theorem 1.1
  • definition thmcounterdefinition