Tag Info

propositional proof systems and corresponding bounded arithmetic theories

Proof Complexity is a branch of computational complexity theory and logic concerned with the efficiency of proving theorems in various propositional proof systems, and first and higher order theories.

One of the major objectives is finding hard tautologies and proving lower-bounds on the proof size of these tautologies in propositional proof systems like Resolution, Frege, Polynomial Calculus, Extended Frege.

Propositional proof systems are related to bounded arithmetic theories in a similar way to the relation between uniform and nonuniform complexity classes in computational complexity. For example, the translation of any $\Pi^B_1$ statement in the first order theory $TV^0$(which is equal to first order version of $PV$) has polynomial size proofs in Extended Frege. Moreover $TV^0$ proves soundness of Extended Frege and Extended Frege can p-simulate any proof system that $TV^0$ proves its soundness. The theories are also connected to computational complexity classes in a strong sense: the provably total functions of the theory are exactly functions computable in the complexity class, e.g. $TV^0$ can prove a function is total iff the function is in $P$.

Examples of hard tautologies are Pigeon-Hole-Principle (PHP) and random CNF formulas.

Proof Complexity is related to Computational Complexity, Automated Theorem Proving and Proof Search, Bounded Arithmetic.