## Paper: Examining The Fragments of G (at LICS 2007)

**Steven J. Perron**

### Abstract

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.

### BibTeX

@InProceedings{Perron-ExaminingTheFragmen, author = {Steven J. Perron}, title = {Examining The Fragments of G}, booktitle = {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)}, year = {2007}, month = {July}, pages = {225--234}, location = {Wroclaw, Poland}, publisher = {IEEE Computer Society Press} }