A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

TL;DR

This paper introduces FIK, a new intuitionistic modal logic with a complete axiomatization and a bi-nested calculus that offers decision procedures and countermodel extraction, advancing modal logic proof methods.

Contribution

It presents the first complete Hilbert-style axiomatization and a bi-nested calculus for FIK, a natural intuitionistic modal logic based on forward confluence Kripke models.

Findings

Provides a decision procedure for FIK

Enables countermodel extraction from failed proofs

Establishes completeness of the axiomatization

Abstract

We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite countermodel of it.