Paraconsistent Constructive Modal Logic

TL;DR

This paper introduces a family of paraconsistent constructive modal logics designed to handle reasoning about contradictory yet meaningful propositional attitudes, with formal semantics, axiomatizations, and decidability results.

Contribution

It develops new paraconsistent modal logics with Kripke semantics, Hilbert axioms, and sequent calculi, extending constructive modal logic to handle contradictions.

Findings

Semantic framework based on intuitionistic frames with dual valuations.

A family of Hilbert-style axioms for the logics.

Decidability established via modular sequent calculi.

Abstract

We present a family of paraconsistent counterparts of the constructive modal logic CK. These logics aim to formalise reasoning about contradictory but non-trivial propositional attitudes like beliefs or obligations. We define their Kripke-style semantics based on intuitionistic frames with two valuations which provide independent support for truth and falsity; they are connected by strong negation as defined in Nelson's logic. A family of systems is obtained depending on whether both modal operators are defined using the same or by different accessibility relations for their positive and negative support. We propose Hilbert-style axiomatisations for all logics determined by this semantic framework. We also propose a~family of modular cut-free sequent calculi that we use to establish decidability.