As part of a broader family of logics, [2, 4] 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 prove 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.
