The strength of replacement in weak arithmetic
Stephen A Cook, Neil Thapen · ACM Transactions on Computational Logic · 2006
Thereplacement(orcollectionorchoice) axiom scheme BB(Γ) asserts bounded quantifier exchange as follows: ∀i< |a| ∃x<aϕ(i,x) → ∃w∀i< |a|ϕ(i,[w]i), for ϕ in the class Γ of formulas. The theoryS12proves the scheme BB(Σb1), and thus inS12every Σb1formula is equivalent to a strict Σb1formula (in which all non-sharply-bounded quantifiers are in front). Here we prove (sometimes subject to an assumption) that certain theories weaker thanS12do not prove either BB(Σb1) or BB(Σb0). We show (unconditionally) thatV0does not prove BB(Σb0), where V0(essentially IΣ1,b0) is the two-sorted theory associated with the complexity class AC0. We show that PV does not prove BB(Σb0), assuming that integer factoring is not possible in probabilistic polynomial time. Johannsen and Pollett introduced the theoryC02associated with the complexity class TC0, and later introduced an apparently weaker theory Δb1− CR for the same class. We use our methods to show that Δb1− CR is indeed weaker thanC02, assuming that RSA is secure against probabilistic polynomial time attack.Our main tool is the KPT witnessing theorem.