A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels
Abstract
The logic IK is the intuitionistic variant of modal logic introduced by Fischer Servi, Plotkin and Stirling, and studied by Simpson. This logic is considered a fundamental intuitionstic modal system as it corresponds, modulo the standard translation, to a fragment of intuitionstic first-order logic. In this paper we present a labelled-free bi-nested sequent calculus for IK. This proof system comprises two kinds of nesting, corresponding to the two relations of bi-relational models for IK: a pre-order relation, from intuitionistic models, and a binary relation, akin to the accessibility relation of Kripke models. The calculus provides a decision procedure for IK by means of a suitable proof-search strategy. This is the first labelled-free calculus for IK which allows direct counter-model extraction: from a single failed derivation, it is possible to construct a finite countermodel for the formula at the root. We further show the bi-nested calculus can simulate both the (standard) nested calculus and labelled sequent calculus, which are two best known calculi proposed in the literature for IK.
Keywords
Cite
@article{arxiv.2505.08347,
title = {A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels},
author = {Han Gao and Marianna Girlando and Nicola Olivetti},
journal= {arXiv preprint arXiv:2505.08347},
year = {2025}
}