Princeton University
Computer Science Dept.
Computer Science 598g

Advanced Topics in CS: Introduction to Proof Complexity

A. Razborov

What's New?

Spring 2000
General Information | What's New? | Annotated literature | Lecture notes

    This page will be started on January 31 and will contain a brief summary of what we did so far.
If you occasionally miss a lecture of two, this is the place for you to go.
 

      January 31

      We defined the Frege proof system (also known as classical propositional calculus)
and proved for it the most basic facts: deduction theorem, adequacy (soundness +
completeness) theorem and Craig's interpolation theorem.
 

      February 7

       We defined equational theories and proved for them the adequacy theorem. Then we went on to first-order theories based on the predicate calculus with equality (the latter being essentialy the combination of propositional calculus and equational logic, augmented with first-order quantifiers). We stated (without proofs) Goedel's completeness theorem and deduction theorem. All general concepts were exemplified throughout the lecture by three major languages designed to argue about some particular structure/ class of structures: the language of Peano Arithmetic (to argue about integers), the group language (to argue about arbitrary groups), and the language of Boolean algebras (to argue in particular about the two-element Boolean algebra).

      February 14

       We finished our brief introduction to general first-order theories by stating compactness theorem
and Craig's interpolation theorem (without proofs), and the theorem stating that every extension by new
definable function/predicate symbols is conservative. Then we introduced Peano Arithmetic PA and stated
that every recursive function is definable in PA (with a sketch of proof). Next we introduced the language of bounded arithmetic, bounded  quantifiers, the hierarchy of bounded formulas and the core system of bounded arithmetic, $S_2^1$. We stated the main theorem of bounded arithmetic: the set of functions/predicates that are $\Sigma_1^b$-definable in $S_2^1$ coincides with the set of poly-time computable functions/predicates.

      February 21

       The whole lecture was taken up by the (sketch of) the proof of the main theorem of bounded arithmetic.


 

      February 28

       We considered several applications of the main theorem. Then we considered several alternative
axiomatizations of the theories $S_2^i$ and proved their equivalence. We introduced theories $T_2^i$ and proved that they interlace the previous hierarchy $S_2^i$ in the sense $S_2^i\subseteq T_2^i\subseteq
S_2^{i+1}$. We stated (without proof) that $S_2^{i+1}$ is $\Sigma_b^{i+1}$-conservative over $T_2^i$. We stated the theorem that describes $\Sigma_1^b$-definable multi-valued functions in $T_2^1$, with a rough sketch of the proof. We briefly discussed some second-order theories and outlined some of the major definability results for them. We also mentioned the result that basically claims the isomorphism of first-order theories and second-order theories describing the same complexity class (so-called RSUV-isomorphism).

       Then we started to move to our general goal for the rest of this course, which is to study the
provability of formulas that do not involve any essential bounded quantifiers. As the first step toward this
goal, we defined Cook's equational theory PV.


 

      March 6


       We defined a common extension $S_2^1(PV)$, and proved that it is conservative over both $S_2^1$ and $PV$. Then we started Propositional Proof Complexity with the general definition of a proof system given by Cook and Reckhow. We defined Frege and Extended Frege proof systems. We exhibited a translation of $\Sigma_0^b$-formulas in the language of Bounded Arithmetic to (sequences of) propositinal formulas. We formulated a theorem stating that every $S_2^1$-proof or $PV$-proof of a $\Sigma_0^b$-formula (of an equation, respectively) can be translated into poly-size Extended Frege proofs of the corresponding propositional tautologies. We exhibited also the converse (in a sense) statement: $S_2^1$ can prove soundness of the Extended Frege proof system. We gave a general notion of $p$-simulation of one proof system with another. We proved that, under this notion, Extended Frege is equivalent to Frege with the substitution rule.
 


 

      March 27


        We considered ordinary Frege systems, and formulated (with a sketch of the proof) the theorem saying that all possible variants of these systems are polynomially equivalent. We formulated several satellite statements stating that if we restrict a Frege system in a way (like by requiring that all formulas in the proof are of small depth, or that the proof itself is tree-like), we nonetheless get an equivalent system. We defined bounded-depth Frege proof system, and showed how to translate arbitrary $S_2(P)$-proofs of
bounded formulas into quasipolynomial size bounded depth Frege proofs (this result actually preceeded the simulation of $S_2^1$ by EF we considered at the previous lecture). We defined pigeon-hole-principle $PHP^m_n$. Then we proved the highly non-trivial result by Paris, Wilkie and Woods [88] saying that for $m\geq 2n$ this principle has a quasipolynomial size bounded depth Frege proof, and mentioned some very recent refinement of this result.

      April 3

         We began lower bounds for propositional proofs. We formulated lower bounds for the pigeon-hole principle $PHP_n^{n+1}$ with respect to bounded depth Frege proofs and Resolution. Then we formulated the theorem by Ben-Sasson and Wigderson relating size and width of Resolution proofs.
 


 

      April 17

       We proved the theorem by Ben-Sasson and Wigderson and indicated some of its corollaries. Then we formulated and proved the efficient interpolation theorem for Resoultion. We analyzed difficulties surrounding its potential applications, and formulated the structural assumption which is necessary for overcoming them (existence of a pair of disjoint sets in $NP$ which are not $P$-separable). We observed the monotone version of the efficient interpolation theorem and used it for showing that known lower bounds for monotone circuits in computational complexity immediately imply proportionally strong lower bounds for Resolution.


 

     April 24


       We defined the system of bounded-depth Frege proofs with modular gates, the counting combinatorial principle $Count_p$ and mentioned the big open problem that consits in showing that $Count_q$ is hard for $F_d(MOD_p)$, whenever $p.q$ are two different primes. We showed that $Count_p$ is easy for $F_d(MOD_p)$ and formulated the theorem stating that $Count_q$ is difficult for $F_d + Count_p$  Then we went on to algebraic proof systems which historically appeared as an essential ingredient in the proof of the latter theorem. We defined Nullstellensatz and Polynomial Calculus proof systems and surveyed some lower bounds known for them. We also mentioned the relation between width of Resolution and degree in Polynomial Calculus. Then we gave a sketch of the proof of one of these lower bounds. For that purpose, we stated (also with a sketch of the proof) the theorem saying that every PC proof from a system of bynomials can be also assumed w.l.o.g. to be binomial. We defined Tseitin's tautologies and showed how to prove for them lower bounds on the degree of any binomial PC refutation.