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

Authors: 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}
  }