 where in (Id2) \(F(x)\) is an arbitrary formula of \(\bID_1\) and \(A(x,F)\) arises from \(A(x,P)\) by replacing every occurrence of \(P(t)\) in the formula by \(F(t)\). Collectively these axioms assert that \(I_A\) is the least fixed point of \(\Gamma_A\), or more accurately the least among all sets of natural numbers definable in the language of \(\bID_1\). \(\bID_1^i\) will be used to denote the intuitionistic version. Its subtheory \(\bID_{1}^{i}(\cO)\) is obtained by just adding the predicate symbol \(I_A\) and the pertaining axioms (Id1) and (Id2), where \(\Gamma_A\) is the operator that defines Kleene’s \(\cO\) (cf.  Definition 5.1).