Separation of bounded arithmetic using a consistency statement

Abstract

This paper proves Buss's hierarchy of bounded arithmetics $S_2^1\subseteq S_2^2\subseteq \cdots \subseteq S_2^i\subseteq \cdots$ does not entirely collapse. More precisely, we prove that, for a certain $D$, $S_2^1⊊S_2^{2D+5}$ holds. Further, we can allow any finite set of true quantifier free formulas for the BASIC axioms of $S_2^1,S_2^2,\dots$. By Takeuti's argument, this implies $\mathrm{P}\ne \mathrm{NP}$. Let $\mathbf{Ax}$ be a certain formulation of BASIC axioms. We prove that $S_2^1/⊢\mathrm{Con}({\mathrm{PV}}_1^{-}(D)+\mathbf{Ax})$ for sufficiently large $D$, while $S_2^{2D+7}⊢\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_2^1/⊢\mathrm{Con}({\mathrm{PV}}_1^{-}(D)+\mathbf{Ax})$ is proved by straightforward adaption of the proof of $\mathrm{PV}/⊢\mathrm{Con}({\mathrm{PV}}^{-})$ by Buss and Ignjatović. $S_2^{2D+5}⊢\mathrm{Con}({\mathrm{PV}}_1^{-}(D)+\mathbf{Ax})$ is proved by $S_2^{2D+7}⊢\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⊢\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_2^{2D+3}⊢\mathrm{Con}({\mathrm{PV}}_q^{-}(D)+\mathbf{Ax})$ is obtained in a straightforward way.

Too many errors, The correctness proof of translation in Section 6.6 has a gap. Section 7 looks problematic