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 



Weak Bounded Arithmetics
$\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].


