(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.)

Schedule:

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]

[3] S. Cook and P. Nguyen. Logical foundations of proof complexity (book). [pdf]

[4] J. Krajicek. Bounded arithmetic, propositional logic, and complexity theory (book).

References (Part II):

[5] 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.