Lower Bounds to the Size of Constant-Depth Propositional Proofs

Krajicek, Jan

J. Symbolic Logic, Tome 59 (1994) no. 1, p. 73-86 / Harvested from Project Euclid

Résumé

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.

Détail

Publié le : 1994-03-14
Classification:  Lengths of proofs,  propositional calculus,  Frege systems,  pigeonhole principle,  03F20,  03F07,  68Q15,  68R99