Uniformity and Nonuniformity in Proof Complexity
Kaveh Ghasemloo · TSpace (University of Toronto) · 2016
This thesis is dedicated to the study of the relations between uniform and nonuniform proof complexity and computational complexity. Nonuniform proof complexity studies the lengths of proofs in various propositional proof systems such as Frege . Uniform proof complexity studies the provability strength of bounded arithmetic theories which use only concepts computable in specific computational complexity classes, e.g. the two-sorted bounded arithmetic theory VNC1 uses only concepts computable in NC1. We are interested in transferring concepts, tools, and results from computational complexity to proof complexity. We introduce the notion of proof complexity class which corresponds to the notion of computational complexity class. We show the possibility of developing a systematic framework for studying proof complexity classes associated with computational complexity classes. The framework is based on soundness statements for proof complexity classes and evaluation problems for circuit complexity classes. The soundness statements are universal for proof complexity classes as circuit evaluation problems are complete for computational complexity classes. We introduce the notion of io-typed theories to design theories corresponding to computational complexity classes which are not closed under composition. We use io-types to control the composition of provably total functions of theories. We design a new class of theories n^ε-ioV∞ (ε