Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\) (Q1295369)

The theory \(\widehat{\text{ID}}_1\) extends first-order arithmetic PA by adding a predicate \(P_\varphi\) for a fixpoint of each arithmetic formula \(\varphi(n,X)\) positive in \(X\). It contains a fixpoint axiom \(\forall y(P_\varphi(y)\leftrightarrow \varphi(y, P_\varphi)\), but the corresponding induction axiom (saying that \(P_\varphi\) is the least fixpoint) is not postulated. The theory \(\widehat{\text{ID}}_n\) is the result of iterating this construction \(n\) times. The paper provides a Dialectica interpretation of \(\widehat{\text{ID}}_n\) into an equational theory \(P_n\) which is defined using Martin-Löf's universes of transfinite types. Since the ordinals \(\gamma_n= |\widehat{\text{ID}}_n|\) measuring proof-theoretic strength of \(\widehat{\text{ID}}_n\) are cofinal in \(\Gamma_0\), this analysis provides a characterization of ``predicative'' functions.