Short note: least fixed points versus least closed points (Q2238139)

An arithmetical formula \(\varphi[X, n]\) (i.e.\ a formula of the language of second-order arithmetic without bound set variables) in which the set variable \(X\) occurs only positively is called an \(X\)-positive operator form. This short note establishes the equivalence of the least fixed points and least closed points of \(X\)-positive operator forms in a extension \[ \mathsf{FP}_0:= \mathsf{ACA}_0 + \exists Z\, \forall n(\varphi[Z, n] \leftrightarrow n \in Z), \] where \(\mathsf{ACA}_0\) is the well-know subsystem of second-order arithmetic whose non-logical axioms comprise the defining axioms for all primitive recursive functions and relations, the axiom schema of arithmetical comprehension and the induction axiom.