Lengths of propositional proofs
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:
- Motivations, bounded arithmetic, complexity theory.
Basic definitions.
- Effective interpolation, communication complexity,
resolution, cutting planes, discretely ordered modules.
Limits of effective interpolation, cryptographic conjectures.
- Constant-depth Frege systems, partial truth assignments,
switching lemmas, finite forcing. Pigeonhole principle,
counting principles.
- Polynomial rings over finite fields, ideal membership proof
systems, Nullstellensatz, polynomial calculus. Ajtai's theorem
on definability of solutions of symmetric systems of linear
equations.