Turing Functional and $\Sigma_1^0$-formulas in models of fragments of PA

Question

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?

Answer 1

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$.

Answer 2

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?

Answer 3

(This is essentially the same point as in Carl's answer but it avoids fully expanding to second-order models.)

The theory IΣ₁ is the minimal subsystem of PA where all of basic computability theory works as usual. This is because IΣ₁ is equivalent to the fact that total computable functions (i.e. total Σ₁-definable functions) are closed under primitive recursion.

To formalize and understand the idea of oracle computation in a model M of IΣ₁, you need to expand M to a model M_X with a new predicate symbol interpreted by the oracle X. Since the expanded language has new Σ₁ formulas involving the new predicate symbol, it may fail to satisfy IΣ₁ and therefore basic computability theory may not work as expected in M_X.

The example you give, where X is a cut of M illustrates this well but having M-finite initial segments is not enough for M_X to satisfy IΣ₁. Indeed, if M satisfies IΣ₁ then the halting set K (relative to M) has M-finite initial segments, but M_K satisfies IΣ₁ if and only if M satisfies IΣ₂ since every Σ₂ formula over M is equivalent to a Σ₁ formula over M_K. In the case where M fails to satisfy BΣ₂, then M_K will fail to satisfy BΣ₁ and bounded quantifiers will behave very badly in M_K. However, since BΣ₂ is weaker than IΣ₂, bounded quantifiers are not the end of the story.