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

Abstract

As part of a broader family of logics, [1, 3] introduced two key logical systems: $\mathsf{i}{\mathsf{K}}_{\mathsf{d}}$, which encapsulates the basic logical structure of dynamic topological systems, and $\mathsf{i}{\mathsf{K}}_{\mathsf{d}\ast }$, 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{i}{\mathsf{K}}_{\mathsf{d}}$ and $\mathsf{i}{\mathsf{K}}_{\mathsf{d}\ast }$. 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{i}{\mathsf{K}}_{\mathsf{d}}$ enjoys the Craig interpolation property and that its sequent system possesses the deductive interpolation property.

41 pages