Propositional Representation of Arithmetic Proofs

It is well known that the Boolean functions corresponding to a function computable in polynomial time on inputs of bounded length are computable by Boolean circuits of size polynomial in the bound. Similarly, polynomial length propositional formulas exist representing the truth of an equation t = u between terms involving functions computable in polynomial time, on inputs of bounded length. For certain proof systems whose theory is a set of such equations, there is a propositional proof system such that the representing formulas of a provable equation have polynomial length proofs. If a propositional proof system satisfies certain restrictions, then the arithmetic system such that this is true can be constructed. We prove two specific representation theorems; the first was stated by Cook and is proved here for the first time, and the second, involving polynomial space arithmetic and a natural proof system for the valid formulas of the quantified propositional calculus, is stated and proved here for the first time.Ph.D