Reflection and induction for subsystems of HA
Philipp Provenzano
Authors: Philipp Provenzano, Mojtaba Mojtahedi, Fedor Pakhomov and Albert Visser
By a classical result of Leivant and Ono [1,2], the subsystem \(\text{I}\Pi_n\) of PA is equivalent to the scheme of uniform reflection \(\text{RFN}_{\Pi_{n+2}}(\text{EA})\) over elementary arithmetic EA. In the present paper, we study the correspondence between the schemes of induction and reflection for subsystems of Heyting arithmetic HA.
In an intuitionistic setting, complexity classes of formulas behave quite differently than over classical logic. Underpinning this, we show by an application of realizability that reflection over prenex formulas \(\text{RFN}_{\Pi_\infty}(i\text{EA})\) is equivalent over intuitionistic elementary arithmetic \(i\text{EA}\) to just \(\text{RFN}_{\Sigma_1}(i\text{EA})\) or the totality of hyperexponentiation. More generally, for any class \(\Gamma\supseteq\Sigma_1\) of formulas, we have an equivalence between \(\text{RFN}_{\Pi_\infty\Gamma}(i\text{EA})\) and \(\text{RFN}_{\Gamma}(i\text{EA})\). This phenomenon does not have any counterpart in classical logic where \(\Pi_\infty\) exhausts all arithmetical formulas.
As our main result, we show that a suitable generalization of the result by Leivant and Ono holds true intuitionistically. We show for some natural classes \(\Gamma\) of formulas that the principle of induction \(\text{I}\Gamma\) for \(\Gamma\) is equivalent over \(i\text{EA}\) to the reflection principle \(\text{RFN}_{\forall(\Gamma\rightarrow\Gamma)\rightarrow\Gamma}(i\text{EA})\). Here \(\forall(\Gamma\rightarrow\Gamma)\rightarrow\Gamma\) denotes the class of formulas of type \(\forall x. (\phi(x)\rightarrow\psi(x))\rightarrow\theta\) with \(\phi,\psi,\theta\in\Gamma\). This appears as the natural class containing the induction axioms for \(\Gamma\). Note that classically, for \(\Gamma=\Pi_n\), (the universal closure of) this class is just equivalent to \(\Pi_{n+2}\), in harmony with the classical result.
Bibliography
- Daniel Leivant,The optimality of induction as an axiomatization of arithmetic 1,The Journal of Symbolic Logic,vol. 48 (1983), no. 1, pp. 182–184.
- Hiroakira Ono,Reflection principles in fragments of Peano Arithmetic,Mathematical Logic Quarterly,vol. 33 (1987), no. 4, pp. 317–333.