Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels

Han Gao, Marianna Girlando, Nicola Olivetti

TL;DR

This work advances IK proof theory by introducing a label-free bi-nested sequent calculus with two nestings that encode the intuitionistic and modal relations and by integrating interaction rules that capture forward and backward confluence. It provides a terminating proof-search procedure and enables direct countermodel extraction from failed derivations, together with completeness via annotated countermodels. The paper also establishes translations from fully labelled and nested calculi into the bi-nested framework, showing that the new system can simulate existing IK calculi and thus serves as a modular, unifying foundation for IK and its extensions. These results enrich the toolkit for IK, offering a practical decision procedure and a coherent semantic-syntactic bridge that can be extended to the modal cube and related logics.

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.

A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels

TL;DR

This work advances IK proof theory by introducing a label-free bi-nested sequent calculus with two nestings that encode the intuitionistic and modal relations and by integrating interaction rules that capture forward and backward confluence. It provides a terminating proof-search procedure and enables direct countermodel extraction from failed derivations, together with completeness via annotated countermodels. The paper also establishes translations from fully labelled and nested calculi into the bi-nested framework, showing that the new system can simulate existing IK calculi and thus serves as a modular, unifying foundation for IK and its extensions. These results enrich the toolkit for IK, offering a practical decision procedure and a coherent semantic-syntactic bridge that can be extended to the modal cube and related logics.

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.
Paper Structure (10 sections, 19 theorems, 11 equations, 9 figures, 1 algorithm)

This paper contains 10 sections, 19 theorems, 11 equations, 9 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. The intutionistic modal logic IK
  3. A bi-nested calculus for IK
  4. Proof search and termination
  5. Completeness
  6. Relations with other proof systems for IK
  7. From fully labelled to bi-nested sequents
  8. From nested sequents to bi-nested sequents
  9. Relations with other calculi
  10. Conclusion and future work

Key Result

theorem 1

A formula $A$ is provable in $\mathcal{H}_{\textbf{IK}\xspace}$ if and only if $A$ is valid.

Figures (9)

  • Figure 1: Forward confluence (left) and backward confluence (right)
  • Figure 2: Axioms and rules of $\textbf{IK}\xspace$
  • Figure 3: Rules of $\mathbf{C}_{\textbf{IK}\xspace}$
  • Figure 4: Saturation conditions, $\mathbf{CC}_{\textbf{IK}\xspace}$
  • Figure 5: Rules of $\mathbf{CC}_{\mathbf{IK}}^{\text{n}}$
  • ...and 4 more figures

Theorems & Definitions (51)

  • definition 1
  • definition 2
  • theorem 1
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • proposition 1
  • definition 7
  • theorem 2: Soundness
  • ...and 41 more