Forcing with Random Variables and Proof Complexity

or representation theory of groups), and even borrows abstract geometrical concepts like Euler characteristic or Grothendieck ring. However, the most stimulating for proof complexity are its multiple connections to bounded arithmetic. In particular, the task of proving lower bounds (for any particular proof system) is equivalent to the task of constructing suitably non-elementary extensions of models of a bounded arithmetic theory (the theory in question depends on the proof system we want lower bounds for). Most lower bounds can be explained very naturally as constructions of such extensions (and some of the most treasured ones were discovered in this way). In particular, models M to be extended are cuts in models of true arithmetic (they can be "explicitly" obtained as bounded ultrapowers of N). Extensions N of M we are after should preserve polynomial-time properties but should not be elementary w.r.t. NP-properties. There are two things going against each other: Under how...

• Type: Conference
• Year: 2006
• Where: CIE
• Authors: Jan Krajícek
• Keywords: Applied Computing, CIE 2006, Lower Bounds, Most Lower Bounds, Particular Proof System