Logic & Complexity Student Seminar (Summer 2016)
(Jointly organized with Amir Tabatabai)

Time:   Tuesday 3:40pm.
Location:  K334 (Karlin).

Topic: "Bounded Arithmetic and Feasible Complexity Theory"

Description:  A large fraction of complexity theory can be formalized in weak fragments of Peano Arithmetic, including more advanced results such as the PCP Theorem and circuit lower bounds. The goal here is to pinpoint a theory where most results can be formalized, and to show that some conjectures cannot be proved in this theory (see e.g. http://www1.karlin.mff.cuni.cz/~pich/thesis.pdf).

Required Background: Basic knowledge of logic and computational complexity is assumed. Participants are encouraged to ask questions during the lectures in case they are not familiar with a given concept or result.

Plan: We cover background material during the first few meetings (Part I). After this brief review, we will discuss some research papers and open problems (Part II). While most lectures will be given by regular participants, we may have guest talks as well. (There are no exams/homeworks but students taking the class for credit must give a presentation.)


Topic Date Speaker(s)
Introduction and Motivation (Lecture Notes) March 1 Igor Oliveira and Amir Tabatabai
Definitions and Basic Results (Ref. [1], [2]) March 8 Igor Oliveira and Amir Tabatabai
Bounded Arithmetic (Ref. [1], [2]) March 15 Amir Tabatabai
Herbrand's Theorem (Ref. [3], [4]) March 22 Jan Revay
KPT Witnessing Theorem / Introduction to Sequent Calculus (Ref. [3], [4]) March 29 Jan Revay and Martin Smolik
Gentzen's Cut Elimination / Formalization of Circuit Complexity
April 5 Martin Smolik and Raheleh Jalali
Unprovability of Lower Bounds in B. Arithmetic I (Ref. [5], [6], [7], see also [8], [9]) April 12 Raheleh Jalali
Unprovability of Lower Bounds in B. Arithmetic II  April 19 TBD

References (Part I):

[1] S. Buss. Bounded arithmetic and propositional proof complexity (survey). [pdf]
[2] S. Buss. Bounded arithmetic (thesis/book). [pdf]
S. Cook and P. Nguyen. Logical foundations of proof complexity (book). [pdf]
J. Krajicek. Bounded arithmetic, propositional logic, and complexity theory (book).

References (Part II):

J. Pich. Circuit lower bounds in bounded arithmetic. [pdf]
[6] J. Pich. Bounded arithmetic and theory of Razborov and Rudich. [pdf]
[7] J. Krajicek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. [pdf]
[8] A. Razborov. Bounded arithmetic and lower bounds in boolean complexity. [pdf]
[9] A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of arithmetic. [pdf]
[10] S. Cook and J. Krajicek. Consequences of the provability of  NP P/poly. [pdf]
[11] J. Krajicek. Forcing with random variables and proof complexity (Chapters 29 and 30).

Further References*:

[12] E. Jerabek. Approximate counting in bounded arithmetic. [pdf]
[13] P. Pudlak. Incompleteness in the finite domain. [pdf]
[14] A. Atserias and M. Muller. Partially definable forcing and bounded arithmetic. [pdf]

* These will be covered depending on the interest of the participants and time constraints.

Remark: Participants may be interested in the following related courses:

"Proof Complexity and the P vs. NP problem" (Wed 10:40am, Karlin).
"Finite Model Theory" (Tuesday 2pm, Karlin).

If you have questions, please contact Igor Oliveira or Amir Tabatabai.