An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic
Samuel R. Buss, Jan Krajı́ček · Proceedings of the London Mathematical Society · 1994
We develop a method for establishing the independence of some ∑ i b ( α ) formulas from S 2 i ( α ) . In particular, we show that T 2 i ( α ) is not ∀ ∑ 2 i ( α ) -conservative over S 2 i ( α ) . We characterize the ∑ i b -definable functions of T 2 1 as being precisely the functions definable as projections of polynomial local search (PLS) problems.