This paper proves Buss's hierarchy of bounded arithmetics $S^1_2 \subseteq S^2_2 \subseteq \cdots \subseteq S^i_2 \subseteq \cdots$ does not entirely collapse. More precisely, we prove that, for a certain $D$, $S^1_2 \subsetneq S^{ 2D+5}_2$ holds. Further, we can allow any finite set of true quantifier free formulas for the BASIC axioms of $S^1_2, S^2_2, \ldots$. By Takeuti's argument, this implies $\mathrm{ P} \neq \mathrm{ NP}$. Let $\mathbf{ Ax}$ be a certain formulation of BASIC axioms. We prove that $S^1_2 \not\vdash \mathrm{ Con}(\mathrm{ PV}^-_1(D) + \mathbf{ Ax})$ for sufficiently large $D$, while $S^{ 2D+7}_2 \vdash \mathrm{ Con}(\mathrm{ PV}^-_1(D) + \mathbf{ Ax})$ for a system $\mathrm{ PV}^-_1(D)$, a fragment of the system $\mathrm{ PV}^-_1$, induction free first order extension of Cook's $\mathrm{ PV}$, of which proofs contain only formulas with less than $D$ connectives. $S^1_2 \not\vdash \mathrm{ Con}(\mathrm{ PV}^-_1(D) + \mathbf{ Ax})$ is proved by straightforward adaption of the proof of $\mathrm{ PV} \not\vdash \mathrm{ Con}(\mathrm{ PV}^-)$ by Buss and Ignjatovi\'c. $S^{ 2D+5}_2 \vdash \mathrm{ Con}(\mathrm{ PV}^-_1(D) + \mathbf{ Ax})$ is proved by $S^{ 2D+7}_2 \vdash \mathrm{ Con}(\mathrm{ PV}^-_q(D+2) + \mathbf{ Ax})$, where $\mathrm{ PV}^-_q$ is a quantifier-only extension of $\mathrm{ PV}^-$. The later statement is proved by an extension of a technique used for Yamagata's proof of $S^2_2 \vdash \mathrm{ Con}(\mathrm{ PV}^-)$, in which a kind of satisfaction relation $\mathrm{ Sat}$ is defined. By extending $\mathrm{ Sat}$ to formulas with less than $D$-quantifiers, $S^{ 2D+3}_2 \vdash \mathrm{ Con}(\mathrm{ PV}^-_q(D) + \mathbf{ Ax})$ is obtained in a straightforward way.
Categories: math.LO cs.LO