Cut elimination for S4C: A case study (Q817705)

The paper contains a cut-elimination proof for a logic of continuous transformations of a topological space, called S4C [cf. \textit{P. Kremer} and \textit{G. Mints}, Ann. Pure Appl. Logic 131, No. 1--3, 133--158 (2005; Zbl 1067.03028)]. It consists of the modal logic S4 enlarged by another modality operator \(\circ\). In the intended models of dynamic systems, \(\square\) is a topological interior and \(\circ\) is a preimage under a continuous function. This paper is of special interest because of its concise presentation of cut elimination. The rather special case for S4C is developed step by step by presenting the necessary methods for cut elimination in classical propositional calculus, S4, and finally S4C.