[Proof Complexity] new preprint

[Leszek Kolodziejczyk]

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:

http://www.karlin.mff.cuni.cz/~garlik/papers.html
https://www.mimuw.edu.pl/~lak/publik.html

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

Best regards,
Leszek



-------------------------------------

Abstract:

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.