Examining fragments of the quantified propositional calculus

When restricted to proving q i formulas, the quantified propositional proof system G i is closely related to the b i theorems of Buss's theory Si 2. Namely, G i has polynomial-size proofs of the translations of theorems of Si 2, and Si 2 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 i similar in style to the KPT witnessing theorem for T i 2 . This witnessing theorem is then used to show that Si 2 proves G i is sound with respect to q i+1 formulas. Note that unless the polynomial-time hierarchy collapses Si 2 is the weakest theory in the S2 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 for prenex formulas. This is followed by a proof that Gi p-simulates G

• Type: Journal
• Year: 2008
• Where: JSYML
• Authors: Steven Perron
• Keywords: Formulas, JSYML 2008, Quantified Propositional Proof, Theory Si