Modular proof analysis and cut elimination for the Reflection Calculi RC1 and QRC1
Abstract
The reflection calculus with one modality is denoted by RC1 and its quantified generalization is known as QRC1. These decidable calculi are of interest since they generate the strictly positive fragments of the (quantified) provability logic for theories like Peano Arithmetic and Heyting Arithmetic. We introduce analytic cut-free calculi GRC1 and GQRC1 for RC1 and QRC1 respectively. The new calculi derive sequents of the form ALongrightarrow B with A,B strictly positive formulas. In particular, the new calculi do not use (multi)sets nor nested sequents. For both GRC1 and GQRC1 it is shown that the cut-rule is admissible. As a consequence, it is proven that the calculi are deductively equivalent to RC1 and QRC1 respectively. The cutfree systems are used to prove uniform interpolation for the two reflection calculi. In addition, GRC1 is used to give a syntactic proof of Dashkov's Theorem to the extent that RC1 is the strictly positive fragment of the provability logic GL. The paper also introduces non-analytic calculi that are conceptually easier but proof-theoretically behave badly. It is shown that even those systems allow direct cut-elimination: the benefits of the strict positivity outweigh the draw-backs of a non-analytic calculus in these cases.
Related
- Instability of Gaussian elimination is exponentially rare (proof of partial result)
- Modular Heights of Unitary Shimura Varieties III: Proof of the Main Theorem
- An Algebraic Proof of the Non-Modularity of Solutions to the Canonical Modular Differential Equation
- A generalised and modular proof-theoretic semantics for sequent systems
- On the foundations of logic and probability, I. Modal sentential calculi
BibTeX
@misc{joosten2026modular,
title = {{Modular proof analysis and cut elimination for the Reflection Calculi $\mathsfRC_1$ and $\mathsfQRC_1$}},
author = {Joost J. Joosten and Cosimo Perini Brogi},
howpublished = {arXiv},
year = {2026},
month = nov,
doi = {10.48550/arxiv.2611.01248},
eprint = {2611.01248},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2611.01248},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Modular proof analysis and cut elimination for the Reflection Calculi RC_1 and QRC_1
AU - Joost J. Joosten
AU - Cosimo Perini Brogi
PY - 2026
DA - 2026/11/01
PB - arXiv
DO - 10.48550/arxiv.2611.01248
UR - https://arxiv.org/abs/2611.01248
AB - The reflection calculus with one modality is denoted by RC_1 and its quantified generalization is known as QRC_1. These decidable calculi are of interest since they generate the strictly positive fragments of the (quantified) provability logic for theories like Peano Arithmetic and Heyting Arithmetic. We introduce analytic cut-free calculi GRC1 and GQRC1 for RC_1 and QRC_1 respectively. The new calculi derive sequents of the form ALongrightarrow B with A,B strictly positive formulas. In particular, the new calculi do not use (multi)sets nor nested sequents. For both GRC1 and GQRC1 it is shown that the cut-rule is admissible. As a consequence, it is proven that the calculi are deductively equivalent to RC_1 and QRC_1 respectively. The cutfree systems are used to prove uniform interpolation for the two reflection calculi. In addition, GRC1 is used to give a syntactic proof of Dashkov's Theorem to the extent that RC_1 is the strictly positive fragment of the provability logic GL. The paper also introduces non-analytic calculi that are conceptually easier but proof-theoretically behave badly. It is shown that even those systems allow direct cut-elimination: the benefits of the strict positivity outweigh the draw-backs of a non-analytic calculus in these cases.
ER -