Tree Rewriting Calculi for Strictly Positive Logics

Abstract

We study strictly positive logics in the language ${\mathcal{L}}^{+}$, which constructs formulas from $\top$, propositional variables, conjunction, and diamond modalities. We begin with the base system ${\mathbf{K}}^{+}$, the strictly positive fragment of polymodal $\mathbf{K}$, and examine its extensions obtained by adding axioms such as monotonicity, transitivity, and the hierarchy-sensitive interaction axiom $(\mathsf{J})$, which governs the interplay between modalities of different strengths. The strongest of these systems is the Reflection Calculus ($\mathbf{RC}$), which corresponds to the strictly positive fragment of polymodal $\mathbf{GLP}$. Our main contribution is a formulation of these logics as tree rewriting systems, establishing both adequacy and completeness through a correspondence between ${\mathcal{L}}^{+}$ formulas and inductively defined modal trees. We also provide a normalization of the rewriting process, which has exponential complexity when axiom $(\mathsf{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.