Nepomnjascij's Theorem and Independence Proofs in Bounded Arithmetic
Chris Pollett · Electronic colloquium on computational complexity · 2002
The use of Nepomnjascǐi’s Theorem in the proofs of independence results for bounded arithmetic theories is investigated. Using this result and similar ideas, the following statements are proven: (1) At least one of S1 or TLS does not prove the Matiyasevich-Davis-RobinsonPutnam Theorem and (2) TLS does not prove Σ1,1 = Π b 1,1. Here S1 is a conservative extension of the well-studied theory I∆0 and TLS is a theory whose ∆1,2-predicates are precisely LOGSPACE. The relation of TLS from this paper to previously studied theories is also developed and generalizations of the previous two results to quasi-linear settings are discussed as well. Mathematics Subject Classification: 03F30, 68Q15