Weak Bounded Arithmetics

Question

Let $\Sigma^b_i$ and $\Pi^b_i$ formulas be bounded formulas defined by Buss in language of $L_b$. $PIND(\phi(x))$ is the formula:

$$\phi(0)\land \forall x(\phi(\left \lfloor \frac{x}{2} \right \rfloor)\rightarrow \phi(x))\rightarrow \forall x \phi(x)$$

• For $i\geq0, S^i_2=BASIC+PIND\:\Sigma^b_i$,
• For $i\geq0, T^i_2=BASIC+I\Sigma^b_i$ and,
• $S_2=\bigcup_{i\in \mathbb{N}}S^i_2$, $T_2=\bigcup_{i\in\mathbb{N}}T^i_2$.

I see a lot of papers that study these theoreis and their relationship with complexity classes, but I can not find any paper about $S^0_2$ or $T^0_2$. What's the reason?

Is it because they are too weak to prove or disprove any complexity resault? Also I want to know is there any unconditional independent complexity theory statement from $S^0_2$ or $T^0_2$?

Thanks

Answer 1

$\def\dotminus{\mathbin{\dot{-}}}$Actually, there are a number of papers on variants of $S^0_2$, $T^0_2$, and other theories axiomatized by $\Sigma^b_0$ (sharply bounded) schemata, in particular:

[1] Gaisi Takeuti, Sharply bounded arithmetic and the function $a\dotminus1$, in: Logic and Computation (W. Sieg, ed.), Contemporary Mathematics vol. 106, American Mathematical Society, 1990, pp. 281–288.

[2] Jan Johannsen, On the weakness of sharply bounded polynomial induction, in: Computational Logic and Proof Theory (G. Gottlob, A. Leitsch, and D. Mundici, eds.), Lecture Notes in Computer Science vol. 713, Springer, 1993, pp. 223–230.

[3] Jan Johannsen, A note on sharply bounded arithmetic, Archive for Mathematical Logic 33 (1994), no. 2, pp. 159–165.

[4] Jan Johannsen, A model-theoretic property of sharply bounded formulae, with some applications, Mathematical Logic Quarterly 44 (1998), no. 2, pp. 205–215.

[5] Emil Jeřábek, The strength of sharply bounded induction, Mathematical Logic Quarterly 52 (2006), no. 6, pp. 613–624.

[6] Sedki Boughattas and Leszek Kołodziejczyk, The strength of sharply bounded induction requires MSP, Annals of Pure and Applied Logic 161 (2010), no. 4, pp. 504–510.

[7] Leszek Kołodziejczyk, Independence results for variants of sharply bounded induction, Annals of Pure and Applied Logic 162 (2011), no. 12, pp. 981–990.

[8] Emil Jeřábek, Open induction in a bounded arithmetic for $\mathrm{TC}^0$, Archive for Mathematical Logic 54 (2015), no. 3–4, pp. 359–394, Section 7.

You can find details in the papers themselves, but a few general comments en lieu of a reader’s guide:

• These theories tend to be extremely sensitive to the choice of language. The language used by Buss is suitable for extensions of $S^1_2$ or $T^1_2$, but not for weaker theories (even reasonable theories like $R^1_2$): typically, people add function symbols like $\lfloor x/2^y\rfloor$ (aka MSP) or $x\dotminus y$, which also facilitates sequence coding.

• Most of these theories are pathologically weak, in that they are (unconditionally!) known not to prove the totality of ridiculously simple functions like $\lfloor x/3\rfloor$, or even $x\dotminus y$ (in some cases). This also exhibits that they have no meaningful connection to computational complexity, and complexity classes: on the one hand, they all include $\mathrm{TC}^0$-complete functions (viz. multiplication), so the weakest decent class they could correspond to would be $\mathrm{TC}^0$, but on the other hand, they omit various simple $\mathrm{AC}^0$ functions.

An exception to the second point is $T^0_2$ in a language with MSP, which is a well-behaved theory equivalent to the theory $\mathrm{PV}_1$ of poly-time functions [5]. Likewise, $\Sigma^b_0$-MIN in this language is equivalent to $T^1_2$, and $\Sigma^b_0$-LENGTH-MIN to $S^1_2$. However, these theories are still pathologically weak in Buss’s original language: this is known for $T^0_2$ [6,7], and suggested for the MIN schemata by the results of [8].