A Sequent Calculus for Dynamic Topological Logic

Abstract: We introduce a sequent calculus for the temporal-over-topological fragment

e x t b f {D T L}_{0}^{c i r c * s l a s h B o x}

of dynamic topological logic

e x t b f D T L

, prove soundness semantically, and prove completeness syntactically using the axiomatization of

e x t b f {D T L}_{0}^{c i r c * s l a s h B o x}

given in cite{paper3}. A cut-free sequent calculus for

e x t b f {D T L}_{0}^{c i r c * s l a s h B o x}

is obtained as the union of the propositional fragment of Gentzen's classical sequent calculus, two

B o x

structural rules for the modal extension, and nine

c i r c

(next) and

*

(henceforth) structural rules for the temporal extension. Future research will focus on the construction of a hypersequent calculus for dynamic topological

e x t b f S 5

logic in order to prove Kremer's Next Removal Conjecture for the logic of homeomorphisms on almost discrete spaces

e x t b f S 5 H

.

This page was built for publication: A Sequent Calculus for Dynamic Topological Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6253523)