Non-normal logics: semantic analysis and proof theory (extended version)

TL;DR

This paper develops proper display calculi for various non-normal modal logics, ensuring soundness, completeness, and desirable proof-theoretic properties through a multi-type semantic approach.

Contribution

It introduces a novel multi-type methodology for designing display calculi for non-normal modal logics, extending proof-theoretic tools to these systems.

Findings

Calculi are sound, complete, and enjoy cut elimination.

Semantic analysis guides syntactic translations to multi-type normal logics.

Framework applies to basic monotonic and conditional logics, with extensions.

Abstract

We introduce proper display calculi for basic monotonic modal logic, the conditional logic CK and a number of their axiomatic extensions. These calculi are sound, complete, conservative and enjoy cut elimination and subformula property. Our proposal applies the multi-type methodology in the design of proper display calculi, starting from a semantic analysis which motivates syntactic translations from single-type non-normal modal logics to multi-type normal poly-modal logics.