Modular proof analysis and cut elimination for the Reflection Calculi $\mathsf{RC}_1$ and $\mathsf{QRC}_1$

Abstract

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 not use (multi)sets nor nested sequents. For both ${\mathrm{GRC1}}$ and ${\mathrm{GQRC1}}$ it is shown that the cut-rule is admissible. As a consequence, it is proven that the calculi are deductively equivalent to $\mathsf{RC}_1$ and $\mathsf{QRC}_1$ respectively. The cutfree systems are used to prove uniform interpolation for the two reflection calculi. In addition, ${\mathrm{GRC1}}$ is used to give a syntactic proof of Dashkov's Theorem to the extent that $\mathsf{RC}_1$ is the strictly positive fragment of the provability logic ${\mathsf{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.