Proof complexity lectures in Spring 2021
This page will contain slides (and other comments) used in my lectures during the Spring 2021 Proof complexity course.
Slides accompany the lectures but are not the whole lectures: not everything said is also written in the slides.
Errata discovered during or after each lecture will be marked in yellow in the pdf file holding the respective slides.
Sections/pages refer to my 2019 "Proof Complexity" book, see the main course page for a link.
Slides often do not contain attributions or complete references - these can be found in the book.
The book ought to be the main source for individual study.
Lecture 1 (2.III.2021)
Course introduction, the P/NP problem, limited extension.
Slides.
Sections: 1.1 - 1.3 (for intro) and 5.1 (for limited extension).
Remarks:
- links to Cook's 1971 paper and to Godel's letter to von Neumann are at the page of the Logic and Complexity course:
https://www2.karlin.mff.cuni.cz/~krajicek/ls.html
- a proof-sketch of the *existence* of a NP-complete problem: two slides (a response to Mr.Jezil's question)
Lecture 2 (9.III.2021)
Examples of proof systems
Slides.
Sections: 5.1 (Frege systems), 6.1 (R), 6.3 (CP), 6.2 (PC), 7.4.3 (theory T)
Lecture 3 (16.III.2021)
Basic notions and problems, from SAT algorithms to proof systems
Slides.
Sections: 1.5 (basic notions and problems), 5.2 (DPLL and R^*)
Remarks:
- more on proof complexity analysis of SAT algorithms can be found in
S.Buss and J.Nordstrom, Proof complexity and SAT solving, (2019).
Lecture 4 (23.III.2021)
Upper bounds on lengths-of-proofs, propositional translations of FO formulas and proofs
Slides.
Sections: 2.5 (depth dp), 6.4 (semi-algebraic systems), 8.1. (bounded arithmetic), 8.2 (the translation), 8.6 (general correspondence)
Lecture 5 (6.IV.2021)
Towards lower bounds
Slides.
Sections: 1.5 (PHP), 2.4 + 10.3 (EF), 11.2+3 (PHP in F - counting flas), 13.1 (adversary arguments), 15.1 (depth, systems F_d)
Lecture 6 (13.IV.2021)
Ajtai's theorem, part 1
Slides.
Section: 15.1
Lecture 7 (20.IV.2021)
Ajtai's theorem, part 2
Slides and extra slides 29-31.
Sections: 15.2, 15.3
Lecture 8 (27.IV.2021)
Ajtai's theorem: corollaries, variants, open problems
Slides.
Sections: 8.1 (\Delta_0-PHP problem), 11.4 (weak PHP), 15.4 and 15.5 (other comb.principles and relations among them), 15.6 (the system with parity connective)
Lecture 9 (4.V.2021)
Feasible interpolation, part 1 (basic set-up)
Slides.
Sections: 1.1 (DNF representation of functions, Thm.1.1.3 - Craig's and Lyndon's), 1.4 (circuits), 5.6 (FI for R), 13.5 (FI implies lower bounds, Clique/Color), 17.1 (basic FI set-up).
Lecture 10 (11.V.2021)
Feasible interpolation, part 2 (communication complexity)
Slides.
Section: 17.4 (communication complexity, protocols and circuits).
Lecture 11 (18.V.2021)
Feasible interpolation, part 3 (FI for semantic derivations and consequences)
Slides.
Sections: 17.5 (semantic derivations) and 17.6 (simple examples)
Lecture 12 (25.V.2021)
Feasible interpolation, part 4 (generalizations, limitations, automatizability)
Slides.
Sections: 18.1-2 (an example generalization), 17.3 (automatizability), 18.7 (limitations)
Lecture 13 (1.VI.2021)
Optimality of proof systems and proof search algorithms, concluding metamathematical remarks
Slides.
Sections: 21.1-3
Remarks:
- formulas in the set H_Q are a more pedestrian version of reflection formulasused in Sec.21.1 (see also end of Lecture 4)
- more on the strength of proof systems in my Toronto lecture Logical foundations of complexity theory
- for optimality of proof search see also my paper
- for further problems equivalent to the optimality problem see p.471 (Subsec.21.6.1)
- pp.475-476: how SAT alg's find their own failure
- p.475 (2nd para): more on strength of theories behind proof systems