slideshow 3

Logic seminar

Bounded Arithmetic and Propositional Inconsistency Search Functions

Samuel R. Buss
University of California, San Diego

 

Monday, 27. July 2015 - 13:30
IM, rear building, ground floor
We discuss the strength of fragments of second order bounded arithmetic in defining total NP search (TFNP) problems based on consistency of Frege and extended Frege proofs. This gives new examples of problems that are many-one complete for the second order theories U-1-2 and V-1-2 with proof theoretic strength characterized by polynomial space computation and exponential time computation. (Joint work with Arnold Beckmann.) The talk will begin with a review of the relevant theories of bounded arithmetic, and of the Frege and extended Frege proof systems. It might also cover recent results on propositional proofs of the pigeonhole principle and the Kneser-Lovasz theorem.