Analogy of $\omega$-models in constructive mathematics I was thinking maybe you should try something smaller, like odels of second-order Heyting arithmetic. However, I do not know good references, as I was still in the kindergarten in the 70's.

Analogy of $\omega$-models in constructive mathematics While you're at it please also add an explanation of what sort of language and logic you're trying to model. Are you going for intuitionistic (subsystems of) second-order arithmetic?

Is every computable real primitively recursively computable? You could just ask: Is every real number that is the limit of a computable Cauchy sequence of rationals with a fixed rate of convergence also the limit of a primitive recursive such sequence?