The provably total NP search problems of weak second order bounded arithmetic

We define a new NP search problem, the “local improvement” principle, about labellings of an acyclic, bounded-degree graph. We show that, provably in PV, it characterizes the ∀Σb 1 consequences of V 1 2 and that natural restrictions of it characterize the ∀Σb 1 consequences of U1 2 and of the bounded arithmetic hierarchy. We also show that over V 0 it characterizes the ∀ΣB 0 consequences of V 1 and hence that, in some sense, a miniaturized version of the principle gives a new characterization of the ∀Πb 1 consequences of S1 2 . Throughout our search problems are “type-2” NP search problems, which take second-order objects as parameters.

• Type: Journal
• Year: 2011
• Where: APAL
• Authors: Leszek Aleksander Kolodziejczyk, Phuong Nguyen, Neil Thapen
• Keywords: APAL 2011, Local Improvement, Np Search Problems, Search Problems, Software Engineering