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+\forallred, 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+\forallred and that G^*_1 is strictly stronger under standard complexity-theoretic hardness assumptions.

Secondly, we show a correspondence of EF+\forallred to bounded arithmetic: EF+\forallred 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+\forallred proofs, and EF+\forallred is in a sense the weakest system with this property.

Finally, we show that unconditional lower bounds for EF+\forallred 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+\forallred naturally unites the central problems from circuit and proof complexity.

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