Full and hat inductive definitions are equivalent in NBG

Abstract

A new research project has, quite recently, been launched to clarify how different, from systems in second order number theory extending ACA ₀, those in second order set theory extending NBG (as well as those in n + 3-th order number theory extending the so-called Bernays−Gödel expansion of full n + 2-order number theory etc.) are. In this article, we establish the equivalence between ${\Delta^1_0\mbox{\bf-LFP}}$ and ${\Delta^1_0\mbox{\bf-FP}}$, which assert the existence of a least and of a (not necessarily least) fixed point, respectively, for positive elementary operators (or between ${\Delta^{n+2}_0\mbox{\bf-LFP}}$ and ${\Delta^{n+2}_0\mbox{\bf-FP}}$). Our proof also shows the equivalence between ID ₁ and ${\widehat{\it ID}_1}$, both of which are defined in the standard way but with the starting theory PA replaced by ZFC (or full n + 2-th order number theory with global well-ordering).