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.