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?

  • $\begingroup$ I'm not sure your second paragraph is quite right: consider $\varphi(X, k)\equiv$ "$X(k+2)=1$". Then the first set is just $\{X: \exists y>1(y\in X)\}$, while the second set is $\emptyset$. $\endgroup$ – Noah Schweber Nov 10 '13 at 7:19
  • $\begingroup$ Also, when defining Turing functionals, what do you mean by "r.e.?" Do you mean $\Sigma^0_1$ in $M$? $\endgroup$ – Noah Schweber Nov 10 '13 at 7:22
  • $\begingroup$ @NoahS: Sorry it was a typo should be $\{X\in 2^\omega: \exists k \exists y,z<k \varphi(X|y,z)\}$. Yeah I mean $\Sigma_1^0$ in M. $\endgroup$ – Jing Zhang Nov 10 '13 at 7:28
  • $\begingroup$ That first $\exists k$ is unnecessary. $\endgroup$ – Noah Schweber Nov 10 '13 at 7:57
  • $\begingroup$ I think there's another typo in the sentence beginning "Then the following set . . . :" a verb is missing, and the definition of the following set seems to be incomplete (what is not equal to $X(j)$?). $\endgroup$ – Noah Schweber Nov 10 '13 at 7:59

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

  • 1
    $\begingroup$ Stated differently: the use of a quantifier free formula is always a standard finite number. $\endgroup$ – François G. Dorais Nov 10 '13 at 17:48
  • $\begingroup$ Exactly. If considering $M$-finite instead of $standard$ finite, a special class of r.e. sets, Turing functionals, would always have M-finite use. Since the elements are of the form $(x,y,P,N)$ and it only uses X on the segment of P and N. Obviously the same thing could not be said about any r.e. set. I'm wondering if there is some nice characterization of this. $\endgroup$ – Jing Zhang Nov 11 '13 at 4:41
  • $\begingroup$ @Zhang Jing: Sorry, I am afraid I don't have anything meaningful to say on this question. I guess this depends on the particular $M$ and $X$ you are studying. $\endgroup$ – Lawrence Wong Nov 12 '13 at 7:21
  • $\begingroup$ @LawrenceWong: I feel pretty much the same way as you do. It may get very model dependent indeed. $\endgroup$ – Jing Zhang Nov 13 '13 at 15:02

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?

  • $\begingroup$ My question is exactly your latter formulation. Actually, in the second-order arithmetic if the set is in the second-order part of the universe, it is considered M-finite already therefore, there is no issue about normal form theorem. In general, if we only look at the first-order universe and sets in the second-order universe are those that can be coded by a number (binary representation), a cut can not be M-finite (i.e. coded as a number in M), otherwise, it contradicts with the failure of some induction scheme (for example failure of $\Sigma_2^0$). $\endgroup$ – Jing Zhang Nov 10 '13 at 12:32
  • $\begingroup$ Sure. But if a set causes an induction scheme to fail (e.g. by coding a cut), then that set can never appear in the model, and so that set is not directly relevant to the normal form theorem. You can't expect a normal form theorem provable in $\mathsf{RCA}_0$ or some other system to apply to things that are not models of that system. Nevertheless the normal form theorem itself generalizes without any trouble to give the theorem stated by Simpson. $\endgroup$ – Carl Mummert Nov 10 '13 at 12:34
  • $\begingroup$ I was actually looking at the non-standard first-order universe and trying to see how much computability theory can be developed there. Therefore, different from second-order arithmetic, the induction schemes and comprehension schemes are totally first-order (no set parameters). I wasn't expecting normal form theorem to be true there either. I am wondering if there is any analog that we can say in the non-standard universe. $\endgroup$ – Jing Zhang Nov 10 '13 at 12:40
  • 1
    $\begingroup$ I think the answer to the question "I believe the problem occurs with the consideration of bounded quantifiers here. Is that the root of all evil?" is "yes". If you look at a first-order model $M$ of arithmetic and a set $Z \subseteq M$, if the second-order model generated by $Z$ over $M$ is well defined and satisfies $\Sigma^0_1$ induction, then there will be a normal form theorem for formulas of second-order arithmetic with $Z$ as a parameter. Your example will show that manipulating the bounded quantifiers correctly is more or less exactly the purpose of assuming $\Sigma^0_1$ induction. $\endgroup$ – Carl Mummert Nov 10 '13 at 12:49
  • $\begingroup$ I doubt it is still not true even without bounded quantifiers in general. This may be the result of failure of $I\Sigma_1^{0,X}$ for some set $X$ and a $\Sigma_1^0$-formula without bounded quantifiers. For example, the set could be very complex, like $\emptyset^{(100)}$ for example. $\endgroup$ – Jing Zhang Nov 10 '13 at 14:00

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.