CSC 2429H: Introduction to Bounded Arithmetic and Propositional Translations
Fall, 2007

Announcements

Solutions to all four assignments are posted below.

NOTES: Click here for five pages of auxiliary course Notes (Addendum added Dec 22, 2007)

TIME AND ROOM CHANGES: Starting September 25 this class meets Monday 12-1 in GB 248, and Thursday 3-4 in GB 220. (There are no more Tuesday classes.)

NOTE: This course is Section L0101 of CSC 2429H. If you register in this course, please be sure you have the right section number. (The other section is Toni Pitassi's course on PCPs.)

Instructor: Stephen Cook
Office SF 2303C
Tel: (416) 978-5183
email: sacook@cs

Description

This course develops a three-way connection between complexity classes, formal theories of arithmetic, and propositional proof systems. Each of several standard complexity classes, including AC0, NC1, Polytime, and PH has a corresponding theory formalizing reasoning using concepts in that class, and corresponding to each theory there is a propositional proof system representing a nonuniform version of the theory.

Prerequisites

Knowledge of predicate calculus and some knowledge of Peano arithmetic. Also some knowledge of complexity theory, including complexity classes based on time, space, or Boolean circuit families. CSC 2404H is perfect for the logic, and CSC 2401H more than suffices for the complexity theory. The draft textbook by Arora and Barak (available on the Web) Complexity Theory: A Modern Approach is a good general reference.

Course Requirements: Three or four problem sets

Text (draft) : Foundations of Proof Complexity: Bounded Arithmetic and Propositional Translations by Stephen Cook and Phuong Nguyen (on the Web). Read the Preface for an introduction to the material of the course.

Topics

Basic References:

Handbook of Proof Theory, Chapters I and II

Jan Krajicek: Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge, 1995.

Annotated references

Assignment 1 (Due October 11, in class)

1. (Optional) Do Exercise 2.51, page 29. (Prove Herbrand Form 2 from Form 1)
NOTE: This is solved on pp 47-48)

2. Show that the following formulas are theorems of IDelta0 (see page 36): O4, D7, D10.

In each case, you may use the fact that earlier formulas are theorems (for example in proving O4 you may use O1,O2,O3). Justify each line in your argument by either an axiom or one of the earlier theorems.

3. Do Exercise 3.17 on page 38

4. Do Exercise 3.28 on page 44.

Click here for solutions to Assignment 1.

Assignment 2 (Due November 8, in class)

1. Do the following excercises showing various things are provable in I\Delta_0:

3.47 (Show that I\Delta_0 can \Delta_0-define gp(x).)
3.48c (Propery of gp(x))
3.50 (distinct numbers have distinct binary notations)

Here you may freely use properties of 0,1,+,x,< = as given on page 36, without refering to them. Also you may use other results and exercises preceeding 3.47 (but you should refer to these).

2. Give more details of the inclusion LTH \subset \Delta_0^N in the proof of Theorem 3.58. For the base case, NLinTime \subset \Delta_0^N, use the relation Numones(x,y) (Defined in Lemma 3.57) as suggested. For the induction step, use the recurrence (3.27). For this, given a nondeterminisitic linear time oracle Turing machine M, it is useful to define the relation R_M(x,y,b) asserting "M accepts input x, assuming that it makes the sequence of oracle queries coded by y, and the answers to those queries are coded by b". Show that the relation R_M is accepted by some nondeterministic linear time Turing machine (with no oracle), and hence is \Delta_0-definable (by your base case).

Click here for solutions to Assignment 2.

Assignment 3 (due Monday, November 26, in class)

1. (This extends Exercise 5.12) In the proof of Lemma 5.10 (Any model M for I\Delta0 can be expanded to a model of V^0), suppose that instead of defining U_2 as in (5.5) we defined U_2 to be the set of all subsets of U_1 which have a largest element, together with the empty set. Then for each set S \subset U_1 in U_2 we define |S| in the obvious way to satisfy axioms L1 and L2. Prove that if M is a nonstandard model, then the resulting two-sorted structure (U_1,U_2) is not a model of V^0.

2. Do Exercise 5.19, page 92: Show that the number functions of FAC^0 are precisely the lengths of string functions of FAC^0.

3. Do Exercise 5.43 parts a,b,c, page 101 (Show V^0 proves properties of binary addition and successor).

4. Do Exercise 5.54, page 103 (Show, using the Row function, that theories extending V0 prove the equivalence of Sigma^B_1 formulas with formulas with a single existential string quantifier.)

Click here for solutions to Assignment 3.

Assignment 4 (due Friday, Dec 14)

1. Do Exercise 0.6 page 2 of 2429 Notes (Show that every polytime function is Sigma^B_1 definable in VP.)

2. Do Exercise 0.11 page 3 of 2429 Notes (Show every polytime function is represented by a term in VPhat.)

3. Do Exercise 6.31, page 135: Show that V^1 proves the prime factorization theorem.

4. Do Exercise 0.14 page 3 of 2429 Notes (Use KPT Witnessing to show that if VP proves prime factorization, then RSA Encryption can be broken.)

5. Do Exercise 0.18 page 5 of the 2429 Notes: Show that V0(2) proves the Bijective Pigeonhole Principle.

Click here for solutions to Assignment 4.