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.
- Cut-elimination for weak Grzegorczyk logic Go
- scientific article; zbMATH DE number 440027 (Why is no real title available?)
- The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination
- Embedding theorems for LTL and its variants
- The modal logic of continuous functions on Cantor space
This page was built for publication: Cut elimination for S4C: A case study
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q817705)
