Tree Rewriting Calculi for Strictly Positive Logics

We study strictly positive logics in the language \({L}⁺\) , which constructs formulas from \(\) , propositional variables, conjunction, and diamond modalities. We begin with the base system \( K⁺\) , the strictly positive fragment of polymodal \( K\) , and examine its extensions obtained by adding axioms such as monotonicity, transitivity, and the hierarchy-sensitive interaction axiom \(( J)\) , which governs the interplay between modalities of different strengths. The strongest of these systems is the Reflection Calculus ( \( RC\) ), which corresponds to the strictly positive fragment of polymodal \( GLP\) . Our main contribution is a formulation of these logics as tree rewriting systems, establishing both adequacy and completeness through a correspondence between \({L}⁺\) formulas and inductively defined modal trees. We also provide a normalization of the rewriting process, which has exponential complexity when axiom \(( J)\) is absent; otherwise we provide a double-exponential bound. By introducing tree rewriting calculi as practical provability tools for strictly positive logics, we aim to deepen their proof-theoretic analysis and computational applications.