Fall school - Prague 2010

A preliminary syllabus and references

Here is a brief preliminary syllabus for my tutorial at the Fall school; it will get more detailed in time. I list now also a few references good for the background (and I will add specific references for the more advanced topics later on). Looking at some of them could make it easier to follow the lectures but it is not necessary: The tutorial should be more or less self-contained modulo
- some basic logic (e.g. completeness, incompleteness, formal arithmetic, Herbrand's theorem, etc.),
- some basic complexity theory (e.g. P, NP, polynomial hierarchy, Boolean circuits, the notions of one-way functions and pseudo-random generators, the Nisan-Wigderson construction, etc.), and
- some basic proof complexity (Cook-Reckhow proof systems, simulation and p-simulation, basic examples of proof systems like resolution, Frege systems, etc.).

Background references

  • sections 5-8 in Buss's survey on b.a. and proof complexity

  • first two sections in both Buss's chapters in the "Handbook of Proof Theory"

  • S.Cook's and P.Nguyen's book

  • my book Bounded Arithmetic, Propositional Logic and Complexity Theory.

  • chapters 27-30 in my recent book Forcing with random variables and proof complexity (for general proof complexity background and for proof complexity generators)

  • my two older lecture notes on proof complexity

  • my two brief surveys on topics in proof complexity and "feasible witnessing"

  • Pudlak's survey on proof complexity

    Preliminary syllabus

    Proof systems and examples, (p)-simulation, (p)-optimal proof systems, their existence and links to finitistic Godel's theorem. Feasible interpolation, automatizability, disjoint NP pairs.

    Formal arithmetic, language of PV and various theories in this language, 2nd-order extensions, translations of formulas and proofs into propositional logic. Reflection principles and p-simulation.

    Hard tautologies, failure of combinatorial examples. Proof complexity generators: examples, iterability and pseudo-surjectivity, conjectures and known lower bounds.

    Model theory of bounded arithmetic and lengths-of-proofs lower bounds. Versions of forcing.