[Proof Complexity] [New Draft] Separation of bounded arithmetic using a consistency statement
Yoriyuki Yamagata
yoriyuki.y at gmail.com
Mon Apr 15 02:44:50 CEST 2019
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
More information about the Proof-Complexity
mailing list