Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Paper:

TR16-011 | 27th January 2016 16:25

#### Understanding Gentzen and Frege systems for QBF

TR16-011
Authors: Olaf Beyersdorff, Ján Pich
Publication: 29th January 2016 09:21
Keywords:

Abstract:

Recently Beyersdorff, Bonacina, and Chew (ITCS'16) introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of the new extended Frege system from Beyersdorff et al., denoted EF+\$\forall\$red, which is a natural extension of classical extended Frege EF.

Our main results are the following: Firstly, we prove that the standard Gentzen-style system \$G^*_1\$ p-simulates EF+\$\forall\$red and that \$G^*_1\$ is strictly stronger under standard complexity-theoretic hardness assumptions.

Secondly, we show a correspondence of EF+\$\forall\$red to bounded arithmetic: EF+\$\forall\$red can be seen as the non-uniform propositional version of intuitionistic \$S^1_2\$. Specifically, intuitionistic \$S^1_2\$ proofs of arbitrary statements in prenex form translate to polynomial-size EF+\$\forall\$red proofs, and EF+\$\forall\$red is in a sense the weakest system with this property.

Finally, we show that unconditional lower bounds for EF+\$\forall\$red would imply either a major breakthrough in circuit complexity or in classical proof complexity, and in fact the converse implications hold as well. Therefore, the system EF+\$\forall\$red naturally unites the central problems from circuit and proof complexity.

Technically, our results rest on a formalised strategy extraction theorem for EF+\$\forall\$red akin to witnessing in intuitionistic \$S^1_2\$ and a normal form for EF+\$\forall\$red proofs.

ISSN 1433-8092 | Imprint