Girard has a representation theorem claiming:
The functions representable in $F$ are exactly those which are provably total in second-order peano arithmetic $PA_2$.
I believe the usual way to prove a function total in $PA_2$ is by induction. Does it matter on which ordinal we do induction on? If so, do we know anything about which classes of functions are provably total under induction for each ordinal?