Turing Functional and $\Sigma_1^0$-formulas in models of fragments of PA 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?
 A: I am not sure whether I've correctly understood your question, but here is my attempt.
What I wish to say is (that not much induction is needed to show) that if we take away the bounded universal quantifiers in $\Sigma_1$, then only a finite amount of the oracle is read in any run of the corresponding Turing machine that leads to a halt.
Consider an existential sentence $\varphi(X)$ in the language of arithmetic that looks like
 $$\exists\bar v\ \Bigl(\bigwedge_{i=1}^np_i(\bar v)\in X
                  \wedge\bigwedge_{j=1}^mq_j(\bar v)\not\in X
                  \wedge\bigwedge_{k=1}^\ell r_k(\bar v)=s_k(\bar v)\Bigr),$$
where the $p_i$'s, $q_j$'s, $r_k$'s and $s_k$'s are terms.
Suppose $A\subseteq M\models\mathrm I\Delta_0+{\exp}$ such that $M\models\varphi(A)$.  Take $\bar c\in M$ which witnesses this fact.  Then any $X\subseteq M$ whose behaviour on
 $p_1(\bar c),\ldots,p_n(\bar c),q_1(\bar c),\ldots,q_m(\bar c)$ agrees with that of $A$ would satisfy $\varphi(X)$ too.  With $\mathrm I\Delta_0+{\exp}$, one can find $M$-finite sets $X$ that agree with $A$ on those $m+n$ elements of $M$.
A: Simpson, Subsystems of Second-Order Arithmetic, states an analogue of the normal form theorem that is provable in $\mathsf{RCA}_0$:

Theorem II.2.7 (normal form theorem) Let $\phi(X)$ be a $\Sigma^0_1$ formula. Then we can find a $\Sigma^0_0$ formula $\theta(s)$ such that $\mathsf{RCA}_0$ proves
  $$
(\forall X)[\phi(x) \leftrightarrow (\exists m)\theta(X[m])].
$$
  Here we write $X[m] = \langle \xi_0, \xi_1, \ldots, \xi_{m-1}\rangle$ where $\xi_i = 1$ if $i \in X$, $0$ if $i \not \in X$. 

$\mathsf{RCA}_0$ is a standard system of second-order arithmetic with induction for $\Sigma^0_1$ formulas with set parameters and with the $\Delta^0_1$ comprehension scheme.  
Therefore, there is some problem with the example that the question tries to construct. I don't see any problem with putting the defining formula $\phi(X)$ from $B$ into normal form. 

It may help to realize that $\mathsf{RCA}_0$ does prove 
$$
(\forall X)(\forall m)(\exists \sigma)[\sigma = X[m]].
$$
This is provable directly by $\Sigma^0_1$ induction. So if $X$ is any set in a model of $\mathsf{RCA}_0$, every initial segment of $X$ is coded by a number in the model. Perhaps (this is just speculation) the question is trying to apply the universal quantifier $(\forall X)$ to a set $X$ that is not actually going to appear in the model, because the existence of that set would force $\Sigma^0_1$ induction to fail? 
A: (This is essentially the same point as in Carl's answer but it avoids fully expanding to second-order models.)
The theory IΣ1 is the minimal subsystem of PA where all of basic computability theory works as usual. This is because IΣ1 is equivalent to the fact that total computable functions (i.e. total Σ1-definable functions) are closed under primitive recursion.
To formalize and understand the idea of oracle computation in a model M of IΣ1, you need to expand M to a model MX with a new predicate symbol interpreted by the oracle X. Since the expanded language has new Σ1 formulas involving the new predicate symbol, it may fail to satisfy IΣ1 and therefore basic computability theory may not work as expected in MX.
The example you give, where X is a cut of M illustrates this well but having M-finite initial segments is not enough for MX to satisfy IΣ1. Indeed, if M satisfies IΣ1 then the halting set K (relative to M) has M-finite initial segments, but MK satisfies IΣ1 if and only if M satisfies IΣ2 since every Σ2 formula over M is equivalent to a Σ1 formula over MK. In the case where M fails to satisfy BΣ2, then MK will fail to satisfy BΣ1 and bounded quantifiers will behave very badly in MK. However, since BΣ2 is weaker than IΣ2, bounded quantifiers are not the end of the story.
