Quantified Propositional Calculus and aSecond-Order Theory for NC1

Abstract Let H be a proof system for the quantified propositional calculus (QPC). Wedefine the \Sigma q j-witnessing problem for H to be: given a prenex \Sigma qj-formula A, anH-proof of A, and a truth assignment to the free variables in A, find a witness for the outermost existential quantifiers in A. We point out that the \Sigma q1 witnessingproblems for the systems G \Lambda 1 and G1 are complete for polynomial time and PLS (polynomial local search), respectively.We introduce and study the systems G \Lambda 0 and G0, in which cuts are restricted to quantifier-free formulas, and prove that the \Sigma q1-witnessing problem for each is com-plete for NC1. Our proof involves proving a polynomial time version of Gentzen's midsequent theorem for G\Lambda 0 and proving that G0-proofs are TC0-recognizable. Wealso introduce QPC systems for TC0 and prove witnessing theorems for them. We introduce a finitely axiomatizable second-order system VNC1 of boundedarithmetic which we prove isomorphic to Arai's first order theory AID + \Sigma b 0-CAfor uniform NC1. We describe simple translations of VNC1 proofs of all bounded theorems to polynomial size families of G\Lambda 0 proofs. From this and the above the-orem we get alternative proofs of the NC1 witnessing theorems for VNC1 and AID