Structure and definability in general bounded arithmetic theories

✍ Scribed by Chris Pollett

• Publisher: Elsevier Science
• Year: 1999
• Tongue: English
• Weight: 399 KB
• Volume: 100
• Category: Article
• ISSN: 0168-0072
• DOI: 10.1016/s0168-0072(99)00008-1

✦ Synopsis

The bounded arithmetic theories R i 2 ; S i 2 , and T i 2 are closely connected with complexity theory. This paper is motivated by the questions: what are the b i+1 -deÿnable multifunctions of R i 2 ? and when is one theory conservative over another? To answer these questions we consider theories Ri 2 ; Ŝi 2 , and T i 2 where induction is restricted to prenex formulas. We also deÿne T i; 2 which has induction up to the 0 or 1-ary L2-terms in the set . We show Ŝi 2 = S i 2 and T i 2 = T i 2 and

We show that the ˆ b i+1 -multifunctions of T i; 2 are FP p i (wit; | |) and that those of Ri 2 are FP p i (wit; loglog). For ˆ b i+k+2 -deÿnability we get FP p i+k+1

(wit; 1) for all these theories. Write 2 ˙ for the set of terms 2 min('(x);|t(x)|) where ' is a ÿnite product of terms in and t ∈ L2. We prove T i;2 ˙ 2 4 B( ˆ b i+1 ) T i+1; 2 and we show T i; 2 ˆ b i+1 -IND provided ⊆ O2(|id|). This gives a proof theoretic proof that S i 2 b i+1 -LIND and Ri 2