[Proof Complexity] [New Draft] Separation of bounded arithmetic using a consistency statement

[Yoriyuki Yamagata]

A new draft titled "Separation of bounded arithmetic using a
consistency statement" is available from
https://www.dropbox.com/s/g22x84rfdqmyx82/separation-of-bounded-arithmetic.pdf?dl=0

The identical preprint will appear at arXiv soon.

Abstract
---
This paper proves Buss's hierarchy of bounded arithmetics S^1_2
\subseteq S^2_2 \subseteq \cdots \subseteq S^i_2 \subseteq \codes 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, ....  By Takeuti's argument, this implies P != NP.  Let
Ax be a certain formulation of BASIC axioms.  We prove that S^1_2
\not\vdash Con(PV^-_1(D) + Ax) for sufficiently large D, while
S^{2D+5}_2 \vdash Con(PV^-_1(D) + Ax for a system PV^-_1(D), a
fragment of the system PV^-_1, induction free first order extension of
Cook's PV, of which proofs contain only formulas with less than D
connectives.  S^1_2 \not\vdash Con(\PV^-_1(D) + Ax) is proved by
straightforward adaption of the proof of PV \not\vdash Con(\PV^-) by
Buss and Ignjatovic.  S^{2D+7}_2 \vdash Con(PV^-_1(D) + Ax) is proved
by S^{2D+7}_2 \vdash Con(PV^-_q(D+2) + Ax), where PV^-_q is a
quantifier-only extension of PV^-.  The later statement is proved by
an extension of a technique used for Yamagata's proof of S^2_2 \vdash
Con(PV^-), in which a kind of satisfaction relation Sat is defined.
By extending Sat to formulas with less than D-quantifiers, S^{2D+3}_2
\vdash Con(PV^-_q(D) + Ax) is obtained in a straightforward way.
---

Ok, I don't believe it at all,  but I think techniques may have
something worth discussing.

Best,
--
Yoriyuki Yamagata