Lengths of propositional proofs

Jan Krajicek

Two fundamental problems connecting logic and computational complexity theory are:

1. Is there a polynomial time algorithm recognizing the set of satisfiable propositional formulas?

This is the famous "P versus NP" problem of S.Cook. If the answer is negative then it still makes a sense to ask:

2. Is there a propositional calculus admitting short proofs of all tautologies ("short" meaning "of size polynomial in the size of the tautology")?

(This is the "NP versus coNP" problem.)

Both problems are expected to have a negative answer. The negative answer to the second problem implies, in particular, super-polynomial lengths-of-proofs lower bounds for all concrete calculi considered in logic (e.g., resolution or Hilbert-style calculi).

Some such lower bounds have been, in fact, established. The aim of the course is to explain main results and methods (and problems) in this area, with emphasis on topics that appear to me to be stimulating for further research. I shall also treat necessary background from boolean complexity, and some connections to bounded arithmetic.

Brief outline of the course: