Syllabus for J. Krajicek's lectures at the
Most lower bound methods in propositional proof complexity have their origin in bounded arithmetic (not to speak about upper bounds!). The problem in bounded arithmetic that is equivalent to proving proof complexity lower bounds is the problem how to construct extensions of models with suitable properties (non-elementarity). For example, the random restriction method as applied to constant depth proofs is "just" a simple model-theoretic forcing.
Fall school (Sept.'02)
Model theory of bounded arithmetic
I shall discuss natural model-theoretic interpretations of other methods and for other proof systems. The aim is to reduce the main problems to tasks how to construct set systems with particular combinatorial/complexity-theoretic/logical properties. The basic set-up is simple and does not require a preliminary knowledge of either bounded arithmetic or proof complexity.
More detailed syllabus:
Lectures 1 and 2:
Counting mod 3 principle. Lower bound for tree-like resolution. Basic language and canonical structures. Provability and satisfiability predicates. Soundness formula. Extensions of canonical models and lower bounds to the length-of-proofs. Soudness of R^*, R and F_d and the Least Number principle for Sigma^b_1-, bounded universal and bounded formulas respectively.
Lecture 3:
Forcing and games. A construction of an extension of a canonical structure relevant to R^*. The generalization to F_d.
Lecture 4:
Extensions of the canonical models relevant to constant depth Frege systems with modular counting gates. 2-coverings and a reduction theorem.
References for the lectures (symbols x.y refer to a section in my book):
Lectures 1 and 2: 9.1, 9.3, 9.5, and my paper On the weak pigeonhole principle.
Lecture 3: 11.3, 12.7 and W.Hodges's book "Building Models by Games" (OUP).
Lecture 4: 12.6 and some unpublished notes.