Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Local Intuitionistic Modal Logics and Their Calculi

Philippe Balbiani, Han Gao, Çiğdem Gencer, Nicola Olivetti

Abstract

We investigate intuitionistic modal logics with locally interpreted $\square$ and $\lozenge$. The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization of LIK and some of its extensions. We propose bi-nested calculi for LIK and these extensions, thus providing both a decision procedure and a procedure of finite countermodel extraction.

Local Intuitionistic Modal Logics and Their Calculi

Abstract

We investigate intuitionistic modal logics with locally interpreted and . The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization of LIK and some of its extensions. We propose bi-nested calculi for LIK and these extensions, thus providing both a decision procedure and a procedure of finite countermodel extraction.
Paper Structure (3 sections, 10 theorems, 4 equations)

This paper contains 3 sections, 10 theorems, 4 equations.

Table of Contents

  1. Introduction
  2. The logic
  3. Bi-nested sequent calculi

Key Result

lemma 1.2.1

Let $(W,{\leq},{R},V)$ be a forward and downward confluent model. For all $A \in {\mathcal{L}}$ and for all $x,x'\in W$, if $x\Vdash A$ and $x\leq x'$ then $x'\Vdash A$.

Theorems & Definitions (19)

  • definition 1.2.0: Formulas
  • definition 1.2.0: Frames
  • definition 1.2.0: Valuations, models and truth conditions
  • lemma 1.2.1: Heredity Property
  • proposition 1.2.1
  • definition 1.2.1: Axiom system
  • lemma 1.2.2
  • theorem thmcountertheorem
  • definition 1.2.1: Theories
  • lemma 1.2.3
  • ...and 9 more