4
$\begingroup$

Does anyone know whether the following hierarchy of fragments of $\mathrm{I} \Sigma_1$ (or rather $\mathrm{I} \Pi_1$) collapses or not?

Let $\Sigma^b_n$ denote formulas in the language of arithmetic with $n-1$ alternations of bounded quantifiers where the front quantifier is a bounded existential. Let $\forall \Sigma^b_n$ denote $\Sigma^b_n$ formulas with some potentially unbounded universal quantifiers in front.

Let $\mathrm{I} \forall \Sigma^b_n$ be the fragment of $\mathrm{I} \Pi_1$ that only has induction on $\forall \Sigma^b_n$ formulas.

Does the hierarchy $\mathrm{I} \forall \Sigma^b_1 \subseteq \mathrm{I} \forall \Sigma^b_2 \subseteq \ ... $ collapse at a finite level?

(The question could just as well be asked for the theories $\mathrm{I} \exists \Pi^b_n $ but it was the hierarchy of $\mathrm{I} \forall \Sigma^b_n$ theories that I ran into in my research.)

At first glance, it seemed to me that this hierarchy would collapse due to the existence of a universal $\Pi_1$ formula $U(x,y)$. Since $U \in \forall \Sigma^b_k$ for some $k$ any instance of $\forall \Sigma^b_n$ induction with $n \geq k$ is equivlanet to $\forall \Sigma^b_k$ induction on $U(m,y)$ for some $m$. But the problem is, that I don't know how strong a theory is needed to prove $\forall x ( U(m,x) \iff \phi(x) ) $ for a given $\phi$. I am pretty sure that for any $\phi \in \Pi_1$ we have $\mathrm{I} \Pi_1 \vdash \forall x ( U(m,x) \iff \phi(x) )$ for some $m$ but for all I know this proof might only go through in a fragment $\mathrm{I} \forall \Sigma^b_n$ of $\mathrm{I} \Pi_1$ such that $\phi \in \forall \Sigma^b_n$ (i.e. the amount of bounded quanitifers needed to prove this in $\mathrm{I} \Pi_1$ might depend on the amount of bounded quantifiers in $\phi$)

Maybe someone here can help shed light on this?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ The standard notation for your $\Sigma^b_n$ is $E_n$. The standard meaning of $\Sigma^b_n$ is that it refers to an analogous hierarchy of bounded formulas in the language of Buss’s theories (which in particular includes the $\#$ function that grows faster than any term in the usual language of arithmetic, and the length function $|x|$ that, among others, makes the graph of $2^x$ trivialy definable by a quantifier-free formula), where additionally sharply bounded quantifiers can apear anywhere in the quantifier prefix and do not count towards the complexity. $\endgroup$
    – Emil Jeřábek
    Commented Mar 12 at 11:20

1 Answer 1

Reset to default
7
$\begingroup$

That the hierarchy collapses follows immediately from the fact that $I\Sigma_1$ (or equivalently, $I\Pi_1$) is finitely axiomatizable.

As a matter of fact, the hierachy collapses already to its $0$th level. By the standard argument, $I\forall_1$ ($I\forall\Sigma^b_0$ in your notation) proves $I\exists_1$. By a result of Kaye [1], $I\exists_1$ (or even its parameter-free version $I\exists_1^-$) proves the MRDP theorem, in the sense that every $\Sigma_1$-formula is provably equivalent to an $\exists_1$-formula. Thus, $I\exists_1$ is equivalent to $I\Sigma_1$.

[1] Richard Kaye: Diophantine induction, Annals of Pure and Applied Logic 46 (1990), no. 1, pp. 1–40, doi 10.1016/0168-0072(90)90076-E.

Improve this answer
$\endgroup$
4
  • $\begingroup$ That's perfect, thanks! Do you have a reference for the fact that $I \Sigma_1$ is finitely axiomatizable? Also, do you know if the same holds for Buss style theories? That is, do the two hierachies of $\forall S_2^n$ theories and $\forall T_2^n$ theories collapse (where $\forall T_2^n$ and $\forall S_2^n$ are supposed to be the theories with induction and polynomial induction respectively on $\forall \Sigma_n^b$ formulas where $\Sigma_n^b$ uses the expanded Buss language and may include sharply bounded quantifiers.) $\endgroup$
    – Lukas Holter Melgaard
    Commented Mar 12 at 16:23
  • $\begingroup$ It seems to me like Kaye's result might generalize to the expanded Buss language but I'm not sure if the sharply bounded quantifiers change the picture. In fact, I've never seen anyone consider Buss style theories with induction on formulas containing unbounded quantifiers. Do you know if that can be found in the literature? $\endgroup$
    – Lukas Holter Melgaard
    Commented Mar 12 at 16:32
  • $\begingroup$ There is no point, as they will coincide with the corresponding theories in the usual language of arithmetic. E.g., $I\Sigma_1$ coincides on the one hand with $I\exists_1$ in the basic language of arithmetic, on the other hand with $I\Sigma_1(L)$ for any language $L$ extending it with provably (in $I\Sigma_1$) $\Delta_1$ predicates and provably total $\Sigma_1$-definable fuinctions. $\endgroup$
    – Emil Jeřábek
    Commented Mar 12 at 18:05
  • $\begingroup$ Oh, I missed the first comment. The finite axiomatizability of $I\Sigma_1$ can be found e.g. in Hájek and Pudlák. I believe I answered the rest of the comment already: all those theories will coincide with (a definitional extension of) $I\Sigma_1$. $\endgroup$
    – Emil Jeřábek
    Commented Mar 12 at 19:36

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .