{"id":"arxiv/2611.01248","url":"https://arxiv.org/abs/2611.01248","tags":["math.LO"],"score":0,"title":"Modular proof analysis and cut elimination for the Reflection Calculi $\\mathsf{RC}_1$ and $\\mathsf{QRC}_1$","domain":"math.LO","source":"arxiv","authors":["Joost J. Joosten","Cosimo Perini Brogi"],"reviews":0,"subject":"math.LO","summary":"The reflection calculus with one modality is denoted by $\\mathsf{RC}_1$ and its quantified generalization is known as $\\mathsf{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 ${\\mathrm{GRC1}}$ and ${\\mathrm{GQRC1}}$ for $\\mathsf{RC}_1$ and $\\mathsf{QRC}_1$ respectively. The new calculi derive sequents of the form $A\\Longrightarrow B$ with $A,B$ strictly positive formulas. In particular, the new calculi do…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-31","reactions":{}}