Logic in Computer Science (LICS 2004)

Paper: The Strength of Replacement in Weak Arithmetic (at LICS 2004)

Authors: Stephen Cook Neil Thapen

Abstract

The replacement (or collection or choice) axiom scheme BB(T) asserts bounded quantifier exchange as follows: ∀i<|a|Ǝx<aϕ(i,x) → Ǝw∀i<|a|ϕ(i,[w]{i}) where ϕ is in the class T of formulas. The theory S_2^1 proves the scheme BB(\sum\nolimits_1^b), and thus in S_2^1 every \sum\nolimits_1^b formula is equivalent to a strict \sum\nolimits_1^b formula (in which all non-sharply-bounded quantifiers are in front). Here we prove (sometimes subject to an assumption) that certain theories weaker than S_2^1 do not prove either BB(\sum\nolimits_1^b) or BB(\sum\nolimits_0^b). We show (unconditionally) that V{0} does not prove BB(\sum\nolimits_0^B), where V{0} (essentially I\sum\nolimits_0^{1,b}) is the two-sorted theory associated with the complexity class AC{0}. We show that PV does not prove BB(\sum\nolimits_0^b), assuming that integer factoring is not possible in probabilistic polynomial time. Johannsen and Pollet introduced the theory C_2^0 associated with the complexity class TC^0 , and later introduced an apparently weaker theory \Delta _1^b - CR for the same class. We use our methods to show that \Delta _1^b - CR is indeed weaker than C_2^0, assuming that RSA is secure against probabilistic polynomial time attack. Our main tool is the KPT witnessing theorem.

BibTeX

  @InProceedings{CookThapen-TheStrengthofReplac,
    author = 	 {Stephen Cook and Neil Thapen},
    title = 	 {The Strength of Replacement in Weak Arithmetic},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {256--264},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }