# Sequent calculi and interpolation for non-normal modal and deonticlogics

## TL;DR

This paper develops sequent calculi for non-normal modal and deontic logics, proving key properties like cut admissibility and subformula property, and establishing their soundness, completeness, and interpolation results.

## Contribution

It introduces G3-style sequent calculi for these logics, demonstrating their admissibility, decidability, and equivalence to axiomatic systems, with new interpolation proofs.

## Key findings

- Calculi are sound and complete with respect to neighbourhood semantics
- Weakening and contraction are height-preserving admissible
- Decidability is in PSPACE

## Abstract

G3-style sequent calculi for the logics in the cube of non-normal modal logics and for their deontic extensions are studied. For each calculus we prove that weakening and contraction are height-preserving admissible, and we give a syntactic proof of the admissibility of cut. This implies that the subformula property holds and that derivability can be decided by a terminating proof search whose complexity is in PSPACE. These calculi are shown to be equivalent to the axiomatic ones and, therefore, they are sound and complete with respect to neighbourhood semantics. Finally, it is given a Maehara-style proof of Craig's interpolation theorem for most of the logics considered.