Timeline for Does this hierarchy of fragments of $I \Sigma_1$ collapse?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 12 at 19:36 | comment | added | Emil Jeřábek | 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$. | |
| Mar 12 at 18:05 | comment | added | Emil Jeřábek | 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. | |
| Mar 12 at 16:32 | comment | added | Lukas Holter Melgaard | 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? | |
| Mar 12 at 16:23 | vote | accept | Lukas Holter Melgaard | ||
| Mar 12 at 16:23 | comment | added | Lukas Holter Melgaard | 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.) | |
| Mar 12 at 11:11 | history | answered | Emil Jeřábek | CC BY-SA 4.0 |