An outline of the syllabus - Fall school 2010
References will be given during the lectures.
Big picture
Problems in complexity theory and their reduction to circuit
size problems, the NP/coNP problem and Cook's program.
Background
Proof systems, simulations, theories in the language L_{PV}
and PV in particular. The relevance of lengths-of-proofs lower
bounds for the P/NP problem. Propositional translations.
The existence of an optimal proof system
and of a 'non-trivial' proof search.
Case study (Buss/Nguyen)
EF, G^*_1, PV and S^1_2, and their relations.
Non-examples
Candidate hard tautologies and lower bound methods that
do not work: combinatorial principles, consistency statements,
restriction method, feasible interpolation, boolean
valuations. Possible remedies.
Proof complexity generators
Definitions, examples, statements, applications, conjectures
and problems.
Model-theoretic approach to lower bounds
A general set-up (after Ajtai) and a forcing example. An application
to a Nisan-Wigderson type function.