Forcing with Random Variables

COMPUTER SCIENCE/DISCRETE MATH SEMINAR, II
Topic:Forcing with Random Variables
Speaker:Jan Krajicek
Affiliation:Academy of Sciences of Czech Republic
Date:Tuesday, February 8
Time/Room:10:30am - 12:30pm/S-101

The links between propositional proof systems and bounded arithmetic (a generic name for a collection of first-order theories of arithmetic) have many facets but informally one can view them as two sides of the same thing: The former is a non-uniform version of the latter. In particular, it is known that proving lengths-of-proofs lower bounds for propositional proof systems is very much related (even equivalent, when formulated properly) to constructing models of bounded arithmetic. This offers a very clean and coherent framework for thinking about lengths-of-proofs lower bounds. I shall describe a new method for constructing relevant bounded arithmetic models, and hence for lengths-of-proofs lower bounds. I will attempt to specialize this to proof complexity without going (explicitly) through bounded arithmetic. The models are Boolean-valued and are built from random variables. Some of the models appear interesting in their own right but we interpret the construction primarily as a method that reduces a lengths-of-proofs lower bound to a purely combinatorial/complexity-theoretic statement about a family of random variables samplable in a particular way. In the talk I will put emphasis on this aspect of the method.