Tree Rewriting Calculi for Strictly Positive Logics
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913807541993472 |
|---|---|
| author | Santiago-Fernández, Sofía Fernández-Duque, David Joosten, Joost J. |
| author_facet | Santiago-Fernández, Sofía Fernández-Duque, David Joosten, Joost J. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_18240 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Tree Rewriting Calculi for Strictly Positive Logics Santiago-Fernández, Sofía Fernández-Duque, David Joosten, Joost J. Logic in Computer Science Logic 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. |
| title | Tree Rewriting Calculi for Strictly Positive Logics |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2504.18240 |