This is a purely logical question, but I think it's adjacent enough to CS that it's worth a shot here.
Take 2nd order Heyting Arithmetic, say Heyting Arithmetic with an extra sort of (unary) predicates, a membership relation $\in$, and the full comprehension axiom $$ \exists X\forall n\quad n\in X \Leftrightarrow \phi(n) $$
for every formula not containing $X$.
Suppose I have a formula $\psi(X)$ with some free predicate variable $X$, and some base formula $\phi$. I want to define the following predicate $I$:
$$I(0) \equiv \phi$$ $$ I(n+1)\equiv \psi(I(n))$$
A related question convinced me that it is possible to do this in classical 2nd order arithmetic, but there it is possible to apply a trick, namely have $I(n+1)$ depend on a number $k$ such that $k = 1$ iff $I(n)$ holds. Such a number does not (necessarily) exist in the intuitionistic setting.
As a side note, in 3rd order logic, one could simply define the graph of $I$, no classical logic needed.
So my question is:
Is it always possible to define the predicate $I$ in the intuitionistic setting?