A modified subformula property for the modal logic KC4 (Q2027110)

KC4 is the extension of the well-known modal propositional logic K by the axiom C4, which says that double box implies box (the converse of the transitivity axiom known as 4). The author gives it a Gentzen style axiomatization for which he shows that, while it fails cut elimination, it nevertheless satisfies a subformula property that suffices for decidability and the finite model property. The paper is one of a series with similar results for various modal propositional logics; each instance requires a different definition of a suitable subformula property generalizing the standard one.