# 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.