|
Published Articles >> Table of Contents >> Abstract
19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)
pp. 256-264
The Strength of Replacement in Weak Arithmetic
Stephen Cook, University of Toronto
Neil Thapen, University of Toronto
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2004.1319620
Send link to a friend
| 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.
|
 Additional Information
|
Citation:
Stephen Cook, Neil Thapen,
"The Strength of Replacement in Weak Arithmetic,"
lics,
pp. 256-264,
19th Annual IEEE Symposium on Logic in Computer Science (LICS'04),
2004
|
|
