In models of PA with restricted induction power (for example, only $I\Sigma_n$ is present), the failure of higher induction scheme is characterised by the existence of definable cuts (like $\Sigma_2$ cuts).

In the standard model (classical setting where the first order universe is just the standard numbers), we have the following normal form $\{X\in 2^\omega: \exists k \varphi(X,k)\}$ (here $\varphi$ is $\Delta_0^0$-formula) is equivalent to $\{X\in2^\omega: \exists k \exists y,z<k \varphi(X|y, z)\}$. Intuitively, it just states that some Oracle Turing Functional characterised by the given $\Sigma_1^0$-formula always has finite use in any convergent computation.

By saying Turing functional, I mean the r.e. set ($\Sigma_1^0$ in $M$) $\phi$ consisting of quardruples $(x,y,P,N)\in M^4$ where $M$ is some given model of arithmetic.

Now my question is to what extent can this be generalized to the non-standard models. More precisely, the naive lift of the previous statement is not true in the non-standard models. For example, consider the model M of $I\Sigma_1 + \neg B\Sigma_2$, then there is a $\Sigma_2$(in fact $\Delta_2$)-cut $I$. Let $a>I$ be some non-standard element. Then the following set $B=\{X\subset M: \exists k \forall z<2^{k+1}-1 \exists j<k \ \ z(j)\neq X(j)\}$ may not be open in the sense that there does not exist a set $A$ consisting of $M$-finite functions in M such that $B=[A]^\prec$ unlike the standard situation. Since every number in $M$ has some binary representation, thus it codes a M-finite set. Therefore, intuitively it says there is some initial segment which is not coded in the model. And we know that $I$ is such a candidate. Furthermore, there is no normal form for this. Even worse, it cannot be considered as a Turing functional as well, since neither the positive use or the negative use is M-finite. I believe the problem occurs with the consideration of bounded quantifiers here. Is that the root of all evil?

1more comment