Tree Rewriting Calculi for Strictly Positive Logics

We study strictly positive logics in the language \(\cal{L}^{+}\) , which constructs formulas from \(\top\) , propositional variables, conjunction, and diamond modalities. We begin with the base system \(\bf K^{+}\) , the strictly positive fragment of polymodal \(\bf K\) , and examine its extensions obtained by adding axioms such as monotonicity, transitivity, and the hierarchy-sensitive interaction axiom \((\sf J)\) , which governs the interplay between modalities of different strengths. The strongest of these systems is the Reflection Calculus ( \(\bf RC\) ), which corresponds to the strictly positive fragment of polymodal \(\bf GLP\) .

Our main contribution is a formulation of these logics as tree rewriting systems, establishing both adequacy and completeness through a correspondence between \(\cal{L}^{+}\) formulas and inductively defined modal trees. We also provide a normalization of the rewriting process, which has exponential complexity when axiom \((\sf 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.