A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916735071813632 |
|---|---|
| author | Gao, Han Girlando, Marianna Olivetti, Nicola |
| author_facet | Gao, Han Girlando, Marianna Olivetti, Nicola |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_08347 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels Gao, Han Girlando, Marianna Olivetti, Nicola Logic in Computer Science 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. |
| title | A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2505.08347 |