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.