4
$\begingroup$

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

$\endgroup$

1 Answer 1

5
$\begingroup$

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

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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