> That phenomenon also occurs in classical computable analysis. The subsystem RCA0 of second-order arithmetic has a model in which every real number is computable. But this subsystem still proves that there is no surjection N -> R.

Huh? It's trivial to create an injection R -> N, by encoding each computational algorithm - whether valid or invalid - as a number.