On the conservation results for local reflection principles

TL;DR

This paper generalizes conservation results for local reflection principles in arithmetic, extending to nonstandard provability predicates and analyzing the conditions under which conservation theorems hold for Rosser predicates.

Contribution

It extends the conservation theorem to nonstandard provability predicates and explores the validity of the theorem for various Rosser provability predicates.

Findings

The second derivability condition D2 ensures the conservation theorem holds.

Conservation theorem validity varies among different Rosser predicates.

Constructed examples show both the holding and failure of the conservation theorem for Rosser predicates.

Abstract

For a class $\Gamma$ of formulas, $\Gamma$ local reflection principle $\mathrm{Rfn}_{\Gamma}(T)$ for a theory $T$ of arithmetic is a scheme formalizing the $\Gamma$-soundness of $T$. Beklemishev proved that for every $\Gamma \in \{\Sigma_n, \Pi_{n+1} \mid n \geq 1\}$, the full local reflection principle $\mathrm{Rfn}(T)$ is $\Gamma$-conservative over $T + \mathrm{Rfn}_{\Gamma}(T)$. We firstly generalize the conservation theorem to nonstandard provability predicates: we prove that the second condition $\mathbf{D2}$ of the derivability conditions is a sufficient condition for the conservation theorem to hold. We secondly investigate the conservation theorem in terms of Rosser provability predicates. We construct Rosser predicates for which the conservation theorem holds and Rosser predicates for which the theorem does not hold.