---
abstract: 'As is well known, Buss’ theory of bounded arithmetic $S^{1}_{2}$ proves $\Sigma_{0}^{b}(\Sigma_{1}^{b})-LIND$; however, we show that Allen’s $D_{2}^{1}$ does not prove $\Sigma_{0}^{b}(\Sigma_{1}^{b})-LLIND$ unless $P = NC$. We also give some interesting alternative axiomatisations of $S^{1}_{2}$.'
author:
- Aleksandar Ignjatović
title: A Note on Induction Schemas in Bounded Arithmetic
---

\[The\][Proposition]{}

We assume familiarity with the theory of bounded arithmetic $S^1_2$ as introduced in Buss’ [@B], as well as with the theory $D^{1}_2$ formulated by Allen in [@A]. In particular, we use the general notation as introduced in [@B] and in [@A]. We denote the language of the theory $S^1_2$ by $L_b$, and the language of the theory $D^1_2$ by $L_d$. Thus, $L_b = \{
0, S, +, \cdot, |x|, {\lfloor {\textstyle \frac{1}{2}} x \rfloor}, \#, \leq \}$, and $L_d=L_b\cup \{
{\mathbin{\mathchoice{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.4ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.3ex\hbox{\vphantom{.}} \over {\smash-}}}}, Bit(x,y), Msp(x,y), $Lsp(x,y) }. The most basic theory for bounded arithmetic (which corresponds to Robinson’s $Q$ in case of $PA$) for the language $L_{b}$ is $BASIC$, introduced by Buss (see [@B]), and for the language $L_{d}$ is $BASIC^{+}$ introduced by Allen (see [@A]) which extends $BASIC$ by a few additional axioms for the extra symbols. Following [@A], we abbreviate $Msp(x,{\lfloor {\textstyle \frac{1}{2}} |x| \rfloor})$ by $Fh(x)$, and $Lsp(x,{\lfloor {\textstyle \frac{1}{2}} |x| \rfloor})$ by $Bh(x)$.

We use the usual hierarchies of formulas to measure the (bounded) quantifier complexity of formulas in our first order theories: $\Sigma^b_i, \Pi^b_i$ and $\Sigma^b_0(\Sigma^b_i)$. Here $\Sigma^b_0(\Sigma^b_i)$ denotes the class of formulas obtained as the least closure of $\Sigma^b_i$ formulas for Boolean connectives and sharply bounded quantifiers.

Theory $D^1_2$ is defined as $BASIC^+$ together with the schema of $\Sigma^b_1$-DCI: $$A(0)\wedge  A(1)\wedge (\forall x)(A(Fh(x))\wedge A(Bh(x)){\rightarrow}A(x)){\rightarrow}(\forall x)A(x).$$

It is shown in [@A] that $D^1_2$ is a sub-theory of (an extension by definitions) of $S^1_2$. In the same paper Allen proves that the following schemas are provable in $D^1_2$:

$\Sigma^b_1$-LPIND

:   $A(0) \wedge  (\forall x) (A({\lfloor {\textstyle \frac{1}{2}} x \rfloor}){\rightarrow}A(x)) {\rightarrow}(\forall x)A(|x|),$

$\Sigma^b_1$-LLIND

:   $A(0) \wedge  (\forall x) (A(x){\rightarrow}A(x+1))
    {\rightarrow}(\forall x)A(||x||).$

Theory $D^{1+}_2$ is the theory obtained from the theory $D^1_2$ by replacing $\Sigma^b_1$-DCI schema with $\Sigma^b_0(\Sigma^b_1)$-LLIND schema.

The method used in the following theorem was introduced in [@I] and applied several times in [@BI].

\[t1\] Every instance of $\Sigma^b_1$-LIND is provable in $D^{1+}_2$.

[[[**Proof: **]{}]{}]{}We argue informally, but working within the framework of $D^{1+}_2$. Let $A(x,\vec{v})$ be an arbitrary $\Sigma^b_1$ formula and assume that for some value of the parameters $\vec{v}$ $$A(0,\vec{v}) \wedge (\forall x)(A(x,\vec{v}){\rightarrow}A(x+1,\vec{v}))$$ holds. Fix these parameters (we do not write them from now on) and pick an arbitrary $x_0$. We must show that $A(|x_0|)$ holds. Consider the formula $${\overline}{A}(x_0,z)\equiv (\forall y,s \leq |x_0|)(y\leq s
\wedge s\leq y+z \wedge A(y){\rightarrow}A(s)).$$ Notice that this is a $\Sigma^b_0(\Sigma^b_1)$ formula.

$$\begin{aligned}
&BASIC^+{\mathrel{\vdash}}(\forall x)(A(x){\rightarrow}A(x+1)){\rightarrow}&\nonumber\\
&({\overline}{A}(x_0,0)\wedge 
(\forall z \leq |x_0|)({\overline}{A}(x_0,{\lfloor {\textstyle \frac{1}{2}} z \rfloor}){\rightarrow}{\overline}{A}(x_0,z)))&\end{aligned}$$

[[[**Proof: **]{}]{}]{}The first two conjuncts hold trivially due to our assumption. Fix an arbitrary $z\leq |x_0|$ such ${\overline}{A}(x_0,{\lfloor {\textstyle \frac{1}{2}} z \rfloor})$ holds, and let $y,s\leq |x_0|$ be such that $y\leq s$, $s\leq y+z$ and such that $A(y)$ is true. Then, by our assumption, if $s\leq y+{\lfloor {\textstyle \frac{1}{2}} z \rfloor}$ we immediately have that $A(s)$ holds. If not, we do know that $A(y+{\lfloor {\textstyle \frac{1}{2}} z \rfloor})$ must be true. Applying our assumption again, this time to the pair $y+{\lfloor {\textstyle \frac{1}{2}} z \rfloor}$ and $y+2\cdot {\lfloor {\textstyle \frac{1}{2}} z \rfloor}$, we get that if $s\leq y+2\cdot {\lfloor {\textstyle \frac{1}{2}} z \rfloor}$ then again $A(s)$ must hold. If $z=2\cdot {\lfloor {\textstyle \frac{1}{2}} z \rfloor}$ this clearly finishes the proof; if $z=2\cdot {\lfloor {\textstyle \frac{1}{2}} z \rfloor}+1$, then we again use the assumption that $(\forall x)(A(x){\rightarrow}A(x+1))$to get $A(s)$, and this implies our claim.

Let $$A^*(x_0,t)\equiv {\overline}{A}(x_0,Msp(|x_0|,||x_0||{\mathbin{\mathchoice{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.4ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.3ex\hbox{\vphantom{.}} \over {\smash-}}}}t)).$$ Then, since $$Msp(u,|u|{\mathbin{\mathchoice{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.4ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.3ex\hbox{\vphantom{.}} \over {\smash-}}}}t)={\lfloor {\textstyle \frac{1}{2}} Msp(u,|u|{\mathbin{\mathchoice{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.4ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.3ex\hbox{\vphantom{.}} \over {\smash-}}}}(t+1)) \rfloor}$$ and $$Msp(|x_0|,||x_0||)=0; \; Msp(|x_0|,||x_0||{\mathbin{\mathchoice{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.4ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.3ex\hbox{\vphantom{.}} \over {\smash-}}}}1)\leq 1$$ the above claim implies that $$\begin{aligned}
&BASIC^+{\mathrel{\vdash}}(\forall x)(A(x){\rightarrow}A(x+1)){\rightarrow}(A^*(x_0,0)\wedge &\nonumber\\
&(\forall t < ||x_0||)(A^*(x_0,t){\rightarrow}A^*(x_0,t+1)).&\end{aligned}$$ Notice that $A^*$ is also a $\Sigma^b_0(\Sigma^b_1)$ formula. Consider the formula $A^1(x_0,t)\equiv (t\leq ||x_0||\wedge
A^{*}(x_0,t))\vee t>||x_0||$. For such a formula we have $$BASIC^+{\mathrel{\vdash}}(\forall x)(A(x){\rightarrow}A(x+1)){\rightarrow}A^1(x_0,0)\wedge
(\forall t)(A^1(x_0,t){\rightarrow}A^1(x_0,t+1)).$$ Since we have LLIND axiom available for $A^1(x_0,t)$, we get $A^1(x_0,||x_0||)$. This means that $A^*(x_0,||x_0||)$ holds; thus $${\overline}{A}(x_0,Msp(|x_0|,||x_0||{\mathbin{\mathchoice{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.4ex\hbox{\vphantom{.}} \over {\smash-}}{\buildrel .\lower.3ex\hbox{\vphantom{.}} \over {\smash-}}}}||x_0||))$$ also holds, and so ${\overline}{A}(x_0,|x_0|)$ holds. This implies $$(\forall y,s \leq |x_0|)(y\leq s \wedge s\leq y+|x_0| 
\wedge A(y){\rightarrow}A(s))$$ is also true. Taking $y=0$ and $s=|x_0|$ we get $A(0){\rightarrow}A(|x_0|)$. By our assumption $A(0)$ holds and thus so does $A(|x_0|)$. This finishes our proof. [$\blacksquare$]{}

Unlike $S^{1}_{2}$ which proves $\Sigma_{0}^{b}(\Sigma_{1}^{b})-LIND$, the next theorem shows that $D^{1}_2$ does not prove $\Sigma_{0}^{b}(\Sigma_{1}^{b})-LLIND$ unless $P = NC$.

If $D^{1}_2$ proves $\Sigma_{0}^{b}(\Sigma_{1}^{b})-LLIND$, then $P=NC$.

[[[**Proof: **]{}]{}]{}Provably total functions of $D^{1}_2$ with $\Sigma_{1}^{b}$ graphs are NC class functions while provably total functions of $S^{1}_{2}$ with $\Sigma_{1}^{b}$ graphs are P-time functions. Thus if $D^{1}_2$ proves $\Sigma_{0}^{b}(\Sigma_{1}^{b})-LLIND$, by the above theorem it also proves $\Sigma_{1}^{b}-LIND$ and thus all P-time functions would be provably total in $D^{1}_2$ and thus also in NC. [$\blacksquare$]{}

We now show a generalisation of the above theorem.

Let $|x|^{(0)}=x$; $|x|^{(n+1)}=|\,|x|^{(n)}\,|$ Then $L^{(n)}IND$ is the schema $$A(0,\vec{u})\wedge(\forall x)(A(x,\vec{u}){\rightarrow}A(x+1,\vec{u})){\rightarrow}A(|x|^{(n)},\vec{u})$$

Thus, for n=0 we get the standard induction; for $A$ a $\Sigma_{1}^{b}$ formula and n=1 we get $\Sigma_{1}^{b}-LIND$; for n=2 we get $\Sigma_{1}^{b}-LLIND$.

For all $n$, $\Sigma_{0}^{b}(\Sigma_{1}^{b})-L^{(n)}IND$ proves $\Sigma_{1}^{b}-LIND$, i.e., in $BASIC^{+}$ the schema $$A(0,\vec{u})\wedge(\forall x)(A(x,\vec{u}){\rightarrow}A(x+1,\vec{u})){\rightarrow}A(||\ldots|x|\ldots||,\vec{u})$$ for all $\Sigma_{0}^{b}(\Sigma_{1}^{b})$ formulas and with arbitrary number of length functions on the right implies the schema $$A(0,\vec{u})\wedge(\forall x)(A(x,\vec{u}){\rightarrow}A(x+1,\vec{u})){\rightarrow}A(|x|,\vec{u})$$ for all $\Sigma^{b}_{1}$ formulas.

[[[**Proof: **]{}]{}]{}In the proof of the Theorem \[t1\] for a $\Sigma_{1}^{b}$ formula $A$ we constructed a $\Sigma_{0}^{b}(\Sigma_{1}^{b})$ formula $A^{1}$ such that $$BASIC^+{\mathrel{\vdash}}(\forall x)(A(x){\rightarrow}A(x+1)){\rightarrow}A^1(x_0,0)\wedge
(\forall t)(A^1(x_0,t){\rightarrow}A^1(x_0,t+1))$$ and $$BASIC^+{\mathrel{\vdash}}A^{1}(x_0,||x||){\rightarrow}(A(x_0,0){\rightarrow}A(x_0,|x|))$$ Repeating this construction with $A^{1}$ in place of $A$ we get a formula $A^{2}$ such that $$\begin{aligned}
 BASIC^+&{\mathrel{\vdash}}&(\forall x)(A^{1}(x_0,x){\rightarrow}A^{1}(x_0,x+1)) \nonumber\\
&& {\rightarrow}A^2(x_0,0)\wedge
(\forall t)(A^2(x_0,t){\rightarrow}A^2(x_0,t+1))\end{aligned}$$ and $$BASIC^+{\mathrel{\vdash}}A^{2}(x_0,|||x|||){\rightarrow}(A^{1}(x_0,0){\rightarrow}A^{1}(x_0,||x||)$$ Continuing this process we get $$\begin{aligned}
    & BASIC^+{\mathrel{\vdash}}(\forall x)(A^{n-2}¥(x_0,x){\rightarrow}A^{n-2}¥(x_0,x+1)){\rightarrow}&
    \nonumber\\
& A^{n-1}(x_0,0)\wedge
(\forall t)(A^{n-1}(x_0,t){\rightarrow}A^{n-1}(x_0,t+1))&\end{aligned}$$ and $$BASIC^+{\mathrel{\vdash}}A^{n-1}(x_0,|x|^{(n)}¥){\rightarrow}(A^{n-2}(x_0,0){\rightarrow}A^{n-2}(x_0,|x|^{(n-1)}¥)$$ By applying $\Sigma_{0}^{b}(\Sigma_{1}^{b})-L^{(n)}IND$ on $A^{n-1}(x_0,t)$ we get $A^{n-1}(x_0,|x|^{(n)})$ which is then easily shown to imply $A(|x|)$.

[9]{} B. Allen: Arithmetising Uniform NC, Annals of pure and applied logic, 53, (1991) S. Buss: , Bibliopolis, 1986. S. Buss and A. Ignjatović: [*Unprovability of consistency statements in fragments of bounded arithmetic*]{}, Annals of Pure and Applied Logic 74 (1995) 221-244. P. Clote, G. Takeuti: Bounded Arithmetic for NC, ALogTIME, L and NL, Annals of pure and applied logic, 56, (1992). A. Ignjatović: [*Delineating computational complexity classes via second order theories with comprehension (I)*]{}, [**Journal of Symbolic Logic**]{}, Volume 60, Number 1, March 1995.

School of Computer Science and Engineering\
University of New South Wales\
Sydney, NSW 2052, Australia
