Abstract
Does every Boolean tautology have a short propositionalcalculus proof? Here, a propositionalcalculus (i.e. Frege) proof is any proof starting from a set of axioms and deriving new Boolean formulas using a fixed set of sound derivation rules. Establishing any superpolynomial size lower bound on Frege proofs (in terms of the size of the formula proved) is a major open problem in proof complexity, and among a handful of fundamental hardness questions in complexity theory by and large. Noncommutative arithmetic formulas, on the other hand, constitute a quite weak computational model, for which exponentialsize lower bounds were shown already back in 1991 by Nisan [STOC 1991], using a particularly transparent argument.
In this work we show that Frege lower bounds in fact follow from corresponding size lower bounds on noncommutative formulas computing certain polynomials (and that such lower bounds on noncommutative formulas must exist, unless NP=coNP). More precisely, we demonstrate a natural association between tautologies T to noncommutative polynomials p, such that:
(*) if T has a polynomialsize Frege proof then p has a polynomialsize noncommutative arithmetic formula; and conversely, when T is a DNF, if p has a polynomialsize noncommutative arithmetic formula over GF(2) then T has a Frege proof of quasipolynomial size.
The argument is a characterization of Frege proofs as noncommutative formulas: we show that the Frege system is (quasi)polynomially equivalent to a noncommutative Ideal Proof System (IPS), following the recent work of Grochow and Pitassi [FOCS 2014] that introduced a propositional proof system in which proofs are arithmetic circuits, and the work in [Tzameret 2011] that considered adding the commutator as an axiom in algebraic propositional proof systems. This gives a characterization of propositional Frege proofs in terms of (noncommutative) arithmetic formulas that is tighter than (the formula version of IPS) in Grochow and Pitassi [FOCS 2014], in the following sense:
(i) The noncommutative IPS is polynomialtime checkable  whereas the original IPS was checkable in probabilistic polynomialtime; and
(ii) Frege proofs unconditionally quasipolynomially simulate the noncommutative IPS  whereas Frege was shown to efficiently simulate IPS only assuming that the decidability of PIT for (commutative) arithmetic formulas by polynomialsize circuits is efficiently provable in Frege.
BibTeX  Entry
@InProceedings{li_et_al:LIPIcs:2015:5058,
author = {Fu Li and Iddo Tzameret and Zhengyu Wang},
title = {{NonCommutative Formulas and Frege Lower Bounds: a New Characterization of Propositional Proofs}},
booktitle = {30th Conference on Computational Complexity (CCC 2015)},
pages = {412432},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897811},
ISSN = {18688969},
year = {2015},
volume = {33},
editor = {David Zuckerman},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5058},
URN = {urn:nbn:de:0030drops50585},
doi = {10.4230/LIPIcs.CCC.2015.412},
annote = {Keywords: Proof complexity, algebraic complexity, arithmetic circuits, Frege, noncommutative formulas}
}
Keywords: 

Proof complexity, algebraic complexity, arithmetic circuits, Frege, noncommutative formulas 
Collection: 

30th Conference on Computational Complexity (CCC 2015) 
Issue Date: 

2015 
Date of publication: 

06.06.2015 