Formulas that can be proved from the uniform reflection schema

45 Views Asked by At

Let $T$ be a sound, r.e. theory containing elementary arithmetic. By the uniform reflection schema of $T$ ($\mathrm{RFN}(T)$) I mean the schema that expresses the soundness of $T$:
$\forall x(\square_T\phi(\dot{x})\to \phi(x))$
where $\phi(x)$ is a formula, $\square_T\phi(\dot{x})$ means $\mathrm{Prov}_T(\ulcorner\phi(\dot{x})\urcorner)$, i.e. $\phi(x)$ is $T$-provable. Every such instance is also equivalent to $\forall x\,\square_T\phi(\dot{x})\to \forall x\,\phi(x)$.

Consider a $\Sigma_n$-formula $\phi(x)$; let $\mathrm{RFN}_{\Sigma_n}(T)$ denote $\mathrm{RFN}(T)$ restricted to $\Sigma_n$-formulas, $n\geq 1$. If $T\vdash \forall x\,\square^m_T\phi(\dot{x})$ for some $m$ (here $\square_T^m$ means $\square_T\square_T...\square_T$ $m$ times), then clearly $T+\mathrm{RFN}_{\Sigma_n}(T)\vdash \forall x\,\phi(x)$.

But is the converse also true? I feel I might be missing some silly counterexample, but until now I can only find examples supporting the converse.
For example, $\mathrm{RFN}_{\Pi_1}(T)$ is equivalent to $\mathrm{Con}(T)$, and also $\forall x\,\square_T(\mathrm{Proof}_T(x,\ulcorner\bot\urcorner)\to \bot)$ is an instance of explicit reflection principle which is provable in $T$.
I also read from Takeuti (page 131) that the same probably goes for Paris-Harrington principle (which is equivalent to $\Pi_2$-reflection of PA).