22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007) Examining The Fragments of G Wroclaw, Poland July 10-July 14 ISBN: 0-7695-2908-9
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2007.18
When restricted to proving \Sigma _i^q i formulas, the quantified propositional proof system G_i^* is closely related to the \Sigma_i^b theorems of Buss's theory S_2^i . Namely, G_i^* has polynomialsize proofs of the translations of theorems of S_2^i , and S_2^i proves that G_i^* is sound. However, little is known about G_i^* when proving more complex formulas. In this paper, we prove a witnessing theorem for G_1^* similar in style to the KPT witnessing theorem for T_2^i. This witnessing theorem is then used to show that S_2^i proves G_1^* is sound with respect to prenex \Sigma_i+1^q formulas. Note that unless the polynomial hierarchy collapses S_2^i is the weakest theory in the S_2 hierarchy for which this is true. The witnessing theorem is also used to show that G_1^* is p-equivalent to a quantified version of extended-Frege. This is followed by a proof that G_i p-simulates G_i+1^*. We finish by proving that S_2 can be axiomatized by S_2^1 plus axioms stating that the cut-free version of G* is sound. All together this shows that the connection between G_i^* and S_2^i does not extend to more complex formulas.
Citation:
Steven James Perron, "Examining The Fragments of G," lics, pp.225-234, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||