Godel's system $T$ means different, although equivalent, things to different people. To people working in the traditon of mathematical logic, $T$ is a quantifier-free equational theory of arithmetic higher-order functionals of finite type closed under higher-order primitive recursion, which can be given as the natural extension of $PRA$ to higher-order functionals of finite type. To a type theorist or someone working in programming language foundations, $T$ is an extension of the simply typed lambda calculus, given by adding typing rules for the natural numbers, higher order functionals, and zero, successor, and primitive recursion on the functionals. Again, it is clear how these are distinct and yet equivalent formulations. As is well known, the proof theoretic strength of $T$ is equivalent to that of $PA$.

Dana Scott introduced a system now called $PCF$ (c.f. this note on Wikipedia for the relevant history), which is an extension of the simply typed lambda calculus in the same way as $T$, and is defined the same ways as $T$ is but with the addition of some mechanism, usually the fixedpoint Y combinator, to allow for general recursion of the higher-order functionals. Thus the difference between $T$ and $PCF$ is the difference between primitive and general recursion, and as a result $PCF$ breaks $T$'s strong normalization/termination property.

What is the proof theoretic strength of $PCF$, that is, $T$ + a mechanism for higher-order general recursion? I have been looking through the literature to see if this is known and the only thing I could find was section 8 of Avigad and Feferman's paper on $T$, where they introduce a $\mu$ operator that converts all arithmetical formulae to a quantifier free form and derive the proof theoretic strength of $T + \mu$, but I cannot follow the arguments of some of that section and if a higher-order general recursion scheme is derivable from $\mu$ (which would make sense given the name), then I am having trouble seeing that argument. Is the argument a higher-order analog of Kleene's normal form theorem?