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 $GRC1$ and $GQRC1$ for ${\mathsf{RC}}_1$ and ${\mathsf{QRC}}_1$ respectively. The new calculi derive sequents of the form $A⟹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 ${\mathsf{RC}}_1$ and ${\mathsf{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 ${\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.