Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Intuitionistic modal logic LIK4 is decidable

Philippe Balbiani, Çigdem Gencer, Tinko Tinchev

TL;DR

The paper proves the decidability of LIK4, an intuitionistic modal logic, by developing a constructive, labelled-tree based framework. It builds a canonical model, introduces a defect-repair saturation process, and demonstrates a finite frame property via regular clips and finite saturation, culminating in a finite-frame completeness result. This yields a practical decision procedure and provides structural insights into semantics and proof theory for intuitionistic modal logics. The approach also situates LIK4 within the landscape of finite-frame techniques, enabling standard decidability arguments.

Abstract

In this note, we prove that intuitionistic modal logic LIK4 is decidable.

Intuitionistic modal logic LIK4 is decidable

TL;DR

The paper proves the decidability of LIK4, an intuitionistic modal logic, by developing a constructive, labelled-tree based framework. It builds a canonical model, introduces a defect-repair saturation process, and demonstrates a finite frame property via regular clips and finite saturation, culminating in a finite-frame completeness result. This yields a practical decision procedure and provides structural insights into semantics and proof theory for intuitionistic modal logics. The approach also situates LIK4 within the landscape of finite-frame techniques, enabling standard decidability arguments.

Abstract

In this note, we prove that intuitionistic modal logic LIK4 is decidable.

Paper Structure

This paper contains 15 sections, 44 theorems, 1 equation.

Table of Contents

  1. Introduction
  2. Some notations
  3. Labelled trees
  4. Syntax
  5. Relational semantics
  6. Axiomatization
  7. Canonical model
  8. Maximality
  9. Tips and clips
  10. Defects
  11. Repair of maximality defects
  12. Repair of accessibility defects
  13. Repair of confluence defects
  14. A decision procedure
  15. Finite frame property

Key Result

Lemma 1

Let $(N,{E},\lambda)$ be a $P$-labelled tree and $(i,j)$ be a duplicate in $(N,{E},$$\lambda)$. The structure $(N^{\prime},{E^{\prime}},\lambda^{\prime})$ such that is a $P$-labelled tree.

Theorems & Definitions (44)

  • Lemma 1
  • Lemma 2
  • Lemma 3
  • Lemma 4
  • Lemma 5
  • Lemma 6
  • Lemma 7
  • Lemma 8
  • Lemma 9
  • Lemma 10
  • ...and 34 more