[Proof Complexity] new preprint

Leszek Kolodziejczyk lak at mimuw.edu.pl
Thu Mar 23 13:23:34 CET 2017

Dear colleagues,

Michal Garlik and I have a preprint titled

    "Some subsystems of constant-depth Frege with parity"

which is now available at our webpages:


The abstract is below. Comments, suggestions and corrections appreciated.

Best regards,



We consider three relatively strong families of subsystems of
$AC^0[2]$-Frege for which exponential lower bounds on proof size are known.
In order of increasing strength, these subsystems are: $AC^0$-Frege with
parity axioms and the treelike and daglike versions of systems introduced
by Krajicek which we call $PK^c_d(\oplus)$. In a $PK^c_d(\oplus)$-proof,
lines are cedents in which all formulas have depth at most $d$, parity
connectives can only appear as the outermost connectives in formulas, and
all but $c$ formulas contain no parity connective at all.

We give simple arguments proving that $AC^0[2]$-Frege is exponentially
stronger than daglike $PK^{O(1)}_{O(1)}(\oplus)$, which is exponentially
stronger than treelike $PK^{O(1)}_{O(1)}(\oplus)$. On the other hand, we
point out that the best available technique for comparing the performance
of such systems on De Morgan formulas, due to Impagliazzo and Segerlind,
only leads to superpolynomial separations. In fact, we prove that treelike
$PK^{O(1)}_{O(1)}(\oplus)$ is quasipolynomially but not polynomially
equivalent to $AC^0$-Frege with parity axioms. This leads us to ask the
question whether any of our systems is quasipolynomially equivalent to
$AC^0[2]$-Frege on De Morgan formulas; a positive answer would imply an
exponential lower bound for $AC^0[2]$-Frege.

We also study Itsykson and Sokolov's system Res-Lin. We prove that an
extension of treelike Res-Lin is polynomially simulated by a system related
to daglike $PK^{O(1)}_{O(1)}(\oplus)$, and obtain an exponential lower
bound for this system.

More information about the Proof-Complexity mailing list