Tree Rewriting Calculi for Strictly Positive Logics

TL;DR

The paper develops tree rewriting calculi for strictly positive logics in the language $\mathscr{L}^+$, embedding formulas into finite modal trees and proving adequacy and completeness of a rewriting semantics for base and extended logics (notably $\mathbf{K}^+$, $\mathbf{K4}^+$, and $\mathbf{RC}$). It introduces a detailed normalization theory, establishing exponential and double-exponential bounds on rewrite sequences depending on the presence of the axiom $(\sf J)$, and demonstrates how normalized rewrites provide practical provability tools for analyzing these logics. The approach yields a tight correspondence between syntactic derivations and tree-transformations, enabling robust proof-search strategies and offering a foundation for formal verification in proof assistants. The framework also points toward future extensions to additional axioms (like $(\sf 5)$ and $(\sf T)$) and broader positive fragments, with an eye toward formalization in systems such as Rocq for certified reasoning about provability. Overall, the work advances the proof theory and computational handling of strictly positive modal logics by unifying semantic tree representations with concrete, structured rewrite dynamics.

Abstract

We study strictly positive logics in the language $\mathscr{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 $\mathscr{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.

Figures (11)

• Figure 1: Modal tree embedding.
• Figure 2: $\sf 4$-rule and $\sf J$-rule. The dash lines indicate portions of the tree that are not affected by the rule.
• Figure 3: The $\sf J$-rule may increase the width and height of a tree.
• Figure 4: ${\tt T} \hookrightarrow^{\mu} \circ \hookrightarrow^{\pi^+} {\tt T}'$ implies ${\tt T} \hookrightarrow^{\pi^+} \circ \hookrightarrow^{\mu} \circ \hookrightarrow^{\mu} {\tt T}'$ if $\mu \in \mathscr{R}$ is applied within the subtree that is duplicated.
• Figure 5: Example of erasing child $6$ after being permuted with $2$.

Theorems & Definitions (72)

• Definition 3.1: $\sf Tree^{\diamond}$
• Lemma 3.2
• proof
• Definition 3.3
• Definition 3.4: Positions
• Definition 3.5: Subtree
• Definition 3.6: Replacement
• Lemma 3.7
• proof
• Definition 3.8: $\mathcal{T}$