Separation of bounded arithmetic using a consistency statement
share
This paper proves Buss's hierarchy of bounded arithmetics S^1_2 ⊆ S^2_2 ⊆...⊆ S^i_2 ⊆... does not entirely collapse. More precisely, we prove that, for a certain D, S^1_2 ⊊ 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 Con(PV^-_1(D) + Ax) for sufficiently large D, while S^2D+7_2 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 Con(PV^-_1(D) + Ax) is proved by straightforward adaption of the proof of PVCon(PV^-) by Buss and Ignjatović. S^2D+5_2 Con(PV^-_1(D) + Ax) is proved by S^2D+7_2 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 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 Con(PV^-_q(D) + Ax) is obtained in a straightforward way.
READ FULL TEXT