Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Cut-free Sequent Calculus for Basic Intuitionistic Dynamic Topological Logic

Amirhossein Akbar Tabatabai, Majid Alizadeh, Alireza Mahmoudian

TL;DR

The paper develops cut-free sequent calculi $\mathbf{iK_d}$ and $\mathbf{iK_{d*}}$ for the intuitionistic dynamic topological logics $\mathsf{iK_d}$ and $\mathsf{iK_{d*}}$, addressing a previous gap in proof theory. It introduces $\nabla$-analyticity to overcome non-analyticity in prior systems and proves that these calculi are sound and complete for their respective logics, via equivalence with $\mathbf{STL(N, H)}$ and $\mathbf{STL(N)}$, and conservativity of $\mathbf{iK_d}$ over $\mathbf{iK_{d*}}$. The authors establish foundational metatheorems: cut admissibility (for the generalized cut), the disjunction property, and generalized Visser rules, as well as Craig interpolation for $\mathsf{iK_d}$ and deductive interpolation for $\mathbf{iK_d^{+}}$. Collectively, the results provide a robust proof-theoretic framework for basic intuitionistic dynamic topological logic, linking algebraic, topological, and Kripke-style perspectives and enabling precise interpolation and modular reasoning about dynamic-topological modalities.

Abstract

As part of a broader family of logics, [1, 3] introduced two key logical systems: $\mathsf{iK_{d}}$, which encapsulates the basic logical structure of dynamic topological systems, and $\mathsf{iK_{d*}}$, which provides a well-behaved yet sufficiently general framework for an abstract notion of implication. These logics have been thoroughly examined through their algebraic, Kripke-style, and topological semantics. To complement these investigations with their missing proof-theoretic analysis, this paper introduces a cut-free G3-style sequent calculus for $\mathsf{iK_{d}}$ and $\mathsf{iK_{d*}}$. Using these systems, we demonstrate that they satisfy the disjunction property and, more broadly, admit a generalization of Visser's rules. Additionally, we establish that $\mathsf{iK_{d}}$ enjoys the Craig interpolation property and that its sequent system possesses the deductive interpolation property.

A Cut-free Sequent Calculus for Basic Intuitionistic Dynamic Topological Logic

TL;DR

The paper develops cut-free sequent calculi and for the intuitionistic dynamic topological logics and , addressing a previous gap in proof theory. It introduces -analyticity to overcome non-analyticity in prior systems and proves that these calculi are sound and complete for their respective logics, via equivalence with and , and conservativity of over . The authors establish foundational metatheorems: cut admissibility (for the generalized cut), the disjunction property, and generalized Visser rules, as well as Craig interpolation for and deductive interpolation for . Collectively, the results provide a robust proof-theoretic framework for basic intuitionistic dynamic topological logic, linking algebraic, topological, and Kripke-style perspectives and enabling precise interpolation and modular reasoning about dynamic-topological modalities.

Abstract

As part of a broader family of logics, [1, 3] introduced two key logical systems: , which encapsulates the basic logical structure of dynamic topological systems, and , which provides a well-behaved yet sufficiently general framework for an abstract notion of implication. These logics have been thoroughly examined through their algebraic, Kripke-style, and topological semantics. To complement these investigations with their missing proof-theoretic analysis, this paper introduces a cut-free G3-style sequent calculus for and . Using these systems, we demonstrate that they satisfy the disjunction property and, more broadly, admit a generalization of Visser's rules. Additionally, we establish that enjoys the Craig interpolation property and that its sequent system possesses the deductive interpolation property.

Paper Structure

This paper contains 9 sections, 19 theorems, 17 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. A $\nabla$-analytic system for $\mathsf{iK_d}$ and $\mathsf{iK_{d*}}$
  4. Some Properties of $\mathbf{iK_d}$ and $\mathbf{iK_{d*}}$
  5. Equivalence of $\mathbf{STL(N, H)}$ and $\mathbf{iK_d}$
  6. Deduction Theorem
  7. Admissibility of $cut$ in $\mathbf{iK_d}$
  8. Visser's Rules and Disjunction Property
  9. Interpolation Theorems

Key Result

Lemma 1

Let $\Gamma$, $\Sigma$ and $\Delta$ be multisets of formulas and $A$ and $B$ be formulas. Then: All claims also hold for the language $\mathcal{L}_*$ and the system $\mathbf{iK_{d*}}$.

Figures (2)

  • Figure 1: The sequent calculus $\mathbf{STL(N, H)}$
  • Figure 2: The sequent calculus $\mathbf{iK_d}$. In the axiom $(Id^p)$, the letter $p$ is an atom.

Theorems & Definitions (45)

  • Definition 1
  • Definition 2
  • Remark 1
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Lemma 3
  • proof
  • Lemma 4: Inversion
  • ...and 35 more