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

TL;DR

This paper develops a cut-free sequent calculus for basic intuitionistic dynamic topological logic, enabling proof-theoretic analysis and establishing properties like disjunction, interpolation, and Visser's rules.

Contribution

It introduces the first cut-free sequent calculus for $ ext{iK}_d$ and $ ext{iK}_{d*}$, advancing proof-theoretic understanding of these dynamic topological logics.

Findings

The calculus satisfies the disjunction property.

It admits a generalization of Visser's rules.

$ ext{iK}_d$ enjoys the Craig interpolation property.

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.