Forcing with random variables
(proof complexity and arithmetic)

Fall 2004, code TIN069,
Czech title: Dukazova slozitost a aritmetika

Extent: 2/0, an exam at the end of the course.

Time and place: Thursday 13.15 - 15.oo, MU (Zitna 25, Praha 1), seminar room on the 3rd floor.

Lectures will be in English as a courtesy to our foreign students and postdocs.
Lecturer: Jan Krajicek

Proof complexity studies the time complexity of nondeterministic algorithms. The main problem is the "NP versus coNP" problem, a question whether the computational complexity class NP is closed under the complementation. Central objects studied are propositional proof systems (nondeterministic algorithms for accepting the set of propositional tautologies). Time lower bounds correspond then to lengths-of-proofs lower bounds.

Bounded arithmetic is a generic name for a collection of first-order theories of arithmetic linked to propositional proof systems (and to a variety of other computational complexity topics). The qualification "bounded" refers to the fact that the induction axiom is typically restricted to a subclass of bounded formulas.

The links between propositional proof systems and bounded arithmetic theories 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 to proving independence results in bounded arithmetic. In fact, proving such lower bounds is equivalent to constructing non-elementary extensions of particular models of bounded arithmetic. This offers a very clean and coherent framework for thinking about lengths-of-proofs lower bounds, a one that has been quite successful in the past.

In this course we present a new method for constructing extensions of bounded arithmetic models, and hence for proving independence results and lengths-of-proofs lower bounds. Its brief description could be "forcing with random variables" but it has also features of non-standard analysis and of definable ultraproducts.

The method is flexible enough to allow new proofs of many basic results in bounded arithmetic (and proof complexity), and can serve as an introduction to the area that is alternative to the usual proof-theoretic treatment.


I shall expect that the participants of the course are familiar with basic concepts of mathematical logic on an undergraduate level (e.g., Peano arithmetic, saturated models, ...) and of computational complexity theory (p-time computation, NP-completeness, boolean circuits) but I will not expect any familiarity with bounded arithmetic or proof complexity.


I shall provide copies of relevant material and I shall also write during the semestr lecture notes containing the material covered. Part I. is now available.

Interested to attend?

If you are potentially interested to attend the lectures, send me an email ( - we shall negotiate (at the beginning of the semester) a suitable time schedule via email.