Fixed points in Peano arithmetic with ordinals (Q1210139): Difference between revisions

By modern proof theory this paper shows that some basic fixed point theory of finitely iterated approximations is conservative over Peano arithmetic PA. The finite iteration is hidden in the \(\Sigma^ \Omega\)- reflection axioms and vanishes when \(\leq_{0n}\)-relativization is substituted for \(<_{0n}\)-relativization: then by chancelling all ordinal quantifiers and replacing throughout \(P^ \alpha_ A\), \(<_{0n}\) and ordinal variables \(\alpha,\beta,\dots\) by \(P^ 0_ A\equiv\lambda xA(\bot,x)\), \(<_{\mathbb{N}}\), 0 respectively \textit{all} the systems considered become conservative over PA. The question now is how far conservativity over PA holds when ordinal terms \(\omega,\dots\) and appropriate axioms for them are added.