Power of non-uniformity in proof complexity
Steven Perron · TSpace (University of Toronto) · 2009
As the title indicates, this thesis is concerned with the strength of non-uniformity in proof complexity. The non-uniform part is there because we look at quantified propositional proof systems. With these proof systems we are interested in the minimum size of proofs that prove a family of tautologies. Like circuits, these proofs are not necessarily easy to construct. We measure the strength of a proof system by characterizing which families of tautologies have polynomial-size proofs in the proof system. The proof systems we examine were first introduced by Kraj\\'{\\i}cek and Pudl{\\'a}k \\cite{KP90}, but have only received limited attention since then. These systems are called $G_i$ and $G_i^*$. $G_i$ is the propositional version of Gentzen's $LK$ with cut formulas restricted to formulas with $i-1$ quantifier alternations, and $G_i^*$ is the treelike version of $G_i$. We look at the strength of these proof systems in three ways. The first is to compare them with bounded arithmetic. We find the weakest theory that can prove that a given proof system is sound. The second method is to compare proof systems with respect to computational complexity. We determine the complexity of finding a witness for the outermost existential quantifiers of a formula given a proof of that formula. The final method is to compare the proof systems to each other. This is done using the notion of $p$-simulations. An important tool in all of this work is an adaptation of the Herbrand theorem for the propositional setting. Most proof-theoretic proofs of the Herbrand theorem require cut-elimination which causes the size of the proof to increase exponentially. We adapt the statement of the theorem and the proof to avoid this increase. We finish by defining new proof systems that meet given requirements. The goal is to determine where proof systems get their strength. In all cases, it comes down to the eigenvariables. The strength of a proof system that allows quantifiers in the cut formulas is determined by the difficulty of witnessing the eigenvariables.