LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives $\neg$ and $\bigwedge, \bigvee$ (both of bounded arity). Then for every $d \geq 0$ and $n \geq 2$, there is a set $T^d_n$ of depth $d$ sequents of total size $O(n^{3 + d})$ which are refutable in LK by depth $d + 1$ proof of size $\exp(O(\log^2 n))$ but such that every depth $d$ refutation must have the size at least $\exp(n^{\Omega(1)})$. The sets $T^d_n$ express a weaker form of the pigeonhole principle.
Publié le : 1994-03-14
Classification:
Lengths of proofs,
propositional calculus,
Frege systems,
pigeonhole principle,
03F20,
03F07,
68Q15,
68R99
@article{1183744434,
author = {Krajicek, Jan},
title = {Lower Bounds to the Size of Constant-Depth Propositional Proofs},
journal = {J. Symbolic Logic},
volume = {59},
number = {1},
year = {1994},
pages = { 73-86},
language = {en},
url = {http://dml.mathdoc.fr/item/1183744434}
}
Krajicek, Jan. Lower Bounds to the Size of Constant-Depth Propositional Proofs. J. Symbolic Logic, Tome 59 (1994) no. 1, pp. 73-86. http://gdmltest.u-ga.fr/item/1183744434/